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.

Equations

MonoidAlgebra.mapDomain f x = Finsupp.mapDomain f x

Instances For

source

@[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.

Equations

AddMonoidAlgebra.mapDomain f x = Finsupp.mapDomain f x

Instances For

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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

source

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

source

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)

source

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)

source

@[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

source

@[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

source

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

source

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

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

@[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

source

@[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

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

@[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)

source

@[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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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₂)

source

@[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₂)

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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

source

@[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

source

@[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₂)

source

@[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₂)

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

@[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

source

@[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

source

theorem MonoidAlgebra.ringHom_ext_iff {M : Type u_2} {R : Type u_6} {S : Type u_7} [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)

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

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.

Equations

MonoidAlgebra.mapRangeRingHom M f = { toFun := Finsupp.mapRange ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

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.

Equations

AddMonoidAlgebra.mapRangeRingHom M f = { toFun := Finsupp.mapRange ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

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)

source

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)

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

@[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)

source

@[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)

source

@[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

source

@[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

source

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

source

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

source

@[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

source

@[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

source

@[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₂)

source

@[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₂)

source

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.

Equations

MonoidAlgebra.mapRangeRingEquiv M e = RingEquiv.ofRingHom (MonoidAlgebra.mapRangeRingHom M ↑e) (MonoidAlgebra.mapRangeRingHom M ↑e.symm) ⋯ ⋯

Instances For

source

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.

Equations

AddMonoidAlgebra.mapRangeRingEquiv M e = RingEquiv.ofRingHom (AddMonoidAlgebra.mapRangeRingHom M ↑e) (AddMonoidAlgebra.mapRangeRingHom M ↑e.symm) ⋯ ⋯

Instances For

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

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

source

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

source

@[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

source

@[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

source

@[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₂)

source

@[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₂)

source

def MonoidAlgebra.commRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [Monoid M] [Monoid N] [DecidableEq M] [DecidableEq 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)

Instances For

source

def AddMonoidAlgebra.commRingEquiv {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] [DecidableEq M] [DecidableEq 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)

Instances For

source

@[simp]

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

commRingEquiv.symm = commRingEquiv

source

@[simp]

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

commRingEquiv.symm = commRingEquiv

source

@[simp]

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

commRingEquiv (single m (single n r)) = single n (single m r)

source

@[simp]

theorem AddMonoidAlgebra.commRingEquiv_single_single {R : Type u_2} {M : Type u_5} {N : Type u_6} [Semiring R] [AddMonoid M] [AddMonoid N] [DecidableEq M] [DecidableEq 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 _.

source

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

Equations

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

Instances For

source

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

Equations

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

Instances For

Documentation

Mathlib.Algebra.MonoidAlgebra.MapDomain

Maps of monoid algebras #

Multiplicative monoids #

Conversions between `AddMonoidAlgebra` and `MonoidAlgebra` #

Maps of monoid algebras #

Multiplicative monoids #

Conversions between AddMonoidAlgebra and MonoidAlgebra #

Conversions between `AddMonoidAlgebra` and `MonoidAlgebra` #