MonoidAlgebra.mapDomain

Multiplicative monoids

@[reducible, inline]

abbrev MonoidAlgebra.mapDomain {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (v : MonoidAlgebra R M) : MonoidAlgebra R N

theorem MonoidAlgebra.mapDomain_sum {R : Type u_2} {S : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] [Semiring S] (f : M → N) (s : MonoidAlgebra S M) (v : M → S → MonoidAlgebra R M) : mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : M) (b : S) => mapDomain f (v a b)

theorem MonoidAlgebra.mapDomain_single {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} {a : M} {r : R} : mapDomain f (single a r) = single (f a) r

theorem MonoidAlgebra.mapDomain_injective {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} (hf : Function.Injective f) : Function.Injective (mapDomain f)

@[simp]

theorem MonoidAlgebra.mapDomain_one {α : Type u_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [One α] [One α₂] {F : Type u_11} [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_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [Mul α] [Mul α₂] {F : Type u_11} [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_4} (k : Type u_8) {H : Type u_9} {F : Type u_10} [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.

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_apply {G : Type u_4} (k : Type u_8) {H : Type u_9} {F : Type u_10} [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 {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (v : AddMonoidAlgebra R M) : AddMonoidAlgebra R N

theorem AddMonoidAlgebra.mapDomain_sum {R : Type u_2} {S : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] [Semiring S] (f : M → N) (s : AddMonoidAlgebra S M) (v : M → S → AddMonoidAlgebra R M) : mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : M) (b : S) => mapDomain f (v a b)

theorem AddMonoidAlgebra.mapDomain_single {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} {a : M} {r : R} : mapDomain f (single a r) = single (f a) r

theorem AddMonoidAlgebra.mapDomain_injective {R : Type u_2} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} (hf : Function.Injective f) : Function.Injective (mapDomain f)

@[simp]

theorem AddMonoidAlgebra.mapDomain_one {α : Type u_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [Zero α] [Zero α₂] {F : Type u_11} [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_8} {β : Type u_9} {α₂ : Type u_10} [Semiring β] [Add α] [Add α₂] {F : Type u_11} [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_4} (k : Type u_8) [Semiring k] {H : Type u_9} {F : Type u_10} [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.

@[simp]

theorem AddMonoidAlgebra.mapDomainRingHom_apply {G : Type u_4} (k : Type u_8) [Semiring k] {H : Type u_9} {F : Type u_10} [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_1) (G : Type u_4) [Semiring k] [Add G] : AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G)

The equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative

def MonoidAlgebra.toAdditive (k : Type u_1) (G : Type u_4) [Semiring k] [Mul G] : MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G)

The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive