English
From a split exact sequence 0 → K → M → P → 0, with a retraction s of f and a basis v of M, one can construct a basis for P indexed by κ by taking the images under g of a subset of v. This gives a Basis κ R P.
Русский
Из разложения 0 → K → M → P → 0 с выборами разложения и базиса v для M можно получить базис для P, индексируемый κ, из образов элементов v под действием g.
LaTeX
$$$\exists b: \Basis(\kappa, R, P)\text{ such that } b = \{ g(v(a(i))) \}_{i\in \kappa} \text{ и условия точности выполняются. }$$$
Lean4
/-- Let `0 → K → M → P → 0` be a split exact sequence of `R`-modules, let `s : M → K` be a
retraction of `f` and `v` be a basis of `M` indexed by `κ ⊕ σ`. Then
if `s vᵢ = 0` for `i : κ` and `(s vⱼ)ⱼ` is linear independent for `j : σ`, then
the images of `vᵢ` for `i : κ` form a basis of `P`.
For convenience this is stated for an arbitrary type `ι` with two maps `κ → ι` and `σ → ι`. -/
noncomputable def ofSplitExact (hg : Function.Surjective g) (v : Basis ι R M) (hainj : Function.Injective a)
(hsa : ∀ i, s (v (a i)) = 0) (hlib : LinearIndependent R (s ∘ v ∘ b))
(hab : Codisjoint (Set.range a) (Set.range b)) : Basis κ R P :=
.mk (v.linearIndependent.linearIndependent_of_exact_of_retraction hs hfg hainj hsa)
(Submodule.top_le_span_of_exact_of_retraction hs hfg hg hsa hlib hab (by rw [v.span_eq]))
