Maps of monoid algebras

This file defines maps of monoid algebras along both the ring and monoid arguments.

Multiplicative monoids

@[reducible, inline]

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

Given a function f : M → N between magmas, return the corresponding map R[M] → R[N] obtained by summing the coefficients along each fiber of f.

@[reducible, inline]

abbrev AddMonoidAlgebra.mapDomain {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] (f : M → N) (x : AddMonoidAlgebra R M) : AddMonoidAlgebra R N

Given a function f : M → N between magmas, return the corresponding map R[M] → R[N] obtained by summing the coefficients along each fiber of f.

theorem MonoidAlgebra.mapDomain_zero {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] (f : M → N) : mapDomain f 0 = 0

theorem AddMonoidAlgebra.mapDomain_zero {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] (f : M → N) : mapDomain f 0 = 0

theorem MonoidAlgebra.mapDomain_add {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] (f : M → N) (x y : MonoidAlgebra R M) : mapDomain f (x + y) = mapDomain f x + mapDomain f y

theorem AddMonoidAlgebra.mapDomain_add {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] (f : M → N) (x y : AddMonoidAlgebra R M) : mapDomain f (x + y) = mapDomain f x + mapDomain f y

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

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

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

theorem AddMonoidAlgebra.mapDomain_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [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_5} {N : Type u_6} [Semiring R] {f : M → N} (hf : Function.Injective f) : Function.Injective (mapDomain f)

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

@[simp]

theorem MonoidAlgebra.mapDomain_one {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [One M] [One N] {F : Type u_8} [FunLike F M N] [OneHomClass F M N] (f : F) : mapDomain (⇑f) 1 = 1

@[simp]

theorem AddMonoidAlgebra.mapDomain_one {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Zero M] [Zero N] {F : Type u_8} [FunLike F M N] [ZeroHomClass F M N] (f : F) : mapDomain (⇑f) 1 = 1

theorem MonoidAlgebra.mapDomain_mul {F : Type u_1} {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (x y : MonoidAlgebra R M) : mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

theorem AddMonoidAlgebra.mapDomain_mul {F : Type u_1} {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (x y : AddMonoidAlgebra R M) : mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

def MonoidAlgebra.mapDomainNonUnitalRingHom (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Mul M] [Mul N] (f : M →ₙ* N) : MonoidAlgebra R M →ₙ+* MonoidAlgebra R N

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

See also MulEquiv.monoidAlgebraCongrRight.

def AddMonoidAlgebra.mapDomainNonUnitalRingHom (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Add M] [Add N] (f : M →ₙ+ N) : AddMonoidAlgebra R M →ₙ+* AddMonoidAlgebra R N

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

@[simp]

theorem AddMonoidAlgebra.mapDomainNonUnitalRingHom_apply (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Add M] [Add N] (f : M →ₙ+ N) (x : AddMonoidAlgebra R M) : (mapDomainNonUnitalRingHom R f) x = mapDomain (⇑f) x

@[simp]

theorem MonoidAlgebra.mapDomainNonUnitalRingHom_apply (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Mul M] [Mul N] (f : M →ₙ* N) (x : MonoidAlgebra R M) : (mapDomainNonUnitalRingHom R f) x = mapDomain (⇑f) x

@[simp]

theorem MonoidAlgebra.mapDomainNonUnitalRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [Mul M] : mapDomainNonUnitalRingHom R (MulHom.id M) = NonUnitalRingHom.id (MonoidAlgebra R M)

@[simp]

theorem AddMonoidAlgebra.mapDomainNonUnitalRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [Add M] : mapDomainNonUnitalRingHom R (AddHom.id M) = NonUnitalRingHom.id (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.mapDomainNonUnitalRingHom_comp {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [Mul M] [Mul N] [Mul O] (f : N →ₙ* O) (g : M →ₙ* N) : mapDomainNonUnitalRingHom R (f.comp g) = (mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)

@[simp]

theorem AddMonoidAlgebra.mapDomainNonUnitalRingHom_comp {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [Add M] [Add N] [Add O] (f : N →ₙ+ O) (g : M →ₙ+ N) : mapDomainNonUnitalRingHom R (f.comp g) = (mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)

def MonoidAlgebra.mapDomainAddEquiv (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Mul M] [Mul N] (e : M ≃ N) : MonoidAlgebra R M ≃+ MonoidAlgebra R N

Equivalent monoids have additively isomorphic monoid algebras.

MonoidAlgebra.mapDomain as an AddEquiv.

def AddMonoidAlgebra.mapDomainAddEquiv (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Add M] [Add N] (e : M ≃ N) : AddMonoidAlgebra R M ≃+ AddMonoidAlgebra R N

Equivalent additive monoids have additively isomorphic additive monoid algebras.

AddMonoidAlgebra.mapDomain as an AddEquiv.

@[simp]

theorem MonoidAlgebra.mapDomainAddEquiv_apply {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Mul M] [Mul N] (e : M ≃ N) (x : MonoidAlgebra R M) (n : N) : ((mapDomainAddEquiv R e) x) n = x (e.symm n)

@[simp]

theorem AddMonoidAlgebra.mapDomainAddEquiv_apply {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Add M] [Add N] (e : M ≃ N) (x : AddMonoidAlgebra R M) (n : N) : ((mapDomainAddEquiv R e) x) n = x (e.symm n)

@[simp]

theorem MonoidAlgebra.mapDomainAddEquiv_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Mul M] [Mul N] (e : M ≃ N) (r : R) (m : M) : (mapDomainAddEquiv R e) (single m r) = single (e m) r

@[simp]

theorem AddMonoidAlgebra.mapDomainAddEquiv_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Add M] [Add N] (e : M ≃ N) (r : R) (m : M) : (mapDomainAddEquiv R e) (single m r) = single (e m) r

@[simp]

theorem MonoidAlgebra.symm_mapDomainAddEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Mul M] [Mul N] (e : M ≃ N) : (mapDomainAddEquiv R e).symm = mapDomainAddEquiv R e.symm

@[simp]

theorem AddMonoidAlgebra.symm_mapDomainAddEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Add M] [Add N] (e : M ≃ N) : (mapDomainAddEquiv R e).symm = mapDomainAddEquiv R e.symm

@[simp]

theorem MonoidAlgebra.mapDomainAddEquiv_trans {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [Mul M] [Mul N] [Mul O] (e₁ : M ≃ N) (e₂ : N ≃ O) : mapDomainAddEquiv R (e₁.trans e₂) = (mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)

@[simp]

theorem AddMonoidAlgebra.mapDomainAddEquiv_trans {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [Add M] [Add N] [Add O] (e₁ : M ≃ N) (e₂ : N ≃ O) : mapDomainAddEquiv R (e₁.trans e₂) = (mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)

def MonoidAlgebra.mapRangeAddEquiv {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) : MonoidAlgebra R M ≃+ MonoidAlgebra S M

Additively isomorphic rings have additively isomorphic monoid algebras.

Finsupp.mapRange as an AddEquiv.

def AddMonoidAlgebra.mapRangeAddEquiv {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) : AddMonoidAlgebra R M ≃+ AddMonoidAlgebra S M

Additively isomorphic rings have additively isomorphic additive monoid algebras.

Finsupp.mapRange as an AddEquiv.

@[simp]

theorem MonoidAlgebra.mapRangeAddEquiv_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) (x : MonoidAlgebra R M) (m : M) : ((mapRangeAddEquiv M e) x) m = e (x m)

@[simp]

theorem AddMonoidAlgebra.mapRangeAddEquiv_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) (x : AddMonoidAlgebra R M) (m : M) : ((mapRangeAddEquiv M e) x) m = e (x m)

@[simp]

theorem MonoidAlgebra.mapRangeAddEquiv_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) (r : R) (m : M) : (mapRangeAddEquiv M e) (single m r) = single m (e r)

@[simp]

theorem AddMonoidAlgebra.mapRangeAddEquiv_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) (r : R) (m : M) : (mapRangeAddEquiv M e) (single m r) = single m (e r)

@[simp]

theorem MonoidAlgebra.symm_mapRangeAddEquiv {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) : (mapRangeAddEquiv M e).symm = mapRangeAddEquiv M e.symm

@[simp]

theorem AddMonoidAlgebra.symm_mapRangeAddEquiv {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) : (mapRangeAddEquiv M e).symm = mapRangeAddEquiv M e.symm

@[simp]

theorem MonoidAlgebra.mapRangeAddEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [Mul M] (e₁ : R ≃+ S) (e₂ : S ≃+ T) : mapRangeAddEquiv M (e₁.trans e₂) = (mapRangeAddEquiv M e₁).trans (mapRangeAddEquiv M e₂)

@[simp]

theorem AddMonoidAlgebra.mapRangeAddEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [Add M] (e₁ : R ≃+ S) (e₂ : S ≃+ T) : mapRangeAddEquiv M (e₁.trans e₂) = (mapRangeAddEquiv M e₁).trans (mapRangeAddEquiv M e₂)

def MonoidAlgebra.mapDomainRingHom (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (f : M →* N) : MonoidAlgebra R M →+* MonoidAlgebra R N

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

def AddMonoidAlgebra.mapDomainRingHom (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (f : M →+ N) : AddMonoidAlgebra R M →+* AddMonoidAlgebra R N

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

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_apply (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (f : M →* N) (x : MonoidAlgebra R M) : (mapDomainRingHom R f) x = mapDomain (⇑f) x

@[simp]

theorem AddMonoidAlgebra.mapDomainRingHom_apply (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (f : M →+ N) (x : AddMonoidAlgebra R M) : (mapDomainRingHom R f) x = mapDomain (⇑f) x

theorem MonoidAlgebra.ringHom_ext_iff {R : Type u_1} {S : Type u_2} {M : Type u_4} [Semiring R] [MulOneClass M] [Semiring S] {f g : MonoidAlgebra R M →+* S} : f = g ↔ (∀ (r : R), f (single 1 r) = g (single 1 r)) ∧ ∀ (m : M), f (single m 1) = g (single m 1)

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [Monoid M] : mapDomainRingHom R (MonoidHom.id M) = RingHom.id (MonoidAlgebra R M)

@[simp]

theorem AddMonoidAlgebra.mapDomainRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [AddMonoid M] : mapDomainRingHom R (AddMonoidHom.id M) = RingHom.id (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_comp {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [Monoid M] [Monoid N] [Monoid O] (f : N →* O) (g : M →* N) : mapDomainRingHom R (f.comp g) = (mapDomainRingHom R f).comp (mapDomainRingHom R g)

@[simp]

theorem AddMonoidAlgebra.mapDomainRingHom_comp {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [AddMonoid M] [AddMonoid N] [AddMonoid O] (f : N →+ O) (g : M →+ N) : mapDomainRingHom R (f.comp g) = (mapDomainRingHom R f).comp (mapDomainRingHom R g)

noncomputable def MonoidAlgebra.mapRangeRingHom {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) : MonoidAlgebra R M →+* MonoidAlgebra S M

The ring homomorphism of monoid algebras induced by a homomorphism of the base rings.

noncomputable def AddMonoidAlgebra.mapRangeRingHom {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) : AddMonoidAlgebra R M →+* AddMonoidAlgebra S M

The ring homomorphism of additive monoid algebras induced by a homomorphism of the base rings.

theorem MonoidAlgebra.coe_mapRangeRingHom {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) : ⇑(mapRangeRingHom M f) = Finsupp.mapRange ⇑f ⋯

theorem AddMonoidAlgebra.coe_mapRangeRingHom {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) : ⇑(mapRangeRingHom M f) = Finsupp.mapRange ⇑f ⋯

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) (x : MonoidAlgebra R M) (m : M) : ((mapRangeRingHom M f) x) m = f (x m)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) (x : AddMonoidAlgebra R M) (m : M) : ((mapRangeRingHom M f) x) m = f (x m)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) (a : M) (b : R) : (mapRangeRingHom M f) (single a b) = single a (f b)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) (a : M) (b : R) : (mapRangeRingHom M f) (single a b) = single a (f b)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [Monoid M] : mapRangeRingHom M (RingHom.id R) = RingHom.id (MonoidAlgebra R M)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [AddMonoid M] : mapRangeRingHom M (RingHom.id R) = RingHom.id (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [Monoid M] (f : S →+* T) (g : R →+* S) : mapRangeRingHom M (f.comp g) = (mapRangeRingHom M f).comp (mapRangeRingHom M g)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [AddMonoid M] (f : S →+* T) (g : R →+* S) : mapRangeRingHom M (f.comp g) = (mapRangeRingHom M f).comp (mapRangeRingHom M g)

theorem MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom {R : Type u_2} {S : Type u_3} {M : Type u_5} {N : Type u_6} [Semiring R] [Semiring S] [Monoid M] [Monoid N] (f : R →+* S) (g : M →* N) : (mapRangeRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRangeRingHom M f)

theorem AddMonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom {R : Type u_2} {S : Type u_3} {M : Type u_5} {N : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] [AddMonoid N] (f : R →+* S) (g : M →+ N) : (mapRangeRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRangeRingHom M f)

def MonoidAlgebra.mapDomainRingEquiv (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (e : M ≃* N) : MonoidAlgebra R M ≃+* MonoidAlgebra R N

Isomorphic monoids have isomorphic monoid algebras.

def AddMonoidAlgebra.mapDomainRingEquiv (R : Type u_2) {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) : AddMonoidAlgebra R M ≃+* AddMonoidAlgebra R N

Isomorphic monoids have isomorphic additive monoid algebras.

@[simp]

theorem MonoidAlgebra.mapDomainRingEquiv_apply {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (e : M ≃* N) (x : MonoidAlgebra R M) (n : N) : ((mapDomainRingEquiv R e) x) n = x (e.symm n)

@[simp]

theorem AddMonoidAlgebra.mapDomainRingEquiv_apply {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (x : AddMonoidAlgebra R M) (n : N) : ((mapDomainRingEquiv R e) x) n = x (e.symm n)

@[simp]

theorem MonoidAlgebra.mapDomainRingEquiv_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (e : M ≃* N) (r : R) (m : M) : (mapDomainRingEquiv R e) (single m r) = single (e m) r

@[simp]

theorem AddMonoidAlgebra.mapDomainRingEquiv_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (r : R) (m : M) : (mapDomainRingEquiv R e) (single m r) = single (e m) r

theorem MonoidAlgebra.toRingHom_mapDomainRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (e : M ≃* N) : (mapDomainRingEquiv R e).toRingHom = mapDomainRingHom R ↑e

theorem AddMonoidAlgebra.toRingHom_mapDomainRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) : (mapDomainRingEquiv R e).toRingHom = mapDomainRingHom R ↑e

@[simp]

theorem MonoidAlgebra.symm_mapDomainRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (e : M ≃* N) : (mapDomainRingEquiv R e).symm = mapDomainRingEquiv R e.symm

@[simp]

theorem AddMonoidAlgebra.symm_mapDomainRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) : (mapDomainRingEquiv R e).symm = mapDomainRingEquiv R e.symm

@[simp]

theorem MonoidAlgebra.mapDomainRingEquiv_trans {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [Monoid M] [Monoid N] [Monoid O] (e₁ : M ≃* N) (e₂ : N ≃* O) : mapDomainRingEquiv R (e₁.trans e₂) = (mapDomainRingEquiv R e₁).trans (mapDomainRingEquiv R e₂)

@[simp]

theorem AddMonoidAlgebra.mapDomainRingEquiv_trans {R : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [Semiring R] [AddMonoid M] [AddMonoid N] [AddMonoid O] (e₁ : M ≃+ N) (e₂ : N ≃+ O) : mapDomainRingEquiv R (e₁.trans e₂) = (mapDomainRingEquiv R e₁).trans (mapDomainRingEquiv R e₂)

def MonoidAlgebra.mapRangeRingEquiv {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) : MonoidAlgebra R M ≃+* MonoidAlgebra S M

Isomorphic rings have isomorphic monoid algebras.

def AddMonoidAlgebra.mapRangeRingEquiv {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) : AddMonoidAlgebra R M ≃+* AddMonoidAlgebra S M

Isomorphic rings have isomorphic additive monoid algebras.

@[simp]

theorem MonoidAlgebra.mapRangeRingEquiv_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) (x : MonoidAlgebra R M) (m : M) : ((mapRangeRingEquiv M e) x) m = e (x m)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingEquiv_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) (x : AddMonoidAlgebra R M) (m : M) : ((mapRangeRingEquiv M e) x) m = e (x m)

@[simp]

theorem MonoidAlgebra.mapRangeRingEquiv_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) (r : R) (m : M) : (mapRangeRingEquiv M e) (single m r) = single m (e r)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingEquiv_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) (r : R) (m : M) : (mapRangeRingEquiv M e) (single m r) = single m (e r)

theorem MonoidAlgebra.toRingHom_mapRangeRingEquiv {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) : (mapRangeRingEquiv M e).toRingHom = mapRangeRingHom M ↑e

theorem AddMonoidAlgebra.toRingHom_mapRangeRingEquiv {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) : (mapRangeRingEquiv M e).toRingHom = mapRangeRingHom M ↑e

@[simp]

theorem MonoidAlgebra.symm_mapRangeRingEquiv {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) : (mapRangeRingEquiv M e).symm = mapRangeRingEquiv M e.symm

@[simp]

theorem AddMonoidAlgebra.symm_mapRangeRingEquiv {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) : (mapRangeRingEquiv M e).symm = mapRangeRingEquiv M e.symm

@[simp]

theorem MonoidAlgebra.mapRangeRingEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [Monoid M] (e₁ : R ≃+* S) (e₂ : S ≃+* T) : mapRangeRingEquiv M (e₁.trans e₂) = (mapRangeRingEquiv M e₁).trans (mapRangeRingEquiv M e₂)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [AddMonoid M] (e₁ : R ≃+* S) (e₂ : S ≃+* T) : mapRangeRingEquiv M (e₁.trans e₂) = (mapRangeRingEquiv M e₁).trans (mapRangeRingEquiv M e₂)

def MonoidAlgebra.commRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] : MonoidAlgebra (MonoidAlgebra R M) N ≃+* MonoidAlgebra (MonoidAlgebra R N) M

Nested monoid algebras can be taken in an arbitrary order.

def AddMonoidAlgebra.commRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] : AddMonoidAlgebra (AddMonoidAlgebra R M) N ≃+* AddMonoidAlgebra (AddMonoidAlgebra R N) M

Nested additive monoid algebras can be taken in an arbitrary order.

@[simp]

theorem MonoidAlgebra.symm_commRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] : commRingEquiv.symm = commRingEquiv

@[simp]

theorem AddMonoidAlgebra.symm_commRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] : commRingEquiv.symm = commRingEquiv

@[simp]

theorem MonoidAlgebra.commRingEquiv_single_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] (m : M) (n : N) (r : R) : commRingEquiv (single m (single n r)) = single n (single m r)

@[simp]

theorem AddMonoidAlgebra.commRingEquiv_single_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] (m : M) (n : N) (r : R) : commRingEquiv (single m (single n r)) = single n (single m r)

Conversions between AddMonoidAlgebra and MonoidAlgebra

We have not defined AddMonoidAlgebra 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_8) (G : Type u_9) [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_8) (G : Type u_9) [Semiring k] [Mul G] : MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G)

The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive