English
For any ideal I in the codomain, comap f I = ⊤ iff I = ⊤. The preimage of top characterizes top in the codomain under f.
Русский
Для любого идеала I в кодомоне, comap f I = ⊤ тогда и только тогда, когда I = ⊤. Предобраз верхнего идеала характеризует верхний в кодомоне под действием f.
LaTeX
$$$I = \\top \\;\\text{in the codomain} \\;\\Longrightarrow\\; \\operatorname{comap} f(I) = \\top \\quad\\text{and}\\quad \\operatorname{comap} f(I) = \\top \\Longrightarrow I = \\top$$$
Lean4
@[simp]
theorem comap_eq_top_iff {I : Ideal S} : I.comap f = ⊤ ↔ I = ⊤ :=
⟨fun h => I.eq_top_iff_one.mpr (map_one f ▸ mem_comap.mp ((I.comap f).eq_top_iff_one.mp h)), fun h => by
rw [h, comap_top]⟩
