Exact sequences with free modules

This file proves results about linear independence and span in exact sequences of modules.

Main theorems

• linearIndependent_shortExact: Given a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of R-modules and linearly independent families v : ι → X₁ and w : ι' → X₃, we get a linearly independent family ι ⊕ ι' → X₂
• span_rightExact: Given an exact sequence X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of R-modules and spanning families v : ι → X₁ and w : ι' → X₃, we get a spanning family ι ⊕ ι' → X₂
• Using linearIndependent_shortExact and span_rightExact, we prove free_shortExact: In a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 where X₁ and X₃ are free, X₂ is free as well.

Tags

linear algebra, module, free

theorem ModuleCat.disjoint_span_sum {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS : S.Exact) {v : ι → ↑S.X₁} {u : ι ⊕ ι' → ↑S.X₂} (hw : LinearIndependent R (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)) (huv : u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v) : Disjoint (Submodule.span R (Set.range (u ∘ Sum.inl))) (Submodule.span R (Set.range (u ∘ Sum.inr)))

theorem ModuleCat.linearIndependent_leftExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS : S.Exact) {v : ι → ↑S.X₁} (hv : LinearIndependent R v) {u : ι ⊕ ι' → ↑S.X₂} (hw : LinearIndependent R (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)) (hm : CategoryTheory.Mono S.f) (huv : u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v) : LinearIndependent R u

In the commutative diagram

             f     g
    0 --→ X₁ --→ X₂ --→ X₃
          ↑      ↑      ↑
         v|     u|     w|
          ι  → ι ⊕ ι' ← ι'

where the top row is an exact sequence of modules and the maps on the bottom are Sum.inl and Sum.inr. If u is injective and v and w are linearly independent, then u is linearly independent.

theorem ModuleCat.linearIndependent_shortExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS' : S.ShortExact) {v : ι → ↑S.X₁} (hv : LinearIndependent R v) {w : ι' → ↑S.X₃} (hw : LinearIndependent R w) : LinearIndependent R (Sum.elim (⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w))

Given a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of R-modules and linearly independent families v : ι → N and w : ι' → P, we get a linearly independent family ι ⊕ ι' → M

theorem ModuleCat.span_exact {ι : Type u_1} {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS : S.Exact) {v : ι → ↑S.X₁} {β : Type u_4} {u : ι ⊕ β → ↑S.X₂} (huv : u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v) (hv : ⊤ ≤ Submodule.span R (Set.range v)) (hw : ⊤ ≤ Submodule.span R (Set.range (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))) : ⊤ ≤ Submodule.span R (Set.range u)

In the commutative diagram

    f     g
 X₁ --→ X₂ --→ X₃
 ↑      ↑      ↑
v|     u|     w|
 ι  → ι ⊕ ι' ← ι'

where the top row is an exact sequence of modules and the maps on the bottom are Sum.inl and Sum.inr. If v spans X₁ and w spans X₃, then u spans X₂.

theorem ModuleCat.span_rightExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS : S.Exact) {v : ι → ↑S.X₁} {w : ι' → ↑S.X₃} (hv : ⊤ ≤ Submodule.span R (Set.range v)) (hw : ⊤ ≤ Submodule.span R (Set.range w)) (hE : CategoryTheory.Epi S.g) : ⊤ ≤ Submodule.span R (Set.range (Sum.elim (⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w)))

Given an exact sequence X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of R-modules and spanning families v : ι → X₁ and w : ι' → X₃, we get a spanning family ι ⊕ ι' → X₂

noncomputable def ModuleCat.Basis.ofShortExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS' : S.ShortExact) (bN : Module.Basis ι R ↑S.X₁) (bP : Module.Basis ι' R ↑S.X₃) : Module.Basis (ι ⊕ ι') R ↑S.X₂

In a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0, given bases for X₁ and X₃ indexed by ι and ι' respectively, we get a basis for X₂ indexed by ι ⊕ ι'.

Equations

• ModuleCat.Basis.ofShortExact hS' bN bP = Module.Basis.mk ⋯ ⋯

theorem ModuleCat.free_shortExact {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS' : S.ShortExact) [Module.Free R ↑S.X₁] [Module.Free R ↑S.X₃] : Module.Free R ↑S.X₂

In a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0, if X₁ and X₃ are free, then X₂ is free.

theorem ModuleCat.free_shortExact_rank_add {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS' : S.ShortExact) [Module.Free R ↑S.X₁] [Module.Free R ↑S.X₃] [StrongRankCondition R] : Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

theorem ModuleCat.free_shortExact_finrank_add {R : Type u_3} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS' : S.ShortExact) {n p : ℕ} [Module.Free R ↑S.X₁] [Module.Free R ↑S.X₃] [Module.Finite R ↑S.X₁] [Module.Finite R ↑S.X₃] (hN : Module.finrank R ↑S.X₁ = n) (hP : Module.finrank R ↑S.X₃ = p) [StrongRankCondition R] : Module.finrank R ↑S.X₂ = n + p