English
The range of mapRange.linearMap with f is the submodule generated by the ranges of f on each coordinate.
Русский
Образ mapRange.linearMap по f образует подмодуль, порождаемый образами f на каждой координате.
LaTeX
$$$\operatorname{range}(\,mapRange.linearMap f\,)=\operatorname{submodule}(\lambda _ . \operatorname{range} f)$$$
Lean4
theorem range_mapRange_linearMap (f : M →ₗ[R] N) (hf : LinearMap.ker f = ⊥) (I : Type*) :
LinearMap.range (mapRange.linearMap (α := I) f) = submodule (fun _ => LinearMap.range f) :=
by
ext x
constructor
· rintro ⟨y, hy⟩
simp [← hy]
· intro hx
choose y hy using hx
refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩
constructor <;> contrapose! <;>
simp_all (config := { contextual := true }) [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]
