pointedToTwoPSnd

Mathlib.CategoryTheory.Category.TwoP

URI: https://scilib.ai/kg/mathlib#pointedToTwoPSnd

Lean4

/-- The functor from `Pointed` to `TwoP` which adds a first point. -/
@[simps]
noncomputable def pointedToTwoPSnd : Pointed.{u} ⥤ TwoP
    where
  obj X := ⟨Option X, ⟨none, X.point⟩, (some_ne_none _).symm⟩
  map f := ⟨Option.map f.toFun, rfl, congr_arg _ f.map_point⟩
  map_id _ := Bipointed.Hom.ext Option.map_id
  map_comp f g := Bipointed.Hom.ext (Option.map_comp_map f.1 g.1).symm

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

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

Разделы

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

Аффилиация

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