HoRel₂

Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

URI: https://scilib.ai/kg/mathlib#SSet.Truncated.HoRel₂

Lean4

/-- The 2-simplices in a 2-truncated simplicial set `V` generate a hom relation on the free
category on the underlying refl quiver of `V`. -/
inductive HoRel₂ {V : SSet.Truncated 2} : (X Y : Cat.FreeRefl (OneTruncation₂ V)) → (f g : X ⟶ Y) → Prop
  |
  mk (φ : V _⦋2⦌₂) :
    HoRel₂ _ _ (Quot.mk _ (Quiver.Hom.toPath (ev02₂ φ)))
      (Quot.mk _ ((Quiver.Hom.toPath (ev01₂ φ)).comp (Quiver.Hom.toPath (ev12₂ φ))))

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

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

Разделы

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

Аффилиация

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