Theorems · Definition · algebraic geometry

Ideal.Fiber.algEquivQuotient

{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] →
              p.Fiber S ≃ₐ[S]
                Localization (Algebra.algebraMapSubmonoid S p.primeCompl) ⧸
                  Ideal.map
                    (algebraMap (Localization p.primeCompl) (Localization (Algebra.algebraMapSubmonoid S p.primeCompl)))
                    (IsLocalRing.maximalIdeal (Localization p.primeCompl))

p.Fiber S is isomorphic to the quotient Sₚ ⧸ pSₚ.

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIdeal.IsPrime