Maps of monoid algebras

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

@[reducible, inline]

noncomputable abbrev MonoidAlgebra.mapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [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.

Equations

• MonoidAlgebra.mapDomain f x = Finsupp.mapDomain f x

@[reducible, inline]

noncomputable abbrev AddMonoidAlgebra.mapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [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.

Equations

• AddMonoidAlgebra.mapDomain f x = Finsupp.mapDomain f x

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

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

theorem MonoidAlgebra.mapDomain_add {R : Type u_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [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_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [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_3} {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_single {R : Type u_3} {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_3} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} (hf : Function.Injective f) : Function.Injective (mapDomain f)

theorem AddMonoidAlgebra.mapDomain_injective {R : Type u_3} {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 {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] [One M] [One N] {F : Type u_9} [FunLike F M N] [OneHomClass F M N] (f : F) : mapDomain (⇑f) 1 = 1

@[simp]

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

noncomputable def MonoidAlgebra.map {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x : MonoidAlgebra R M) : MonoidAlgebra S M

Given a map f : R →+ S, return the corresponding map R[M] → S[M] obtained by mapping each coefficient along f.

Equations

• MonoidAlgebra.map f x = MonoidAlgebra.ofCoeff (Finsupp.mapRange ⇑f ⋯ x.coeff)

noncomputable def AddMonoidAlgebra.map {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x : AddMonoidAlgebra R M) : AddMonoidAlgebra S M

Given a map f : R →+ S, return the corresponding map R[M] → S[M] obtained by mapping each coefficient along f.

Equations

• AddMonoidAlgebra.map f x = AddMonoidAlgebra.ofCoeff (Finsupp.mapRange ⇑f ⋯ x.coeff)

@[simp]

theorem MonoidAlgebra.coeff_map {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x : MonoidAlgebra R M) : (map f x).coeff = Finsupp.mapRange ⇑f ⋯ x.coeff

@[simp]

theorem AddMonoidAlgebra.coeff_map {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x : AddMonoidAlgebra R M) : (map f x).coeff = Finsupp.mapRange ⇑f ⋯ x.coeff

theorem MonoidAlgebra.ofCoeff_mapRange {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x : M →₀ R) : ofCoeff (Finsupp.mapRange ⇑f ⋯ x) = map f (ofCoeff x)

This isn't marked as simp to avoid looping with unfolding coeff.

theorem AddMonoidAlgebra.ofCoeff_mapRange {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x : M →₀ R) : ofCoeff (Finsupp.mapRange ⇑f ⋯ x) = map f (ofCoeff x)

This isn't marked as simp to avoid looping with unfolding coeff.

@[simp]

theorem MonoidAlgebra.map_zero {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) : map f 0 = 0

@[simp]

theorem AddMonoidAlgebra.map_zero {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) : map f 0 = 0

theorem MonoidAlgebra.map_add {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x y : MonoidAlgebra R M) : map f (x + y) = map f x + map f y

theorem AddMonoidAlgebra.map_add {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (x y : AddMonoidAlgebra R M) : map f (x + y) = map f x + map f y

theorem MonoidAlgebra.map_sum {ι : Type u_1} {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (s : Finset ι) (x : ι → MonoidAlgebra R M) : map f (∑ i ∈ s, x i) = ∑ i ∈ s, map f (x i)

theorem AddMonoidAlgebra.map_sum {ι : Type u_1} {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (s : Finset ι) (x : ι → AddMonoidAlgebra R M) : map f (∑ i ∈ s, x i) = ∑ i ∈ s, map f (x i)

@[simp]

theorem MonoidAlgebra.map_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (r : R) (m : M) : map f (single m r) = single m (f r)

@[simp]

theorem AddMonoidAlgebra.map_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] (f : R →+ S) (r : R) (m : M) : map f (single m r) = single m (f r)

@[simp]

theorem MonoidAlgebra.map_id {R : Type u_3} {M : Type u_6} [Semiring R] (x : MonoidAlgebra R M) : map (AddMonoidHom.id R) x = x

@[simp]

theorem AddMonoidAlgebra.map_id {R : Type u_3} {M : Type u_6} [Semiring R] (x : AddMonoidAlgebra R M) : map (AddMonoidHom.id R) x = x

@[simp]

theorem MonoidAlgebra.map_map {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [Semiring R] [Semiring S] [Semiring T] (f : S →+ T) (g : R →+ S) (x : MonoidAlgebra R M) : map f (map g x) = map (f.comp g) x

@[simp]

theorem AddMonoidAlgebra.map_map {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [Semiring R] [Semiring S] [Semiring T] (f : S →+ T) (g : R →+ S) (x : AddMonoidAlgebra R M) : map f (map g x) = map (f.comp g) x

noncomputable def MonoidAlgebra.comapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x : MonoidAlgebra R N) : MonoidAlgebra R M

Pullback the coefficients of an element of R[N] under an injective f : M → N.

Coefficients not in the range of f are dropped.

Equations

• MonoidAlgebra.comapDomain f hf x = MonoidAlgebra.ofCoeff (Finsupp.comapDomain f x.coeff ⋯)

noncomputable def AddMonoidAlgebra.comapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x : AddMonoidAlgebra R N) : AddMonoidAlgebra R M

Pullback the coefficients of an element of R[N] under an injective f : M → N.

Coefficients not in the range of f are dropped.

Equations

• AddMonoidAlgebra.comapDomain f hf x = AddMonoidAlgebra.ofCoeff (Finsupp.comapDomain f x.coeff ⋯)

@[simp]

theorem MonoidAlgebra.coeff_comapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x : MonoidAlgebra R N) : (comapDomain f hf x).coeff = Finsupp.comapDomain f x.coeff ⋯

@[simp]

theorem AddMonoidAlgebra.coeff_comapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x : AddMonoidAlgebra R N) : (comapDomain f hf x).coeff = Finsupp.comapDomain f x.coeff ⋯

@[simp]

theorem MonoidAlgebra.comapDomain_zero {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) : comapDomain f hf 0 = 0

@[simp]

theorem AddMonoidAlgebra.comapDomain_zero {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) : comapDomain f hf 0 = 0

@[simp]

theorem MonoidAlgebra.comapDomain_add {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x y : MonoidAlgebra R N) : comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

@[simp]

theorem AddMonoidAlgebra.comapDomain_add {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x y : AddMonoidAlgebra R N) : comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

@[simp]

theorem MonoidAlgebra.comapDomain_single_of_not_mem_range {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} {r : R} {n : N} (hn : n ∉ Set.range f) (hf : Function.Injective f) : comapDomain f hf (single n r) = 0

noncomputable def MonoidAlgebra.comapDomainAddMonoidHom {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) : MonoidAlgebra R N →+ MonoidAlgebra R M

comapDomain as an `AddMonoidHom.

Equations

• MonoidAlgebra.comapDomainAddMonoidHom f hf = { toFun := MonoidAlgebra.comapDomain f hf, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def AddMonoidAlgebra.comapDomainAddMonoidHom {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) : AddMonoidAlgebra R N →+ AddMonoidAlgebra R M

comapDomain as an `AddMonoidHom.

Equations

• AddMonoidAlgebra.comapDomainAddMonoidHom f hf = { toFun := AddMonoidAlgebra.comapDomain f hf, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.comapDomainAddMonoidHom_apply {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x : AddMonoidAlgebra R N) : (comapDomainAddMonoidHom f hf) x = comapDomain f hf x

@[simp]

theorem MonoidAlgebra.comapDomainAddMonoidHom_apply {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (x : MonoidAlgebra R N) : (comapDomainAddMonoidHom f hf) x = comapDomain f hf x

@[simp]

theorem MonoidAlgebra.comapDomain_single_map {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (m : M) (r : R) : comapDomain f hf (single (f m) r) = single m r

@[simp]

theorem AddMonoidAlgebra.comapDomain_single_map {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] (f : M → N) (hf : Function.Injective f) (m : M) (r : R) : comapDomain f hf (single (f m) r) = single m r

theorem MonoidAlgebra.mapDomain_comapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} {x : MonoidAlgebra R N} (hx : ↑x.coeff.support ⊆ Set.range f) (hf : Function.Injective f) : mapDomain f (comapDomain f hf x) = x

theorem AddMonoidAlgebra.mapDomain_comapDomain {R : Type u_3} {M : Type u_6} {N : Type u_7} [Semiring R] {f : M → N} {x : AddMonoidAlgebra R N} (hx : ↑x.coeff.support ⊆ Set.range f) (hf : Function.Injective f) : mapDomain f (comapDomain f hf x) = x

theorem MonoidAlgebra.mapDomain_mul {F : Type u_2} {R : Type u_3} {M : Type u_6} {N : Type u_7} [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_2} {R : Type u_3} {M : Type u_6} {N : Type u_7} [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

noncomputable def MonoidAlgebra.mapDomainNonUnitalRingHom (R : Type u_3) {M : Type u_6} {N : Type u_7} [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.

Equations

• MonoidAlgebra.mapDomainNonUnitalRingHom R f = { toFun := MonoidAlgebra.mapDomain ⇑f, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def AddMonoidAlgebra.mapDomainNonUnitalRingHom (R : Type u_3) {M : Type u_6} {N : Type u_7} [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.

Equations

• AddMonoidAlgebra.mapDomainNonUnitalRingHom R f = { toFun := AddMonoidAlgebra.mapDomain ⇑f, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.mapDomainNonUnitalRingHom_apply (R : Type u_3) {M : Type u_6} {N : Type u_7} [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_3) {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} [Semiring R] [Mul M] : mapDomainNonUnitalRingHom R (MulHom.id M) = NonUnitalRingHom.id (MonoidAlgebra R M)

@[simp]

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

@[simp]

theorem MonoidAlgebra.mapDomainNonUnitalRingHom_comp {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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)

noncomputable def MonoidAlgebra.mapDomainAddEquiv (R : Type u_3) {M : Type u_6} {N : Type u_7} [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.

Equations

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

noncomputable def AddMonoidAlgebra.mapDomainAddEquiv (R : Type u_3) {M : Type u_6} {N : Type u_7} [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.

Equations

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

@[simp]

theorem MonoidAlgebra.mapDomainAddEquiv_apply {R : Type u_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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₂)

noncomputable def MonoidAlgebra.mapAddEquiv {R : Type u_3} {S : Type u_4} (M : Type u_6) [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) : MonoidAlgebra R M ≃+ MonoidAlgebra S M

Additively isomorphic rings have additively isomorphic monoid algebras.

MonoidAlgebra.map as an AddEquiv.

Equations

• MonoidAlgebra.mapAddEquiv M e = { toFun := MonoidAlgebra.map ↑e, invFun := MonoidAlgebra.map ↑e.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

noncomputable def AddMonoidAlgebra.mapAddEquiv {R : Type u_3} {S : Type u_4} (M : Type u_6) [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) : AddMonoidAlgebra R M ≃+ AddMonoidAlgebra S M

Additively isomorphic rings have additively isomorphic additive monoid algebras.

AddMonoidAlgebra.map as an AddEquiv.

Equations

• AddMonoidAlgebra.mapAddEquiv M e = { toFun := AddMonoidAlgebra.map ↑e, invFun := AddMonoidAlgebra.map ↑e.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[deprecated MonoidAlgebra.mapAddEquiv (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapAddEquiv.

---

Additively isomorphic rings have additively isomorphic monoid algebras.

MonoidAlgebra.map as an AddEquiv.

Equations

• @MonoidAlgebra.mapRangeAddEquiv = @MonoidAlgebra.mapAddEquiv

@[simp]

theorem MonoidAlgebra.mapAddEquiv_apply {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) (x : MonoidAlgebra R M) (m : M) : ((mapAddEquiv M e) x) m = e (x m)

@[simp]

theorem AddMonoidAlgebra.mapAddEquiv_apply {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) (x : AddMonoidAlgebra R M) (m : M) : ((mapAddEquiv M e) x) m = e (x m)

@[deprecated MonoidAlgebra.mapAddEquiv_apply (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapAddEquiv_apply.

@[simp]

theorem MonoidAlgebra.mapAddEquiv_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) (r : R) (m : M) : (mapAddEquiv M e) (single m r) = single m (e r)

@[simp]

theorem AddMonoidAlgebra.mapAddEquiv_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) (r : R) (m : M) : (mapAddEquiv M e) (single m r) = single m (e r)

@[deprecated MonoidAlgebra.mapAddEquiv_single (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapAddEquiv_single.

@[simp]

theorem MonoidAlgebra.symm_mapAddEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) : (mapAddEquiv M e).symm = mapAddEquiv M e.symm

@[simp]

theorem AddMonoidAlgebra.symm_mapAddEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Add M] (e : R ≃+ S) : (mapAddEquiv M e).symm = mapAddEquiv M e.symm

@[deprecated MonoidAlgebra.symm_mapAddEquiv (since := "2026-03-20")]

theorem MonoidAlgebra.symm_mapRangeAddEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Mul M] (e : R ≃+ S) : (mapAddEquiv M e).symm = mapAddEquiv M e.symm

Alias of MonoidAlgebra.symm_mapAddEquiv.

@[simp]

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

@[simp]

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

@[deprecated MonoidAlgebra.mapAddEquiv_trans (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapAddEquiv_trans.

@[simp]

theorem MonoidAlgebra.map_mul {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Mul M] (f : R →+* S) (x y : MonoidAlgebra R M) : map (↑f) (x * y) = map (↑f) x * map (↑f) y

@[simp]

theorem AddMonoidAlgebra.map_mul {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Add M] (f : R →+* S) (x y : AddMonoidAlgebra R M) : map (↑f) (x * y) = map (↑f) x * map (↑f) y

noncomputable def MonoidAlgebra.mapDomainRingHom (R : Type u_3) {M : Type u_6} {N : Type u_7} [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.

Equations

• MonoidAlgebra.mapDomainRingHom R f = { toFun := MonoidAlgebra.mapDomain ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def AddMonoidAlgebra.mapDomainRingHom (R : Type u_3) {M : Type u_6} {N : Type u_7} [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.

Equations

• AddMonoidAlgebra.mapDomainRingHom R f = { toFun := AddMonoidAlgebra.mapDomain ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_apply (R : Type u_3) {M : Type u_6} {N : Type u_7} [Semiring R] [Monoid M] [Monoid N] (f : M →* N) (x : MonoidAlgebra 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_3} {M : Type u_6} [Semiring R] [Monoid M] : mapDomainRingHom R (MonoidHom.id M) = RingHom.id (MonoidAlgebra R M)

@[simp]

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

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_comp {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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)

@[simp]

theorem MonoidAlgebra.map_one {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) : map (↑f) 1 = 1

@[simp]

theorem AddMonoidAlgebra.map_one {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) : map (↑f) 1 = 1

noncomputable def MonoidAlgebra.mapRingHom {R : Type u_3} {S : Type u_4} (M : Type u_6) [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.

Equations

• MonoidAlgebra.mapRingHom M f = { toFun := MonoidAlgebra.map ↑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def AddMonoidAlgebra.mapRingHom {R : Type u_3} {S : Type u_4} (M : Type u_6) [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.

Equations

• AddMonoidAlgebra.mapRingHom M f = { toFun := AddMonoidAlgebra.map ↑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[deprecated MonoidAlgebra.mapRingHom (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingHom.

---

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

Equations

• @MonoidAlgebra.mapRangeRingHom = @MonoidAlgebra.mapRingHom

theorem MonoidAlgebra.coe_mapRingHom {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) : ⇑(mapRingHom M f) = map ↑f

theorem AddMonoidAlgebra.coe_mapRingHom {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) : ⇑(mapRingHom M f) = map ↑f

@[deprecated MonoidAlgebra.coe_mapRingHom (since := "2026-03-20")]

theorem MonoidAlgebra.coe_mapRangeRingHom {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) : ⇑(mapRingHom M f) = map ↑f

Alias of MonoidAlgebra.coe_mapRingHom.

@[simp]

theorem MonoidAlgebra.mapRingHom_apply {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) (x : MonoidAlgebra R M) (m : M) : ((mapRingHom M f) x) m = f (x m)

@[simp]

theorem AddMonoidAlgebra.mapRingHom_apply {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) (x : AddMonoidAlgebra R M) (m : M) : ((mapRingHom M f) x) m = f (x m)

@[deprecated MonoidAlgebra.mapRingHom_apply (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingHom_apply.

@[simp]

theorem MonoidAlgebra.mapRingHom_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) (a : M) (b : R) : (mapRingHom M f) (single a b) = single a (f b)

@[simp]

theorem AddMonoidAlgebra.mapRingHom_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) (a : M) (b : R) : (mapRingHom M f) (single a b) = single a (f b)

@[deprecated MonoidAlgebra.mapRingHom_single (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingHom_single.

@[simp]

theorem MonoidAlgebra.mapRingHom_id {R : Type u_3} {M : Type u_6} [Semiring R] [Monoid M] : mapRingHom M (RingHom.id R) = RingHom.id (MonoidAlgebra R M)

@[simp]

theorem AddMonoidAlgebra.mapRingHom_id {R : Type u_3} {M : Type u_6} [Semiring R] [AddMonoid M] : mapRingHom M (RingHom.id R) = RingHom.id (AddMonoidAlgebra R M)

@[deprecated MonoidAlgebra.mapRingHom_id (since := "2026-03-20")]

theorem MonoidAlgebra.mapRangeRingHom_id {R : Type u_3} {M : Type u_6} [Semiring R] [Monoid M] : mapRingHom M (RingHom.id R) = RingHom.id (MonoidAlgebra R M)

Alias of MonoidAlgebra.mapRingHom_id.

@[simp]

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

@[simp]

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

@[deprecated MonoidAlgebra.mapRingHom_comp (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingHom_comp.

theorem MonoidAlgebra.mapRingHom_comp_mapDomainRingHom {R : Type u_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [Semiring R] [Semiring S] [Monoid M] [Monoid N] (f : R →+* S) (g : M →* N) : (mapRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRingHom M f)

theorem AddMonoidAlgebra.mapRingHom_comp_mapDomainRingHom {R : Type u_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [Semiring R] [Semiring S] [AddMonoid M] [AddMonoid N] (f : R →+* S) (g : M →+ N) : (mapRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRingHom M f)

@[deprecated MonoidAlgebra.mapRingHom_comp_mapDomainRingHom (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingHom_comp_mapDomainRingHom.

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

Isomorphic monoids have isomorphic monoid algebras.

Equations

• MonoidAlgebra.mapDomainRingEquiv R e = RingEquiv.ofRingHom (MonoidAlgebra.mapDomainRingHom R ↑e) (MonoidAlgebra.mapDomainRingHom R ↑e.symm) ⋯ ⋯

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

Isomorphic monoids have isomorphic additive monoid algebras.

Equations

• AddMonoidAlgebra.mapDomainRingEquiv R e = RingEquiv.ofRingHom (AddMonoidAlgebra.mapDomainRingHom R ↑e) (AddMonoidAlgebra.mapDomainRingHom R ↑e.symm) ⋯ ⋯

@[simp]

theorem MonoidAlgebra.mapDomainRingEquiv_apply {R : Type u_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [Semiring R] [Monoid M] [Monoid N] (e : M ≃* N) : (mapDomainRingEquiv R e).toRingHom = mapDomainRingHom R ↑e

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

@[simp]

theorem MonoidAlgebra.symm_mapDomainRingEquiv {R : Type u_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [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₂)

noncomputable def MonoidAlgebra.mapRingEquiv {R : Type u_3} {S : Type u_4} (M : Type u_6) [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) : MonoidAlgebra R M ≃+* MonoidAlgebra S M

Isomorphic rings have isomorphic monoid algebras.

Equations

• MonoidAlgebra.mapRingEquiv M e = RingEquiv.ofRingHom (MonoidAlgebra.mapRingHom M ↑e) (MonoidAlgebra.mapRingHom M ↑e.symm) ⋯ ⋯

noncomputable def AddMonoidAlgebra.mapRingEquiv {R : Type u_3} {S : Type u_4} (M : Type u_6) [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) : AddMonoidAlgebra R M ≃+* AddMonoidAlgebra S M

Isomorphic rings have isomorphic additive monoid algebras.

Equations

• AddMonoidAlgebra.mapRingEquiv M e = RingEquiv.ofRingHom (AddMonoidAlgebra.mapRingHom M ↑e) (AddMonoidAlgebra.mapRingHom M ↑e.symm) ⋯ ⋯

@[deprecated MonoidAlgebra.mapRingEquiv (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingEquiv.

---

Isomorphic rings have isomorphic monoid algebras.

Equations

• @MonoidAlgebra.mapRangeRingEquiv = @MonoidAlgebra.mapRingEquiv

@[simp]

theorem MonoidAlgebra.mapRingEquiv_apply {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) (x : MonoidAlgebra R M) (m : M) : ((mapRingEquiv M e) x) m = e (x m)

@[simp]

theorem AddMonoidAlgebra.mapRingEquiv_apply {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) (x : AddMonoidAlgebra R M) (m : M) : ((mapRingEquiv M e) x) m = e (x m)

@[deprecated MonoidAlgebra.mapRingEquiv_apply (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingEquiv_apply.

@[simp]

theorem MonoidAlgebra.mapRingEquiv_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) (r : R) (m : M) : (mapRingEquiv M e) (single m r) = single m (e r)

@[simp]

theorem AddMonoidAlgebra.mapRingEquiv_single {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) (r : R) (m : M) : (mapRingEquiv M e) (single m r) = single m (e r)

@[deprecated MonoidAlgebra.mapRingEquiv_single (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingEquiv_single.

theorem MonoidAlgebra.toRingHom_mapRingEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) : (mapRingEquiv M e).toRingHom = mapRingHom M ↑e

theorem AddMonoidAlgebra.toRingHom_mapRingEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) : (mapRingEquiv M e).toRingHom = mapRingHom M ↑e

@[deprecated MonoidAlgebra.toRingHom_mapRingEquiv (since := "2026-03-20")]

theorem MonoidAlgebra.toRingHom_mapRangeRingEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) : (mapRingEquiv M e).toRingHom = mapRingHom M ↑e

Alias of MonoidAlgebra.toRingHom_mapRingEquiv.

@[simp]

theorem MonoidAlgebra.symm_mapRingEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [Monoid M] (e : R ≃+* S) : (mapRingEquiv M e).symm = mapRingEquiv M e.symm

@[simp]

theorem AddMonoidAlgebra.symm_mapRingEquiv {R : Type u_3} {S : Type u_4} {M : Type u_6} [Semiring R] [Semiring S] [AddMonoid M] (e : R ≃+* S) : (mapRingEquiv M e).symm = mapRingEquiv M e.symm

@[deprecated MonoidAlgebra.symm_mapRingEquiv (since := "2026-03-20")]

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

Alias of MonoidAlgebra.symm_mapRingEquiv.

@[simp]

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

@[simp]

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

@[deprecated MonoidAlgebra.mapRingEquiv_trans (since := "2026-03-20")]

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

Alias of MonoidAlgebra.mapRingEquiv_trans.

noncomputable def MonoidAlgebra.commRingEquiv {R : Type u_3} {M : Type u_6} {N : Type u_7} [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.

Equations

• MonoidAlgebra.commRingEquiv = MonoidAlgebra.curryRingEquiv.symm.trans ((MonoidAlgebra.mapDomainRingEquiv R MulEquiv.prodComm).trans MonoidAlgebra.curryRingEquiv)

noncomputable def AddMonoidAlgebra.commRingEquiv {R : Type u_3} {M : Type u_6} {N : Type u_7} [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.

Equations

• AddMonoidAlgebra.commRingEquiv = AddMonoidAlgebra.curryRingEquiv.symm.trans ((AddMonoidAlgebra.mapDomainRingEquiv R AddEquiv.prodComm).trans AddMonoidAlgebra.curryRingEquiv)

@[simp]

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

@[simp]

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

@[simp]

theorem MonoidAlgebra.commRingEquiv_single_single {R : Type u_3} {M : Type u_6} {N : Type u_7} [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_3} {M : Type u_6} {N : Type u_7} [Semiring R] [AddMonoid M] [AddMonoid N] (m : M) (n : N) (r : R) : commRingEquiv (single m (single n r)) = single n (single m r)

theorem MonoidAlgebra.map_neg {R : Type u_3} {S : Type u_4} {M : Type u_6} [Ring R] [Ring S] (f : R →+ S) (x : MonoidAlgebra R M) : map f (-x) = -map f x

theorem AddMonoidAlgebra.map_neg {R : Type u_3} {S : Type u_4} {M : Type u_6} [Ring R] [Ring S] (f : R →+ S) (x : AddMonoidAlgebra R M) : map f (-x) = -map f x

theorem MonoidAlgebra.map_sub {R : Type u_3} {S : Type u_4} {M : Type u_6} [Ring R] [Ring S] (f : R →+ S) (x y : MonoidAlgebra R M) : map f (x - y) = map f x - map f y

theorem AddMonoidAlgebra.map_sub {R : Type u_3} {S : Type u_4} {M : Type u_6} [Ring R] [Ring S] (f : R →+ S) (x y : AddMonoidAlgebra R M) : map f (x - y) = map f x - map f y

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 _.

noncomputable def AddMonoidAlgebra.toMultiplicative (k : Type u_9) (G : Type u_10) [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.

noncomputable def MonoidAlgebra.toAdditive (k : Type u_9) (G : Type u_10) [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.