Long exact sequence for the kernel and cokernel of a composition #
If f : M →ₗ[A] N and g : N →ₗ[A] P are A-module homomorphisms, then there is a natural
long exact sequence
0 → ker f → ker (g ∘ f) → ker g → coker f → coker (g ∘ f) → coker g → 0.
This is the same as in Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
but we don't import category theory in this file.
@[reducible, inline]
abbrev
Module.KerCokerComp.f₁
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
The map ker f → ker (g ∘ f) given by inclusion.
Equations
Instances For
@[reducible, inline]
abbrev
Module.KerCokerComp.f₂
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
The map ker (g ∘ f) → ker g induced by f.
Equations
- Module.KerCokerComp.f₂ f g = f.restrict ⋯
Instances For
@[reducible, inline]
abbrev
Module.KerCokerComp.f₃
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
The map ker g → coker f given by ker g ↪ N ↠ coker f.
Equations
- Module.KerCokerComp.f₃ f g = (LinearMap.range f).mkQ ∘ₗ (LinearMap.ker g).subtype
Instances For
@[reducible, inline]
abbrev
Module.KerCokerComp.f₄
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
The map coker f → coker (g ∘ f) induced by g.
Equations
- Module.KerCokerComp.f₄ f g = (LinearMap.range f).mapQ (LinearMap.range (g ∘ₗ f)) g ⋯
Instances For
@[reducible, inline]
abbrev
Module.KerCokerComp.f₅
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
The map coker (g ∘ f) → coker g given by projection.
Equations
Instances For
theorem
Module.KerCokerComp.injective_f₁
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
Function.Injective ⇑(f₁ f g)
theorem
Module.KerCokerComp.exact_f₁_f₂
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
Function.Exact ⇑(f₁ f g) ⇑(f₂ f g)
theorem
Module.KerCokerComp.exact_f₂_f₃
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
Function.Exact ⇑(f₂ f g) ⇑(f₃ f g)
theorem
Module.KerCokerComp.exact_f₃_f₄
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
Function.Exact ⇑(f₃ f g) ⇑(f₄ f g)
theorem
Module.KerCokerComp.exact_f₄_f₅
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
Function.Exact ⇑(f₄ f g) ⇑(f₅ f g)
theorem
Module.KerCokerComp.surjective_f₅
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
{N : Type w}
[AddCommGroup N]
[Module A N]
{P : Type x}
[AddCommGroup P]
[Module A P]
(f : M →ₗ[A] N)
(g : N →ₗ[A] P)
:
Function.Surjective ⇑(f₅ f g)