English
The lemma that ensures the range of the lifted map equals the A-span of the range of the original map, with a straightforward inductive proof using tmul and addition.
Русский
Лемма, что диапазон поднятого отображения равен A-подпространству диапазона исходного отображения, доказуемая по индукции с использованием tmul и сложения.
LaTeX
$$$\\mathrm{range}(l.liftBaseChange A) = \\mathrm{span}_A(\\mathrm{range}(l))$$$
Lean4
@[simp]
theorem range_liftBaseChange (l : M →ₗ[R] N) :
LinearMap.range (l.liftBaseChange A) = Submodule.span A (LinearMap.range l) :=
by
apply le_antisymm
· rintro _ ⟨x, rfl⟩
induction x using TensorProduct.induction_on
· simp
· rw [LinearMap.liftBaseChange_tmul]
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)
· rw [map_add]
exact add_mem ‹_› ‹_›
· rw [Submodule.span_le]
rintro _ ⟨x, rfl⟩
exact ⟨1 ⊗ₜ x, by simp⟩
