toCocone

Mathlib.Algebra.Category.Grp.Colimits

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.Colimits.toCocone

Lean4

/-- (implementation detail) A morphism of commutative additive groups `Quot F →+ A`
induces a cocone on `F` as long as the universes work out.
-/
@[simps]
def toCocone [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) : Cocone F
    where
  pt := AddCommGrpCat.of A
  ι.app j := ofHom <| f.comp (Quot.ι F j)

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

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

Разделы

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

Аффилиация

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