English
Let hg: g is surjective, hsa: s(v(a i)) = 0, hlib: linear independence of s ∘ v ∘ b, hab: Codisjoint(range a, range b), hsp: ⊤ ≤ span v. Then ⊤ ≤ span(g ∘ v ∘ a). In words: the images under g of the selected vectors generate the entire P.
Русский
Пусть g сюрьективна, s(v(a i)) = 0, s ∘ v ∘ b линейно независимы, диапазоны a и b взаимно-исключают друг друга, и ⊤ ≤ span v. Тогда ⊤ ≤ span(g ∘ v ∘ a). Иными словами, образы через g от выбранных векторов порождают весь P.
LaTeX
$$$\top \le \operatorname{span}_R \{ g(v(a(i))) : i \in \kappa \} $$$
Lean4
theorem top_le_span_of_exact_of_retraction (hg : Function.Surjective g) (hsa : ∀ i, s (v (a i)) = 0)
(hlib : LinearIndependent R (s ∘ v ∘ b)) (hab : Codisjoint (Set.range a) (Set.range b))
(hsp : ⊤ ≤ Submodule.span R (Set.range v)) : ⊤ ≤ Submodule.span R (Set.range <| g ∘ v ∘ a) :=
by
apply top_le_span_of_aux hs hfg (Sum.elim (v ∘ a) (v ∘ b)) hg hsa hlib
simp only [codisjoint_iff, Set.sup_eq_union, Set.top_eq_univ] at hab
rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
