Documentation

Mathlib.Algebra.Category.ModuleCat.Free

Exact sequences with free modules #

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

Main theorems #

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)))
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) :

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.

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) :

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

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))) :

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.

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) :

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

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
    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] :

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

    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
    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] :