Theorems · Definition · commutative algebra

IsLocalization.AtPrime.equivQuotMaximalIdeal

{R : Type u_7} →
  [inst : CommRing R] →
    (p : Ideal R) →
      [inst_1 : p.IsMaximal] →
        (Rₚ : Type u_8) →
          [inst_2 : CommRing Rₚ] →
            [inst_3 : Algebra R Rₚ] →
              [IsLocalization.AtPrime Rₚ p] → [inst_5 : IsLocalRing Rₚ] → R ⧸ p ≃+* Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ

The isomorphism R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ, where Rₚ satisfies IsLocalization.AtPrime Rₚ p. In particular, localization preserves the residue field.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingIdeal.IsMaximalCommRingAlgebraIsLocalization.AtPrimeIsLocalRing