Lean4
/-- Simplices in the nerve of categories are uniquely determined by their spine.
Indeed, this property describes the essential image of the nerve functor. -/
noncomputable def strictSegal : StrictSegal (nerve C)
where
spineToSimplex {n}
F :=
ComposableArrows.mkOfObjOfMapSucc (fun i ↦ (F.vertex i).obj 0)
(fun i ↦
eqToHom (Functor.congr_obj (F.arrow_src i).symm 0) ≫
(F.arrow i).map' 0 1 ≫ eqToHom (Functor.congr_obj (F.arrow_tgt i) 0))
spine_spineToSimplex
n := by
ext F i
· exact ComposableArrows.ext₀ rfl
· refine ComposableArrows.ext₁ ?_ ?_ ?_
· exact Functor.congr_obj (F.arrow_src i).symm 0
· exact Functor.congr_obj (F.arrow_tgt i).symm 0
· dsimp
apply ComposableArrows.mkOfObjOfMapSucc_map_succ
spineToSimplex_spine
n := by
ext F
fapply ComposableArrows.ext
· intro i
rfl
· intro i hi
dsimp
exact ComposableArrows.mkOfObjOfMapSucc_map_succ _ _ i hi
