English
The kernel of Submodule.mulRightMap equals ⊥ if and only if A is linearly independent over the image of B via the right map.
Русский
Ядро Submodule.mulRightMap равно ⊥ тогда и только тогда, когда A линейно независим над изображением B через правое отображение.
LaTeX
$$$\\ker(Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b)=\\{0\\} \\iff \\ LinearIndependent A (B.val \\circ b)$$$
Lean4
theorem mulRightMap_ker_eq_bot_iff_linearIndependent {ι : Type*} (b : ι → B) :
LinearMap.ker (Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b) = ⊥ ↔
LinearIndependent A (B.val ∘ b) :=
by
simp_rw [LinearIndependent, LinearMap.ker_eq_bot]
let i : (ι →₀ A) →ₗ[R] S := Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b
let j : (ι →₀ A) →ₗ[R] S := (Finsupp.linearCombination A (B.val ∘ b)).restrictScalars R
suffices i = j by change Function.Injective i ↔ Function.Injective j; rw [this]
ext
simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val, LinearMap.coe_restrictScalars,
Finsupp.linearCombination_single, i, j]
exact Submodule.mulRightMap_apply_single _ _ _
