Theorems · Theorem · commutative algebra

IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ]
  [inst_6 : IsLocalization.AtPrime Rₚ p] [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ]
  [inst_9 : Algebra S Sₚ] [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [inst_11 : Algebra Rₚ Sₚ] (P : Ideal S) [hPp : P.LiesOver p] [inst_12 : Algebra R Sₚ] [IsScalarTower R S Sₚ]
  [IsScalarTower R Rₚ Sₚ] [inst_15 : p.IsMaximal] [inst_16 : P.IsMaximal]
  [inst_17 : (Ideal.map (algebraMap S Sₚ) P).LiesOver (IsLocalRing.maximalIdeal Rₚ)]
  (x : Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ),
  (algebraMap (R ⧸ p) (S ⧸ P)) ((IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ).symm x) =
    (IsLocalization.AtPrime.equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x)

The following diagram where the vertical maps are the algebra maps and the horizontal maps are Localization.AtPrime.equivQuotMaximalIdeal.symm and Localization.AtPrime.equivQuotientMapOfIsMaximal.symm commutes: `` Rₚ ⧸ 𝓂 ──▶ R ⧸ p │ │ Sₚ ⧸ 𝒫 ──▶ S ⧸ P ` Here, 𝓂 denotes the maximal ideal of Rₚ and 𝒫 the image of P in Sₚ. Note that result is stated in that direction since this is the formulation needed for the proof of Localization.AtPrime.inertiaDeg_map_eq_inertiaDeg`.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Extension

Cited by

1 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIdeal.IsPrimeCommRingAlgebraIsLocalization.AtPrimeIsLocalRingCommRingAlgebraIsLocalizationAlgebraIdeal.LiesOverAlgebraIsScalarTowerIsScalarTowerIdeal.IsMaximalIdeal.IsMaximalIdeal.LiesOver