comap_le_comap_iff_of_surjective — Mathlib

English

If f is surjective, then comap preserves order bijectively: comap f I ≤ comap f J iff I ≤ J for ideals I,J in S.

Русский

Пусть f сюръективно. Тогда comap сохраняет порядок в обе стороны: comap f I ≤ comap f J эквивалентно I ≤ J для идеалов I,J в S.

LaTeX

$$$hf : \mathrm{Function.Surjective}(f) \Rightarrow \forall I,J\in \mathrm{Ideal}(S),\; \mathrm{comap}(f,I) \le \mathrm{comap}(f,J) \iff I \le J$$$

Lean4

theorem comap_le_comap_iff_of_surjective (hf : Function.Surjective f) (I J : Ideal S) : comap f I ≤ comap f J ↔ I ≤ J :=
  ⟨fun h => (map_comap_of_surjective f hf I).symm.le.trans (map_le_of_le_comap h), fun h =>
    le_comap_of_map_le ((map_comap_of_surjective f hf I).le.trans h)⟩

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