English
In a short exact sequence 0 → X1 → X2 → X3 → 0, if there are bases bN for X1 and bP for X3, one can construct a basis for X2 indexed by the disjoint sum ι ⊕ ι'.
Русский
В короткой точной последовательности 0 → X1 → X2 → X3 → 0, если заданы базы bN для X1 и bP для X3, можно построить базис для X2, индексируемый по дизjointной сумме ι ⊕ ι'.
LaTeX
$$$\text{Basis}.ofShortExact(hS')(bN)(bP) : \text{Basis } (ι \oplus ι') R X₂$$$
Lean4
/-- In a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`, given bases for `X₁` and `X₃`
indexed by `ι` and `ι'` respectively, we get a basis for `X₂` indexed by `ι ⊕ ι'`. -/
noncomputable def ofShortExact (bN : Basis ι R S.X₁) (bP : Basis ι' R S.X₃) : Basis (ι ⊕ ι') R S.X₂ :=
Basis.mk (linearIndependent_shortExact hS' bN.linearIndependent bP.linearIndependent)
(span_rightExact hS'.exact (le_of_eq (bN.span_eq.symm)) (le_of_eq (bP.span_eq.symm)) hS'.epi_g)
