submoduleImage_apply_of_le — Mathlib

English

Inclusion range equality as a standard lemma: range (inclusion h) = comap q.subtype p.

Русский

Связь образа включения с предобразом через comap: range (inclusion h) = comap q.subtype p.

LaTeX

$$$$ \operatorname{range}(\mathrm{inclusion}(h)) = \operatorname{comap}(q.\mathrm{subtype}, p) $$$$

Lean4

theorem submoduleImage_apply_of_le {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} (ϕ : O →ₗ[R] M')
    (N : Submodule R M) (hNO : N ≤ O) : ϕ.submoduleImage N = range (ϕ.comp (Submodule.inclusion hNO)) := by
  rw [submoduleImage, range_comp, Submodule.range_inclusion]

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