Residue field of primes in polynomial algebras

Main results

• Polynomial.residueFieldMapCAlgEquiv: κ(I[X]) ≃ₐ[κ(I)] κ(I)(X)
• Polynomial.fiberEquivQuotient: κ(p) ⊗[R] (R[X] ⧸ I) = κ(p)[X] / I

noncomputable def Polynomial.residueFieldMapCAlgEquiv {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] (hJ : J = Ideal.map C I) : J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.residueFieldMapCAlgEquiv_algebraMap {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] (hJ : J = Ideal.map C I) (p : Polynomial R) : (residueFieldMapCAlgEquiv I J hJ) ((algebraMap (Polynomial R) J.ResidueField) p) = (algebraMap (Polynomial I.ResidueField) (RatFunc I.ResidueField)) (map (algebraMap R I.ResidueField) p)

@[simp]

theorem Polynomial.residueFieldMapCAlgEquiv_symm_C {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] (hJ : J = Ideal.map C I) (r : I.ResidueField) : (residueFieldMapCAlgEquiv I J hJ).symm (RatFunc.C r) = (algebraMap I.ResidueField J.ResidueField) r

@[simp]

theorem Polynomial.residueFieldMapCAlgEquiv_symm_X {R : Type u_1} [CommRing R] (I : Ideal R) [I.IsPrime] (J : Ideal (Polynomial R)) [J.IsPrime] [J.LiesOver I] (hJ : J = Ideal.map C I) : (residueFieldMapCAlgEquiv I J hJ).symm RatFunc.X = (algebraMap (Polynomial R) J.ResidueField) X

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

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

Equations

• One or more equations did not get rendered due to their size.