English
In a short exact sequence 0 → X1 → X2 → X3 → 0 of R-modules, with spanning families v for X1 and w for X3, there is a spanning family for X2 given by Sum.elim of the induced maps, under the hypotheses hv, hw, hE.
Русский
В короткой точной последовательности 0 → X1 → X2 → X3 → 0 модулей над R, с базами v для X1 и w для X3, существует базис для X2, задаваемый функцией Sum.elim применительно к индуцированным отображениям, при условиях hv, hw, hE.
LaTeX
$$$\top \le span_R( range ( Sum.elim (S.f \circ v) (S.g.hom.toFun.invFun \circ w) ))$ under hv hw hE$$
Lean4
/-- Given an exact sequence `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` of `R`-modules and spanning
families `v : ι → X₁` and `w : ι' → X₃`, we get a spanning family `ι ⊕ ι' → X₂` -/
theorem span_rightExact {w : ι' → S.X₃} (hv : ⊤ ≤ span R (range v)) (hw : ⊤ ≤ span R (range w)) (hE : Epi S.g) :
⊤ ≤ span R (range (Sum.elim (S.f ∘ v) (S.g.hom.toFun.invFun ∘ w))) :=
by
refine span_exact hS ?_ hv ?_
· simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
· convert hw
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
rw [ModuleCat.epi_iff_surjective] at hE
rw [← Function.comp_assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE), Function.id_comp]
