Theorems · Definition · linear algebra

Module.Basis.ofSplitExact

{R : Type u_1} →
  {M : Type u_2} →
    {K : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup K] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R K] →
                    [inst_6 : Module R P] →
                      {f : K →ₗ[R] M} →
                        {g : M →ₗ[R] P} →
                          {s : M →ₗ[R] K} →
                            s ∘ₗ f = LinearMap.id →
                              Function.Exact ⇑f ⇑g →
                                {ι : Type u_5} →
                                  {κ : Type u_6} →
                                    {σ : Type u_7} →
                                      {a : κ → ι} →
                                        {b : σ → ι} →
                                          Function.Surjective ⇑g →
                                            (v : Module.Basis ι R M) →
                                              Function.Injective a →
                                                (∀ (i : κ), s (v (a i)) = 0) →
                                                  LinearIndependent R (⇑s ∘ ⇑v ∘ b) →
                                                    Codisjoint (Set.range a) (Set.range b) → Module.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 σ → ι.

Defined in

Mathlib.LinearAlgebra.Basis.Exact

Cited by

2 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupAddCommGroupAddCommGroupModuleModuleModule