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 lemma
• LinearMap.injective_of_surjective_of_injective_of_injective: another four lemma
• LinearMap.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).

theorem AddMonoidHom.surjective_of_surjective_of_surjective_of_injective {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} {N₄ : Type u_9} [AddGroup M₁] [AddGroup M₂] [AddGroup M₃] [AddGroup M₄] [AddGroup N₁] [AddGroup N₂] [AddGroup N₃] [AddGroup N₄] (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (f₃ : M₃ →+ M₄) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (g₃ : N₃ →+ N₄) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃) (i₄ : M₄ →+ N₄) (hc₁ : g₁.comp i₁ = i₂.comp f₁) (hc₂ : g₂.comp i₂ = i₃.comp f₂) (hc₃ : g₃.comp i₃ = i₄.comp f₃) (hf₂ : Function.Exact ⇑f₂ ⇑f₃) (hg₁ : Function.Exact ⇑g₁ ⇑g₂) (hg₂ : Function.Exact ⇑g₂ ⇑g₃) (hi₁ : Function.Surjective ⇑i₁) (hi₃ : Function.Surjective ⇑i₃) (hi₄ : Function.Injective ⇑i₄) : Function.Surjective ⇑i₂

One four lemma in terms of (additive) groups. For a diagram explaining the variables, see the module docstring.

theorem AddMonoidHom.injective_of_surjective_of_injective_of_injective {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} {N₄ : Type u_9} [AddGroup M₁] [AddGroup M₂] [AddGroup M₃] [AddGroup M₄] [AddGroup N₁] [AddGroup N₂] [AddGroup N₃] [AddGroup N₄] (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (f₃ : M₃ →+ M₄) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (g₃ : N₃ →+ N₄) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃) (i₄ : M₄ →+ N₄) (hc₁ : g₁.comp i₁ = i₂.comp f₁) (hc₂ : g₂.comp i₂ = i₃.comp f₂) (hc₃ : g₃.comp i₃ = i₄.comp f₃) (hf₁ : Function.Exact ⇑f₁ ⇑f₂) (hf₂ : Function.Exact ⇑f₂ ⇑f₃) (hg₁ : Function.Exact ⇑g₁ ⇑g₂) (hi₁ : Function.Surjective ⇑i₁) (hi₂ : Function.Injective ⇑i₂) (hi₄ : Function.Injective ⇑i₄) : Function.Injective ⇑i₃

One four lemma in terms of (additive) groups. For a diagram explaining the variables, see the module docstring.

theorem AddMonoidHom.bijective_of_surjective_of_bijective_of_bijective_of_injective {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {M₅ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} {N₄ : Type u_9} {N₅ : Type u_10} [AddGroup M₁] [AddGroup M₂] [AddGroup M₃] [AddGroup M₄] [AddGroup M₅] [AddGroup N₁] [AddGroup N₂] [AddGroup N₃] [AddGroup N₄] [AddGroup N₅] (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (f₃ : M₃ →+ M₄) (f₄ : M₄ →+ M₅) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (g₃ : N₃ →+ N₄) (g₄ : N₄ →+ N₅) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃) (i₄ : M₄ →+ N₄) (i₅ : M₅ →+ N₅) (hc₁ : g₁.comp i₁ = i₂.comp f₁) (hc₂ : g₂.comp i₂ = i₃.comp f₂) (hc₃ : g₃.comp i₃ = i₄.comp f₃) (hc₄ : g₄.comp i₄ = i₅.comp f₄) (hf₁ : Function.Exact ⇑f₁ ⇑f₂) (hf₂ : Function.Exact ⇑f₂ ⇑f₃) (hf₃ : Function.Exact ⇑f₃ ⇑f₄) (hg₁ : Function.Exact ⇑g₁ ⇑g₂) (hg₂ : Function.Exact ⇑g₂ ⇑g₃) (hg₃ : Function.Exact ⇑g₃ ⇑g₄) (hi₁ : Function.Surjective ⇑i₁) (hi₂ : Function.Bijective ⇑i₂) (hi₄ : Function.Bijective ⇑i₄) (hi₅ : Function.Injective ⇑i₅) : Function.Bijective ⇑i₃

The five lemma in terms of (additive) groups. For a diagram explaining the variables, see the module docstring.

theorem LinearMap.surjective_of_surjective_of_surjective_of_injective {R : Type u_1} [CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} {N₁ : Type u_7} {N₂ : Type u_8} {N₃ : Type u_9} {N₄ : Type u_10} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₃] [AddCommGroup N₄] [Module R N₁] [Module R N₂] [Module R N₃] [Module R N₄] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (f₃ : M₃ →ₗ[R] M₄) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (g₃ : N₃ →ₗ[R] N₄) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (i₄ : M₄ →ₗ[R] N₄) (hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (hc₃ : g₃ ∘ₗ i₃ = i₄ ∘ₗ f₃) (hf₂ : Function.Exact ⇑f₂ ⇑f₃) (hg₁ : Function.Exact ⇑g₁ ⇑g₂) (hg₂ : Function.Exact ⇑g₂ ⇑g₃) (hi₁ : Function.Surjective ⇑i₁) (hi₃ : Function.Surjective ⇑i₃) (hi₄ : Function.Injective ⇑i₄) : Function.Surjective ⇑i₂

One four lemma in terms of modules. For a diagram explaining the variables, see the module docstring.

theorem LinearMap.injective_of_surjective_of_injective_of_injective {R : Type u_1} [CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} {N₁ : Type u_7} {N₂ : Type u_8} {N₃ : Type u_9} {N₄ : Type u_10} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₃] [AddCommGroup N₄] [Module R N₁] [Module R N₂] [Module R N₃] [Module R N₄] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (f₃ : M₃ →ₗ[R] M₄) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (g₃ : N₃ →ₗ[R] N₄) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (i₄ : M₄ →ₗ[R] N₄) (hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (hc₃ : g₃ ∘ₗ i₃ = i₄ ∘ₗ f₃) (hf₁ : Function.Exact ⇑f₁ ⇑f₂) (hf₂ : Function.Exact ⇑f₂ ⇑f₃) (hg₁ : Function.Exact ⇑g₁ ⇑g₂) (hi₁ : Function.Surjective ⇑i₁) (hi₂ : Function.Injective ⇑i₂) (hi₄ : Function.Injective ⇑i₄) : Function.Injective ⇑i₃

One four lemma in terms of modules. For a diagram explaining the variables, see the module docstring.

theorem LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective {R : Type u_1} [CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {M₄ : Type u_5} {M₅ : Type u_6} {N₁ : Type u_7} {N₂ : Type u_8} {N₃ : Type u_9} {N₄ : Type u_10} {N₅ : Type u_11} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [AddCommGroup M₅] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Module R M₅] [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₃] [AddCommGroup N₄] [AddCommGroup N₅] [Module R N₁] [Module R N₂] [Module R N₃] [Module R N₄] [Module R N₅] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (f₃ : M₃ →ₗ[R] M₄) (f₄ : M₄ →ₗ[R] M₅) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (g₃ : N₃ →ₗ[R] N₄) (g₄ : N₄ →ₗ[R] N₅) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (i₄ : M₄ →ₗ[R] N₄) (i₅ : M₅ →ₗ[R] N₅) (hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (hc₃ : g₃ ∘ₗ i₃ = i₄ ∘ₗ f₃) (hc₄ : g₄ ∘ₗ i₄ = i₅ ∘ₗ f₄) (hf₁ : Function.Exact ⇑f₁ ⇑f₂) (hf₂ : Function.Exact ⇑f₂ ⇑f₃) (hf₃ : Function.Exact ⇑f₃ ⇑f₄) (hg₁ : Function.Exact ⇑g₁ ⇑g₂) (hg₂ : Function.Exact ⇑g₂ ⇑g₃) (hg₃ : Function.Exact ⇑g₃ ⇑g₄) (hi₁ : Function.Surjective ⇑i₁) (hi₂ : Function.Bijective ⇑i₂) (hi₄ : Function.Bijective ⇑i₄) (hi₅ : Function.Injective ⇑i₅) : Function.Bijective ⇑i₃

The five lemma in terms of modules. For a diagram explaining the variables, see the module docstring.