liftAddHom — Mathlib

Lean4
/-- The canonical isomorphism between families of additive monoid homomorphisms `α → (M →+ N)`
and monoid homomorphisms `(α →₀ M) →+ N`. -/
def liftAddHom [AddZeroClass M] [AddCommMonoid N] : (α → M →+ N) ≃+ ((α →₀ M) →+ N)
    where
  toFun
    F :=
    { toFun := fun f ↦ f.sum fun x ↦ F x
      map_zero' := Finset.sum_empty
      map_add' := fun _ _ => sum_add_index' (fun x => (F x).map_zero) fun x => (F x).map_add }
  invFun F x := F.comp (singleAddHom x)
  left_inv
    F := by
    ext
    simp [singleAddHom]
  right_inv
    F := by
    ext
    simp [singleAddHom, AddMonoidHom.comp, Function.comp_def]
  map_add' F
    G := by
    ext x
    exact sum_add
Похожие утверждения