English
Let s ∘ f = id and f, g be exact (im f = ker g). If v is a family of vectors in M that is linearly independent and a : κ → ι is injective, then g ∘ v ∘ a is a linearly independent family in P.
Русский
Пусть s ∘ f = id и f,g образуют точную последовательность (im f = ker g). Если v : ι → M линейно независим и a : κ → ι инъективна, то g ∘ v ∘ a линейно независима в P.
LaTeX
$$$\text{If } s \circ f = \mathrm{id},\ \operatorname{Im} f = \ker g,\ v:\,\iota\to M\text{ линейно независимо},\ a:\,\kappa\to \iota\text{ инъективно},\text{ то } g\circ v\circ a\text{ линейно независим в } P.$$$
Lean4
theorem linearIndependent_of_exact_of_retraction (hainj : Function.Injective a) (hsa : ∀ i, s (v (a i)) = 0)
(hli : LinearIndependent R v) : LinearIndependent R (g ∘ v ∘ a) :=
by
apply (LinearIndependent.comp hli a hainj).map
rw [Submodule.disjoint_def, hfg.linearMap_ker_eq]
rintro - hy ⟨y, rfl⟩
have hz : s (f y) = 0 := by
revert hy
generalize f y = x
intro hy
induction hy using Submodule.span_induction with
| mem m hm => obtain ⟨i, rfl⟩ := hm; apply hsa
| zero => simp_all
| add => simp_all
| smul => simp_all
replace hs := DFunLike.congr_fun hs y
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq] at hs
rw [← hs, hz, map_zero]
