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 G (MonoidAlgebra k G) for AddMonoidAlgebra because mathlib does not have the notion of distributive actions of additive groups.

Multiplicative monoids

@[implicit_reducible]

noncomputable instance MonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] : DistribMulAction R (MonoidAlgebra k G)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] : DistribMulAction R (AddMonoidAlgebra k G)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.module {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] : Module R (MonoidAlgebra S M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.module {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] : Module R (AddMonoidAlgebra S M)

noncomputable def MonoidAlgebra.coeffLinearEquiv (R : Type u_2) {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] : MonoidAlgebra S M ≃ₗ[R] M →₀ S

MonoidAlgebra.coeff as a linear equiv.

noncomputable def AddMonoidAlgebra.coeffLinearEquiv (R : Type u_2) {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] : AddMonoidAlgebra S M ≃ₗ[R] M →₀ S

MonoidAlgebra.coeff as a linear equiv.

@[simp]

theorem AddMonoidAlgebra.coeffLinearEquiv_symm_apply (R : Type u_2) {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (a✝ : M →₀ S) : (coeffLinearEquiv R).symm a✝ = ofCoeff a✝

@[simp]

theorem MonoidAlgebra.coeffLinearEquiv_apply (R : Type u_2) {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (a✝ : MonoidAlgebra S M) : (coeffLinearEquiv R) a✝ = a✝.coeff

@[simp]

theorem MonoidAlgebra.coeffLinearEquiv_symm_apply (R : Type u_2) {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (a✝ : M →₀ S) : (coeffLinearEquiv R).symm a✝ = ofCoeff a✝

@[simp]

theorem AddMonoidAlgebra.coeffLinearEquiv_apply (R : Type u_2) {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (a✝ : AddMonoidAlgebra S M) : (coeffLinearEquiv R) a✝ = a✝.coeff

noncomputable def MonoidAlgebra.supported (R : Type u_2) {M : Type u_4} (S : Type u_5) [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.

noncomputable def AddMonoidAlgebra.supported (R : Type u_2) {M : Type u_4} (S : Type u_5) [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.

theorem MonoidAlgebra.mem_supported {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] {s : Set M} {x : MonoidAlgebra S M} : x ∈ supported R S s ↔ ↑x.coeff.support ⊆ s

theorem AddMonoidAlgebra.mem_supported {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] {s : Set M} {x : AddMonoidAlgebra S M} : x ∈ supported R S s ↔ ↑x.coeff.support ⊆ s

theorem MonoidAlgebra.mem_supported' {R : Type u_2} {M : Type u_4} {S : Type u_5} [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

theorem AddMonoidAlgebra.mem_supported' {R : Type u_2} {M : Type u_4} {S : Type u_5} [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

theorem MonoidAlgebra.supported_eq_map (R : Type u_2) {M : Type u_4} (S : Type u_5) [Semiring R] [Semiring S] [Module R S] (s : Set M) : supported R S s = Submodule.map (↑(coeffLinearEquiv R).symm) (Finsupp.supported S R s)

theorem AddMonoidAlgebra.supported_eq_map (R : Type u_2) {M : Type u_4} (S : Type u_5) [Semiring R] [Semiring S] [Module R S] (s : Set M) : supported R S s = Submodule.map (↑(coeffLinearEquiv R).symm) (Finsupp.supported S R s)

theorem MonoidAlgebra.supported_eq_span_single (R : Type u_2) {M : Type u_4} [Semiring R] (s : Set M) : supported R R s = Submodule.span R ((fun (m : M) => single m 1) '' s)

theorem AddMonoidAlgebra.supported_eq_span_single (R : Type u_2) {M : Type u_4} [Semiring R] (s : Set M) : supported R R s = Submodule.span R ((fun (m : M) => single m 1) '' s)

theorem MonoidAlgebra.supported_mono {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] {s t : Set M} (hst : s ⊆ t) : supported R S s ≤ supported R S t

theorem AddMonoidAlgebra.supported_mono {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] {s t : Set M} (hst : s ⊆ t) : supported R S s ≤ supported R S t

noncomputable def MonoidAlgebra.supportedEquivFinsupp {R : Type u_2} {M : Type u_4} {S : Type u_5} [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.

noncomputable def AddMonoidAlgebra.supportedEquivFinsupp {R : Type u_2} {M : Type u_4} {S : Type u_5} [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.

@[simp]

theorem AddMonoidAlgebra.supportedEquivFinsupp_apply_apply {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↥(supported R S s)) (a✝¹ : { x : M // x ∈ s }) : ((supportedEquivFinsupp s) a✝) a✝¹ = (↑a✝).coeff ↑a✝¹

@[simp]

theorem MonoidAlgebra.supportedEquivFinsupp_apply_apply {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↥(supported R S s)) (a✝¹ : { x : M // x ∈ s }) : ((supportedEquivFinsupp s) a✝) a✝¹ = (↑a✝).coeff ↑a✝¹

@[simp]

theorem MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) : (↑((supportedEquivFinsupp s).symm a✝)).support.val = Multiset.map Subtype.val a✝.support.val

@[simp]

theorem AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) : (↑((supportedEquivFinsupp s).symm a✝)).support.val = Multiset.map Subtype.val a✝.support.val

@[simp]

theorem AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↥(supported R S s)) : ((supportedEquivFinsupp s) a✝).support.val = Multiset.map (fun (x : ↥({x ∈ (↑a✝).coeff.support | x ∈ s})) => ⟨↑x, ⋯⟩) (Multiset.filter (fun (x : M) => x ∈ s) (↑a✝).coeff.support.val).attach

@[simp]

theorem AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) (a : M) : ↑((supportedEquivFinsupp s).symm a✝) a = if h : a ∈ s then a✝ ⟨a, h⟩ else 0

@[simp]

theorem MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↑s →₀ S) (a : M) : ↑((supportedEquivFinsupp s).symm a✝) a = if h : a ∈ s then a✝ ⟨a, h⟩ else 0

@[simp]

theorem MonoidAlgebra.supportedEquivFinsupp_apply_support_val {R : Type u_2} {M : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] [Module R S] (s : Set M) (a✝ : ↥(supported R S s)) : ((supportedEquivFinsupp s) a✝).support.val = Multiset.map (fun (x : ↥({x ∈ (↑a✝).coeff.support | x ∈ s})) => ⟨↑x, ⋯⟩) (Multiset.filter (fun (x : M) => x ∈ s) (↑a✝).coeff.support.val).attach

instance MonoidAlgebra.instIsTorsionFree {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] [Module.IsTorsionFree R k] : Module.IsTorsionFree R (MonoidAlgebra k G)

instance AddMonoidAlgebra.instIsTorsionFree {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] [Module.IsTorsionFree R k] : Module.IsTorsionFree R (AddMonoidAlgebra k G)

instance MonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] : FaithfulSMul R (MonoidAlgebra k G)

instance AddMonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] : FaithfulSMul R (AddMonoidAlgebra k G)

noncomputable def MonoidAlgebra.basis (R : Type u_6) (k : Type u_7) [Semiring k] : Module.Basis R k (MonoidAlgebra k R)

The standard basis for a monoid algebra.

noncomputable def AddMonoidAlgebra.basis (R : Type u_6) (k : Type u_7) [Semiring k] : Module.Basis R k (AddMonoidAlgebra k R)

The standard basis for an additive monoid algebra.

@[simp]

theorem MonoidAlgebra.basis_apply {R : Type u_2} (k : Type u_6) [Semiring k] (r : R) : (basis R k) r = single r 1

@[simp]

theorem AddMonoidAlgebra.basis_apply {R : Type u_2} (k : Type u_6) [Semiring k] (r : R) : (basis R k) r = single r 1

@[implicit_reducible]

noncomputable def MonoidAlgebra.comapDistribMulActionSelf {k : Type u₁} {G : Type u₂} [Group G] [Semiring k] : DistribMulAction G (MonoidAlgebra k G)

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

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

Copies of ext lemmas and bundled singles from Finsupp

As MonoidAlgebra is a type synonym, ext will not unfold it to find ext lemmas. We need bundled version of Finsupp.single with the right types to state these lemmas. It is good practice to have those, regardless of the ext issue.

noncomputable def MonoidAlgebra.singleDistribMulActionHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid R] [DistribMulAction R k] (a : G) : k →+[R] MonoidAlgebra k G

MonoidAlgebra.single as a DistribMulActionHom.

noncomputable def AddMonoidAlgebra.singleDistribMulActionHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid R] [DistribMulAction R k] (a : G) : k →+[R] AddMonoidAlgebra k G

AddMonoidAlgebra.single as a DistribMulActionHom.

theorem MonoidAlgebra.distribMulActionHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f g : MonoidAlgebra k G →+[R] N} (h : ∀ (a : G), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)) : f = g

A copy of Finsupp.distribMulActionHom_ext' for MonoidAlgebra.

theorem AddMonoidAlgebra.distribMulActionHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f g : AddMonoidAlgebra k G →+[R] N} (h : ∀ (a : G), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)) : f = g

A copy of Finsupp.distribMulActionHom_ext' for AddMonoidAlgebra.

theorem MonoidAlgebra.distribMulActionHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f g : MonoidAlgebra k G →+[R] N} : f = g ↔ ∀ (a : G), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)

theorem AddMonoidAlgebra.distribMulActionHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Monoid R] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f g : AddMonoidAlgebra k G →+[R] N} : f = g ↔ ∀ (a : G), f.comp (singleDistribMulActionHom a) = g.comp (singleDistribMulActionHom a)

@[reducible, inline]

noncomputable abbrev MonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Semiring R] [Module R k] (a : G) : k →ₗ[R] MonoidAlgebra k G

A copy of Finsupp.lsingle for MonoidAlgebra.

@[reducible, inline]

noncomputable abbrev AddMonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Semiring R] [Module R k] (a : G) : k →ₗ[R] AddMonoidAlgebra k G

A copy of Finsupp.lsingle for AddMonoidAlgebra.

@[simp]

theorem MonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Semiring R] [Module R k] (a : G) (b : k) : (lsingle a) b = single a b

@[simp]

theorem AddMonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Semiring R] [Module R k] (a : G) (b : k) : (lsingle a) b = single a b

theorem MonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [Module R k] ⦃f g : MonoidAlgebra k G →ₗ[R] N⦄ (H : ∀ (x : G), f ∘ₗ lsingle x = g ∘ₗ lsingle x) : f = g

A copy of Finsupp.lhom_ext' for MonoidAlgebra.

theorem AddMonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [Module R k] ⦃f g : AddMonoidAlgebra k G →ₗ[R] N⦄ (H : ∀ (x : G), f ∘ₗ lsingle x = g ∘ₗ lsingle x) : f = g

theorem AddMonoidAlgebra.lhom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [Module R k] {f g : AddMonoidAlgebra k G →ₗ[R] N} : f = g ↔ ∀ (x : G), f ∘ₗ lsingle x = g ∘ₗ lsingle x

theorem MonoidAlgebra.lhom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [Module R k] {f g : MonoidAlgebra k G →ₗ[R] N} : f = g ↔ ∀ (x : G), f ∘ₗ lsingle x = g ∘ₗ lsingle x

theorem MonoidAlgebra.smul_of {R : Type u_2} {M : Type u_4} [Semiring R] [MulOneClass M] (m : M) (r : R) : r • (of R M) m = single m r

theorem MonoidAlgebra.of_mem_span_of_iff {R : Type u_2} {M : Type u_4} [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.

theorem MonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_2} {M : Type u_4} [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.

theorem MonoidAlgebra.liftNC_smul {R : Type u_2} {S : Type u_3} {M : Type u_4} [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

instance MonoidAlgebra.isScalarTower_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [IsScalarTower R k k] : IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G)

instance AddMonoidAlgebra.isScalarTower_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [IsScalarTower R k k] : IsScalarTower R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G)

instance MonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [SMulCommClass R k k] : SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G)

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

instance AddMonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [SMulCommClass R k k] : SMulCommClass R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G)

instance MonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [SMulCommClass k R k] : SMulCommClass (MonoidAlgebra k G) R (MonoidAlgebra k G)

instance AddMonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [SMulCommClass k R k] : SMulCommClass (AddMonoidAlgebra k G) R (AddMonoidAlgebra k G)

def MonoidAlgebra.submoduleOfSMulMem {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {V : Type u_5} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (W : Submodule k V) (h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W) : Submodule (MonoidAlgebra k G) V

A submodule over k which is stable under scalar multiplication by elements of G is a submodule over k[G]

Additive monoids

theorem AddMonoidAlgebra.of'_mem_span {R : Type u_2} {M : Type u_4} [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.

theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure {R : Type u_2} {M : Type u_4} [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.

theorem AddMonoidAlgebra.liftNC_smul {R : Type u_2} {S : Type u_3} {M : Type u_4} [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) φ