lift

Mathlib.Algebra.Category.Grp.Biproducts

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.HasLimit.lift

Lean4

/-- The map from an arbitrary cone over an indexed family of abelian groups
to the Cartesian product of those groups.
-/
@[simps!]
def lift (s : Fan f) : s.pt ⟶ AddCommGrpCat.of (∀ j, f j) :=
  ofHom
    { toFun x j := s.π.app ⟨j⟩ x
      map_zero' := by
        simp only [Functor.const_obj_obj, map_zero]
        rfl
      map_add' x
        y := by
        simp only [Functor.const_obj_obj, map_add]
        rfl }

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

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

Разделы

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

Аффилиация

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