pointedToTwoPFst

Mathlib.CategoryTheory.Category.TwoP

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

Lean4

/-- The functor from `Pointed` to `TwoP` which adds a second point. -/
@[simps]
noncomputable def pointedToTwoPFst : Pointed.{u} ⥤ TwoP
    where
  obj X := ⟨Option X, ⟨X.point, none⟩, some_ne_none _⟩
  map f := ⟨Option.map f.toFun, congr_arg _ f.map_point, rfl⟩
  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