Skew Monoid Algebras

Given a monoid G acting on a ring k, the skew monoid algebra of G over k is the set of finitely supported functions f : G → k for which addition is defined pointwise and multiplication of two elements f and g is given by 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, where • denotes the action of G on k. When this action is trivial, this product is the usual convolution product.

In fact the construction of the skew monoid algebra makes sense when G is not even a monoid, but merely a magma, i.e., when G carries a multiplication which is not required to satisfy any conditions at all, and k is a not-necessarily-associative semiring. In this case the construction yields a not-necessarily-unital, not-necessarily-associative algebra.

Main Definitions

• SkewMonoidAlgebra k G: the skew monoid algebra of G over k is the type of finite formal k-linear combinations of terms of G, endowed with a skewed convolution product.

TODO

• some rewrite statements for single, coeff and others (see #10541)
• the algebra instance (see #10541)
• lifting lemmas (see #10541)

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

The skew monoid algebra of G over k 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} [AddMonoid k] (f : SkewMonoidAlgebra k G) : { toFinsupp := f.toFinsupp } = f

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

Equations

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

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

Equations

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

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

Equations

• SkewMonoidAlgebra.instSMulZeroClass = { smul := fun (s : S) (f : SkewMonoidAlgebra k G) => SkewMonoidAlgebra.smul✝ s f, smul_zero := ⋯ }

@[simp]

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

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_add {k : Type u_1} {G : Type u_2} [AddMonoid 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} [AddMonoid 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} [AddMonoid k] : toFinsupp 0 = 0

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_add {k : Type u_1} {G : Type u_2} [AddMonoid 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} [AddMonoid 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} [AddMonoid 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} [AddMonoid k] : Function.Injective toFinsupp

@[simp]

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

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

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

A variant of SkewMonoidAlgebra.ofFinsupp_injective in terms of Iff.

@[simp]

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

@[simp]

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

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

Equations

• SkewMonoidAlgebra.instInhabited = { default := 0 }

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

instance SkewMonoidAlgebra.instUniqueOfSubsingleton {k : Type u_1} {G : Type u_2} [AddMonoid k] [Subsingleton k] : Unique (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instUniqueOfSubsingleton = ⋯.unique

instance SkewMonoidAlgebra.instAddMonoid {k : Type u_1} {G : Type u_2} [AddMonoid k] : AddMonoid (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instAddMonoid = Function.Injective.addMonoid SkewMonoidAlgebra.toFinsupp ⋯ ⋯ ⋯ ⋯

def SkewMonoidAlgebra.support {k : Type u_1} {G : Type u_2} [AddMonoid 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} [AddMonoid k] (p : G →₀ k) : { toFinsupp := p }.support = p.support

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

@[simp]

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

@[simp]

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

def SkewMonoidAlgebra.coeff {k : Type u_1} {G : Type u_2} [AddMonoid k] : SkewMonoidAlgebra k G → G → k

coeff f a (often denoted f.coeff a) is the coefficient of a in f.

Equations

• { toFinsupp := p }.coeff = ⇑p

@[simp]

theorem SkewMonoidAlgebra.coeff_ofFinsupp {k : Type u_1} {G : Type u_2} [AddMonoid k] (p : G →₀ k) : { toFinsupp := p }.coeff = ⇑p

theorem SkewMonoidAlgebra.coeff_injective {k : Type u_1} {G : Type u_2} [AddMonoid k] : Function.Injective coeff

@[simp]

theorem SkewMonoidAlgebra.coeff_inj {k : Type u_1} {G : Type u_2} [AddMonoid k] (p q : SkewMonoidAlgebra k G) : p.coeff = q.coeff ↔ p = q

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_apply {k : Type u_1} {G : Type u_2} [AddMonoid k] (f : SkewMonoidAlgebra k G) (g : G) : f.toFinsupp g = f.coeff g

@[simp]

theorem SkewMonoidAlgebra.coeff_zero {k : Type u_1} {G : Type u_2} [AddMonoid k] (g : G) : coeff 0 g = 0

@[simp]

theorem SkewMonoidAlgebra.mem_support_iff {k : Type u_1} {G : Type u_2} [AddMonoid k] {f : SkewMonoidAlgebra k G} {a : G} : a ∈ f.support ↔ f.coeff a ≠ 0

theorem SkewMonoidAlgebra.notMem_support_iff {k : Type u_1} {G : Type u_2} [AddMonoid k] {f : SkewMonoidAlgebra k G} {a : G} : a ∉ f.support ↔ f.coeff a = 0

@[deprecated SkewMonoidAlgebra.notMem_support_iff (since := "2025-05-23")]

theorem SkewMonoidAlgebra.not_mem_support_iff {k : Type u_1} {G : Type u_2} [AddMonoid k] {f : SkewMonoidAlgebra k G} {a : G} : a ∉ f.support ↔ f.coeff a = 0

Alias of SkewMonoidAlgebra.notMem_support_iff.

theorem SkewMonoidAlgebra.ext_iff {k : Type u_1} {G : Type u_2} [AddMonoid k] {p q : SkewMonoidAlgebra k G} : p = q ↔ ∀ (n : G), p.coeff n = q.coeff n

theorem SkewMonoidAlgebra.ext {k : Type u_1} {G : Type u_2} [AddMonoid k] {p q : SkewMonoidAlgebra k G} : (∀ (a : G), p.coeff a = q.coeff a) → p = q

@[simp]

theorem SkewMonoidAlgebra.coeff_add {k : Type u_1} {G : Type u_2} [AddMonoid k] (p q : SkewMonoidAlgebra k G) (a : G) : (p + q).coeff a = p.coeff a + q.coeff a

@[simp]

theorem SkewMonoidAlgebra.coeff_smul {k : Type u_1} {G : Type u_2} [AddMonoid k] {S : Type u_3} [SMulZeroClass S k] (r : S) (p : SkewMonoidAlgebra k G) (a : G) : (r • p).coeff a = r • p.coeff a

def SkewMonoidAlgebra.single {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) (b : k) : SkewMonoidAlgebra k G

single a b is the finitely supported function with value b at a and zero otherwise.

Equations

• SkewMonoidAlgebra.single a b = { toFinsupp := Finsupp.single a b }

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_single {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) (b : k) : (single a b).toFinsupp = Finsupp.single a b

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_single {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) (b : k) : { toFinsupp := Finsupp.single a b } = single a b

theorem SkewMonoidAlgebra.coeff_single {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) (b : k) [DecidableEq G] : (single a b).coeff = Pi.single a b

theorem SkewMonoidAlgebra.coeff_single_apply {k : Type u_1} {G : Type u_2} [AddMonoid k] {a a' : G} {b : k} [Decidable (a = a')] : (single a b).coeff a' = if a = a' then b else 0

theorem SkewMonoidAlgebra.single_zero_right {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) : single a 0 = 0

@[simp]

theorem SkewMonoidAlgebra.single_add {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂

@[simp]

theorem SkewMonoidAlgebra.single_zero {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) : single a 0 = 0

theorem SkewMonoidAlgebra.single_eq_zero {k : Type u_1} {G : Type u_2} [AddMonoid k] {a : G} {b : k} : single a b = 0 ↔ b = 0

def SkewMonoidAlgebra.toFinsuppAddEquiv {k : Type u_1} {G : Type u_2} [AddMonoid k] : SkewMonoidAlgebra k G ≃+ (G →₀ k)

Group isomorphism between SkewMonoidAlgebra k G and G →₀ k.

Equations

• SkewMonoidAlgebra.toFinsuppAddEquiv = { toFun := SkewMonoidAlgebra.toFinsupp, invFun := SkewMonoidAlgebra.ofFinsupp, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem SkewMonoidAlgebra.toFinsuppAddEquiv_apply {k : Type u_1} {G : Type u_2} [AddMonoid k] (self : SkewMonoidAlgebra k G) : toFinsuppAddEquiv self = self.toFinsupp

@[simp]

theorem SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply {k : Type u_1} {G : Type u_2} [AddMonoid k] (toFinsupp : G →₀ k) : toFinsuppAddEquiv.symm toFinsupp = { toFinsupp := toFinsupp }

theorem SkewMonoidAlgebra.smul_single {k : Type u_1} {G : Type u_2} [AddMonoid k] {S : Type u_3} [SMulZeroClass S k] (s : S) (a : G) (b : k) : s • single a b = single a (s • b)

theorem SkewMonoidAlgebra.single_injective {k : Type u_1} {G : Type u_2} [AddMonoid k] (a : G) : Function.Injective (single a)

theorem IsSMulRegular.skewMonoidAlgebra_iff {k : Type u_1} {G : Type u_2} [AddMonoid k] {S : Type u_3} [Monoid S] [DistribMulAction S k] {a : S} [Nonempty G] : IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

instance SkewMonoidAlgebra.instOne {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] : One (SkewMonoidAlgebra k G)

The unit of the multiplication is single 1 1, i.e. the function that is 1 at 1 and zero elsewhere.

Equations

• SkewMonoidAlgebra.instOne = { one := SkewMonoidAlgebra.single 1 1 }

instance SkewMonoidAlgebra.instAddMonoidWithOne {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] : AddMonoidWithOne (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instAddMonoidWithOne = { natCast := Nat.unaryCast, toAddMonoid := SkewMonoidAlgebra.instAddMonoid, toOne := SkewMonoidAlgebra.instOne, natCast_zero := ⋯, natCast_succ := ⋯ }

theorem SkewMonoidAlgebra.ofFinsupp_one {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] : { toFinsupp := Finsupp.single 1 1 } = 1

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_one {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] : toFinsupp 1 = Finsupp.single 1 1

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_eq_single_one_one_iff {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] {a : SkewMonoidAlgebra k G} : a.toFinsupp = Finsupp.single 1 1 ↔ a = 1

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_eq_one {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] {a : G →₀ k} : { toFinsupp := a } = 1 ↔ a = Finsupp.single 1 1

@[simp]

theorem SkewMonoidAlgebra.single_one_one {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] : single 1 1 = 1

theorem SkewMonoidAlgebra.one_def {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] : 1 = single 1 1

@[simp]

theorem SkewMonoidAlgebra.coeff_one_one {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] : coeff 1 1 = 1

theorem SkewMonoidAlgebra.coeff_one {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] {a : G} [Decidable (a = 1)] : coeff 1 a = if a = 1 then 1 else 0

theorem SkewMonoidAlgebra.natCast_def {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] (n : ℕ) : ↑n = single 1 ↑n

@[simp]

theorem SkewMonoidAlgebra.single_nat {k : Type u_1} {G : Type u_2} [One G] [AddMonoidWithOne k] (n : ℕ) : single 1 ↑n = ↑n

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

Equations

• SkewMonoidAlgebra.instAddCommMonoid = Function.Injective.addCommMonoid SkewMonoidAlgebra.toFinsupp ⋯ ⋯ ⋯ ⋯

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

Equations

• SkewMonoidAlgebra.instDecidableEq = SkewMonoidAlgebra.toFinsuppAddEquiv.decidableEq

def SkewMonoidAlgebra.sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] (f : SkewMonoidAlgebra k G) (g : G → k → N) : N

sum f g is the sum of g a (f.coeff a) over the support of f.

Equations

• f.sum g = f.toFinsupp.sum g

theorem SkewMonoidAlgebra.sum_def {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] (f : SkewMonoidAlgebra k G) (g : G → k → N) : f.sum g = f.toFinsupp.sum g

theorem SkewMonoidAlgebra.sum_def' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] (f : SkewMonoidAlgebra k G) (g : G → k → N) : f.sum g = ∑ a ∈ f.support, g a (f.coeff a)

Unfolded version of sum_def in terms of Finset.sum.

@[simp]

theorem SkewMonoidAlgebra.sum_single_index {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) : (single a b).sum h = h a b

theorem SkewMonoidAlgebra.map_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [AddCommMonoid P] {H : Type u_5} [FunLike H N P] [AddMonoidHomClass H N P] (h : H) (f : SkewMonoidAlgebra k G) (g : G → k → N) : h (f.sum g) = f.sum fun (a : G) (b : k) => h (g a b)

theorem SkewMonoidAlgebra.toFinsupp_sum' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [AddCommMonoid k'] (f : SkewMonoidAlgebra k G) (g : G → k → SkewMonoidAlgebra k' G') : (f.sum g).toFinsupp = f.toFinsupp.sum fun (x1 : G) (x2 : k) => (g x1 x2).toFinsupp

Variant where the image of g is a SkewMonoidAlgebra.

theorem SkewMonoidAlgebra.ofFinsupp_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [AddCommMonoid k'] (f : G →₀ k) (g : G → k → G' →₀ k') : { toFinsupp := f.sum g } = { toFinsupp := f }.sum fun (x1 : G) (x2 : k) => { toFinsupp := g x1 x2 }

theorem SkewMonoidAlgebra.sum_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (f : SkewMonoidAlgebra k G) : f.sum single = f

theorem SkewMonoidAlgebra.sum_add_index' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S} (hf : ∀ (i : G), h i 0 = 0) (h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f + g).sum h = f.sum h + g.sum h

Taking the sum under h is an additive homomorphism, if h is an additive homomorphism. This is a more specific version of SkewMonoidAlgebra.sum_add_index with simpler hypotheses.

theorem SkewMonoidAlgebra.sum_add_index {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [DecidableEq G] [AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0) (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f + g).sum h = f.sum h + g.sum h

Taking the sum under h is an additive homomorphism, if h is an additive homomorphism. This is a more general version of SkewMonoidAlgebra.sum_add_index'; the latter has simpler hypotheses.

@[simp]

theorem SkewMonoidAlgebra.sum_add {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [AddCommMonoid S] (p : SkewMonoidAlgebra k G) (f g : G → k → S) : (p.sum fun (n : G) (x : k) => f n x + g n x) = p.sum f + p.sum g

@[simp]

theorem SkewMonoidAlgebra.sum_zero_index {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [AddCommMonoid S] {f : G → k → S} : sum 0 f = 0

@[simp]

theorem SkewMonoidAlgebra.sum_zero {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] {f : SkewMonoidAlgebra k G} : (f.sum fun (x : G) (x : k) => 0) = 0

theorem SkewMonoidAlgebra.sum_sum_index {α : Type u_3} {β : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] {f : SkewMonoidAlgebra M α} {g : α → M → SkewMonoidAlgebra N β} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 0) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f.sum g).sum h = f.sum fun (a : α) (b : M) => (g a b).sum h

@[simp]

theorem SkewMonoidAlgebra.coeff_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [AddCommMonoid k'] {f : SkewMonoidAlgebra k G} {g : G → k → SkewMonoidAlgebra k' G'} {a₂ : G'} : (f.sum g).coeff a₂ = f.sum fun (a₁ : G) (b : k) => (g a₁ b).coeff a₂

theorem SkewMonoidAlgebra.sum_mul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoidAlgebra k G) {f : G → k → S} : s.sum f * b = s.sum fun (a : G) (c : k) => f a c * b

theorem SkewMonoidAlgebra.mul_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {S : Type u_3} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoidAlgebra k G) {f : G → k → S} : b * s.sum f = s.sum fun (a : G) (c : k) => b * f a c

@[simp]

theorem SkewMonoidAlgebra.sum_ite_eq' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddCommMonoid N] [DecidableEq G] (f : SkewMonoidAlgebra k G) (a : G) (b : G → k → N) : (f.sum fun (x : G) (v : k) => if x = a then b x v else 0) = if a ∈ f.support then b a (f.coeff a) else 0

Analogue of Finsupp.sum_ite_eq' for SkewMonoidAlgebra.

theorem SkewMonoidAlgebra.smul_sum {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {M : Type u_3} {R : Type u_4} [AddCommMonoid M] [DistribSMul R M] {v : SkewMonoidAlgebra k G} {c : R} {h : G → k → M} : c • v.sum h = v.sum fun (a : G) (b : k) => c • h a b

theorem SkewMonoidAlgebra.sum_congr {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {f : SkewMonoidAlgebra k G} {M : Type u_3} [AddCommMonoid M] {g₁ g₂ : G → k → M} (h : ∀ x ∈ f.support, g₁ x (f.coeff x) = g₂ x (f.coeff x)) : f.sum g₁ = f.sum g₂

theorem SkewMonoidAlgebra.induction_on {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {p : SkewMonoidAlgebra k G → Prop} (f : SkewMonoidAlgebra k G) (zero : p 0) (single : ∀ (g : G) (a : k), p (single g a)) (add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)) : p f

theorem SkewMonoidAlgebra.induction_on' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] [instNonempty : Nonempty G] {p : SkewMonoidAlgebra k G → Prop} (f : SkewMonoidAlgebra k G) (single : ∀ (g : G) (a : k), p (single g a)) (add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)) : p f

Slightly less general but more convenient version of SkewMonoidAlgebra.induction_on.

theorem SkewMonoidAlgebra.addHom_ext {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {M : Type u_3} [AddZeroClass M] {f g : SkewMonoidAlgebra k G →+ M} (h : ∀ (a : G) (b : k), f (single a b) = g (single a b)) : f = g

If two additive homomorphisms from SkewMonoidAlgebra k G are equal on each single a b, then they are equal.

theorem SkewMonoidAlgebra.addHom_ext_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {M : Type u_3} [AddZeroClass M] {f g : SkewMonoidAlgebra k G →+ M} : f = g ↔ ∀ (a : G) (b : k), f (single a b) = g (single a b)

def SkewMonoidAlgebra.mapDomain {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_3} (f : G → G') : SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G'

Given f : G → G' and v : SkewMonoidAlgebra k G, mapDomain f v : SkewMonoidAlgebra k G' is the finitely supported additive homomorphism whose value at a : G' is the sum of v x over all x such that f x = a. Note that SkewMonoidAlgebra.mapDomain is defined as an AddHom, while MonoidAlgebra.mapDomain is defined as a function.

Equations

• SkewMonoidAlgebra.mapDomain f = { toFun := fun (v : SkewMonoidAlgebra k G) => v.sum fun (a : G) => SkewMonoidAlgebra.single (f a), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SkewMonoidAlgebra.mapDomain_apply {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_3} (f : G → G') (v : SkewMonoidAlgebra k G) : (mapDomain f) v = v.sum fun (a : G) => single (f a)

theorem SkewMonoidAlgebra.toFinsupp_mapDomain {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_3} (f : G → G') (v : SkewMonoidAlgebra k G) : ((mapDomain f) v).toFinsupp = Finsupp.mapDomain f v.toFinsupp

theorem SkewMonoidAlgebra.mapDomain_id {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {v : SkewMonoidAlgebra k G} : (mapDomain id) v = v

theorem SkewMonoidAlgebra.mapDomain_comp {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_3} {G'' : Type u_4} {f : G → G'} {g : G' → G''} {v : SkewMonoidAlgebra k G} : (mapDomain (g ∘ f)) v = (mapDomain g) ((mapDomain f) v)

theorem SkewMonoidAlgebra.sum_mapDomain_index {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_3} {f : G → G'} {v : SkewMonoidAlgebra k G} {k' : Type u_5} [AddCommMonoid k'] {h : G' → k → k'} (h_zero : ∀ (b : G'), h b 0 = 0) (h_add : ∀ (b : G') (m₁ m₂ : k), h b (m₁ + m₂) = h b m₁ + h b m₂) : ((mapDomain f) v).sum h = v.sum fun (a : G) (m : k) => h (f a) m

theorem SkewMonoidAlgebra.mapDomain_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_3} {f : G → G'} {a : G} {b : k} : (mapDomain f) (single a b) = single (f a) b

theorem SkewMonoidAlgebra.mapDomain_smul {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_3} {f : G → G'} {v : SkewMonoidAlgebra k G} {R : Type u_5} [Monoid R] [DistribMulAction R k] {b : R} : (mapDomain f) (b • v) = b • (mapDomain f) v

def SkewMonoidAlgebra.liftNC {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {R : Type u_5} [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) : SkewMonoidAlgebra k G →+ R

A non-commutative version of SkewMonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a homomorphism g : G → R, returns the additive homomorphism from SkewMonoidAlgebra k G such that liftNC f g (single a b) = f b * g a.

If k is a semiring and f is a ring homomorphism and for all x : R, y : G the equality (f (y • x)) * g y = (g y) * (f x)) holds, then the result is a ring homomorphism (see SkewMonoidAlgebra.liftNCRingHom).

If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called SkewMonoidAlgebra.lift.

Equations

• SkewMonoidAlgebra.liftNC f g = (Finsupp.liftAddHom fun (x : G) => (AddMonoidHom.mulRight (g x)).comp f).comp SkewMonoidAlgebra.toFinsuppAddEquiv.toAddMonoidHom

@[simp]

theorem SkewMonoidAlgebra.liftNC_single {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {R : Type u_5} [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) (a : G) (b : k) : (liftNC f g) (single a b) = f b * g a

theorem SkewMonoidAlgebra.eq_liftNC {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {R : Type u_5} [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) (l : SkewMonoidAlgebra k G →+ R) (h : ∀ (a : G) (b : k), l (single a b) = f b * g a) : l = liftNC f g

instance SkewMonoidAlgebra.instNeg {k : Type u_1} {G : Type u_2} [AddGroup k] : Neg (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instNeg = { neg := SkewMonoidAlgebra.neg✝ }

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_neg {k : Type u_1} {G : Type u_2} [AddGroup k] {a : G →₀ k} : { toFinsupp := -a } = -{ toFinsupp := a }

instance SkewMonoidAlgebra.instAddGroup {k : Type u_1} {G : Type u_2} [AddGroup k] : AddGroup (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_neg {k : Type u_1} {G : Type u_2} [AddGroup k] (a : SkewMonoidAlgebra k G) : (-a).toFinsupp = -a.toFinsupp

@[simp]

theorem SkewMonoidAlgebra.ofFinsupp_sub {k : Type u_1} {G : Type u_2} [AddGroup k] {a b : G →₀ k} : { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }

@[simp]

theorem SkewMonoidAlgebra.toFinsupp_sub {k : Type u_1} {G : Type u_2} [AddGroup k] (a b : SkewMonoidAlgebra k G) : (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

@[simp]

theorem SkewMonoidAlgebra.single_neg {k : Type u_1} {G : Type u_2} [AddGroup k] (a : G) (b : k) : single a (-b) = -single a b

instance SkewMonoidAlgebra.instAddCommGroup {k : Type u_1} {G : Type u_2} [AddCommGroup k] : AddCommGroup (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instAddCommGroup = { toAddGroup := SkewMonoidAlgebra.instAddGroup, add_comm := ⋯ }

instance SkewMonoidAlgebra.instAddGroupWithOne {k : Type u_1} {G : Type u_2} [AddGroupWithOne k] [One G] : AddGroupWithOne (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

theorem SkewMonoidAlgebra.intCast_def {k : Type u_1} {G : Type u_2} [AddGroupWithOne k] [One G] (z : ℤ) : ↑z = single 1 ↑z

theorem SkewMonoidAlgebra.sum_smul_index {k : Type u_1} {G : Type u_2} {N : Type u_3} [AddCommMonoid N] [NonUnitalNonAssocSemiring k] {g : SkewMonoidAlgebra k G} {b : k} {h : G → k → N} (h0 : ∀ (i : G), h i 0 = 0) : (b • g).sum h = g.sum fun (x1 : G) (x2 : k) => h x1 (b * x2)

theorem SkewMonoidAlgebra.sum_smul_index' {k : Type u_1} {G : Type u_2} {N : Type u_3} {R : Type u_4} [AddCommMonoid k] [DistribSMul R k] [AddCommMonoid N] {g : SkewMonoidAlgebra k G} {b : R} {h : G → k → N} (h0 : ∀ (i : G), h i 0 = 0) : (b • g).sum h = g.sum fun (x1 : G) (x2 : k) => h x1 (b • x2)

@[simp]

theorem SkewMonoidAlgebra.liftNC_one {k : Type u_1} {G : Type u_2} {g_hom : Type u_3} {R : Type u_4} [NonAssocSemiring k] [One G] [Semiring R] [FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) : (liftNC ↑f ⇑g) 1 = 1

instance SkewMonoidAlgebra.instMul {k : Type u_1} {G : Type u_2} [Mul G] [SMul G k] [NonUnitalNonAssocSemiring k] : Mul (SkewMonoidAlgebra k G)

The product of 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. (Think of a skew group ring.)

Equations

• SkewMonoidAlgebra.instMul = { mul := fun (f g : SkewMonoidAlgebra k G) => f.sum fun (a₁ : G) (b₁ : k) => g.sum fun (a₂ : G) (b₂ : k) => SkewMonoidAlgebra.single (a₁ * a₂) (b₁ * a₁ • b₂) }

theorem SkewMonoidAlgebra.mul_def {k : Type u_1} {G : Type u_2} [Mul G] [SMul G k] [NonUnitalNonAssocSemiring k] {f g : SkewMonoidAlgebra k G} : f * g = f.sum fun (a₁ : G) (b₁ : k) => g.sum fun (a₂ : G) (b₂ : k) => single (a₁ * a₂) (b₁ * a₁ • b₂)

instance SkewMonoidAlgebra.instNonUnitalNonAssocSemiring {k : Type u_1} {G : Type u_2} [Mul G] [NonUnitalNonAssocSemiring k] [DistribSMul G k] : NonUnitalNonAssocSemiring (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

theorem SkewMonoidAlgebra.liftNC_mul {k : Type u_1} {G : Type u_2} [Mul G] {R : Type u_3} [Semiring R] [NonAssocSemiring k] [SMul G k] {g_hom : Type u_4} [FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom) (a b : SkewMonoidAlgebra k G) (h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)) : (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

Semiring structure

instance SkewMonoidAlgebra.instNonUnitalSemiring {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] : NonUnitalSemiring (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instNonUnitalSemiring = { toNonUnitalNonAssocSemiring := SkewMonoidAlgebra.instNonUnitalNonAssocSemiring, mul_assoc := ⋯ }

instance SkewMonoidAlgebra.instNonAssocSemiring {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] : NonAssocSemiring (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

instance SkewMonoidAlgebra.instSemiring {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] : Semiring (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

def SkewMonoidAlgebra.liftNCRingHom {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] {R : Type u_3} [Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ {x : k} {y : G}, f (y • x) * g y = g y * f x) : SkewMonoidAlgebra k G →+* R

liftNC as a RingHom, for when f x and g y commute

Equations

• SkewMonoidAlgebra.liftNCRingHom f g h_comm = { toFun := (↑(SkewMonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Derived instances

instance SkewMonoidAlgebra.instNonUnitalNonAssocRing {k : Type u_1} {G : Type u_2} [Ring k] [Monoid G] [MulSemiringAction G k] : NonUnitalNonAssocRing (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

instance SkewMonoidAlgebra.instNonUnitalRing {k : Type u_1} {G : Type u_2} [Ring k] [Monoid G] [MulSemiringAction G k] : NonUnitalRing (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

instance SkewMonoidAlgebra.instNonAssocRing {k : Type u_1} {G : Type u_2} [Ring k] [Monoid G] [MulSemiringAction G k] : NonAssocRing (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

instance SkewMonoidAlgebra.instRing {k : Type u_1} {G : Type u_2} [Ring k] [Monoid G] [MulSemiringAction G k] : Ring (SkewMonoidAlgebra k G)

Equations

• One or more equations did not get rendered due to their size.

instance SkewMonoidAlgebra.instDistribSMul {k : Type u_1} {G : Type u_2} {S : Type u_3} [AddMonoid k] [DistribSMul S k] : DistribSMul S (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instDistribSMul = Function.Injective.distribSMul { toFun := SkewMonoidAlgebra.toFinsupp, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance SkewMonoidAlgebra.instDistribMulAction {k : Type u_1} {G : Type u_2} {S : Type u_3} [Monoid S] [AddMonoid k] [DistribMulAction S k] : DistribMulAction S (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instDistribMulAction = Function.Injective.distribMulAction { toFun := SkewMonoidAlgebra.toFinsupp, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance SkewMonoidAlgebra.instModule {k : Type u_1} {G : Type u_2} {S : Type u_3} [Semiring S] [AddCommMonoid k] [Module S k] : Module S (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instModule = Function.Injective.module S { toFun := SkewMonoidAlgebra.toFinsupp, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance SkewMonoidAlgebra.instFaithfulSMul {k : Type u_1} {G : Type u_2} {S : Type u_3} [AddMonoid k] [SMulZeroClass S k] [FaithfulSMul S k] [Nonempty G] : FaithfulSMul S (SkewMonoidAlgebra k G)

instance SkewMonoidAlgebra.instIsScalarTower {k : Type u_1} {G : Type u_2} {S₁ : Type u_4} {S₂ : Type u_5} [AddMonoid k] [SMul S₁ S₂] [SMulZeroClass S₁ k] [SMulZeroClass S₂ k] [IsScalarTower S₁ S₂ k] : IsScalarTower S₁ S₂ (SkewMonoidAlgebra k G)

instance SkewMonoidAlgebra.instSMulCommClass {k : Type u_1} {G : Type u_2} {S₁ : Type u_4} {S₂ : Type u_5} [AddMonoid k] [SMulZeroClass S₁ k] [SMulZeroClass S₂ k] [SMulCommClass S₁ S₂ k] : SMulCommClass S₁ S₂ (SkewMonoidAlgebra k G)

instance SkewMonoidAlgebra.instIsCentralScalar {k : Type u_1} {G : Type u_2} {S : Type u_3} [AddMonoid k] [SMulZeroClass S k] [SMulZeroClass Sᵐᵒᵖ k] [IsCentralScalar S k] : IsCentralScalar S (SkewMonoidAlgebra k G)

def SkewMonoidAlgebra.toFinsuppLinearEquiv {k : Type u_1} {G : Type u_2} {S : Type u_3} [Semiring S] [AddCommMonoid k] [Module S k] : SkewMonoidAlgebra k G ≃ₗ[S] G →₀ k

Linear equivalence between SkewMonoidAlgebra k G and G →₀ k.

Equations

• SkewMonoidAlgebra.toFinsuppLinearEquiv = SkewMonoidAlgebra.toFinsuppAddEquiv.toLinearEquiv ⋯

def SkewMonoidAlgebra.basisSingleOne {k : Type u_1} {G : Type u_2} [Semiring k] : Module.Basis G k (SkewMonoidAlgebra k G)

The basis on SkewMonoidAlgebra k G with basis vectors fun i ↦ single i 1

Equations

• SkewMonoidAlgebra.basisSingleOne = { repr := SkewMonoidAlgebra.toFinsuppLinearEquiv }

instance SkewMonoidAlgebra.instFree {k : Type u_1} {G : Type u_2} [Semiring k] : Module.Free k (SkewMonoidAlgebra k G)

def SkewMonoidAlgebra.comapSMul {G : Type u_2} {M : Type u_6} {α : Type u_7} [Monoid G] [MulAction G α] [AddCommMonoid M] : SMul G (SkewMonoidAlgebra M α)

Scalar multiplication acting on the domain.

This is not an instance as it would conflict with the action on the range. See the file test/instance_diamonds.lean for examples of such conflicts.

Equations

• SkewMonoidAlgebra.comapSMul = { smul := fun (g : G) => ⇑(SkewMonoidAlgebra.mapDomain fun (x : α) => g • x) }

theorem SkewMonoidAlgebra.comapSMul_def {G : Type u_2} {M : Type u_6} {α : Type u_7} [Monoid G] [AddCommMonoid M] [MulAction G α] (g : G) (f : SkewMonoidAlgebra M α) : g • f = (mapDomain fun (x : α) => g • x) f

@[simp]

theorem SkewMonoidAlgebra.comapSMul_single {G : Type u_2} {M : Type u_6} {α : Type u_7} [Monoid G] [AddCommMonoid M] [MulAction G α] (g : G) (a : α) (b : M) : g • single a b = single (g • a) b

def SkewMonoidAlgebra.comapMulAction {G : Type u_2} {M : Type u_6} {α : Type u_7} [Monoid G] [AddCommMonoid M] [MulAction G α] : MulAction G (SkewMonoidAlgebra M α)

comapSMul is multiplicative

Equations

• SkewMonoidAlgebra.comapMulAction = { toSMul := SkewMonoidAlgebra.comapSMul, one_smul := ⋯, mul_smul := ⋯ }

def SkewMonoidAlgebra.comapDistribMulActionSelf {k : Type u_1} {G : Type u_2} [Monoid G] [AddCommMonoid k] : DistribMulAction G (SkewMonoidAlgebra k G)

This is not an instance as it conflicts with SkewMonoidAlgebra.distribMulAction when G = kˣ.

Equations

• SkewMonoidAlgebra.comapDistribMulActionSelf = { toMulAction := SkewMonoidAlgebra.comapMulAction, smul_zero := ⋯, smul_add := ⋯ }