The five lemma in terms of modules #
The five lemma for all abelian categories is proven in
CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
. But for universe generality
and ease of application in the unbundled setting, we reprove them here.
Main results #
LinearMap.surjective_of_surjective_of_surjective_of_injective
: a four lemmaLinearMap.injective_of_surjective_of_injective_of_injective
: another four lemmaLinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective
: the five lemma
Explanation of the variables #
In this file we always consider the following commutative diagram of additive groups (resp. modules)
M₁ --f₁--> M₂ --f₂--> M₃ --f₃--> M₄ --f₄--> M₅
| | | | |
i₁ i₂ i₃ i₄ i₅
| | | | |
v v v v v
N₁ --g₁--> N₂ --g₂--> N₃ --g₃--> N₄ --g₄--> N₅
with exact rows.
Implementation details #
In theory, we could prove these in the multiplicative version and let to_additive
prove
the additive variants. But Function.Exact
currently has no multiplicative analogue (yet).
One four lemma in terms of (additive) groups. For a diagram explaining the variables, see the module docstring.
One four lemma in terms of (additive) groups. For a diagram explaining the variables, see the module docstring.
The five lemma in terms of (additive) groups. For a diagram explaining the variables, see the module docstring.
One four lemma in terms of modules. For a diagram explaining the variables, see the module docstring.
One four lemma in terms of modules. For a diagram explaining the variables, see the module docstring.
The five lemma in terms of modules. For a diagram explaining the variables, see the module docstring.