orderEmbeddingOfSurjective — Mathlib

English

With surjective f, comap f I ≤ comap f J is equivalent to I ≤ J for ideals I,J in S.

Русский

При сюръективности f, 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),\; Iff(\mathrm{comap}(f,I) \le \mathrm{comap}(f,J), \ I \le J)$$$

Lean4

/-- The map on ideals induced by a surjective map preserves inclusion. -/
def orderEmbeddingOfSurjective (hf : Function.Surjective f) : Ideal S ↪o Ideal R
    where
  toFun := comap f
  inj' _ _ eq := SetLike.ext' (Set.preimage_injective.mpr hf <| SetLike.ext'_iff.mp eq)
  map_rel_iff' := comap_le_comap_iff_of_surjective _ hf ..

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