mapDomain

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.mapDomain

Lean4

/-- Given `f : G → G'` and `v : SkewMonoidAlgebra k G`, `mapDomain f v : SkewMonoidAlgebra k G'`
is the finitely supported additive homomorphism whose value at `a : G'` is the sum of `v x` over
all `x` such that `f x = a`.
Note that `SkewMonoidAlgebra.mapDomain` is defined as an `AddHom`, while `MonoidAlgebra.mapDomain`
is defined as a function. -/
@[simps]
def mapDomain : SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G'
    where
  toFun v := v.sum fun a ↦ single (f a)
  map_zero' := sum_zero_index
  map_add' _ _ := sum_add_index' (fun _ ↦ single_zero _) fun _ ↦ single_add _

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru