English
In a short exact sequence with bases {v} and {w}, the concatenation of their images under the appropriate injections is linearly independent.
Русский
В короткой точной последовательности и основаниях {v} и {w} линейная независимость сохраняется в сочетаниях по инъекциям.
LaTeX
$$$\text{LinearIndependent}_R\big(\mathrm{Sum.elim}(\mathrm{f}\circ v, \mathrm{g}^{-1}\circ w)\big)$$$
Lean4
/-- Given a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` of `R`-modules and linearly independent
families `v : ι → N` and `w : ι' → P`, we get a linearly independent family `ι ⊕ ι' → M` -/
theorem linearIndependent_shortExact {w : ι' → S.X₃} (hw : LinearIndependent R w) :
LinearIndependent R (Sum.elim (S.f ∘ v) (S.g.hom.toFun.invFun ∘ w)) :=
by
apply linearIndependent_leftExact hS'.exact hv _ hS'.mono_f rfl
dsimp
convert hw
ext
apply Function.rightInverse_invFun ((epi_iff_surjective _).mp hS'.epi_g)
