Theorems · Definition · commutative algebra

Polynomial.residueFieldMapCAlgEquiv

{R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      [inst_1 : I.IsPrime] →
        (J : Ideal (Polynomial R)) →
          [inst_2 : J.IsPrime] →
            [inst_3 : J.LiesOver I] →
              [inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)] →
                [inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J] →
                  J = Ideal.map Polynomial.C I → J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField

κ(I[X]) ≃ₐ[κ(I)] κ(I)(X).

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIdeal.IsPrimeIdeal.IsPrimeIdeal.LiesOverAlgebraLocalization.AtPrime.IsLiesOverAlgebra