MonoidAlgebra.mapDomain

Multiplicative monoids

@[reducible, inline]

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} : mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : G) (b : k') => mapDomain f (v a b)

@[simp]

theorem MonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [One α] [One α₂] {F : Type u_6} [FunLike F α α₂] [OneHomClass F α α₂] (f : F) : 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} [FunLike F α α₂] [MulHomClass F α α₂] (f : F) (x y : MonoidAlgebra β α) : mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

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

def MonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [Semiring k] [Monoid G] [Monoid H] [FunLike F G 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

• MonoidAlgebra.mapDomainRingHom k f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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] [FunLike F G H] [MonoidHomClass F G H] (f : F) (a✝ : G →₀ k) : (mapDomainRingHom k f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝

Additive monoids

@[reducible, inline]

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} : mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : G) (b : k') => 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} : mapDomain f (single a b) = single (f a) b

@[simp]

theorem AddMonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [Zero α] [Zero α₂] {F : Type u_6} [FunLike F α α₂] [ZeroHomClass F α α₂] (f : F) : 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} [FunLike F α α₂] [AddHomClass F α α₂] (f : F) (x y : AddMonoidAlgebra β α) : mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

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

def AddMonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) [Semiring k] {H : Type u_4} {F : Type u_5} [AddMonoid G] [AddMonoid H] [FunLike F G 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

• AddMonoidAlgebra.mapDomainRingHom k f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) (a✝ : G →₀ k) : (mapDomainRingHom k f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝

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.