map_covBy_of_injective — Mathlib

English

For submodules p and q, p.map f ≤ q.map f if and only if p ≤ q.

Русский

Для подмодулей p и q выполняется: p.map f ≤ q.map f тогда и только тогда, когда p ≤ q.

LaTeX

$$$\forall p\, q:\, Submodule\; R\; M,\ p.map f \le q.map f \;\Leftrightarrow\; p \le q$$$

Lean4

theorem map_covBy_of_injective {p q : Submodule R M} (h : p ⋖ q) : p.map f ⋖ q.map f :=
  by
  refine ⟨lt_of_le_of_ne (map_mono h.1.le) ((map_injective_of_injective hf).ne h.1.ne), ?_⟩
  intro P h₁ h₂
  refine h.2 ?_ (Submodule.comap_lt_of_lt_map_of_injective hf h₂)
  rw [← Submodule.map_lt_map_iff_of_injective hf]
  refine h₁.trans_le ?_
  exact (Set.image_preimage_eq_of_subset (.trans h₂.le (Set.image_subset_range _ _))).superset

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