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 ⟶ N ⟶ M ⟶ P ⟶ 0 of R-modules and linearly independent families v : ι → N and w : ι' → M, we get a linearly independent family ι ⊕ ι' → M
span_rightExact: Given an exact sequence N ⟶ M ⟶ P ⟶ 0 of R-modules and spanning families v : ι → N and w : ι' → M, we get a spanning family ι ⊕ ι' → M
Using linearIndependent_shortExact and span_rightExact, we prove free_shortExact: In a short exact sequence 0 ⟶ N ⟶ M ⟶ P ⟶ 0 where N and P are free, M 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] {N : ModuleCat R} {P : ModuleCat R} {v : ι → ↑N} {M : ModuleCat R} {u : ι ⊕ ι' → ↑M} {f : N ⟶ M} {g : M ⟶ P} (hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)) (he : CategoryTheory.Exact f g) (huv : u ∘ Sum.inl = ↑f ∘ v) :

Disjoint (Submodule.span R (Set.range (u ∘ Sum.inl))) (Submodule.span R (Set.range (u ∘ Sum.inr)))

source

theorem ModuleCat.linearIndependent_leftExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {v : ι → ↑N} (hv : LinearIndependent R v) {M : ModuleCat R} {u : ι ⊕ ι' → ↑M} {f : N ⟶ M} {g : M ⟶ P} (hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)) (hm : CategoryTheory.Mono f) (he : CategoryTheory.Exact f g) (huv : u ∘ Sum.inl = ↑f ∘ v) :

LinearIndependent R u

In the commutative diagram

             f     g
    0 --→ N --→ M --→  P
          ↑     ↑      ↑
         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.

source

theorem ModuleCat.linearIndependent_shortExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {v : ι → ↑N} (hv : LinearIndependent R v) {M : ModuleCat R} {f : N ⟶ M} {g : M ⟶ P} {w : ι' → ↑P} (hw : LinearIndependent R w) (hse : CategoryTheory.ShortExact f g) :

LinearIndependent R (Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w))

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

source

theorem ModuleCat.span_exact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {v : ι → ↑N} {M : ModuleCat R} {u : ι ⊕ ι' → ↑M} {f : N ⟶ M} {g : M ⟶ P} (he : CategoryTheory.Exact f g) (huv : u ∘ Sum.inl = ↑f ∘ v) (hv : ⊤ ≤ Submodule.span R (Set.range v)) (hw : ⊤ ≤ Submodule.span R (Set.range (↑g ∘ u ∘ Sum.inr))) :

⊤ ≤ Submodule.span R (Set.range u)

In the commutative diagram

    f     g
 N --→ M --→  P
 ↑     ↑      ↑
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 N and w spans P, then u spans M.

source

theorem ModuleCat.span_rightExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {v : ι → ↑N} {M : ModuleCat R} {f : N ⟶ M} {g : M ⟶ P} {w : ι' → ↑P} (hv : ⊤ ≤ Submodule.span R (Set.range v)) (hw : ⊤ ≤ Submodule.span R (Set.range w)) (hE : CategoryTheory.Epi g) (he : CategoryTheory.Exact f g) :

⊤ ≤ Submodule.span R (Set.range (Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w)))

Given an exact sequence N ⟶ M ⟶ P ⟶ 0 of R-modules and spanning families v : ι → N and w : ι' → P, we get a spanning family ι ⊕ ι' → M

source

noncomputable def ModuleCat.Basis.ofShortExact {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {M : ModuleCat R} {f : N ⟶ M} {g : M ⟶ P} (h : CategoryTheory.ShortExact f g) (bN : Basis ι R ↑N) (bP : Basis ι' R ↑P) :

Basis (ι ⊕ ι') R ↑M

In a short exact sequence 0 ⟶ N ⟶ M ⟶ P ⟶ 0, given bases for N and P indexed by ι and ι' respectively, we get a basis for M indexed by ι ⊕ ι'.

Instances For

source

theorem ModuleCat.free_shortExact {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {M : ModuleCat R} {f : N ⟶ M} {g : M ⟶ P} (h : CategoryTheory.ShortExact f g) [Module.Free R ↑N] [Module.Free R ↑P] :

Module.Free R ↑M

In a short exact sequence 0 ⟶ N ⟶ M ⟶ P ⟶ 0, if N and P are free, then M is free.

source

theorem ModuleCat.free_shortExact_rank_add {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {M : ModuleCat R} {f : N ⟶ M} {g : M ⟶ P} (h : CategoryTheory.ShortExact f g) [Module.Free R ↑N] [Module.Free R ↑P] [StrongRankCondition R] :

Module.rank R ↑M = Module.rank R ↑N + Module.rank R ↑P

source

theorem ModuleCat.free_shortExact_finrank_add {R : Type u_3} [Ring R] {N : ModuleCat R} {P : ModuleCat R} {n : ℕ} {p : ℕ} {M : ModuleCat R} {f : N ⟶ M} {g : M ⟶ P} (h : CategoryTheory.ShortExact f g) [Module.Free R ↑N] [Module.Finite R ↑N] [Module.Free R ↑P] [Module.Finite R ↑P] (hN : FiniteDimensional.finrank R ↑N = n) (hP : FiniteDimensional.finrank R ↑P = p) [StrongRankCondition R] :

FiniteDimensional.finrank R ↑M = n + p