Monoid algebras

When the domain of a Finsupp has a multiplicative or additive structure, we can define a convolution product. To mathematicians this structure is known as the "monoid algebra", i.e. the finite formal linear combinations over a given semiring of elements of the monoid. The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.

In fact the construction of the "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. In this case the construction yields a not-necessarily-unital, not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such algebras to magmas, and we prove this as MonoidAlgebra.liftMagma.

In this file we define MonoidAlgebra k G := G →₀ k, and AddMonoidAlgebra k G in the same way, and then define the convolution product on these.

When the domain is additive, this is used to define polynomials:

Polynomial R := AddMonoidAlgebra R ℕ
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)

When the domain is multiplicative, e.g. a group, this will be used to define the group ring.

Notation

We introduce the notation R[A] for AddMonoidAlgebra R A.

Implementation note

Unfortunately because additive and multiplicative structures both appear in both cases, it doesn't appear to be possible to make much use of to_additive, and we just settle for saying everything twice.

Similarly, I attempted to just define k[G] := MonoidAlgebra k (Multiplicative G), but the definitional equality Multiplicative G = G leaks through everywhere, and seems impossible to use.

Multiplicative monoids

def MonoidAlgebra (k : Type u₁) (G : Type u₂) [Semiring k] : Type (max u₁ u₂)

The 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 the convolution product.

Equations

• MonoidAlgebra k G = (G →₀ k)

instance MonoidAlgebra.inhabited (k : Type u₁) (G : Type u₂) [Semiring k] : Inhabited (MonoidAlgebra k G)

Equations

• MonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))

instance MonoidAlgebra.addCommMonoid (k : Type u₁) (G : Type u₂) [Semiring k] : AddCommMonoid (MonoidAlgebra k G)

Equations

• MonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))

instance MonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] : CoeFun (MonoidAlgebra k G) fun x => G → k

Equations

• MonoidAlgebra.coeFun k G = Finsupp.coeFun

@[inline, reducible]

abbrev MonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) : MonoidAlgebra k G

Equations

• MonoidAlgebra.single a b = fun₀ | a => b

theorem MonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) : MonoidAlgebra.single a 0 = 0

theorem MonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b₁ : k) (b₂ : k) : MonoidAlgebra.single a (b₁ + b₂) = MonoidAlgebra.single a b₁ + MonoidAlgebra.single a b₂

@[simp]

theorem MonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [Semiring k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) : Finsupp.sum (MonoidAlgebra.single a b) h = h a b

@[simp]

theorem MonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [Semiring k] (f : MonoidAlgebra k G) : Finsupp.sum f MonoidAlgebra.single = f

theorem MonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {a' : G} {b : k} [Decidable (a = a')] : ↑(MonoidAlgebra.single a b) a' = if a = a' then b else 0

@[simp]

theorem MonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {b : k} : MonoidAlgebra.single a b = 0 ↔ b = 0

@[inline, reducible]

abbrev MonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} (f : G → G') (v : MonoidAlgebra k G) : MonoidAlgebra k G'

Equations

• MonoidAlgebra.mapDomain f v = Finsupp.mapDomain f v

theorem MonoidAlgebra.mapDomain_sum {k : Type u₁} {G : Type u₂} [Semiring k] {k' : Type u_3} {G' : Type u_4} [Semiring k'] {f : G → G'} {s : MonoidAlgebra k' G} {v : G → k' → MonoidAlgebra k G} : MonoidAlgebra.mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun a b => MonoidAlgebra.mapDomain f (v a b)

def MonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) : MonoidAlgebra k G →+ R

A non-commutative version of MonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a homomorphism g : G → R, returns the additive homomorphism from MonoidAlgebra k G such that liftNC f g (single a b) = f b * g a. If f is a ring homomorphism and the range of either f or g is in center of R, then the result is a ring homomorphism. If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called MonoidAlgebra.lift.

Equations

• MonoidAlgebra.liftNC f g = ↑Finsupp.liftAddHom fun x => AddMonoidHom.comp (AddMonoidHom.mulRight (g x)) f

@[simp]

theorem MonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) (a : G) (b : k) : ↑(MonoidAlgebra.liftNC f g) (MonoidAlgebra.single a b) = ↑f b * g a

instance MonoidAlgebra.mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] : Mul (MonoidAlgebra k G)

The product of f g : MonoidAlgebra k G is the finitely supported function whose value at a is the sum of f x * g y over all pairs x, y such that x * y = a. (Think of the group ring of a group.)

Equations

• MonoidAlgebra.mul = { mul := fun f g => Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂) }

theorem MonoidAlgebra.mul_def {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {f : MonoidAlgebra k G} {g : MonoidAlgebra k G} : f * g = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)

instance MonoidAlgebra.nonUnitalNonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] : NonUnitalNonAssocSemiring (MonoidAlgebra k G)

Equations

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

theorem MonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Mul G] [Semiring R] {g_hom : Type u_3} [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom) (a : MonoidAlgebra k G) (b : MonoidAlgebra k G) (h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g y)) : ↑(MonoidAlgebra.liftNC ↑f ↑g) (a * b) = ↑(MonoidAlgebra.liftNC ↑f ↑g) a * ↑(MonoidAlgebra.liftNC ↑f ↑g) b

instance MonoidAlgebra.nonUnitalSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [Semigroup G] : NonUnitalSemiring (MonoidAlgebra k G)

Equations

• MonoidAlgebra.nonUnitalSemiring = let src := MonoidAlgebra.nonUnitalNonAssocSemiring; NonUnitalSemiring.mk (_ : ∀ (f g h : MonoidAlgebra k G), f * g * h = f * (g * h))

instance MonoidAlgebra.one {k : Type u₁} {G : Type u₂} [Semiring k] [One G] : One (MonoidAlgebra k G)

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

Equations

• MonoidAlgebra.one = { one := MonoidAlgebra.single 1 1 }

theorem MonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [Semiring k] [One G] : 1 = MonoidAlgebra.single 1 1

@[simp]

theorem MonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [NonAssocSemiring R] [Semiring k] [One G] {g_hom : Type u_3} [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) : ↑(MonoidAlgebra.liftNC ↑f ↑g) 1 = 1

instance MonoidAlgebra.nonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] : NonAssocSemiring (MonoidAlgebra k G)

Equations

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

theorem MonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (n : ℕ) : ↑n = MonoidAlgebra.single 1 ↑n

Semiring structure

instance MonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] : Semiring (MonoidAlgebra k G)

Equations

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

def MonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid G] [Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (↑f x) (↑g y)) : MonoidAlgebra k G →+* R

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

Equations

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

instance MonoidAlgebra.nonUnitalCommSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [CommSemigroup G] : NonUnitalCommSemiring (MonoidAlgebra k G)

Equations

• MonoidAlgebra.nonUnitalCommSemiring = let src := MonoidAlgebra.nonUnitalSemiring; NonUnitalCommSemiring.mk (_ : ∀ (f g : MonoidAlgebra k G), f * g = g * f)

instance MonoidAlgebra.nontrivial {k : Type u₁} {G : Type u₂} [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial (MonoidAlgebra k G)

Equations

• @MonoidAlgebra.nontrivial = @MonoidAlgebra.nontrivial.proof_1

Derived instances

instance MonoidAlgebra.commSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [CommMonoid G] : CommSemiring (MonoidAlgebra k G)

Equations

• MonoidAlgebra.commSemiring = let src := MonoidAlgebra.nonUnitalCommSemiring; let src_1 := MonoidAlgebra.semiring; CommSemiring.mk (_ : ∀ (a b : MonoidAlgebra k G), a * b = b * a)

instance MonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [Semiring k] [Subsingleton k] : Unique (MonoidAlgebra k G)

Equations

• MonoidAlgebra.unique = Finsupp.uniqueOfRight

instance MonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] : AddCommGroup (MonoidAlgebra k G)

Equations

• MonoidAlgebra.addCommGroup = Finsupp.addCommGroup

instance MonoidAlgebra.nonUnitalNonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [Mul G] : NonUnitalNonAssocRing (MonoidAlgebra k G)

Equations

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

instance MonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [Semigroup G] : NonUnitalRing (MonoidAlgebra k G)

Equations

• MonoidAlgebra.nonUnitalRing = let src := MonoidAlgebra.addCommGroup; let src_1 := MonoidAlgebra.nonUnitalSemiring; NonUnitalRing.mk (_ : ∀ (a b c : MonoidAlgebra k G), a * b * c = a * (b * c))

instance MonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] : NonAssocRing (MonoidAlgebra k G)

Equations

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

theorem MonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] (z : ℤ) : ↑z = MonoidAlgebra.single 1 ↑z

instance MonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [Monoid G] : Ring (MonoidAlgebra k G)

Equations

• MonoidAlgebra.ring = let src := MonoidAlgebra.nonAssocRing; let src_1 := MonoidAlgebra.semiring; Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : MonoidAlgebra k G), -a + a = 0)

instance MonoidAlgebra.nonUnitalCommRing {k : Type u₁} {G : Type u₂} [CommRing k] [CommSemigroup G] : NonUnitalCommRing (MonoidAlgebra k G)

Equations

• MonoidAlgebra.nonUnitalCommRing = let src := MonoidAlgebra.nonUnitalCommSemiring; let src := MonoidAlgebra.nonUnitalRing; NonUnitalCommRing.mk (_ : ∀ (a b : MonoidAlgebra k G), a * b = b * a)

instance MonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [CommMonoid G] : CommRing (MonoidAlgebra k G)

Equations

• MonoidAlgebra.commRing = let src := MonoidAlgebra.nonUnitalCommRing; let src_1 := MonoidAlgebra.ring; CommRing.mk (_ : ∀ (a b : MonoidAlgebra k G), a * b = b * a)

instance MonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] : SMulZeroClass R (MonoidAlgebra k G)

Equations

• MonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass

instance MonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] : DistribSMul R (MonoidAlgebra k G)

Equations

• MonoidAlgebra.distribSMul = Finsupp.distribSMul G k

instance MonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] : DistribMulAction R (MonoidAlgebra k G)

Equations

• MonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k

instance MonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] : Module R (MonoidAlgebra k G)

Equations

• MonoidAlgebra.module = Finsupp.module G k

instance MonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] [FaithfulSMul R k] [Nonempty G] : FaithfulSMul R (MonoidAlgebra k G)

Equations

• @MonoidAlgebra.faithfulSMul = @MonoidAlgebra.faithfulSMul.proof_1

instance MonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] : IsScalarTower R S (MonoidAlgebra k G)

Equations

• @MonoidAlgebra.isScalarTower = @MonoidAlgebra.isScalarTower.proof_1

instance MonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k] [DistribMulAction S k] [SMulCommClass R S k] : SMulCommClass R S (MonoidAlgebra k G)

Equations

• @MonoidAlgebra.smulCommClass = @MonoidAlgebra.smulCommClass.proof_1

instance MonoidAlgebra.isCentralScalar {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] [DistribMulAction Rᵐᵒᵖ k] [IsCentralScalar R k] : IsCentralScalar R (MonoidAlgebra k G)

Equations

• @MonoidAlgebra.isCentralScalar = @MonoidAlgebra.isCentralScalar.proof_1

def MonoidAlgebra.comapDistribMulActionSelf {k : Type u₁} {G : Type u₂} [Group G] [Semiring k] : DistribMulAction G (MonoidAlgebra k G)

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

Equations

• MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction

theorem MonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) : ↑(f * g) x = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

theorem MonoidAlgebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p ∈ s ↔ p.fst * p.snd = x) : ↑(f * g) x = Finset.sum s fun p => ↑f p.fst * ↑g p.snd

@[simp]

theorem MonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} : MonoidAlgebra.single a₁ b₁ * MonoidAlgebra.single a₂ b₂ = MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)

@[simp]

theorem MonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] {a : G} {b : k} (n : ℕ) : MonoidAlgebra.single a b ^ n = MonoidAlgebra.single (a ^ n) (b ^ n)

@[simp]

theorem MonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [One α] [One α₂] {F : Type u_6} [OneHomClass F α α₂] (f : F) : MonoidAlgebra.mapDomain (↑f) 1 = 1

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

theorem MonoidAlgebra.mapDomain_mul {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [Mul α] [Mul α₂] {F : Type u_6} [MulHomClass F α α₂] (f : F) (x : MonoidAlgebra β α) (y : MonoidAlgebra β α) : MonoidAlgebra.mapDomain (↑f) (x * y) = MonoidAlgebra.mapDomain (↑f) x * MonoidAlgebra.mapDomain (↑f) y

Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

@[simp]

theorem MonoidAlgebra.ofMagma_apply (k : Type u₁) (G : Type u₂) [Semiring k] [Mul G] (a : G) : ↑(MonoidAlgebra.ofMagma k G) a = MonoidAlgebra.single a 1

def MonoidAlgebra.ofMagma (k : Type u₁) (G : Type u₂) [Semiring k] [Mul G] : G →ₙ* MonoidAlgebra k G

The embedding of a magma into its magma algebra.

Equations

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

@[simp]

theorem MonoidAlgebra.of_apply (k : Type u₁) (G : Type u₂) [Semiring k] [MulOneClass G] (a : G) : ↑(MonoidAlgebra.of k G) a = MonoidAlgebra.single a 1

def MonoidAlgebra.of (k : Type u₁) (G : Type u₂) [Semiring k] [MulOneClass G] : G →* MonoidAlgebra k G

The embedding of a unital magma into its magma algebra.

Equations

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

theorem MonoidAlgebra.smul_of {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (g : G) (r : k) : r • ↑(MonoidAlgebra.of k G) g = MonoidAlgebra.single g r

theorem MonoidAlgebra.of_injective {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] [Nontrivial k] : Function.Injective ↑(MonoidAlgebra.of k G)

@[simp]

theorem MonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (a : k × G) : ↑MonoidAlgebra.singleHom a = MonoidAlgebra.single a.snd a.fst

def MonoidAlgebra.singleHom {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] : k × G →* MonoidAlgebra k G

Finsupp.single as a MonoidHom from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of Finsupp.single.

Equations

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

theorem MonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) {r : k} {x : G} {y : G} {z : G} (H : ∀ (a : G), a * x = z ↔ a = y) : ↑(f * MonoidAlgebra.single x r) z = ↑f y * r

theorem MonoidAlgebra.mul_single_one_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) : ↑(f * MonoidAlgebra.single 1 r) x = ↑f x * r

theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : k) {g : G} {g' : G} (x : MonoidAlgebra k G) (h : ¬∃ d, g' = d * g) : ↑(x * MonoidAlgebra.single g r) g' = 0

theorem MonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) {r : k} {x : G} {y : G} {z : G} (H : ∀ (a : G), x * a = y ↔ a = z) : ↑(MonoidAlgebra.single x r * f) y = r * ↑f z

theorem MonoidAlgebra.single_one_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) : ↑(MonoidAlgebra.single 1 r * f) x = r * ↑f x

theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : k) {g : G} {g' : G} (x : MonoidAlgebra k G) (h : ¬∃ d, g' = g * d) : ↑(MonoidAlgebra.single g r * x) g' = 0

theorem MonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] {R : Type u_3} [Semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : MonoidAlgebra k G) : ↑(MonoidAlgebra.liftNC ↑f ↑g) (c • φ) = ↑f c * ↑(MonoidAlgebra.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)

Equations

• MonoidAlgebra.isScalarTower_self = MonoidAlgebra.isScalarTower_self.proof_1

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.

Equations

• MonoidAlgebra.smulCommClass_self = MonoidAlgebra.smulCommClass_self.proof_1

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)

Equations

• MonoidAlgebra.smulCommClass_symm_self = MonoidAlgebra.smulCommClass_symm_self.proof_1

theorem MonoidAlgebra.nonUnitalAlgHom_ext (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ : MonoidAlgebra k G →ₙₐ[k] A} {φ₂ : MonoidAlgebra k G →ₙₐ[k] A} (h : ∀ (x : G), ↑φ₁ (MonoidAlgebra.single x 1) = ↑φ₂ (MonoidAlgebra.single x 1)) : φ₁ = φ₂

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

theorem MonoidAlgebra.nonUnitalAlgHom_ext' (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ : MonoidAlgebra k G →ₙₐ[k] A} {φ₂ : MonoidAlgebra k G →ₙₐ[k] A} (h : MulHom.comp (NonUnitalAlgHom.toMulHom φ₁) (MonoidAlgebra.ofMagma k G) = MulHom.comp (NonUnitalAlgHom.toMulHom φ₂) (MonoidAlgebra.ofMagma k G)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

@[simp]

theorem MonoidAlgebra.liftMagma_apply_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (f : G →ₙ* A) (a : MonoidAlgebra k G) : ↑(↑(MonoidAlgebra.liftMagma k) f) a = Finsupp.sum a fun m t => t • ↑f m

@[simp]

theorem MonoidAlgebra.liftMagma_symm_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (F : MonoidAlgebra k G →ₙₐ[k] A) : ↑(MonoidAlgebra.liftMagma k).symm F = MulHom.comp (NonUnitalAlgHom.toMulHom F) (MonoidAlgebra.ofMagma k G)

def MonoidAlgebra.liftMagma (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (G →ₙ* A) ≃ (MonoidAlgebra k G →ₙₐ[k] A)

The functor G ↦ MonoidAlgebra k G, from the category of magmas to the category of non-unital, non-associative algebras over k is adjoint to the forgetful functor in the other direction.

Equations

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

Algebra structure

theorem MonoidAlgebra.single_one_comm {k : Type u₁} {G : Type u₂} [CommSemiring k] [MulOneClass G] (r : k) (f : MonoidAlgebra k G) : MonoidAlgebra.single 1 r * f = f * MonoidAlgebra.single 1 r

@[simp]

theorem MonoidAlgebra.singleOneRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] : ∀ (a : k), ↑MonoidAlgebra.singleOneRingHom a = ZeroHom.toFun (↑(Finsupp.singleAddHom 1)) a

def MonoidAlgebra.singleOneRingHom {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] : k →+* MonoidAlgebra k G

Finsupp.single 1 as a RingHom

Equations

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

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_apply {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [Semiring k] [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) : ∀ (a : G →₀ k), ↑(MonoidAlgebra.mapDomainRingHom k f) a = ZeroHom.toFun (↑(Finsupp.mapDomain.addMonoidHom ↑f)) a

def MonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [Semiring k] [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) : MonoidAlgebra k G →+* MonoidAlgebra k H

If f : G → H is a multiplicative homomorphism between two monoids, then Finsupp.mapDomain f is a ring homomorphism between their monoid algebras.

Equations

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

theorem MonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f : MonoidAlgebra k G →+* R} {g : MonoidAlgebra k G →+* R} (h₁ : ∀ (b : k), ↑f (MonoidAlgebra.single 1 b) = ↑g (MonoidAlgebra.single 1 b)) (h_of : ∀ (a : G), ↑f (MonoidAlgebra.single a 1) = ↑g (MonoidAlgebra.single a 1)) : f = g

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

theorem MonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f : MonoidAlgebra k G →+* R} {g : MonoidAlgebra k G →+* R} (h₁ : RingHom.comp f MonoidAlgebra.singleOneRingHom = RingHom.comp g MonoidAlgebra.singleOneRingHom) (h_of : MonoidHom.comp (↑f) (MonoidAlgebra.of k G) = MonoidHom.comp (↑g) (MonoidAlgebra.of k G)) : f = g

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

See note [partially-applied ext lemmas].

instance MonoidAlgebra.algebra {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : Algebra k (MonoidAlgebra A G)

The instance Algebra k (MonoidAlgebra A G) whenever we have Algebra k A.

In particular this provides the instance Algebra k (MonoidAlgebra k G).

Equations

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

@[simp]

theorem MonoidAlgebra.singleOneAlgHom_apply {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : ∀ (a : A), ↑MonoidAlgebra.singleOneAlgHom a = fun₀ | 1 => a

def MonoidAlgebra.singleOneAlgHom {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : A →ₐ[k] MonoidAlgebra A G

Finsupp.single 1 as an AlgHom

Equations

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

@[simp]

theorem MonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : ↑(algebraMap k (MonoidAlgebra A G)) = MonoidAlgebra.single 1 ∘ ↑(algebraMap k A)

theorem MonoidAlgebra.single_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] (a : G) (b : k) : MonoidAlgebra.single a b = ↑(algebraMap k (MonoidAlgebra k G)) b * ↑(MonoidAlgebra.of k G) a

theorem MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] (a : G) (b : k) : MonoidAlgebra.single a (↑(algebraMap k A) b) = ↑(algebraMap k (MonoidAlgebra A G)) b * ↑(MonoidAlgebra.of A G) a

theorem MonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G) (hM : (g : G) → p (↑(MonoidAlgebra.of k G) g)) (hadd : (f g : MonoidAlgebra k G) → p f → p g → p (f + g)) (hsmul : (r : k) → (f : MonoidAlgebra k G) → p f → p (r • f)) : p f

def MonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] {B : Type u_3} [Semiring B] [Algebra k B] (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ (x : A) (y : G), Commute (↑f x) (↑g y)) : MonoidAlgebra A G →ₐ[k] B

liftNCRingHom as an AlgHom, for when f is an AlgHom

Equations

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

theorem MonoidAlgebra.algHom_ext {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : MonoidAlgebra k G →ₐ[k] A⦄ ⦃φ₂ : MonoidAlgebra k G →ₐ[k] A⦄ (h : ∀ (x : G), ↑φ₁ (MonoidAlgebra.single x 1) = ↑φ₂ (MonoidAlgebra.single x 1)) : φ₁ = φ₂

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

theorem MonoidAlgebra.algHom_ext' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : MonoidAlgebra k G →ₐ[k] A⦄ ⦃φ₂ : MonoidAlgebra k G →ₐ[k] A⦄ (h : MonoidHom.comp (↑φ₁) (MonoidAlgebra.of k G) = MonoidHom.comp (↑φ₂) (MonoidAlgebra.of k G)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

def MonoidAlgebra.lift (k : Type u₁) (G : Type u₂) [CommSemiring k] [Monoid G] (A : Type u₃) [Semiring A] [Algebra k A] : (G →* A) ≃ (MonoidAlgebra k G →ₐ[k] A)

Any monoid homomorphism G →* A can be lifted to an algebra homomorphism MonoidAlgebra k G →ₐ[k] A.

Equations

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

theorem MonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (f : MonoidAlgebra k G) : ↑(↑(MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => ↑(algebraMap k A) b * ↑F a

theorem MonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (f : MonoidAlgebra k G) : ↑(↑(MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => b • ↑F a

theorem MonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) : ↑(↑(MonoidAlgebra.lift k G A) F) = ↑(MonoidAlgebra.liftNC ↑(algebraMap k A) ↑F)

@[simp]

theorem MonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) (x : G) : ↑(↑(MonoidAlgebra.lift k G A).symm F) x = ↑F (MonoidAlgebra.single x 1)

theorem MonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (x : G) : ↑(↑(MonoidAlgebra.lift k G A) F) (↑(MonoidAlgebra.of k G) x) = ↑F x

@[simp]

theorem MonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (a : G) (b : k) : ↑(↑(MonoidAlgebra.lift k G A) F) (MonoidAlgebra.single a b) = b • ↑F a

theorem MonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) : F = ↑(MonoidAlgebra.lift k G A) (MonoidHom.comp (↑F) (MonoidAlgebra.of k G))

theorem MonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) : ↑F f = Finsupp.sum f fun a b => b • ↑F (MonoidAlgebra.single a 1)

Decomposition of a k-algebra homomorphism from MonoidAlgebra k G by its values on F (single a 1).

@[simp]

theorem MonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [MulHomClass F G H] (f : F) : ∀ (a : G →₀ A), ↑(MonoidAlgebra.mapDomainNonUnitalAlgHom k A f) a = ZeroHom.toFun (↑(Finsupp.mapDomain.addMonoidHom ↑f)) a

def MonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [MulHomClass F G H] (f : F) : MonoidAlgebra A G →ₙₐ[k] MonoidAlgebra A H

If f : G → H is a homomorphism between two magmas, then Finsupp.mapDomain f is a non-unital algebra homomorphism between their magma algebras.

Equations

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

theorem MonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] {F : Type u_4} [MonoidHomClass F G H] (f : F) (r : k) : MonoidAlgebra.mapDomain (↑f) (↑(algebraMap k (MonoidAlgebra A G)) r) = ↑(algebraMap k (MonoidAlgebra A H)) r

@[simp]

theorem MonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} [Monoid G] (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_6} {F : Type u_7} [Monoid H] [MonoidHomClass F G H] (f : F) : ∀ (a : G →₀ A), ↑(MonoidAlgebra.mapDomainAlgHom k A f) a = Finsupp.mapDomain (↑f) a

def MonoidAlgebra.mapDomainAlgHom {G : Type u₂} [Monoid G] (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_6} {F : Type u_7} [Monoid H] [MonoidHomClass F G H] (f : F) : MonoidAlgebra A G →ₐ[k] MonoidAlgebra A H

If f : G → H is a multiplicative homomorphism between two monoids, then Finsupp.mapDomain f is an algebra homomorphism between their monoid algebras.

Equations

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

def MonoidAlgebra.domCongr (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) : MonoidAlgebra A G ≃ₐ[k] MonoidAlgebra A H

If e : G ≃* H is a multiplicative equivalence between two monoids, then MonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.

Equations

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

theorem MonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) : ↑(MonoidAlgebra.domCongr k A e) = MonoidAlgebra.mapDomainAlgHom k A e

@[simp]

theorem MonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (f : MonoidAlgebra A G) (h : H) : ↑(↑(MonoidAlgebra.domCongr k A e) f) h = ↑f (↑(MulEquiv.symm e) h)

@[simp]

theorem MonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (f : MonoidAlgebra A G) : (↑(MonoidAlgebra.domCongr k A e) f).support = Finset.map (Equiv.toEmbedding ↑e) f.support

@[simp]

theorem MonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (g : G) (a : A) : ↑(MonoidAlgebra.domCongr k A e) (MonoidAlgebra.single g a) = MonoidAlgebra.single (↑e g) a

@[simp]

theorem MonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} [CommSemiring k] [Monoid G] (A : Type u₃) [Semiring A] [Algebra k A] : MonoidAlgebra.domCongr k A (MulEquiv.refl G) = AlgEquiv.refl

@[simp]

theorem MonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) : AlgEquiv.symm (MonoidAlgebra.domCongr k A e) = MonoidAlgebra.domCongr k A (MulEquiv.symm e)

def MonoidAlgebra.GroupSmul.linearMap (k : Type u₁) {G : Type u₂} [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) : V →ₗ[k] V

When V is a k[G]-module, multiplication by a group element g is a k-linear map.

Equations

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

@[simp]

theorem MonoidAlgebra.GroupSmul.linearMap_apply (k : Type u₁) {G : Type u₂} [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) (v : V) : ↑(MonoidAlgebra.GroupSmul.linearMap k V g) v = MonoidAlgebra.single g 1 • v

def MonoidAlgebra.equivariantOfLinearOfComm {k : Type u₁} {G : Type u₂} [Monoid G] [CommSemiring k] {V : Type u₃} {W : Type u₄} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] [AddCommMonoid W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), ↑f (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • ↑f v) : V →ₗ[MonoidAlgebra k G] W

Build a k[G]-linear map from a k-linear map and evidence that it is G-equivariant.

Equations

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

@[simp]

theorem MonoidAlgebra.equivariantOfLinearOfComm_apply {k : Type u₁} {G : Type u₂} [Monoid G] [CommSemiring k] {V : Type u₃} {W : Type u₄} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] [AddCommMonoid W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), ↑f (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • ↑f v) (v : V) : ↑(MonoidAlgebra.equivariantOfLinearOfComm f h) v = ↑f v

theorem MonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} : (Finset.prod s fun i => MonoidAlgebra.single (a i) (b i)) = MonoidAlgebra.single (Finset.prod s fun i => a i) (Finset.prod s fun i => b i)

@[simp]

theorem MonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (r : k) (x : G) (y : G) : ↑(f * MonoidAlgebra.single x r) y = ↑f (y * x⁻¹) * r

@[simp]

theorem MonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (r : k) (x : G) (f : MonoidAlgebra k G) (y : G) : ↑(MonoidAlgebra.single x r * f) y = r * ↑f (x⁻¹ * y)

theorem MonoidAlgebra.mul_apply_left {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) : ↑(f * g) x = Finsupp.sum f fun a b => b * ↑g (a⁻¹ * x)

theorem MonoidAlgebra.mul_apply_right {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) : ↑(f * g) x = Finsupp.sum g fun a b => ↑f (x * a⁻¹) * b

@[simp]

theorem MonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] : ∀ (a : Gᵐᵒᵖ →₀ kᵐᵒᵖ), ↑(RingEquiv.symm MonoidAlgebra.opRingEquiv) a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop (_ : MulOpposite.unop 0 = 0) (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a))

@[simp]

theorem MonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] : ∀ (a : (G →₀ k)ᵐᵒᵖ), ↑MonoidAlgebra.opRingEquiv a = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op (_ : ↑MulOpposite.opAddEquiv 0 = 0) (MulOpposite.unop a))

noncomputable def MonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] : (MonoidAlgebra k G)ᵐᵒᵖ ≃+* MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ

The opposite of a MonoidAlgebra R I equivalent as a ring to the MonoidAlgebra Rᵐᵒᵖ Iᵐᵒᵖ over the opposite ring, taking elements to their opposite.

Equations

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

theorem MonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] (r : k) (x : G) : ↑MonoidAlgebra.opRingEquiv (MulOpposite.op (MonoidAlgebra.single x r)) = MonoidAlgebra.single (MulOpposite.op x) (MulOpposite.op r)

theorem MonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) : ↑(RingEquiv.symm MonoidAlgebra.opRingEquiv) (MonoidAlgebra.single x r) = MulOpposite.op (MonoidAlgebra.single (MulOpposite.unop x) (MulOpposite.unop r))

def MonoidAlgebra.submoduleOfSmulMem {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {V : Type u_3} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (W : Submodule k V) (h : ∀ (g : G) (v : V), v ∈ W → ↑(MonoidAlgebra.of k G) g • v ∈ W) : Submodule (MonoidAlgebra k G) V

A submodule over k which is stable under scalar multiplication by elements of G is a submodule over MonoidAlgebra k G

Equations

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

Additive monoids

def AddMonoidAlgebra (k : Type u₁) (G : Type u₂) [Semiring k] : Type (max u₂ u₁)

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

Equations

• AddMonoidAlgebra k G = (G →₀ k)

def AddMonoidAlgebra.«term_[_]» : Lean.TrailingParserDescr

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

Equations

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

instance AddMonoidAlgebra.inhabited (k : Type u₁) (G : Type u₂) [Semiring k] : Inhabited (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))

instance AddMonoidAlgebra.addCommMonoid (k : Type u₁) (G : Type u₂) [Semiring k] : AddCommMonoid (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))

instance AddMonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] : CoeFun (AddMonoidAlgebra k G) fun x => G → k

Equations

• AddMonoidAlgebra.coeFun k G = Finsupp.coeFun

@[inline, reducible]

abbrev AddMonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) : AddMonoidAlgebra k G

Equations

• AddMonoidAlgebra.single a b = fun₀ | a => b

theorem AddMonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) : AddMonoidAlgebra.single a 0 = 0

theorem AddMonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b₁ : k) (b₂ : k) : AddMonoidAlgebra.single a (b₁ + b₂) = AddMonoidAlgebra.single a b₁ + AddMonoidAlgebra.single a b₂

@[simp]

theorem AddMonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [Semiring k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) : Finsupp.sum (AddMonoidAlgebra.single a b) h = h a b

@[simp]

theorem AddMonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [Semiring k] (f : AddMonoidAlgebra k G) : Finsupp.sum f AddMonoidAlgebra.single = f

theorem AddMonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {a' : G} {b : k} [Decidable (a = a')] : ↑(AddMonoidAlgebra.single a b) a' = if a = a' then b else 0

@[simp]

theorem AddMonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {b : k} : AddMonoidAlgebra.single a b = 0 ↔ b = 0

@[inline, reducible]

abbrev AddMonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} (f : G → G') (v : AddMonoidAlgebra k G) : AddMonoidAlgebra k G'

Equations

• AddMonoidAlgebra.mapDomain f v = Finsupp.mapDomain f v

theorem AddMonoidAlgebra.mapDomain_sum {k : Type u₁} {G : Type u₂} [Semiring k] {k' : Type u_3} {G' : Type u_4} [Semiring k'] {f : G → G'} {s : AddMonoidAlgebra k' G} {v : G → k' → AddMonoidAlgebra k G} : AddMonoidAlgebra.mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun a b => AddMonoidAlgebra.mapDomain f (v a b)

theorem AddMonoidAlgebra.mapDomain_single {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} {f : G → G'} {a : G} {b : k} : AddMonoidAlgebra.mapDomain f (AddMonoidAlgebra.single a b) = AddMonoidAlgebra.single (f a) b

def AddMonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative G → R) : AddMonoidAlgebra k G →+ R

A non-commutative version of AddMonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a map g : Multiplicative G → R, returns the additive homomorphism from k[G] such that liftNC f g (single a b) = f b * g a. If f is a ring homomorphism and the range of either f or g is in center of R, then the result is a ring homomorphism. If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called AddMonoidAlgebra.lift.

Equations

• AddMonoidAlgebra.liftNC f g = ↑Finsupp.liftAddHom fun x => AddMonoidHom.comp (AddMonoidHom.mulRight (g (↑Multiplicative.ofAdd x))) f

@[simp]

theorem AddMonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative G → R) (a : G) (b : k) : ↑(AddMonoidAlgebra.liftNC f g) (AddMonoidAlgebra.single a b) = ↑f b * g (↑Multiplicative.ofAdd a)

instance AddMonoidAlgebra.hasMul {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] : Mul (AddMonoidAlgebra k G)

The product of f g : k[G] is the finitely supported function whose value at a is the sum of f x * g y over all pairs x, y such that x + y = a. (Think of the product of multivariate polynomials where α is the additive monoid of monomial exponents.)

Equations

• AddMonoidAlgebra.hasMul = { mul := fun f g => Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂) }

theorem AddMonoidAlgebra.mul_def {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {f : AddMonoidAlgebra k G} {g : AddMonoidAlgebra k G} : f * g = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)

instance AddMonoidAlgebra.nonUnitalNonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] : NonUnitalNonAssocSemiring (AddMonoidAlgebra k G)

Equations

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

theorem AddMonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Add G] [Semiring R] {g_hom : Type u_3} [MulHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) (a : AddMonoidAlgebra k G) (b : AddMonoidAlgebra k G) (h_comm : ∀ {x y : G}, y ∈ a.support → Commute (↑f (↑b x)) (↑g (↑Multiplicative.ofAdd y))) : ↑(AddMonoidAlgebra.liftNC ↑f ↑g) (a * b) = ↑(AddMonoidAlgebra.liftNC ↑f ↑g) a * ↑(AddMonoidAlgebra.liftNC ↑f ↑g) b

instance AddMonoidAlgebra.one {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] : One (AddMonoidAlgebra k G)

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

Equations

• AddMonoidAlgebra.one = { one := AddMonoidAlgebra.single 0 1 }

theorem AddMonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] : 1 = AddMonoidAlgebra.single 0 1

@[simp]

theorem AddMonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Zero G] [NonAssocSemiring R] {g_hom : Type u_3} [OneHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) : ↑(AddMonoidAlgebra.liftNC ↑f ↑g) 1 = 1

instance AddMonoidAlgebra.nonUnitalSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [AddSemigroup G] : NonUnitalSemiring (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.nonUnitalSemiring = let src := AddMonoidAlgebra.nonUnitalNonAssocSemiring; NonUnitalSemiring.mk (_ : ∀ (f g h : AddMonoidAlgebra k G), f * g * h = f * (g * h))

instance AddMonoidAlgebra.nonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] : NonAssocSemiring (AddMonoidAlgebra k G)

Equations

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

theorem AddMonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (n : ℕ) : ↑n = AddMonoidAlgebra.single 0 ↑n

Semiring structure

instance AddMonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] : SMulZeroClass R (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass

instance AddMonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] : Semiring (AddMonoidAlgebra k G)

Equations

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

def AddMonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [AddMonoid G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ (x : k) (y : Multiplicative G), Commute (↑f x) (↑g y)) : AddMonoidAlgebra k G →+* R

liftNC as a RingHom, for when f and g commute

Equations

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

instance AddMonoidAlgebra.nonUnitalCommSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddCommSemigroup G] : NonUnitalCommSemiring (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.nonUnitalCommSemiring = let src := AddMonoidAlgebra.nonUnitalSemiring; NonUnitalCommSemiring.mk (_ : ∀ (a b : MonoidAlgebra k (Multiplicative G)), a * b = b * a)

instance AddMonoidAlgebra.nontrivial {k : Type u₁} {G : Type u₂} [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial (AddMonoidAlgebra k G)

Equations

• @AddMonoidAlgebra.nontrivial = @AddMonoidAlgebra.nontrivial.proof_1

Derived instances

instance AddMonoidAlgebra.commSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddCommMonoid G] : CommSemiring (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.commSemiring = let src := AddMonoidAlgebra.nonUnitalCommSemiring; let src_1 := AddMonoidAlgebra.semiring; CommSemiring.mk (_ : ∀ (a b : AddMonoidAlgebra k G), a * b = b * a)

instance AddMonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [Semiring k] [Subsingleton k] : Unique (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.unique = Finsupp.uniqueOfRight

instance AddMonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] : AddCommGroup (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.addCommGroup = Finsupp.addCommGroup

instance AddMonoidAlgebra.nonUnitalNonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [Add G] : NonUnitalNonAssocRing (AddMonoidAlgebra k G)

Equations

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

instance AddMonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [AddSemigroup G] : NonUnitalRing (AddMonoidAlgebra k G)

Equations

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

instance AddMonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] : NonAssocRing (AddMonoidAlgebra k G)

Equations

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

theorem AddMonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] (z : ℤ) : ↑z = AddMonoidAlgebra.single 0 ↑z

instance AddMonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [AddMonoid G] : Ring (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.ring = let src := AddMonoidAlgebra.nonAssocRing; let src_1 := AddMonoidAlgebra.semiring; Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : AddMonoidAlgebra k G), -a + a = 0)

instance AddMonoidAlgebra.nonUnitalCommRing {k : Type u₁} {G : Type u₂} [CommRing k] [AddCommSemigroup G] : NonUnitalCommRing (AddMonoidAlgebra k G)

Equations

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

instance AddMonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [AddCommMonoid G] : CommRing (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.commRing = let src := AddMonoidAlgebra.nonUnitalCommRing; let src_1 := AddMonoidAlgebra.ring; CommRing.mk (_ : ∀ (a b : AddMonoidAlgebra k G), a * b = b * a)

instance AddMonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] : DistribSMul R (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.distribSMul = Finsupp.distribSMul G k

instance AddMonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] : DistribMulAction R (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k

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)

Equations

• @AddMonoidAlgebra.faithfulSMul = @AddMonoidAlgebra.faithfulSMul.proof_1

instance AddMonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] : Module R (AddMonoidAlgebra k G)

Equations

• AddMonoidAlgebra.module = Finsupp.module G k

instance AddMonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] : IsScalarTower R S (AddMonoidAlgebra k G)

Equations

• @AddMonoidAlgebra.isScalarTower = @AddMonoidAlgebra.isScalarTower.proof_1

instance AddMonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] : SMulCommClass R S (AddMonoidAlgebra k G)

Equations

• @AddMonoidAlgebra.smulCommClass = @AddMonoidAlgebra.smulCommClass.proof_1

instance AddMonoidAlgebra.isCentralScalar {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k] [IsCentralScalar R k] : IsCentralScalar R (AddMonoidAlgebra k G)

Equations

• @AddMonoidAlgebra.isCentralScalar = @AddMonoidAlgebra.isCentralScalar.proof_1

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

theorem AddMonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Add G] (f : AddMonoidAlgebra k G) (g : AddMonoidAlgebra k G) (x : G) : ↑(f * g) x = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => if a₁ + a₂ = x then b₁ * b₂ else 0

theorem AddMonoidAlgebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (g : AddMonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p ∈ s ↔ p.fst + p.snd = x) : ↑(f * g) x = Finset.sum s fun p => ↑f p.fst * ↑g p.snd

theorem AddMonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} : AddMonoidAlgebra.single a₁ b₁ * AddMonoidAlgebra.single a₂ b₂ = AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)

theorem AddMonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] {a : G} {b : k} (n : ℕ) : AddMonoidAlgebra.single a b ^ n = AddMonoidAlgebra.single (n • a) (b ^ n)

@[simp]

theorem AddMonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [Zero α] [Zero α₂] {F : Type u_6} [ZeroHomClass F α α₂] (f : F) : AddMonoidAlgebra.mapDomain (↑f) 1 = 1

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

theorem AddMonoidAlgebra.mapDomain_mul {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [Add α] [Add α₂] {F : Type u_6} [AddHomClass F α α₂] (f : F) (x : AddMonoidAlgebra β α) (y : AddMonoidAlgebra β α) : AddMonoidAlgebra.mapDomain (↑f) (x * y) = AddMonoidAlgebra.mapDomain (↑f) x * AddMonoidAlgebra.mapDomain (↑f) y

Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

@[simp]

theorem AddMonoidAlgebra.ofMagma_apply (k : Type u₁) (G : Type u₂) [Semiring k] [Add G] (a : Multiplicative G) : ↑(AddMonoidAlgebra.ofMagma k G) a = AddMonoidAlgebra.single a 1

def AddMonoidAlgebra.ofMagma (k : Type u₁) (G : Type u₂) [Semiring k] [Add G] : Multiplicative G →ₙ* AddMonoidAlgebra k G

The embedding of an additive magma into its additive magma algebra.

Equations

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

def AddMonoidAlgebra.of (k : Type u₁) (G : Type u₂) [Semiring k] [AddZeroClass G] : Multiplicative G →* AddMonoidAlgebra k G

Embedding of a magma with zero into its magma algebra.

Equations

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

def AddMonoidAlgebra.of' (k : Type u₁) (G : Type u₂) [Semiring k] : G → AddMonoidAlgebra k G

Embedding of a magma with zero G, into its magma algebra, having G as source.

Equations

• AddMonoidAlgebra.of' k G a = AddMonoidAlgebra.single a 1

@[simp]

theorem AddMonoidAlgebra.of_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : Multiplicative G) : ↑(AddMonoidAlgebra.of k G) a = AddMonoidAlgebra.single (↑Multiplicative.toAdd a) 1

@[simp]

theorem AddMonoidAlgebra.of'_apply {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) : AddMonoidAlgebra.of' k G a = AddMonoidAlgebra.single a 1

theorem AddMonoidAlgebra.of'_eq_of {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : G) : AddMonoidAlgebra.of' k G a = ↑(AddMonoidAlgebra.of k G) a

theorem AddMonoidAlgebra.of_injective {k : Type u₁} {G : Type u₂} [Semiring k] [Nontrivial k] [AddZeroClass G] : Function.Injective ↑(AddMonoidAlgebra.of k G)

@[simp]

theorem AddMonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : k × Multiplicative G) : ↑AddMonoidAlgebra.singleHom a = AddMonoidAlgebra.single (↑Multiplicative.toAdd a.snd) a.fst

def AddMonoidAlgebra.singleHom {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] : k × Multiplicative G →* AddMonoidAlgebra k G

Finsupp.single as a MonoidHom from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of Finsupp.single.

Equations

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

theorem AddMonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (r : k) (x : G) (y : G) (z : G) (H : ∀ (a : G), a + x = z ↔ a = y) : ↑(f * AddMonoidAlgebra.single x r) z = ↑f y * r

theorem AddMonoidAlgebra.mul_single_zero_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k) (x : G) : ↑(f * AddMonoidAlgebra.single 0 r) x = ↑f x * r

theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (r : k) {g : G} {g' : G} (x : AddMonoidAlgebra k G) (h : ¬∃ d, g' = d + g) : ↑(x * AddMonoidAlgebra.single g r) g' = 0

theorem AddMonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (r : k) (x : G) (y : G) (z : G) (H : ∀ (a : G), x + a = y ↔ a = z) : ↑(AddMonoidAlgebra.single x r * f) y = r * ↑f z

theorem AddMonoidAlgebra.single_zero_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k) (x : G) : ↑(AddMonoidAlgebra.single 0 r * f) x = r * ↑f x

theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (r : k) {g : G} {g' : G} (x : AddMonoidAlgebra k G) (h : ¬∃ d, g' = g + d) : ↑(AddMonoidAlgebra.single g r * x) g' = 0

theorem AddMonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddGroup G] (f : AddMonoidAlgebra k G) (r : k) (x : G) (y : G) : ↑(f * AddMonoidAlgebra.single x r) y = ↑f (y - x) * r

theorem AddMonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddGroup G] (r : k) (x : G) (f : AddMonoidAlgebra k G) (y : G) : ↑(AddMonoidAlgebra.single x r * f) y = r * ↑f (-x + y)

theorem AddMonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] {R : Type u_3} [AddZeroClass G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (c : k) (φ : MonoidAlgebra k G) : ↑(AddMonoidAlgebra.liftNC ↑f ↑g) (c • φ) = ↑f c * ↑(AddMonoidAlgebra.liftNC ↑f ↑g) φ

theorem AddMonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] {p : AddMonoidAlgebra k G → Prop} (f : AddMonoidAlgebra k G) (hM : (g : G) → p (↑(AddMonoidAlgebra.of k G) (↑Multiplicative.ofAdd g))) (hadd : (f g : AddMonoidAlgebra k G) → p f → p g → p (f + g)) (hsmul : (r : k) → (f : AddMonoidAlgebra k G) → p f → p (r • f)) : p f

@[simp]

theorem AddMonoidAlgebra.mapDomainRingHom_apply {G : Type u₂} (k : Type u_3) [Semiring k] {H : Type u_4} {F : Type u_5} [AddMonoid G] [AddMonoid H] [AddMonoidHomClass F G H] (f : F) : ∀ (a : G →₀ k), ↑(AddMonoidAlgebra.mapDomainRingHom k f) a = ZeroHom.toFun (↑(Finsupp.mapDomain.addMonoidHom ↑f)) a

def AddMonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) [Semiring k] {H : Type u_4} {F : Type u_5} [AddMonoid G] [AddMonoid H] [AddMonoidHomClass F G H] (f : F) : AddMonoidAlgebra k G →+* AddMonoidAlgebra k H

If f : G → H is an additive homomorphism between two additive monoids, then Finsupp.mapDomain f is a ring homomorphism between their add monoid algebras.

Equations

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

Conversions between AddMonoidAlgebra and MonoidAlgebra

We have not defined k[G] = MonoidAlgebra k (Multiplicative G) because historically this caused problems; since the changes that have made nsmul definitional, this would be possible, but for now we just construct the ring isomorphisms using RingEquiv.refl _.

def AddMonoidAlgebra.toMultiplicative (k : Type u₁) (G : Type u₂) [Semiring k] [Add G] : AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G)

The equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative

Equations

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

def MonoidAlgebra.toAdditive (k : Type u₁) (G : Type u₂) [Semiring k] [Mul G] : MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G)

The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive

Equations

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

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)

Equations

• AddMonoidAlgebra.isScalarTower_self = AddMonoidAlgebra.isScalarTower_self.proof_1

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.

Equations

• AddMonoidAlgebra.smulCommClass_self = AddMonoidAlgebra.smulCommClass_self.proof_1

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)

Equations

• AddMonoidAlgebra.smulCommClass_symm_self = AddMonoidAlgebra.smulCommClass_symm_self.proof_1

theorem AddMonoidAlgebra.nonUnitalAlgHom_ext (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ : AddMonoidAlgebra k G →ₙₐ[k] A} {φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A} (h : ∀ (x : G), ↑φ₁ (AddMonoidAlgebra.single x 1) = ↑φ₂ (AddMonoidAlgebra.single x 1)) : φ₁ = φ₂

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

theorem AddMonoidAlgebra.nonUnitalAlgHom_ext' (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ : AddMonoidAlgebra k G →ₙₐ[k] A} {φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A} (h : MulHom.comp (NonUnitalAlgHom.toMulHom φ₁) (AddMonoidAlgebra.ofMagma k G) = MulHom.comp (NonUnitalAlgHom.toMulHom φ₂) (AddMonoidAlgebra.ofMagma k G)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

@[simp]

theorem AddMonoidAlgebra.liftMagma_symm_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (F : AddMonoidAlgebra k G →ₙₐ[k] A) : ↑(AddMonoidAlgebra.liftMagma k).symm F = MulHom.comp (NonUnitalAlgHom.toMulHom F) (AddMonoidAlgebra.ofMagma k G)

@[simp]

theorem AddMonoidAlgebra.liftMagma_apply_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (f : Multiplicative G →ₙ* A) (a : AddMonoidAlgebra k G) : ↑(↑(AddMonoidAlgebra.liftMagma k) f) a = Finsupp.sum a fun m t => t • ↑f (↑Multiplicative.ofAdd m)

def AddMonoidAlgebra.liftMagma (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (Multiplicative G →ₙ* A) ≃ (AddMonoidAlgebra k G →ₙₐ[k] A)

The functor G ↦ k[G], from the category of magmas to the category of non-unital, non-associative algebras over k is adjoint to the forgetful functor in the other direction.

Equations

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

Algebra structure

@[simp]

theorem AddMonoidAlgebra.singleZeroRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] : ∀ (a : k), ↑AddMonoidAlgebra.singleZeroRingHom a = ZeroHom.toFun (↑(Finsupp.singleAddHom 0)) a

def AddMonoidAlgebra.singleZeroRingHom {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] : k →+* AddMonoidAlgebra k G

Finsupp.single 0 as a RingHom

Equations

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

theorem AddMonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [AddMonoid G] [Semiring R] {f : AddMonoidAlgebra k G →+* R} {g : AddMonoidAlgebra k G →+* R} (h₀ : ∀ (b : k), ↑f (AddMonoidAlgebra.single 0 b) = ↑g (AddMonoidAlgebra.single 0 b)) (h_of : ∀ (a : G), ↑f (AddMonoidAlgebra.single a 1) = ↑g (AddMonoidAlgebra.single a 1)) : f = g

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

theorem AddMonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [AddMonoid G] [Semiring R] {f : AddMonoidAlgebra k G →+* R} {g : AddMonoidAlgebra k G →+* R} (h₁ : RingHom.comp f AddMonoidAlgebra.singleZeroRingHom = RingHom.comp g AddMonoidAlgebra.singleZeroRingHom) (h_of : MonoidHom.comp (↑f) (AddMonoidAlgebra.of k G) = MonoidHom.comp (↑g) (AddMonoidAlgebra.of k G)) : f = g

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

See note [partially-applied ext lemmas].

@[simp]

theorem AddMonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] : ∀ (a : G →₀ kᵐᵒᵖ), ↑(RingEquiv.symm AddMonoidAlgebra.opRingEquiv) a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop (_ : MulOpposite.unop 0 = 0) a)

@[simp]

theorem AddMonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] : ∀ (a : (G →₀ k)ᵐᵒᵖ), ↑AddMonoidAlgebra.opRingEquiv a = Finsupp.mapRange MulOpposite.op (_ : ↑MulOpposite.opAddEquiv 0 = 0) (MulOpposite.unop a)

noncomputable def AddMonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] : (AddMonoidAlgebra k G)ᵐᵒᵖ ≃+* AddMonoidAlgebra kᵐᵒᵖ G

The opposite of an R[I] is ring equivalent to the AddMonoidAlgebra Rᵐᵒᵖ I over the opposite ring, taking elements to their opposite.

Equations

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

theorem AddMonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (r : k) (x : G) : ↑AddMonoidAlgebra.opRingEquiv (MulOpposite.op (AddMonoidAlgebra.single x r)) = AddMonoidAlgebra.single x (MulOpposite.op r)

theorem AddMonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) : ↑(RingEquiv.symm AddMonoidAlgebra.opRingEquiv) (AddMonoidAlgebra.single x r) = MulOpposite.op (AddMonoidAlgebra.single x (MulOpposite.unop r))

instance AddMonoidAlgebra.algebra {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : Algebra R (AddMonoidAlgebra k G)

The instance Algebra R k[G] whenever we have Algebra R k.

In particular this provides the instance Algebra k k[G].

Equations

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

@[simp]

theorem AddMonoidAlgebra.singleZeroAlgHom_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : ∀ (a : k), ↑AddMonoidAlgebra.singleZeroAlgHom a = fun₀ | 0 => a

def AddMonoidAlgebra.singleZeroAlgHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : k →ₐ[R] AddMonoidAlgebra k G

Finsupp.single 0 as an AlgHom

Equations

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

@[simp]

theorem AddMonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : ↑(algebraMap R (AddMonoidAlgebra k G)) = AddMonoidAlgebra.single 0 ∘ ↑(algebraMap R k)

def AddMonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] {B : Type u_3} [Semiring B] [Algebra k B] (f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm : ∀ (x : A) (y : Multiplicative G), Commute (↑f x) (↑g y)) : AddMonoidAlgebra A G →ₐ[k] B

liftNCRingHom as an AlgHom, for when f is an AlgHom

Equations

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

theorem AddMonoidAlgebra.algHom_ext {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : AddMonoidAlgebra k G →ₐ[k] A⦄ ⦃φ₂ : AddMonoidAlgebra k G →ₐ[k] A⦄ (h : ∀ (x : G), ↑φ₁ (AddMonoidAlgebra.single x 1) = ↑φ₂ (AddMonoidAlgebra.single x 1)) : φ₁ = φ₂

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

theorem AddMonoidAlgebra.algHom_ext' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : AddMonoidAlgebra k G →ₐ[k] A⦄ ⦃φ₂ : AddMonoidAlgebra k G →ₐ[k] A⦄ (h : MonoidHom.comp (↑φ₁) (AddMonoidAlgebra.of k G) = MonoidHom.comp (↑φ₂) (AddMonoidAlgebra.of k G)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

def AddMonoidAlgebra.lift (k : Type u₁) (G : Type u₂) [CommSemiring k] [AddMonoid G] (A : Type u₃) [Semiring A] [Algebra k A] : (Multiplicative G →* A) ≃ (AddMonoidAlgebra k G →ₐ[k] A)

Any monoid homomorphism G →* A can be lifted to an algebra homomorphism k[G] →ₐ[k] A.

Equations

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

theorem AddMonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (f : MonoidAlgebra k G) : ↑(↑(AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => ↑(algebraMap k A) b * ↑F (↑Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (f : MonoidAlgebra k G) : ↑(↑(AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => b • ↑F (↑Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) : ↑(↑(AddMonoidAlgebra.lift k G A) F) = ↑(AddMonoidAlgebra.liftNC ↑(algebraMap k A) ↑F)

@[simp]

theorem AddMonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) (x : Multiplicative G) : ↑(↑(AddMonoidAlgebra.lift k G A).symm F) x = ↑F (AddMonoidAlgebra.single (↑Multiplicative.toAdd x) 1)

theorem AddMonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (x : Multiplicative G) : ↑(↑(AddMonoidAlgebra.lift k G A) F) (↑(AddMonoidAlgebra.of k G) x) = ↑F x

@[simp]

theorem AddMonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (a : G) (b : k) : ↑(↑(AddMonoidAlgebra.lift k G A) F) (AddMonoidAlgebra.single a b) = b • ↑F (↑Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) : F = ↑(AddMonoidAlgebra.lift k G A) (MonoidHom.comp (↑F) (AddMonoidAlgebra.of k G))

theorem AddMonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) : ↑F f = Finsupp.sum f fun a b => b • ↑F (AddMonoidAlgebra.single a 1)

Decomposition of a k-algebra homomorphism from MonoidAlgebra k G by its values on F (single a 1).

theorem AddMonoidAlgebra.algHom_ext_iff {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] {φ₁ : AddMonoidAlgebra k G →ₐ[k] A} {φ₂ : AddMonoidAlgebra k G →ₐ[k] A} : (∀ (x : G), (↑φ₁ fun₀ | x => 1) = ↑φ₂ fun₀ | x => 1) ↔ φ₁ = φ₂

theorem AddMonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} : (Finset.prod s fun i => AddMonoidAlgebra.single (a i) (b i)) = AddMonoidAlgebra.single (Finset.sum s fun i => a i) (Finset.prod s fun i => b i)

theorem AddMonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} (A : Type u_3) {H : Type u_4} {F : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] [AddMonoid H] [AddMonoidHomClass F G H] (f : F) (r : k) : AddMonoidAlgebra.mapDomain (↑f) (↑(algebraMap k (AddMonoidAlgebra A G)) r) = ↑(algebraMap k (AddMonoidAlgebra A H)) r

@[simp]

theorem AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [AddHomClass F G H] (f : F) : ∀ (a : G →₀ A), ↑(AddMonoidAlgebra.mapDomainNonUnitalAlgHom k A f) a = ZeroHom.toFun (↑(Finsupp.mapDomain.addMonoidHom ↑f)) a

def AddMonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [AddHomClass F G H] (f : F) : AddMonoidAlgebra A G →ₙₐ[k] AddMonoidAlgebra A H

If f : G → H is a homomorphism between two additive magmas, then Finsupp.mapDomain f is a non-unital algebra homomorphism between their additive magma algebras.

Equations

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

@[simp]

theorem AddMonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] {H : Type u_5} {F : Type u_6} [AddMonoid H] [AddMonoidHomClass F G H] (f : F) : ∀ (a : G →₀ A), ↑(AddMonoidAlgebra.mapDomainAlgHom k A f) a = Finsupp.mapDomain (↑f) a

def AddMonoidAlgebra.mapDomainAlgHom {G : Type u₂} (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] {H : Type u_5} {F : Type u_6} [AddMonoid H] [AddMonoidHomClass F G H] (f : F) : AddMonoidAlgebra A G →ₐ[k] AddMonoidAlgebra A H

If f : G → H is an additive homomorphism between two additive monoids, then Finsupp.mapDomain f is an algebra homomorphism between their add monoid algebras.

Equations

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

def AddMonoidAlgebra.domCongr (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) : AddMonoidAlgebra A G ≃ₐ[k] AddMonoidAlgebra A H

If e : G ≃* H is a multiplicative equivalence between two monoids, then AddMonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.

Equations

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

theorem AddMonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) : ↑(AddMonoidAlgebra.domCongr k A e) = AddMonoidAlgebra.mapDomainAlgHom k A e

@[simp]

theorem AddMonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (f : MonoidAlgebra A G) (h : H) : ↑(↑(AddMonoidAlgebra.domCongr k A e) f) h = ↑f (↑(AddEquiv.symm e) h)

@[simp]

theorem AddMonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (f : MonoidAlgebra A G) : (↑(AddMonoidAlgebra.domCongr k A e) f).support = Finset.map (Equiv.toEmbedding ↑e) f.support

@[simp]

theorem AddMonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (g : G) (a : A) : ↑(AddMonoidAlgebra.domCongr k A e) (AddMonoidAlgebra.single g a) = AddMonoidAlgebra.single (↑e g) a

@[simp]

theorem AddMonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} (A : Type u_3) [CommSemiring k] [AddMonoid G] [Semiring A] [Algebra k A] : AddMonoidAlgebra.domCongr k A (AddEquiv.refl G) = AlgEquiv.refl

@[simp]

theorem AddMonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) : AlgEquiv.symm (AddMonoidAlgebra.domCongr k A e) = AddMonoidAlgebra.domCongr k A (AddEquiv.symm e)

def AddMonoidAlgebra.toMultiplicativeAlgEquiv (k : Type u₁) (G : Type u₂) {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : AddMonoidAlgebra k G ≃ₐ[R] MonoidAlgebra k (Multiplicative G)

The algebra equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative.

Equations

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

def MonoidAlgebra.toAdditiveAlgEquiv (k : Type u₁) (G : Type u₂) {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [Monoid G] : MonoidAlgebra k G ≃ₐ[R] AddMonoidAlgebra k (Additive G)

The algebra equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive.

Equations

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