# Module structure on monoid algebras #

## Main results #

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

### Multiplicative monoids #

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

source
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

source
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)
source
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ˣ`.

Equations

- MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction

Instances For

#### Copies of `ext` lemmas and bundled `single`s 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.

source
theorem MonoidAlgebra.distribMulActionHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Monoid R] [Semiring k] [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`.

source
theorem MonoidAlgebra.distribMulActionHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Monoid R] [Semiring k] [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)
source
@[reducible, inline]
abbrev MonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) :
k →ₗ[R] MonoidAlgebra k G

A copy of `Finsupp.lsingle` for `MonoidAlgebra`.

Equations

- MonoidAlgebra.lsingle a = Finsupp.lsingle a

Instances For

source
@[simp]
theorem MonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
(lsingle a) b = single a b
source
theorem MonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Semiring R] [Semiring k] [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`.

source
theorem MonoidAlgebra.lhom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Semiring R] [Semiring k] [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
source
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
source
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 #

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

source
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)
source
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' := ⋯ }

Instances For

### Additive monoids #

source
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

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

It is hard to state the equivalent of `DistribMulAction G k[G]` because we've never discussed actions of additive groups.

#### Semiring structure #

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

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

As `AddMonoidAlgebra` 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.

source
theorem AddMonoidAlgebra.distribMulActionHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Monoid R] [Semiring k] [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`.

source
theorem AddMonoidAlgebra.distribMulActionHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Monoid R] [Semiring k] [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)
source
@[reducible, inline]
abbrev AddMonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) :
k →ₗ[R] AddMonoidAlgebra k G

A copy of `Finsupp.lsingle` for `AddMonoidAlgebra`.

Equations

- AddMonoidAlgebra.lsingle a = Finsupp.lsingle a

Instances For

source
@[simp]
theorem AddMonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
(lsingle a) b = single a b
source
theorem AddMonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Semiring R] [Semiring k] [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

A copy of `Finsupp.lhom_ext'` for `AddMonoidAlgebra`.

source
theorem AddMonoidAlgebra.lhom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_5} [Semiring R] [Semiring k] [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
source
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 #

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

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