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.

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.coeff 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 SkewMonoidAlgebra.single_left_inj {k : Type u_1} {G : Type u_2} [AddMonoid k] {a a' : G} {b : k} (h : b ≠ 0) : single a b = single a' b ↔ a = 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_1 : 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.instCommSemiring {k : Type u_1} {G : Type u_2} [CommSemiring k] [CommMonoid G] [MulSemiringAction G k] [SMulCommClass G k k] : CommSemiring (SkewMonoidAlgebra k G)

Equations

• SkewMonoidAlgebra.instCommSemiring = { toSemiring := SkewMonoidAlgebra.instSemiring, mul_comm := ⋯ }

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

theorem SkewMonoidAlgebra.coeff_mul {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] [DecidableEq G] (f g : SkewMonoidAlgebra k G) (x : G) : (f * g).coeff x = f.sum fun (a₁ : G) (b₁ : k) => g.sum fun (a₂ : G) (b₂ : k) => if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

theorem SkewMonoidAlgebra.coeff_mul_antidiagonal_of_finset {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (f g : SkewMonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) : (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2

theorem SkewMonoidAlgebra.coeff_mul_antidiagonal_finsum {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (f g : SkewMonoidAlgebra k G) (x : G) : (f * g).coeff x = ∑ᶠ (p : G × G) (_ : p ∈ {p : G × G | p.1 * p.2 = x}), f.coeff p.1 * p.1 • g.coeff p.2

theorem SkewMonoidAlgebra.coeff_mul_single_aux {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ (a : G), a * x = z ↔ a = y) : (f * single x r).coeff z = f.coeff y * y • r

theorem SkewMonoidAlgebra.coeff_mul_single_one {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) (r : k) (x : G) : (f * single 1 r).coeff x = f.coeff x * x • r

theorem SkewMonoidAlgebra.coeff_mul_single_of_not_exists_mul {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (r : k) {g g' : G} (x : SkewMonoidAlgebra k G) (h : ∀ (x : G), ¬g' = x * g) : (x * single g r).coeff g' = 0

theorem SkewMonoidAlgebra.coeff_single_mul_aux {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ (a : G), x * a = y ↔ a = z) : (single x r * f).coeff y = r * x • f.coeff z

theorem SkewMonoidAlgebra.coeff_single_one_mul {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) (r : k) (x : G) : (single 1 r * f).coeff x = r * f.coeff x

theorem SkewMonoidAlgebra.coeff_single_mul_of_not_exists_mul {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] (r : k) {g g' : G} (x : SkewMonoidAlgebra k G) (h : ¬∃ (d : G), g' = g * d) : (single g r * x).coeff g' = 0

@[simp]

theorem SkewMonoidAlgebra.coeff_mul_single {k : Type u_1} {G : Type u_2} [Semiring k] [Group G] [MulSemiringAction G k] (f : SkewMonoidAlgebra k G) (r : k) (x y : G) : (f * single x r).coeff y = f.coeff (y * x⁻¹) * (y * x⁻¹) • r

@[simp]

theorem SkewMonoidAlgebra.coeff_single_mul {k : Type u_1} {G : Type u_2} [Semiring k] [Group G] [MulSemiringAction G k] (r : k) (x : G) (f : SkewMonoidAlgebra k G) (y : G) : (single x r * f).coeff y = r * x • f.coeff (x⁻¹ * y)

theorem SkewMonoidAlgebra.coeff_mul_left {k : Type u_1} {G : Type u_2} [Semiring k] [Group G] [MulSemiringAction G k] (f g : SkewMonoidAlgebra k G) (x : G) : (f * g).coeff x = f.sum fun (a : G) (b : k) => b * a • g.coeff (a⁻¹ * x)

theorem SkewMonoidAlgebra.coeff_mul_right {k : Type u_1} {G : Type u_2} [Semiring k] [Group G] [MulSemiringAction G k] (f g : SkewMonoidAlgebra k G) (x : G) : (f * g).coeff x = g.sum fun (a : G) (b : k) => f.coeff (x * a⁻¹) * (x * a⁻¹) • b

def SkewMonoidAlgebra.singleAddHom {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) : k →+ SkewMonoidAlgebra k G

single as an AddMonoidHom.

See lsingle for the stronger version as a linear map.

Equations

• SkewMonoidAlgebra.singleAddHom a = { toFun := SkewMonoidAlgebra.single a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SkewMonoidAlgebra.singleAddHom_apply {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (a : G) (b : k) : (singleAddHom a) b = single a b

theorem SkewMonoidAlgebra.addHom_ext' {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddZeroClass N] ⦃f g : SkewMonoidAlgebra k G →+ N⦄ (H : ∀ (x : G), f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g

theorem SkewMonoidAlgebra.addHom_ext'_iff {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {N : Type u_3} [AddZeroClass N] {f g : SkewMonoidAlgebra k G →+ N} : f = g ↔ ∀ (x : G), f.comp (singleAddHom x) = g.comp (singleAddHom x)

@[simp]

theorem SkewMonoidAlgebra.single_mul_single {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] {a₁ a₂ : G} {b₁ b₂ : k} : single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * a₁ • b₂)

def SkewMonoidAlgebra.singleOneRingHom {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] : k →+* SkewMonoidAlgebra k G

single 1 as a RingHom

Equations

• SkewMonoidAlgebra.singleOneRingHom = { toFun := (↑(SkewMonoidAlgebra.singleAddHom 1)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem SkewMonoidAlgebra.ringHom_ext {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] {f g : SkewMonoidAlgebra k G →+* k} (h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)) (h_of : ∀ (a : G), f (single a 1) = g (single a 1)) : f = g

If two ring homomorphisms from SkewMonoidAlgebra k G are equal on all single a 1 and single 1 b, then they are equal.

theorem SkewMonoidAlgebra.mapDomain_one {α : Type u_3} {α₂ : Type u_4} {β : Type u_5} {F : Type u_6} [Semiring β] [Monoid α] [Monoid α₂] [FunLike F α α₂] [MonoidHomClass F α α₂] (f : F) : (mapDomain ⇑f) 1 = 1

Like mapDomain_zero, but for the 1 we define in this file

theorem SkewMonoidAlgebra.mapDomain_mul {α : Type u_3} {α₂ : Type u_4} {β : Type u_5} {F : Type u_6} [Semiring β] [Monoid α] [Monoid α₂] [FunLike F α α₂] [MulSemiringAction α β] [MulSemiringAction α₂ β] [MulHomClass F α α₂] {f : F} (x y : SkewMonoidAlgebra β α) (hf : ∀ (a : α) (x : β), a • x = f a • x) : (mapDomain ⇑f) (x * y) = (mapDomain ⇑f) x * (mapDomain ⇑f) y

def SkewMonoidAlgebra.mapDomainRingHom {α : Type u_3} {α₂ : Type u_4} {β : Type u_5} {F : Type u_6} [Semiring β] [Monoid α] [Monoid α₂] [FunLike F α α₂] [MulSemiringAction α β] [MulSemiringAction α₂ β] [MonoidHomClass F α α₂] {f : F} (hf : ∀ (a : α) (x : β), a • x = f a • x) : SkewMonoidAlgebra β α →+* SkewMonoidAlgebra β α₂

If f : G → H is a multiplicative homomorphism between two monoids and ∀ (a : G) (x : k), a • x = (f a) • x, then mapDomain f is a ring homomorphism between their skew monoid algebras.

Equations

• SkewMonoidAlgebra.mapDomainRingHom hf = { toFun := (↑(SkewMonoidAlgebra.mapDomain ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def SkewMonoidAlgebra.of (k : Type u_1) (G : Type u_2) [Semiring k] [Monoid G] [MulSemiringAction G k] : G →* SkewMonoidAlgebra k G

The embedding of a monoid into its skew monoid algebra.

Equations

• SkewMonoidAlgebra.of k G = { toFun := fun (a : G) => SkewMonoidAlgebra.single a 1, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SkewMonoidAlgebra.of_apply (k : Type u_1) (G : Type u_2) [Semiring k] [Monoid G] [MulSemiringAction G k] (a : G) : (of k G) a = single a 1

theorem SkewMonoidAlgebra.smul_of (k : Type u_1) (G : Type u_2) [Semiring k] [Monoid G] [MulSemiringAction G k] (g : G) (r : k) : r • (of k G) g = single g r

theorem SkewMonoidAlgebra.of_injective (k : Type u_1) (G : Type u_2) [Semiring k] [Monoid G] [MulSemiringAction G k] [Nontrivial k] : Function.Injective ⇑(of k G)

theorem SkewMonoidAlgebra.ringHom_ext' (k : Type u_1) (G : Type u_2) [Semiring k] [Monoid G] [MulSemiringAction G k] {f g : SkewMonoidAlgebra k G →+* k} (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom) (h_of : (↑f).comp (of k G) = (↑g).comp (of k G)) : f = g

If two ring homomorphisms from SkewMonoidAlgebra k G are equal on all single a 1 and single 1 b, then they are equal.

See note [partially-applied ext lemmas].

theorem SkewMonoidAlgebra.ringHom_ext'_iff {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] {f g : SkewMonoidAlgebra k G →+* k} : f = g ↔ f.comp singleOneRingHom = g.comp singleOneRingHom ∧ (↑f).comp (of k G) = (↑g).comp (of k G)

Non-unital, non-associative algebra structure

theorem SkewMonoidAlgebra.liftNC_smul {k : Type u_1} {G : Type u_2} [Semiring k] [MulOneClass G] {R : Type u_3} [Semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : SkewMonoidAlgebra k G) : (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

instance SkewMonoidAlgebra.isScalarTower_self (k : Type u_1) (G : Type u_2) [Semiring k] [Monoid G] [MulSemiringAction G k] [IsScalarTower k k k] : IsScalarTower k (SkewMonoidAlgebra k G) (SkewMonoidAlgebra k G)

def SkewMonoidAlgebra.DistribMulActionHom.single {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [DistribMulAction R M] {α : Type u_6} (a : α) : M →+[R] SkewMonoidAlgebra M α

single as a DistribMulActionSemiHom.

See also lsingle for the version as a linear map.

Equations

• SkewMonoidAlgebra.DistribMulActionHom.single a = { toFun := (↑(SkewMonoidAlgebra.singleAddHom a)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SkewMonoidAlgebra.DistribMulActionHom.single_toFun {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [DistribMulAction R M] {α : Type u_6} (a : α) (a✝ : M) : (single a) a✝ = (↑(singleAddHom a)).toFun a✝

theorem SkewMonoidAlgebra.distribMulActionHom_ext {R : Type u_3} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R M] [DistribMulAction R N] {α : Type u_6} {f g : SkewMonoidAlgebra M α →+[R] N} (h : ∀ (a : α) (m : M), f (single a m) = g (single a m)) : f = g

theorem SkewMonoidAlgebra.distribMulActionHom_ext' {R : Type u_3} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R M] [DistribMulAction R N] {α : Type u_6} {f g : SkewMonoidAlgebra M α →+[R] N} (h : ∀ (a : α), f.comp (DistribMulActionHom.single a) = g.comp (DistribMulActionHom.single a)) : f = g

See note [partially-applied ext lemmas].

theorem SkewMonoidAlgebra.distribMulActionHom_ext'_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R M] [DistribMulAction R N] {α : Type u_6} {f g : SkewMonoidAlgebra M α →+[R] N} : f = g ↔ ∀ (a : α), f.comp (DistribMulActionHom.single a) = g.comp (DistribMulActionHom.single a)

def SkewMonoidAlgebra.lsingle {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] {α : Type u_6} (a : α) [Module R M] : M →ₗ[R] SkewMonoidAlgebra M α

Interpret single a as a linear map.

Equations

• SkewMonoidAlgebra.lsingle a = { toFun := (↑(SkewMonoidAlgebra.singleAddHom a)).toFun, map_add' := ⋯, map_smul' := ⋯ }

theorem SkewMonoidAlgebra.lhom_ext {R : Type u_3} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] {α : Type u_6} [Module R M] [Module R N] ⦃φ ψ : SkewMonoidAlgebra M α →ₗ[R] N⦄ (h : ∀ (a : α) (b : M), φ (single a b) = ψ (single a b)) : φ = ψ

Two R-linear maps from SkewMonoidAlgebra M α which agree on each single x y agree everywhere.

theorem SkewMonoidAlgebra.lhom_ext' {R : Type u_3} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] {α : Type u_6} [Module R M] [Module R N] ⦃φ ψ : SkewMonoidAlgebra M α →ₗ[R] N⦄ (h : ∀ (a : α), φ ∘ₗ lsingle a = ψ ∘ₗ lsingle a) : φ = ψ

theorem SkewMonoidAlgebra.lhom_ext'_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] {α : Type u_6} [Module R M] [Module R N] {φ ψ : SkewMonoidAlgebra M α →ₗ[R] N} : φ = ψ ↔ ∀ (a : α), φ ∘ₗ lsingle a = ψ ∘ₗ lsingle a

theorem SkewMonoidAlgebra.nonUnitalAlgHom_ext {k : Type u_1} {G : Type u_2} {A : Type u_6} [NonUnitalNonAssocSemiring A] [Monoid G] [Semiring k] [MulSemiringAction G k] [DistribMulAction k A] {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A} (h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂

A non_unital k-algebra homomorphism from SkewMonoidAlgebra k G is uniquely defined by its values on the functions single a 1.

theorem SkewMonoidAlgebra.nonUnitalAlgHom_ext' {k : Type u_1} {G : Type u_2} {A : Type u_6} [NonUnitalNonAssocSemiring A] [Monoid G] [Semiring k] [MulSemiringAction G k] [DistribMulAction k A] {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A} (h : φ₁.toMulHom.comp ↑(of k G) = φ₂.toMulHom.comp ↑(of k G)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

theorem SkewMonoidAlgebra.nonUnitalAlgHom_ext'_iff {k : Type u_1} {G : Type u_2} {A : Type u_6} [NonUnitalNonAssocSemiring A] [Monoid G] [Semiring k] [MulSemiringAction G k] [DistribMulAction k A] {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A} : φ₁ = φ₂ ↔ φ₁.toMulHom.comp ↑(of k G) = φ₂.toMulHom.comp ↑(of k G)

instance SkewMonoidAlgebra.instAlgebraOfSMulCommClass {k : Type u_1} {G : Type u_2} [Monoid G] [CommSemiring k] {A : Type u_3} [Semiring A] [Algebra k A] [MulSemiringAction G A] [SMulCommClass G k A] : Algebra k (SkewMonoidAlgebra A G)

The instance Algebra k (SkewMonoidAlgebra A G) whenever we have Algebra k A. In particular this provides the instance Algebra k (SkewMonoidAlgebra k G).

Equations

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

@[simp]

theorem SkewMonoidAlgebra.coe_algebraMap {k : Type u_1} {G : Type u_2} [Monoid G] [CommSemiring k] {A : Type u_3} [Semiring A] [Algebra k A] [MulSemiringAction G A] [SMulCommClass G k A] : ⇑(algebraMap k (SkewMonoidAlgebra A G)) = single 1 ∘ ⇑(algebraMap k A)

theorem SkewMonoidAlgebra.single_eq_algebraMap_mul_of {k : Type u_1} {G : Type u_2} [Monoid G] [CommSemiring k] [MulSemiringAction G k] [SMulCommClass G k k] (a : G) (b : k) : single a b = (algebraMap k (SkewMonoidAlgebra k G)) b * (of k G) a

theorem SkewMonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of {k : Type u_1} {G : Type u_2} [Monoid G] [CommSemiring k] {A : Type u_3} [Semiring A] [Algebra k A] (a : G) (b : k) [MulSemiringAction G A] [SMulCommClass G k A] : single a ((algebraMap k A) b) = (algebraMap k (SkewMonoidAlgebra A G)) b * (of A G) a

theorem SkewMonoidAlgebra.algHom_ext {k : Type u_1} {G : Type u_2} [Monoid G] [CommSemiring k] {A : Type u_3} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] ⦃φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A⦄ (h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂

A k-algebra homomorphism from SkewMonoidAlgebra k G is uniquely defined by its values on the functions single a 1.

theorem SkewMonoidAlgebra.algHom_ext' {k : Type u_1} {G : Type u_2} [Monoid G] [CommSemiring k] {A : Type u_3} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] ⦃φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A⦄ (h : (↑φ₁).comp (of k G) = (↑φ₂).comp (of k G)) : φ₁ = φ₂

theorem SkewMonoidAlgebra.algHom_ext'_iff {k : Type u_1} {G : Type u_2} [Monoid G] [CommSemiring k] {A : Type u_3} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] {φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A} : φ₁ = φ₂ ↔ (↑φ₁).comp (of k G) = (↑φ₂).comp (of k G)