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)