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 sequence0 ⟶ N ⟶ M ⟶ P ⟶ 0
ofR
-modules and linearly independent familiesv : ι → N
andw : ι' → M
, we get a linearly independent familyι ⊕ ι' → M
span_rightExact
: Given an exact sequenceN ⟶ M ⟶ P ⟶ 0
ofR
-modules and spanning familiesv : ι → N
andw : ι' → M
, we get a spanning familyι ⊕ ι' → M
- Using
linearIndependent_shortExact
andspan_rightExact
, we provefree_shortExact
: In a short exact sequence0 ⟶ N ⟶ M ⟶ P ⟶ 0
whereN
andP
are free,M
is free as well.
Tags #
linear algebra, module, free
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.
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
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
.
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
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
In a short exact sequence 0 ⟶ N ⟶ M ⟶ P ⟶ 0
, if N
and P
are free, then M
is free.