Module structure on monoid algebras #

Main results #

MonoidAlgebra.module, AddMonoidAlgebra.module: lift a module structure to monoid algebras

Implementation notes #

We do not state the equivalent of DistribMulAction M (MonoidAlgebra S M) for AddMonoidAlgebra because mathlib does not have the notion of distributive actions of additive groups.

Multiplicative monoids #

source

@[instance_reducible]

noncomputable instance MonoidAlgebra.distribMulAction {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid S] [Semiring R] [DistribMulAction S R] :

DistribMulAction S (MonoidAlgebra R M)

source

@[instance_reducible]

noncomputable instance AddMonoidAlgebra.distribMulAction {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid S] [Semiring R] [DistribMulAction S R] :

DistribMulAction S (AddMonoidAlgebra R M)

source

@[simp]

theorem MonoidAlgebra.mapDomain_smul {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Monoid S] [Semiring R] [DistribMulAction S R] (f : M → N) (s : S) (x : MonoidAlgebra R M) :

mapDomain f (s • x) = s • mapDomain f x

source

@[simp]

theorem AddMonoidAlgebra.mapDomain_vadd {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Monoid S] [Semiring R] [DistribMulAction S R] (f : M → N) (s : S) (x : AddMonoidAlgebra R M) :

mapDomain f (s • x) = s • mapDomain f x

source

@[instance_reducible]

noncomputable instance MonoidAlgebra.instModule {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] :

Module R (MonoidAlgebra S M)

source

@[instance_reducible]

noncomputable instance AddMonoidAlgebra.instModule {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] :

Module R (AddMonoidAlgebra S M)

source

instance MonoidAlgebra.instIsTorsionFree {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] [Module.IsTorsionFree R S] :

Module.IsTorsionFree R (MonoidAlgebra S M)

source

instance AddMonoidAlgebra.instIsTorsionFree {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] [Module.IsTorsionFree R S] :

Module.IsTorsionFree R (AddMonoidAlgebra S M)

source

noncomputable def MonoidAlgebra.coeffLinearEquiv (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] :

MonoidAlgebra S M ≃ₗ[R] M →₀ S

MonoidAlgebra.coeff as a linear equiv.

Instances For

source

noncomputable def AddMonoidAlgebra.coeffLinearEquiv (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] :

AddMonoidAlgebra S M ≃ₗ[R] M →₀ S

MonoidAlgebra.coeff as a linear equiv.

Instances For

source

@[simp]

theorem AddMonoidAlgebra.coeffLinearEquiv_symm_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (a✝ : M →₀ S) :

(coeffLinearEquiv R).symm a✝ = ofCoeff a✝

source

@[simp]

theorem MonoidAlgebra.coeffLinearEquiv_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (a✝ : MonoidAlgebra S M) :

(coeffLinearEquiv R) a✝ = a✝.coeff

source

@[simp]

theorem AddMonoidAlgebra.coeffLinearEquiv_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (a✝ : AddMonoidAlgebra S M) :

(coeffLinearEquiv R) a✝ = a✝.coeff

source

@[simp]

theorem MonoidAlgebra.coeffLinearEquiv_symm_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (a✝ : M →₀ S) :

(coeffLinearEquiv R).symm a✝ = ofCoeff a✝

source

noncomputable def MonoidAlgebra.mapDomainLinearMap (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (f : M → N) :

MonoidAlgebra S M →ₗ[R] MonoidAlgebra S N

MonoidAlgebra.mapDomain as a linear map.

Instances For

source

noncomputable def AddMonoidAlgebra.mapDomainLinearMap (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (f : M → N) :

AddMonoidAlgebra S M →ₗ[R] AddMonoidAlgebra S N

AddMonoidAlgebra.mapDomain as a linear map.

Instances For

source

@[simp]

theorem MonoidAlgebra.coeff_mapDomainLinearMap {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (f : M → N) (x : MonoidAlgebra S M) :

((mapDomainLinearMap R S f) x).coeff = Finsupp.mapDomain f x.coeff

source

@[simp]

theorem AddMonoidAlgebra.coeff_mapDomainLinearMap {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (f : M → N) (x : AddMonoidAlgebra S M) :

((mapDomainLinearMap R S f) x).coeff = Finsupp.mapDomain f x.coeff

source

@[simp]

theorem MonoidAlgebra.mapDomainLinearMap_single {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (f : M → N) (s : S) (m : M) :

(mapDomainLinearMap R S f) (single m s) = single (f m) s

source

@[simp]

theorem AddMonoidAlgebra.mapDomainLinearMap_single {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (f : M → N) (s : S) (m : M) :

(mapDomainLinearMap R S f) (single m s) = single (f m) s

source

@[simp]

theorem MonoidAlgebra.mapDomainLinearMap_comp {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [Semiring R] [Semiring S] [Module R S] (f : M → N) (g : N → O) :

mapDomainLinearMap R S (g ∘ f) = mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f

source

@[simp]

theorem AddMonoidAlgebra.mapDomainLinearMap_comp {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [Semiring R] [Semiring S] [Module R S] (f : M → N) (g : N → O) :

mapDomainLinearMap R S (g ∘ f) = mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f

source

noncomputable def MonoidAlgebra.mapDomainLinearEquiv (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) :

MonoidAlgebra S M ≃ₗ[R] MonoidAlgebra S N

MonoidAlgebra.mapDomain as a linear equiv.

Instances For

source

noncomputable def AddMonoidAlgebra.mapDomainLinearEquiv (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) :

AddMonoidAlgebra S M ≃ₗ[R] AddMonoidAlgebra S N

AddMonoidAlgebra.mapDomain as a linear equiv.

Instances For

source

@[simp]

theorem MonoidAlgebra.coeff_mapDomainLinearEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) (x : MonoidAlgebra S M) :

((mapDomainLinearEquiv R S e) x).coeff = Finsupp.equivMapDomain e x.coeff

source

@[simp]

theorem AddMonoidAlgebra.coeff_mapDomainLinearEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) (x : AddMonoidAlgebra S M) :

((mapDomainLinearEquiv R S e) x).coeff = Finsupp.equivMapDomain e x.coeff

source

@[simp]

theorem MonoidAlgebra.mapDomainLinearEquiv_single {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) (s : S) (m : M) :

(mapDomainLinearEquiv R S e) (single m s) = single (e m) s

source

@[simp]

theorem AddMonoidAlgebra.mapDomainLinearEquiv_single {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) (s : S) (m : M) :

(mapDomainLinearEquiv R S e) (single m s) = single (e m) s

source

@[simp]

theorem MonoidAlgebra.symm_mapDomainLinearEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) :

(mapDomainLinearEquiv R S e).symm = mapDomainLinearEquiv R S e.symm

source

@[simp]

theorem AddMonoidAlgebra.symm_mapDomainLinearEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [Module R S] (e : M ≃ N) :

(mapDomainLinearEquiv R S e).symm = mapDomainLinearEquiv R S e.symm

source

@[simp]

theorem MonoidAlgebra.mapDomainLinearEquiv_trans {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [Semiring R] [Semiring S] [Module R S] (e₁ : M ≃ N) (e₂ : N ≃ O) :

mapDomainLinearEquiv R S (e₁.trans e₂) = mapDomainLinearEquiv R S e₁ ≪≫ₗ mapDomainLinearEquiv R S e₂

source

@[simp]

theorem AddMonoidAlgebra.mapDomainLinearEquiv_trans {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [Semiring R] [Semiring S] [Module R S] (e₁ : M ≃ N) (e₂ : N ≃ O) :

mapDomainLinearEquiv R S (e₁.trans e₂) = mapDomainLinearEquiv R S e₁ ≪≫ₗ mapDomainLinearEquiv R S e₂

source

noncomputable def MonoidAlgebra.uniqueLinearEquiv (R : Type u_1) {S : Type u_2} (M : Type u_3) [Semiring R] [Semiring S] [Module R S] [One M] [Subsingleton M] :

MonoidAlgebra S M ≃ₗ[R] S

The trivial monoid algebra is the base ring.

Instances For

source

noncomputable def AddMonoidAlgebra.uniqueLinearEquiv (R : Type u_1) {S : Type u_2} (M : Type u_3) [Semiring R] [Semiring S] [Module R S] [Zero M] [Subsingleton M] :

AddMonoidAlgebra S M ≃ₗ[R] S

The trivial monoid algebra is the base ring.

Instances For

source

@[simp]

theorem MonoidAlgebra.uniqueLinearEquiv_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] [One M] [Subsingleton M] (x : MonoidAlgebra S M) :

(uniqueLinearEquiv R M) x = x.coeff 1

source

@[simp]

theorem AddMonoidAlgebra.uniqueLinearEquiv_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] [Zero M] [Subsingleton M] (x : AddMonoidAlgebra S M) :

(uniqueLinearEquiv R M) x = x.coeff 0

source

@[simp]

theorem MonoidAlgebra.uniqueLinearEquiv_symm_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [Semiring R] [Semiring S] [Module R S] [One M] [Subsingleton M] (s : S) :

(uniqueLinearEquiv R M).symm s = single 1 s

source

@[simp]

theorem AddMonoidAlgebra.uniqueLinearEquiv_symm_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [Semiring R] [Semiring S] [Module R S] [Zero M] [Subsingleton M] (s : S) :

(uniqueLinearEquiv R M).symm s = single 0 s

source

noncomputable def MonoidAlgebra.supported (R : Type u_1) (S : Type u_2) {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) :

Submodule R (MonoidAlgebra S M)

The R-submodule of all elements of S[M] supported on a subset s of M.

Instances For

source

noncomputable def AddMonoidAlgebra.supported (R : Type u_1) (S : Type u_2) {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) :

Submodule R (AddMonoidAlgebra S M)

The R-submodule of all elements of S[M] supported on a subset s of M.

Instances For

source

theorem MonoidAlgebra.mem_supported {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] {s : Set M} {x : MonoidAlgebra S M} :

x ∈ supported R S s ↔ ↑x.coeff.support ⊆ s

source

theorem AddMonoidAlgebra.mem_supported {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] {s : Set M} {x : AddMonoidAlgebra S M} :

x ∈ supported R S s ↔ ↑x.coeff.support ⊆ s

source

theorem MonoidAlgebra.mem_supported' {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] {s : Set M} {x : MonoidAlgebra S M} :

x ∈ supported R S s ↔ ∀ m ∉ s, x.coeff m = 0

source

theorem AddMonoidAlgebra.mem_supported' {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] {s : Set M} {x : AddMonoidAlgebra S M} :

x ∈ supported R S s ↔ ∀ m ∉ s, x.coeff m = 0

source

theorem MonoidAlgebra.supported_eq_map (R : Type u_1) (S : Type u_2) {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) :

supported R S s = Submodule.map (↑(coeffLinearEquiv R).symm) (Finsupp.supported S R s)

source

theorem AddMonoidAlgebra.supported_eq_map (R : Type u_1) (S : Type u_2) {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) :

supported R S s = Submodule.map (↑(coeffLinearEquiv R).symm) (Finsupp.supported S R s)

source

theorem MonoidAlgebra.supported_eq_span_single (R : Type u_1) {M : Type u_3} [Semiring R] (s : Set M) :

supported R R s = Submodule.span R ((fun (m : M) => single m 1) '' s)

source

theorem AddMonoidAlgebra.supported_eq_span_single (R : Type u_1) {M : Type u_3} [Semiring R] (s : Set M) :

supported R R s = Submodule.span R ((fun (m : M) => single m 1) '' s)

source

theorem MonoidAlgebra.supported_mono {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] {s t : Set M} (hst : s ⊆ t) :

supported R S s ≤ supported R S t

source

theorem AddMonoidAlgebra.supported_mono {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] {s t : Set M} (hst : s ⊆ t) :

supported R S s ≤ supported R S t

source

noncomputable def MonoidAlgebra.supportedEquivFinsupp {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) :

↥(supported R S s) ≃ₗ[R] ↑s →₀ S

Interpret Finsupp.restrictSupportEquiv as a linear equivalence between supported M R s and s →₀ M.

Instances For

source

noncomputable def AddMonoidAlgebra.supportedEquivFinsupp {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) :

↥(supported R S s) ≃ₗ[R] ↑s →₀ S

Interpret Finsupp.restrictSupportEquiv as a linear equivalence between supported M R s and s →₀ M.

Instances For

source

@[simp]

theorem MonoidAlgebra.supportedEquivFinsupp_apply_support_val {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (x : ↥(supported R S s)) :

((supportedEquivFinsupp s) x).support.val = Multiset.map (fun (x_1 : ↥({x ∈ (↑x).coeff.support | x ∈ s})) => ⟨↑x_1, ⋯⟩) (Multiset.filter (fun (x : M) => x ∈ s) (↑x).coeff.support.val).attach

source

@[simp]

theorem MonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_support_val {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) :

(↑((supportedEquivFinsupp s).symm a✝)).coeff.support.val = Multiset.map Subtype.val a✝.support.val

source

@[simp]

theorem AddMonoidAlgebra.supportedEquivFinsupp_apply_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (x : ↥(supported R S s)) (a✝ : { x : M // x ∈ s }) :

((supportedEquivFinsupp s) x) a✝ = (↑x).coeff ↑a✝

source

@[simp]

theorem MonoidAlgebra.supportedEquivFinsupp_apply_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (x : ↥(supported R S s)) (a✝ : { x : M // x ∈ s }) :

((supportedEquivFinsupp s) x) a✝ = (↑x).coeff ↑a✝

source

@[simp]

theorem MonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) (a : M) :

(↑((supportedEquivFinsupp s).symm a✝)).coeff a = if h : a ∈ s then a✝ ⟨a, h⟩ else 0

source

@[simp]

theorem AddMonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) (a : M) :

(↑((supportedEquivFinsupp s).symm a✝)).coeff a = if h : a ∈ s then a✝ ⟨a, h⟩ else 0

source

@[simp]

theorem AddMonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_support_val {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) :

(↑((supportedEquivFinsupp s).symm a✝)).coeff.support.val = Multiset.map Subtype.val a✝.support.val

source

@[simp]

theorem AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [Module R S] (s : Set M) (x : ↥(supported R S s)) :

source

instance MonoidAlgebra.faithfulSMul {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [SMulZeroClass R S] [FaithfulSMul R S] [Nonempty M] :

FaithfulSMul R (MonoidAlgebra S M)

source

instance AddMonoidAlgebra.faithfulSMul {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [SMulZeroClass R S] [FaithfulSMul R S] [Nonempty M] :

FaithfulSMul R (AddMonoidAlgebra S M)

source

noncomputable def MonoidAlgebra.basis (R : Type u_7) (k : Type u_8) [Semiring k] :

Module.Basis R k (MonoidAlgebra k R)

The standard basis for a monoid algebra.

Instances For

source

noncomputable def AddMonoidAlgebra.basis (R : Type u_7) (k : Type u_8) [Semiring k] :

Module.Basis R k (AddMonoidAlgebra k R)

The standard basis for an additive monoid algebra.

Instances For

source

@[simp]

theorem MonoidAlgebra.basis_apply {R : Type u_1} (k : Type u_7) [Semiring k] (r : R) :

(basis R k) r = single r 1

source

@[simp]

theorem AddMonoidAlgebra.basis_apply {R : Type u_1} (k : Type u_7) [Semiring k] (r : R) :

(basis R k) r = single r 1

source

@[implicit_reducible]

noncomputable def MonoidAlgebra.comapDistribMulActionSelf {S : Type u_2} {G : Type u_6} [Group G] [Semiring S] :

DistribMulAction G (MonoidAlgebra S G)

This is not an instance as it conflicts with MonoidAlgebra.distribMulAction when M = kˣ.

TODO: Change the type to DistribMulAction Gᵈᵐᵃ S[M] and then it can be an instance. TODO: Generalise to a group acting on another, instead of just the left multiplication action.

Instances For

source

theorem MonoidAlgebra.single_mem_span_single {R : Type u_1} {M : Type u_3} [Semiring R] [Nontrivial R] {m : M} {s : Set M} :

single m 1 ∈ Submodule.span R ((fun (x : M) => single x 1) '' s) ↔ m ∈ s

source

theorem AddMonoidAlgebra.single_mem_span_single {R : Type u_1} {M : Type u_3} [Semiring R] [Nontrivial R] {m : M} {s : Set M} :

single m 1 ∈ Submodule.span R ((fun (x : M) => single x 1) '' s) ↔ m ∈ s

Copies of `ext` lemmas and bundled `single`s from `Finsupp` #

source

noncomputable def MonoidAlgebra.singleDistribMulActionHom {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [Monoid R] [DistribMulAction R S] (a : M) :

S →+[R] MonoidAlgebra S M

MonoidAlgebra.single as a DistribMulActionHom.

Instances For

source

noncomputable def AddMonoidAlgebra.singleDistribMulActionHom {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [Monoid R] [DistribMulAction R S] (a : M) :

S →+[R] AddMonoidAlgebra S M

AddMonoidAlgebra.single as a DistribMulActionHom.

Instances For

source

theorem MonoidAlgebra.distribMulActionHom_ext' {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R S] {f g : MonoidAlgebra S M →+[R] N} (h : ∀ (a : M), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)) :

f = g

A copy of Finsupp.distribMulActionHom_ext' for MonoidAlgebra.

source

theorem AddMonoidAlgebra.distribMulActionHom_ext' {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R S] {f g : AddMonoidAlgebra S M →+[R] N} (h : ∀ (a : M), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)) :

f = g

A copy of Finsupp.distribMulActionHom_ext' for AddMonoidAlgebra.

source

theorem AddMonoidAlgebra.distribMulActionHom_ext'_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R S] {f g : AddMonoidAlgebra S M →+[R] N} :

f = g ↔ ∀ (a : M), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)

source

theorem MonoidAlgebra.distribMulActionHom_ext'_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R S] {f g : MonoidAlgebra S M →+[R] N} :

f = g ↔ ∀ (a : M), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)

source

noncomputable def MonoidAlgebra.lsingle {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [Semiring R] [Module R S] (a : M) :

S →ₗ[R] MonoidAlgebra S M

A copy of Finsupp.lsingle for MonoidAlgebra.

Instances For

source

noncomputable def AddMonoidAlgebra.lsingle {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [Semiring R] [Module R S] (a : M) :

S →ₗ[R] AddMonoidAlgebra S M

A copy of Finsupp.lsingle for AddMonoidAlgebra.

Instances For

source

@[simp]

theorem MonoidAlgebra.lsingle_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [Semiring R] [Module R S] (a : M) (b : S) :

(lsingle a) b = single a b

source

@[simp]

theorem AddMonoidAlgebra.lsingle_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] [Semiring R] [Module R S] (a : M) (b : S) :

(lsingle a) b = single a b

source

theorem MonoidAlgebra.lhom_ext' {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Semiring R] [AddCommMonoid N] [Module R N] [Module R S] ⦃f g : MonoidAlgebra S M →ₗ[R] N⦄ (H : ∀ (x : M), f ∘ₗ lsingle x = g ∘ₗ lsingle x) :

f = g

A copy of Finsupp.lhom_ext' for MonoidAlgebra.

source

theorem AddMonoidAlgebra.lhom_ext' {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Semiring R] [AddCommMonoid N] [Module R N] [Module R S] ⦃f g : AddMonoidAlgebra S M →ₗ[R] N⦄ (H : ∀ (x : M), f ∘ₗ lsingle x = g ∘ₗ lsingle x) :

f = g

source

theorem AddMonoidAlgebra.lhom_ext'_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Semiring R] [AddCommMonoid N] [Module R N] [Module R S] {f g : AddMonoidAlgebra S M →ₗ[R] N} :

f = g ↔ ∀ (x : M), f ∘ₗ lsingle x = g ∘ₗ lsingle x

source

theorem MonoidAlgebra.lhom_ext'_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring S] {N : Type u_7} [Semiring R] [AddCommMonoid N] [Module R N] [Module R S] {f g : MonoidAlgebra S M →ₗ[R] N} :

f = g ↔ ∀ (x : M), f ∘ₗ lsingle x = g ∘ₗ lsingle x

source

theorem MonoidAlgebra.smul_of {R : Type u_1} {M : Type u_3} [Semiring R] [MulOneClass M] (m : M) (r : R) :

r • (of R M) m = single m r

source

theorem MonoidAlgebra.of_mem_span_of_iff {R : Type u_1} {M : Type u_3} [Semiring R] [MulOneClass M] {s : Set M} {m : M} [Nontrivial R] :

(of R M) m ∈ Submodule.span R (⇑(of R M) '' s) ↔ m ∈ s

The image of an element m : M in R[M] belongs to the submodule generated by s : Set M if and only if m ∈ s.

source

theorem MonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_3} [Semiring R] [MulOneClass M] {s : Set M} {m : M} [Nontrivial R] (h : (of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(of R M) '' s))) :

m ∈ Submonoid.closure s

If the image of an element m : M in R[M] belongs to the submodule generated by the closure of some s : Set M then m ∈ closure s.

source

theorem MonoidAlgebra.liftNC_smul {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [MulOneClass M] (f : S →+* R) (g : M →* R) (c : S) (φ : MonoidAlgebra S M) :

(liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Non-unital, non-associative algebra structure #

source

instance MonoidAlgebra.isScalarTower_self {R : Type u_1} (S : Type u_2) {M : Type u_3} [Semiring S] [DistribSMul R S] [Mul M] [IsScalarTower R S S] :

IsScalarTower R (MonoidAlgebra S M) (MonoidAlgebra S M)

source

instance AddMonoidAlgebra.isScalarTower_self {R : Type u_1} (S : Type u_2) {M : Type u_3} [Semiring S] [DistribSMul R S] [Add M] [IsScalarTower R S S] :

IsScalarTower R (AddMonoidAlgebra S M) (AddMonoidAlgebra S M)

source

instance MonoidAlgebra.smulCommClass_self {R : Type u_1} (S : Type u_2) {M : Type u_3} [Semiring S] [DistribSMul R S] [Mul M] [SMulCommClass R S S] :

SMulCommClass R (MonoidAlgebra S M) (MonoidAlgebra S M)

Note that if S is a CommSemiring then we have SMulCommClass S S S and so we can take R = S in the below. In other words, if the coefficients are commutative amongst themselves, they also commute with the algebra multiplication.

source

instance AddMonoidAlgebra.smulCommClass_self {R : Type u_1} (S : Type u_2) {M : Type u_3} [Semiring S] [DistribSMul R S] [Add M] [SMulCommClass R S S] :

SMulCommClass R (AddMonoidAlgebra S M) (AddMonoidAlgebra S M)

source

instance MonoidAlgebra.smulCommClass_symm_self {R : Type u_1} (S : Type u_2) {M : Type u_3} [Semiring S] [DistribSMul R S] [Mul M] [SMulCommClass S R S] :

SMulCommClass (MonoidAlgebra S M) R (MonoidAlgebra S M)

source

instance AddMonoidAlgebra.smulCommClass_symm_self {R : Type u_1} (S : Type u_2) {M : Type u_3} [Semiring S] [DistribSMul R S] [Add M] [SMulCommClass S R S] :

SMulCommClass (AddMonoidAlgebra S M) R (AddMonoidAlgebra S M)

source

def MonoidAlgebra.submoduleOfSMulMem {S : Type u_2} {M : Type u_3} [CommSemiring S] [Monoid M] {V : Type u_7} [AddCommMonoid V] [Module S V] [Module (MonoidAlgebra S M) V] [IsScalarTower S (MonoidAlgebra S M) V] (W : Submodule S V) (h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W) :

Submodule (MonoidAlgebra S M) V

A submodule over S which is stable under scalar multiplication by elements of M is a submodule over S[M]

Instances For

Additive monoids #

source

theorem AddMonoidAlgebra.of'_mem_span {R : Type u_1} {M : Type u_3} [Semiring R] [Nontrivial R] {m : M} {s : Set M} :

of' R M m ∈ Submodule.span R (of' R M '' s) ↔ m ∈ s

The image of an element m : M in R[M] belongs the submodule generated by s : Set M if and only if m ∈ s.

source

theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_1} {M : Type u_3} [Semiring R] [AddMonoid M] [Nontrivial R] {m : M} {s : Set M} (h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))) :

m ∈ AddSubmonoid.closure s

If the image of an element m : M in R[M] belongs the submodule generated by the closure of some s : Set M then m ∈ closure s.

source

theorem AddMonoidAlgebra.liftNC_smul {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddZeroClass M] (f : S →+* R) (g : Multiplicative M →* R) (c : S) (φ : AddMonoidAlgebra S M) :

(liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Documentation

Mathlib.Algebra.MonoidAlgebra.Module

Module structure on monoid algebras #

Main results #

Implementation notes #

Multiplicative monoids #

Copies of `ext` lemmas and bundled `single`s from `Finsupp` #

Non-unital, non-associative algebra structure #

Additive monoids #

Module structure on monoid algebras #

Main results #

Implementation notes #

Multiplicative monoids #

Copies of ext lemmas and bundled singles from Finsupp #

Non-unital, non-associative algebra structure #

Additive monoids #

Copies of `ext` lemmas and bundled `single`s from `Finsupp` #