English
In a commutative diagram with an exact top row and contractions v, u, w satisfying the stated injectivity and independence hypotheses, the map u is linearly independent.
Русский
В диаграмме с точной верхней строкой и условиями на v, u, w при условии иньективности и линейной независимости, отображение u линейно независимо.
LaTeX
$$$\text{LinearIndependent}(R,u)$$$
Lean4
/-- In the commutative diagram
```
f g
0 --→ X₁ --→ X₂ --→ X₃
↑ ↑ ↑
v| u| w|
ι → ι ⊕ ι' ← ι'
```
where the top row is an exact sequence of modules and the maps on the bottom are `Sum.inl` and
`Sum.inr`. If `u` is injective and `v` and `w` are linearly independent, then `u` is linearly
independent. -/
theorem linearIndependent_leftExact : LinearIndependent R u :=
by
rw [linearIndependent_sum]
refine ⟨?_, LinearIndependent.of_comp S.g.hom hw, disjoint_span_sum hS hw huv⟩
rw [huv, LinearMap.linearIndependent_iff S.f.hom]; swap
· rw [LinearMap.ker_eq_bot, ← mono_iff_injective]
infer_instance
exact hv
