ι_range_map_map — Mathlib

English

For a morphism f: Q1 →qᵢ Q2, the submodule range of ι_Q1 mapped by map f equals the submodule range of ι_Q2 mapped by ι via range f.

Русский

Для отображения f: Q1 →qᵢ Q2 подмодулями образа ι_Q1 через map f совпадают с образами подмодуля ι_Q2 через ι по отображению диапазона f.

LaTeX

$$$ (\operatorname{range}(\iota Q_1)).\mathrm{map}((\mathrm{map} f).toLinearMap) = (\operatorname{range} f).\mathrm{map}(\iota Q_2). $$$

Lean4

@[simp]
theorem ι_range_map_map (f : Q₁ →qᵢ Q₂) :
    (LinearMap.range (ι Q₁)).map (map f).toLinearMap = (LinearMap.range f).map (ι Q₂) :=
  (ι_range_map_lift _ _).trans (LinearMap.range_comp _ _)

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