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.noZeroSMulDivisors {k : Type u₁} {G : Type u₂} {R : Type u_2} [Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] : NoZeroSMulDivisors R (MonoidAlgebra k G)

instance AddMonoidAlgebra.noZeroSMulDivisors {k : Type u₁} {G : Type u₂} {R : Type u_2} [Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] : NoZeroSMulDivisors R (AddMonoidAlgebra k G)

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)

Equations

• MonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k

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)

Equations

• AddMonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k

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)

Equations

• MonoidAlgebra.module = Finsupp.module G k

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)

Equations

• AddMonoidAlgebra.module = Finsupp.module G k

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.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ᵈᵐᵃ (MonoidAlgebra k G) and then it can be an instance. TODO: Generalise to a group acting on another, instead of just the left multiplication action.

Equations

• MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction

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.

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 (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single 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 (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single 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 (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single 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 (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single 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.

Equations

• MonoidAlgebra.lsingle a = Finsupp.lsingle a

@[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.

Equations

• AddMonoidAlgebra.lsingle a = Finsupp.lsingle a

@[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 {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (g : G) (r : k) : r • (of k G) g = single g r

theorem MonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] {R : Type u_5} [Semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : MonoidAlgebra k G) : (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 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 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)

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 MonoidAlgebra k G

Equations

• MonoidAlgebra.submoduleOfSMulMem W h = { carrier := ↑W, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Additive monoids

theorem AddMonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] {R : Type u_5} [AddZeroClass G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (c : k) (φ : MonoidAlgebra k G) : (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Non-unital, non-associative algebra structure

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

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