English
Let f: R → S be a ring hom and I an ideal of R with ker f ≤ I. If f is integral, then I.map f = ⊤ if and only if I = ⊤.
Русский
Пусть f: R → S — кольцо-гомоморф, и I — идеал R с условием ker f ≤ I. Если f интегрально, то I.map f = ⊤ тогда и только тогда I = ⊤.
LaTeX
$$$I.map f = \top \; \iff \; I = \top$$$
Lean4
theorem map_eq_top_iff_of_ker_le {R S} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal R} (hf₁ : RingHom.ker f ≤ I)
(hf₂ : f.IsIntegral) : I.map f = ⊤ ↔ I = ⊤ := by
constructor; swap
· rintro rfl; exact Ideal.map_top _
contrapose
intro h
obtain ⟨m, _, hm⟩ := Ideal.exists_le_maximal I h
let _ := f.toAlgebra
have : Algebra.IsIntegral _ _ := ⟨hf₂⟩
obtain ⟨m', _, rfl⟩ := exists_ideal_over_maximal_of_isIntegral m (hf₁.trans hm)
rw [← map_le_iff_le_comap] at hm
exact (hm.trans_lt (lt_top_iff_ne_top.mpr (IsMaximal.ne_top ‹_›))).ne
