Finiteness of (sub)modules and finitely supported functions #
noncomputable def
LinearMap.finsuppLinearMap
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
(S : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
:
The linear map from Hom(M,N)^(ι) to Hom(M,N^(ι)). This is the Finsupp version of
the forward direction of LinearEquiv.linearMapPi.
Equations
- LinearMap.finsuppLinearMap S = { toFun := fun (x : M) => Finsupp.mapRange.linearMap (LinearMap.id.flip x), map_add' := ⋯, map_smul' := ⋯ }.flip
Instances For
@[simp]
theorem
LinearMap.finsuppLinearMap_apply_apply_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
(S : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
(m : ι →₀ M →ₗ[R] N)
(m✝ : M)
(a✝ : ι)
:
@[simp]
theorem
LinearMap.finsuppLinearMap_apply_apply_support
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
(S : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
(m : ι →₀ M →ₗ[R] N)
(m✝ : M)
:
theorem
LinearMap.finsuppLinearMap_injective
(R : Type u_1)
(M : Type u_2)
(N : Type u_3)
(ι : Type u_4)
(S : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
:
theorem
LinearMap.finsuppLinearMap_bijective_of_moduleFinite
(R : Type u_1)
(M : Type u_2)
(N : Type u_3)
(ι : Type u_4)
(S : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
[Module.Finite R M]
:
theorem
LinearMap.finsuppLinearMap_bijective_of_finite
(R : Type u_1)
(M : Type u_2)
(N : Type u_3)
(ι : Type u_4)
(S : Type u_5)
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
[Semiring S]
[Module S N]
[SMulCommClass R S N]
[Finite ι]
:
theorem
Submodule.fg_of_fg_map_of_fg_inf_ker
{R : Type u_1}
{M : Type u_2}
{P : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[AddCommGroup P]
[Module R P]
(f : M →ₗ[R] P)
{s : Submodule R M}
(hs1 : (map f s).FG)
(hs2 : (s ⊓ f.ker).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_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)
(hf1 : f.ker.FG)
(hf2 : g.ker.FG)
(hsur : Function.Surjective ⇑f)
:
The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.
theorem
Module.Finite.of_exact
{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}
(h_exact : Function.Exact ⇑f ⇑g)
(h_surj : Function.Surjective ⇑g)
[Module.Finite R M]
[Module.Finite R P]
:
Module.Finite R N
If $M → N → P → 0$ is exact and $M$ and $P$ are finitely generated then so is $N$.
This is the Module.Finite version of Submodule.fg_of_fg_map_of_fg_inf_ker.
theorem
Module.Finite.of_submodule_quotient
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
[Module.Finite R ↥N]
[Module.Finite R (M ⧸ N)]
:
Module.Finite R M
instance
Module.Finite.finsupp
{R : Type u_2}
{V : Type u_3}
[Semiring R]
[AddCommMonoid V]
[Module R V]
{ι : Type u_1}
[Finite ι]
[Module.Finite R V]
:
Module.Finite R (ι →₀ V)
instance
AddMonoidAlgebra.moduleFinite
{M : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Finite M]
[Semiring R]
[Semiring S]
[Module R S]
[Module.Finite R S]
:
Module.Finite R (AddMonoidAlgebra S M)
instance
MonoidAlgebra.moduleFinite
{M : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Finite M]
[Semiring R]
[Semiring S]
[Module R S]
[Module.Finite R S]
:
Module.Finite R (MonoidAlgebra S M)