English
If f is surjective and K is maximal in S, then comap f K is maximal in R.
Русский
Если f сюръективен и K максимален в S, то comap f K максимален в R.
LaTeX
$$comap_isMaximal_of_surjective : IsMaximal (comap f K)$$
Lean4
theorem comap_isMaximal_of_surjective (hf : Function.Surjective f) {K : Ideal S} [H : IsMaximal K] :
IsMaximal (comap f K) := by
refine ⟨⟨comap_ne_top _ H.1.1, fun J hJ => ?_⟩⟩
suffices map f J = ⊤ by
have := congr_arg (comap f) this
rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
rw [eq_top_iff]
exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))
refine
H.1.2 (map f J)
(lt_of_le_of_ne (le_map_of_comap_le_of_surjective _ hf (le_of_lt hJ)) fun h =>
ne_of_lt hJ (_root_.trans (congr_arg (comap f) h) ?_))
rw [comap_map_of_surjective _ hf, sup_eq_left]
exact le_trans (comap_mono bot_le) (le_of_lt hJ)
