English
For an ideal I of S, the integral property of the quotient map I→ is equivalent to the integral property of the composition with the quotient map to S/I.
Русский
Для идеала I в S равноcть интегральности композиции и модуля к S/I эквивалентна интегральности quotientMap.
LaTeX
$$$(Ideal.quotientMap I f le\_rfl).IsIntegral \\Leftrightarrow ((Ideal.Quotient.mk I).comp f) : R →+* S/ I .IsIntegral$$$
Lean4
theorem isIntegral_quotientMap_iff {I : Ideal S} :
(Ideal.quotientMap I f le_rfl).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f : R →+* S ⧸ I).IsIntegral :=
by
let g :=
Ideal.Quotient.mk
(I.comap f)
-- Porting note: added type ascription
have : (Ideal.quotientMap I f le_rfl).comp g = (Ideal.Quotient.mk I).comp f := Ideal.quotientMap_comp_mk le_rfl
refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩
refine this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h
exact g.isIntegral_of_surjective Ideal.Quotient.mk_surjective
