of_comap — Mathlib

English

If a surjective map f yields a principal comap of an ideal I, then I is principal.

Русский

Если отображение f сюръективно и образ I по обратному отображению является главным, то сам I главный.

LaTeX

$$$IsPrincipal(I) \\Rightarrow IsPrincipal(I\\\\mathrm{comap}(f))$$$

Lean4

theorem of_comap (f : F) (hf : Function.Surjective f) (I : Ideal S) [hI : IsPrincipal (I.comap f)] : IsPrincipal I :=
  by
  rw [← map_comap_of_surjective f hf I]
  exact hI.map_ringHom f

Похожие утверждения