English
The construction of a new Basis κ R P from a split exact sequence and a basis v of M, selecting a subset of indices κ, under suitable hypotheses, yields a Basis κ R P.
Русский
Построение нового базиса κ R P из разложения с разбиением на частичные индексы κ и базиса v модуля M при заданных предпосылках.
LaTeX
$$$\text{ofSplitExact} : \text{Basis}(κ, R, P)$$$
Lean4
/-- Let `b` be a basis for a submodule `N` of `M`. If `y : M` is linear independent of `N`
and `y` and `N` together span the whole of `M`, then there is a basis for `M`
whose basis vectors are given by `Fin.cons y b`. -/
noncomputable def mkFinCons {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R N)
(hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z : M, ∃ c : R, z + c • y ∈ N) :
Basis (Fin (n + 1)) R M :=
have span_b : Submodule.span R (Set.range (N.subtype ∘ b)) = N := by
rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]
Basis.mk (v := Fin.cons y (N.subtype ∘ b))
((b.linearIndependent.map' N.subtype (Submodule.ker_subtype _)).fin_cons' _ _
(by
rintro c ⟨x, hx⟩ hc
rw [span_b] at hx
exact hli c x hx hc))
fun x _ => by
rw [Fin.range_cons, Submodule.mem_span_insert', span_b]
exact hsp x
