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).

@[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

theorem Polynomial.fiberEquivQuotient_tmul {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] (a : p.ResidueField) (b : Polynomial R) : (fiberEquivQuotient f hf p) (a ⊗ₜ[R] f b) = (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))) (C a * map (algebraMap R p.ResidueField) b)

theorem Ideal.exists_mem_span_singleton_map_residueField_eq {R : Type u_1} [CommRing R] (P : Ideal R) [P.IsPrime] (I : Ideal (Polynomial R)) : ∃ p ∈ I, span {Polynomial.map (algebraMap R P.ResidueField) p} = map (Polynomial.mapRingHom (algebraMap R P.ResidueField)) I

Given a prime P of R and an ideal I of R[X], the image of I in κ(P)[X] is generated by some p ∈ I (basically because κ(P)[X] is a PID).