Theorems · Definition · commutative algebra

Polynomial.fiberEquivQuotient

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (f : Polynomial R →ₐ[R] S) →
            Function.Surjective ⇑f →
              (p : Ideal R) →
                [inst_3 : p.IsPrime] →
                  p.Fiber S ≃ₐ[p.ResidueField]
                    Polynomial p.ResidueField ⧸
                      Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)

κ(p) ⊗[R] (R[X] ⧸ I) = κ(p)[X] / I

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIdeal.IsPrime