Module structure on monoid algebras

Main results

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

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

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ˣ.

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} {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.

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)

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

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

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.

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

theorem MonoidAlgebra.smul_single' {k : Type u₁} {G : Type u₂} [Semiring k] (c : k) (a : G) (b : k) : c • single a b = single a (c * b)

Copy of Finsupp.smul_single' that avoids the MonoidAlgebra = Finsupp defeq abuse.

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

Additive monoids

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

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 AddMonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_5} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] : SMulCommClass R S (AddMonoidAlgebra k G)

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

Semiring structure

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 singles 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.

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.

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)

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

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

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.

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

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)