natIso — Mathlib

English

If f: X → Y is mono, nondegeneracy is preserved along f.

Русский

Если f: X → Y моно, ненегидность сохраняется вдоль f.

LaTeX

$$$$\text{Mono}(f) \Rightarrow (x \in X_{\mathrm{nondeg}}(n) \iff f.app_{n}(x) \in Y_{\mathrm{nondeg}}(n)),$$$$

Lean4

/-- The refl quiver underlying a nerve is naturally isomorphic to the refl quiver underlying the
category. -/
@[simps! hom_app_obj hom_app_map inv_app_obj_obj inv_app_obj_map inv_app_map]
def natIso : nerveFunctor₂.{u, u} ⋙ SSet.oneTruncation₂ ≅ ReflQuiv.forget :=
  NatIso.ofComponents (fun C => OneTruncation₂.ofNerve₂ C)
    (by ·
        intro C D F
        fapply ReflPrefunctor.ext <;> simp
        · exact fun _ ↦ rfl
        · intro X Y f
          obtain ⟨f, rfl, rfl⟩ := f
          unfold SSet.oneTruncation₂ nerveFunctor₂ SSet.truncation SimplicialObject.truncation nerveFunctor
            toReflPrefunctor
          simp only [comp_obj, whiskeringLeft_obj_obj, ReflQuiv.of_val, Functor.comp_map, whiskeringLeft_obj_map,
            whiskerLeft_app, op_obj, ofNerve₂, Cat.of_α, nerveEquiv, ComposableArrows.obj', Fin.zero_eta, Fin.isValue,
            ReflQuiv.comp_eq_comp, Nat.reduceAdd, op_map, Quiver.Hom.unop_op, nerve_map, SimplexCategory.toCat_map,
            ReflPrefunctor.comp_obj, ReflPrefunctor.comp_map]
          simp [nerveHomEquiv, ReflQuiv.isoOfEquiv, ReflQuiv.isoOfQuivIso, Quiv.isoOfEquiv])

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