MonoidAlgebra.mapDomain

Multiplicative monoids

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

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

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)

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)

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

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

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)

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)

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

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

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

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

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' := ⋯ }

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' := ⋯ }

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

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

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)

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

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

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

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

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)

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

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.

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.