comap_covBy_of_surjective — Mathlib

English

If f is surjective and p ⋖ q (p is covered by q), then p.comap f ⋖ q.comap f.

Русский

Если f сюръективно, и p ⋖ q (p покрыто q), то p.comap f ⋖ q.comap f.

LaTeX

$$$\operatorname{comap}_f p \;\lessdot\\operatorname{comap}_f q$$$

Lean4

theorem comap_covBy_of_surjective {f : F} (hf : Surjective f) {p q : Submodule R₂ M₂} (h : p ⋖ q) :
    p.comap f ⋖ q.comap f :=
  by
  refine ⟨lt_of_le_of_ne (comap_mono h.1.le) ((comap_injective_of_surjective hf).ne h.1.ne), ?_⟩
  intro N h₁ h₂
  refine h.2 (lt_map_of_comap_lt_of_surjective hf h₁) ?_
  rwa [← comap_lt_comap_iff_of_surjective hf, comap_map_eq, sup_eq_left.mpr]
  refine (LinearMap.ker_le_comap (f : M →ₛₗ[τ₁₂] M₂)).trans h₁.le

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