Finiteness of (sub)modules and finitely supported functions #
theorem
Submodule.fg_of_fg_map_of_fg_inf_ker
{R : Type u_4}
{M : Type u_5}
{P : Type u_6}
[Ring R]
[AddCommGroup M]
[Module R M]
[AddCommGroup P]
[Module R P]
(f : M →ₗ[R] P)
{s : Submodule R M}
(hs1 : (Submodule.map f s).FG)
(hs2 : (s ⊓ LinearMap.ker f).FG)
:
s.FG
If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.
theorem
Submodule.fg_ker_comp
{R : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[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)
(hf1 : (LinearMap.ker f).FG)
(hf2 : (LinearMap.ker g).FG)
(hsur : Function.Surjective ⇑f)
:
(LinearMap.ker (g ∘ₗ f)).FG
The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.
instance
Module.Finite.finsupp
{R : Type u_2}
{V : Type u_3}
[Ring R]
[AddCommGroup V]
[Module R V]
{ι : Type u_1}
[Finite ι]
[Module.Finite R V]
:
Module.Finite R (ι →₀ V)
Equations
- ⋯ = ⋯