# 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 #

• 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 : } {P : } {v : ιN} {M : } {u : ι ι'M} {f : N M} {g : M P} (hw : LinearIndependent R (g u Sum.inr)) (he : ) (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 : } {P : } {v : ιN} (hv : ) {M : } {u : ι ι'M} {f : N M} {g : M P} (hw : LinearIndependent R (g u Sum.inr)) (hm : ) (he : ) (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 : } {P : } {v : ιN} (hv : ) {M : } {f : N M} {g : M P} {w : ι'P} (hw : ) (hse : ) :

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 : } {P : } {v : ιN} {M : } {u : ι ι'M} {f : N M} {g : M P} (he : ) (huv : u Sum.inl = f v) (hv : ) (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 : } {P : } {v : ιN} {M : } {f : N M} {g : M P} {w : ι'P} (hv : ) (hw : ) (hE : ) (he : ) :

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 : } {P : } {M : } {f : N M} {g : M P} (h : ) (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 : } {P : } {M : } {f : N M} {g : M P} (h : ) [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 : } {P : } {M : } {f : N M} {g : M P} (h : ) [Module.Free R N] [Module.Free R P] :
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 : } {P : } {n : } {p : } {M : } {f : N M} {g : M P} (h : ) [Module.Free R N] [] [Module.Free R P] [] (hN : ) (hP : ) :
= n + p