Skew monoid algebras

This file presents a skewed version of Mathlib.Algebra.MonoidAlgebra.Basic with an irreducible definition.

The definition is separated from Finsupp by wrapping it with a structure. For https://github.com/leanprover-community/mathlib4/pull/15878, the goal is only to get this separation right. This means that most of what makes these objects skewed is currently missing from this PR.

The goal will then be to define a skewed convolution product on SkewMonoidAlgebra k G. Here, the product of two elements f g : SkewMonoidAlgebra k G is the finitely supported function whose value at a is the sum of f x * (x • g y) over all pairs x, y such that x * y = a. (See https://github.com/leanprover-community/mathlib4/pull/10541 at line 558 for an implementation.)

The associativity of the skewed multiplication depends on the [MulSemiringAction G k] instance. In particular, this means that unlike in Mathlib.Algebra.MonoidAlgebra.Basic, G will need to be a monoid for most of our uses.

structure SkewMonoidAlgebra (k : Type u_1) (G : Type u_2) [Zero k] : Type (max u_1 u_2)

The skew monoid algebra over a semiring k generated by the monoid G. It is the type of finite formal k-linear combinations of terms of G, endowed with a skewed convolution product.

• ofFinsupp :: (
• toFinsupp : G →₀ k

  The natural map from SkewMonoidAlgebra k G to G →₀ k.

• )

@[simp]

theorem SkewMonoidAlgebra.eta {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (f : SkewMonoidAlgebra k G) : { toFinsupp := f.toFinsupp } = f

instance SkewMonoidAlgebra.instZero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : Zero (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instZero = { zero := { toFinsupp := 0 } }

instance SkewMonoidAlgebra.instAdd {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : Add (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instAdd = { add := SkewMonoidAlgebra.add✝ }

instance SkewMonoidAlgebra.instSMulZeroClass {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] : SMulZeroClass S (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instSMulZeroClass = SMulZeroClass.mk ⋯

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : { toFinsupp := 0 } = 0

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a b : G →₀ k} : { toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_smul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] (a : S) (b : G →₀ k) : { toFinsupp := a • b } = a • { toFinsupp := b }

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : SkewMonoidAlgebra.toFinsupp 0 = 0

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a b : SkewMonoidAlgebra k G) : (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_smul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [SMulZeroClass S k] (a : S) (b : SkewMonoidAlgebra k G) : (a • b).toFinsupp = a • b.toFinsupp

theorem IsSMulRegular.skewMonoidAlgebra {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [Monoid S] [DistribMulAction S k] {a : S} (ha : IsSMulRegular k a) : IsSMulRegular (SkewMonoidAlgebra k G) a

theorem SkewMonoidAlgebra.toFinsupp_injective {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : Function.Injective SkewMonoidAlgebra.toFinsupp

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_inj {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a b : SkewMonoidAlgebra k G} : a.toFinsupp = b.toFinsupp ↔ a = b

theorem SkewMonoidAlgebra.ofFinsupp_injective {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : Function.Injective SkewMonoidAlgebra.ofFinsupp

theorem SkewMonoidAlgebra.ofFinsupp_inj {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a b : G →₀ k} : { toFinsupp := a } = { toFinsupp := b } ↔ a = b

A more convenient spelling of SkewMonoidAlgebra.ofFinsupp.injEq in terms of Iff.

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_eq_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a : SkewMonoidAlgebra k G} : a.toFinsupp = 0 ↔ a = 0

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_eq_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {a : G →₀ k} : { toFinsupp := a } = 0 ↔ a = 0

instance SkewMonoidAlgebra.instInhabited {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : Inhabited (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instInhabited = { default := 0 }

instance SkewMonoidAlgebra.instNontrivial {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [Nontrivial k] [Nonempty G] : Nontrivial (SkewMonoidAlgebra k G)

instance SkewMonoidAlgebra.instAddCommMonoid {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : AddCommMonoid (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instAddCommMonoid = AddCommMonoid.mk ⋯

def SkewMonoidAlgebra.support {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : SkewMonoidAlgebra k G → Finset G

For f : SkewMonoidAlgebra k G, f.support is the set of all a ∈ G such that f a ≠ 0.

Equations

• { toFinsupp := p }.support = p.support

@[simp]

theorem SkewMonoidAlgebra.support_ofFinsupp {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (p : G →₀ k) : { toFinsupp := p }.support = p.support

theorem SkewMonoidAlgebra.support_toFinsupp {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (p : SkewMonoidAlgebra k G) : p.toFinsupp.support = p.support

@[simp]

theorem SkewMonoidAlgebra.support_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] : SkewMonoidAlgebra.support 0 = ∅

@[simp]

theorem SkewMonoidAlgebra.support_eq_empty {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {p : SkewMonoidAlgebra k G} : p.support = ∅ ↔ p = 0