English
For a maximal ideal P in R[X], the composite map R → R[X] → R[X]/P is integral.
Русский
Для максимального идеала P в R[X] композиционный переход R → R[X] → R[X]/P является интегралом.
LaTeX
$$$(Ideal.Quotient.mk P) \\circ C$ IsIntegral$$
Lean4
/-- If `R` is a Jacobson ring, and `P` is a maximal ideal of `R[X]`,
then `R → R[X]/P` is an integral map. -/
theorem quotient_mk_comp_C_isIntegral_of_isJacobsonRing : ((Ideal.Quotient.mk P).comp C : R →+* R[X] ⧸ P).IsIntegral :=
by
let P' : Ideal R := P.comap C
have : P'.IsPrime := comap_isPrime C P
let f : R[X] →+* Polynomial (R ⧸ P') := Polynomial.mapRingHom (Ideal.Quotient.mk P')
have hf : Function.Surjective ↑f := map_surjective (Ideal.Quotient.mk P') Quotient.mk_surjective
have hPJ : P = (P.map f).comap f := by
rw [comap_map_of_surjective _ hf]
refine le_antisymm (le_sup_of_le_left le_rfl) (sup_le le_rfl ?_)
refine fun p hp => polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Quotient.eq_zero_iff_mem.mp ?_
simpa only [f, coeff_map, coe_mapRingHom] using (Polynomial.ext_iff.mp hp) n
refine RingHom.IsIntegral.tower_bot (T := (R ⧸ comap C P)[X] ⧸ _) _ _ (injective_quotient_le_comap_map P) ?_
rw [← quotient_mk_maps_eq]
refine ((Ideal.Quotient.mk P').isIntegral_of_surjective Quotient.mk_surjective).trans _ _ ?_
have : IsMaximal (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P) :=
Or.recOn (map_eq_top_or_isMaximal_of_surjective f hf hP)
(fun h => absurd (_root_.trans (h ▸ hPJ : P = comap f ⊤) comap_top : P = ⊤) hP.ne_top) id
apply quotient_mk_comp_C_isIntegral_of_jacobson' _ ?_ (fun x hx => ?_)
any_goals exact isJacobsonRing_quotient
obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective x
rwa [Quotient.eq_zero_iff_mem, mem_comap, hPJ, mem_comap, coe_mapRingHom, map_C]
