English
Under a mono morphism f, degenerate simplex membership reflects exactly from X to Y.
Русский
Для моно отображения f, принадлежность к degenerate точно отражается между X и Y.
LaTeX
$$$$\text{Mono}(f) \Rightarrow (x \in X_{\mathrm{deg}}(n) \iff f.app_{n}(x) \in Y_{\mathrm{deg}}(n)),$$$$
Lean4
/-- The refl quiver underlying a nerve is isomorphic to the refl quiver underlying the category. -/
def ofNerve₂ (C : Type u) [Category.{u} C] :
ReflQuiv.of (OneTruncation₂ (nerveFunctor₂.obj (Cat.of C))) ≅ ReflQuiv.of C :=
by
apply ReflQuiv.isoOfEquiv.{u, u} OneTruncation₂.nerveEquiv OneTruncation₂.nerveHomEquiv ?_
intro X
unfold nerveEquiv nerveHomEquiv
simp only [Cat.of_α, op_obj, ComposableArrows.obj', Fin.zero_eta, Fin.isValue, Equiv.coe_fn_mk, nerveEquiv_apply,
Nat.reduceAdd, id_edge, eqToHom_refl, comp_id, id_comp, ReflQuiver.id_eq_id]
unfold nerve truncation SimplicialObject.truncation SimplexCategory.Truncated.inclusion
simp only [ObjectProperty.ι_obj, SimplexCategory.len_mk, Nat.reduceAdd, Fin.isValue, SimplexCategory.toCat_map,
whiskeringLeft_obj_obj, Functor.comp_map, op_obj, op_map, Quiver.Hom.unop_op, ObjectProperty.ι_map,
ComposableArrows.whiskerLeft_map, Fin.zero_eta, Monotone.functor_obj, Fin.mk_one, homOfLE_leOfHom]
change X.map (𝟙 _) = _
rw [X.map_id]
rfl
