Theorems · Definition · commutative algebra

IsLocalization.AtPrime.equivQuotientMapOfIsMaximal

{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] →
              (Sₚ : Type u_4) →
                [inst_4 : CommRing Sₚ] →
                  [inst_5 : Algebra S Sₚ] →
                    [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] →
                      (P : Ideal S) →
                        [hPp : P.LiesOver p] → [P.IsMaximal] → S ⧸ P ≃+* Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P

The isomorphism S ⧸ P ≃+* Sₚ ⧸ P·Sₚ, where Sₚ is the localization of S at the (image) of the complement of p and P is a maximal ideal of S above p. Note that this isomorphism makes the obvious diagram involving R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ commute, see IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Extension

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIdeal.IsPrimeCommRingAlgebraIsLocalizationIdeal.LiesOverIdeal.IsMaximal