# MonoidAlgebra.mapDomain #

### Multiplicative monoids #

source
@[reducible, inline]
abbrev MonoidAlgebra.mapDomain {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] (f : M → N) (v : 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 v = Finsupp.mapDomain f v

Instances For

source
@[reducible, inline]
abbrev AddMonoidAlgebra.mapDomain {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] (f : M → N) (v : 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 v = Finsupp.mapDomain f v

Instances For

source
theorem MonoidAlgebra.mapDomain_sum {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] (f : M → N) (s : MonoidAlgebra S M) (v : M → S → MonoidAlgebra R M) :
mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : M) (b : S) => mapDomain f (v a b)
source
theorem AddMonoidAlgebra.mapDomain_sum {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] (f : M → N) (s : AddMonoidAlgebra S M) (v : M → S → AddMonoidAlgebra R M) :
mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : M) (b : S) => mapDomain f (v a b)
source
theorem MonoidAlgebra.mapDomain_single {R : Type u_1} {M : Type u_3} {N : Type u_4} [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_1} {M : Type u_3} {N : Type u_4} [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_1} {M : Type u_3} {N : Type u_4} [Semiring R] {f : M → N} (hf : Function.Injective f) :
Function.Injective (mapDomain f)
source
theorem AddMonoidAlgebra.mapDomain_injective {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] {f : M → N} (hf : Function.Injective f) :
Function.Injective (mapDomain f)
source
@[simp]
theorem MonoidAlgebra.mapDomain_one {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [One M] [One N] {F : Type u_6} [FunLike F M N] [OneHomClass F M N] (f : F) :
mapDomain (⇑f) 1 = 1
source
@[simp]
theorem AddMonoidAlgebra.mapDomain_one {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [Zero M] [Zero N] {F : Type u_6} [FunLike F M N] [ZeroHomClass F M N] (f : F) :
mapDomain (⇑f) 1 = 1
source
theorem MonoidAlgebra.mapDomain_mul {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [Mul M] [Mul N] {F : Type u_6} [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 {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [Add M] [Add N] {F : Type u_6} [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.mapDomainRingHom (R : Type u_1) {M : Type u_3} {N : Type u_4} [Semiring R] [Monoid M] [Monoid N] {F : Type u_6} [FunLike F M N] [MonoidHomClass F M N] (f : F) :
MonoidAlgebra R M →+* MonoidAlgebra R N

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

Equations

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

Instances For

source
def AddMonoidAlgebra.mapDomainRingHom (R : Type u_1) {M : Type u_3} {N : Type u_4} [Semiring R] [AddMonoid M] [AddMonoid N] {F : Type u_6} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) :
AddMonoidAlgebra R M →+* AddMonoidAlgebra R N

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

Equations

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

Instances For

source
@[simp]
theorem AddMonoidAlgebra.mapDomainRingHom_apply (R : Type u_1) {M : Type u_3} {N : Type u_4} [Semiring R] [AddMonoid M] [AddMonoid N] {F : Type u_6} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (a✝ : M →₀ R) :
(mapDomainRingHom R f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝
source
@[simp]
theorem MonoidAlgebra.mapDomainRingHom_apply (R : Type u_1) {M : Type u_3} {N : Type u_4} [Semiring R] [Monoid M] [Monoid N] {F : Type u_6} [FunLike F M N] [MonoidHomClass F M N] (f : F) (a✝ : M →₀ R) :
(mapDomainRingHom R f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝
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_1} {M : Type u_3} [Semiring R] [Monoid M] :
mapDomainRingHom R (MonoidHom.id M) = RingHom.id (MonoidAlgebra R M)
source
@[simp]
theorem AddMonoidAlgebra.mapDomainRingHom_id {R : Type u_1} {M : Type u_3} [Semiring R] [AddMonoid M] :
mapDomainRingHom R (AddMonoidHom.id M) = RingHom.id (AddMonoidAlgebra R M)
source
@[simp]
theorem MonoidAlgebra.mapDomainRingHom_comp {R : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [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_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [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
theorem MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [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_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [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)

#### Conversions between `AddMonoidAlgebra` and `MonoidAlgebra` #

We have not defined `k[G] = MonoidAlgebra k (Multiplicative G)` because historically this caused problems; since the changes that have made `nsmul` definitional, this would be possible, but for now we just construct the ring isomorphisms using `RingEquiv.refl _`.

source
def AddMonoidAlgebra.toMultiplicative (k : Type u_6) (G : Type u_7) [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_6) (G : Type u_7) [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