Pushing coefficients of a monoid algebra forward along a map

Functoriality of MonoidAlgebra.mapDomain, the map R[M] → R[N] induced by a map M → N of the index types, in the form of the corresponding Finsupp.mapDomain lemmas: the identity induces the identity, a composite induces the composite, and a surjection induces a surjection. Mathlib states the first two only for the bundled ring and algebra homomorphisms mapDomainRingHom and mapDomainAlgHom; the unbundled forms are what a computation with the coefficients of an inverse system of group algebras uses. Also: the image of mapDomain f commutes with a monomial single n r as soon as every f m commutes with n and r is central.

Main results

• MonoidAlgebra.mapDomain_id, MonoidAlgebra.mapDomain_mapDomain: the functor laws.
• MonoidAlgebra.mapDomain_surjective: the map induced by a surjection is surjective.
• MonoidAlgebra.mapDomain_commute_single: the image of mapDomain f commutes with single n r when the values of f commute with n and r is central.

@[simp]

theorem MonoidAlgebra.mapDomain_id {R : Type u_1} [Semiring R] {M : Type u_2} (x : MonoidAlgebra R M) : mapDomain id x = x

Pushing the coefficients forward along the identity does nothing.

@[simp]

theorem MonoidAlgebra.mapDomain_mapDomain {R : Type u_1} [Semiring R] {M : Type u_2} {N : Type u_3} {O : Type u_4} (f : M → N) (g : N → O) (x : MonoidAlgebra R M) : mapDomain g (mapDomain f x) = mapDomain (g ∘ f) x

Pushing the coefficients forward along two maps in turn is pushing them forward along the composite.

theorem MonoidAlgebra.mapDomain_surjective {R : Type u_1} [Semiring R] {M : Type u_2} {N : Type u_3} {f : M → N} (hf : Function.Surjective f) : Function.Surjective (mapDomain f)

Pushing the coefficients forward along a surjection is surjective.

theorem MonoidAlgebra.mapDomain_commute_single {R : Type u_1} [Semiring R] {M : Type u_2} {N : Type u_3} [Mul N] {f : M → N} {n : N} {r : R} (hm : ∀ (m : M), Commute (f m) n) (hr : ∀ (s : R), Commute s r) (x : MonoidAlgebra R M) : Commute (mapDomain f x) (single n r)

The image of mapDomain f commutes with the monomial single n r when every value of f commutes with n and r is central.