Theorems · Definition · algebraic geometry

Ideal.Fiber.localizationAlgEquivQuotient

{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] →
              (q : Ideal (p.Fiber S)) →
                [inst_4 : q.IsPrime] →
                  [inst_5 :
                      Algebra (Localization.AtPrime p)
                        (Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q))] →
                    [Localization.AtPrime.IsLiesOverAlgebra p (Ideal.comap Algebra.TensorProduct.includeRight q)] →
                      Localization.AtPrime q ≃ₐ[Localization.AtPrime p]
                        Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q) ⧸
                          Ideal.map
                            (algebraMap R (Localization.AtPrime (Ideal.comap Algebra.TensorProduct.includeRight q))) p

The localization of the fiber p.Fiber S is isomorphic to a quotient of a localization.

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIdeal.IsPrimeIdeal.IsPrimeAlgebraLocalization.AtPrime.IsLiesOverAlgebra