lt_map_of_comap_lt_of_surjective — Mathlib

English

If f is surjective, the map/comap pair forms a Galois insertion between submodules.

Русский

Если f сюръективно, пара map/comap образует вложение Гало между подмодулями.

LaTeX

$$GaloisInsertion (Submodule.map f) (Submodule.comap f)$$

Lean4

theorem lt_map_of_comap_lt_of_surjective (h : q.comap f < p) : q < p.map f :=
  by
  rw [lt_iff_le_not_ge] at h ⊢; rw [map_le_iff_le_comap]
  exact h.imp_left (le_map_of_comap_le_of_surjective hf)

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