Finiteness of kernels and cokernels of composites #
For linear maps f : M → N and g : N → P, the cokernels fit into an exact sequence
N ⧸ range f → P ⧸ range (g ∘ f) → P ⧸ range g → 0 (LinearMap.exact_cokerToCokerComp_factor),
so the cokernel of g ∘ f is finitely generated when those of f and g are. Over a noetherian
ring, the kernel of g ∘ f is likewise finitely generated when those of f and g are: it is an
extension of a submodule of ker g by ker f.
Main results #
Module.Finite.quotient_range_comp: the cokernel ofg ∘ fis finite if those offandgare.Module.Finite.ker_comp: over a noetherian ring, the kernel ofg ∘ fis finite if those offandgare.
theorem
Module.Finite.quotient_range_comp
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[AddCommGroup P]
[Module R P]
(f : M →ₗ[R] N)
(g : N →ₗ[R] P)
[Module.Finite R (N ⧸ f.range)]
[Module.Finite R (P ⧸ g.range)]
:
Module.Finite R (P ⧸ (g ∘ₗ f).range)
If the cokernels of f : M → N and g : N → P are finitely generated, then so is the
cokernel of g ∘ f.
theorem
Module.Finite.ker_comp
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[AddCommGroup P]
[Module R P]
[IsNoetherianRing R]
(f : M →ₗ[R] N)
(g : N →ₗ[R] P)
[Module.Finite R ↥f.ker]
[Module.Finite R ↥g.ker]
:
Module.Finite R ↥(g ∘ₗ f).ker
Over a noetherian ring, if the kernels of f : M → N and g : N → P are finitely generated,
then so is the kernel of g ∘ f.