Basis from a split exact sequence

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.

We treat linear independence and the span condition separately. For convenience this is stated not for κ ⊕ σ, but for an arbitrary type ι with two maps κ → ι and σ → ι.

theorem LinearIndependent.linearIndependent_of_exact_of_retraction {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup K] [AddCommGroup P] [Module R M] [Module R K] [Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact ⇑f ⇑g) {ι : Type u_5} {κ : Type u_6} {v : ι → M} {a : κ → ι} (hainj : Function.Injective a) (hsa : ∀ (i : κ), s (v (a i)) = 0) (hli : LinearIndependent R v) : LinearIndependent R (⇑g ∘ v ∘ a)

theorem Submodule.top_le_span_of_exact_of_retraction {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup K] [AddCommGroup P] [Module R M] [Module R K] [Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact ⇑f ⇑g) {ι : Type u_5} {κ : Type u_6} {σ : Type u_7} {v : ι → M} {a : κ → ι} {b : σ → ι} (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 : ⊤ ≤ span R (Set.range v)) : ⊤ ≤ span R (Set.range (⇑g ∘ v ∘ a))

noncomputable def Module.Basis.ofSplitExact {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup K] [AddCommGroup P] [Module R M] [Module R K] [Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact ⇑f ⇑g) {ι : Type u_5} {κ : Type u_6} {σ : Type u_7} {a : κ → ι} {b : σ → ι} (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

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 σ → ι.

Equations

• Module.Basis.ofSplitExact hs hfg hg v hainj hsa hlib hab = Module.Basis.mk ⋯ ⋯