faithful — Mathlib

English

The 2-truncated nerve functor nerveFunctor₂ is faithful; i.e., it injectively maps morphisms: if nerveFunctor₂.map f = nerveFunctor₂.map g, then f = g.

Русский

2‑уровневый функтор нерва nerveFunctor₂ верен; то есть отображение морфизмов под ним инъективно: если nerveFunctor₂.map f = nerveFunctor₂.map g, то f = g.

LaTeX

$$$ \forall X,Y\, \forall f,g:\, X \to Y,\; nerveFunctor_2.map f = nerveFunctor_2.map g \Rightarrow f = g $$$

Lean4

instance faithful : nerveFunctor₂.{u, u}.Faithful :=
  Functor.Faithful.of_comp_iso (G := oneTruncation₂) (H := ReflQuiv.forget) OneTruncation₂.ofNerve₂.natIso

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