comap_leq_ker_subToSupQuotient — Mathlib

English

The comap of the subtyping map into p by p ⊓ p' is contained in ker of subToSupQuotient.

Русский

Обратное отображение подтипизации в p ⊓ p' содержится в ядре subToSupQuotient.

LaTeX

$$comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p')$$

Lean4

theorem comap_leq_ker_subToSupQuotient (p p' : Submodule R M) :
    comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p') :=
  by
  rw [LinearMap.ker_comp, Submodule.inclusion, comap_codRestrict, ker_mkQ, map_comap_subtype]
  exact comap_mono (inf_le_inf_right _ le_sup_left)

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