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

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)

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)

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

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

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)

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.

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

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.

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.

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 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)

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)

@[reducible, inline]

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]

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 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 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) φ