English
If f: X → Y is an isomorphism, then the degenerate n-simplices are preserved back and forth along f.
Русский
Если f: X → Y изоморфизм, то вырожденные n-граней сохраняются при обратном и прямом отображении.
LaTeX
$$$$\text{IsIso}(f) \Rightarrow (f.app_{n}(x) \in Y_{\mathrm{deg}}(n) \iff x \in X_{\mathrm{deg}}(n)),$$$$
Lean4
/-- The functor that carries a 2-truncated simplicial set to its underlying refl quiver. -/
@[simps]
def oneTruncation₂ : SSet.Truncated.{u} 2 ⥤ ReflQuiv.{u, u}
where
obj S := ReflQuiv.of (OneTruncation₂ S)
map {S T}
F :=
{ obj := F.app (op ⦋0⦌₂)
map := fun f ↦
{ edge := F.app _ f.edge
src_eq := by rw [← FunctorToTypes.naturality, f.src_eq]
tgt_eq := by rw [← FunctorToTypes.naturality, f.tgt_eq] }
map_id := fun X ↦
OneTruncation₂.Hom.ext
(by
dsimp
rw [← FunctorToTypes.naturality]) }
