mk — Mathlib · SciLib

English

For i ∈ Fin 3, the δ₂-face naturality holds for mk.app, ensuring coherent gluing at the 2-skeleton.

Русский

Для i ∈ Fin 3 справедлива натуральность δ₂ для mk.app, обеспечивая когерентность сцепления на 2-слое.

LaTeX

$$$\forall i:\, Fin(3),\; toNerve₂.mk.naturalityProperty F (δ₂ i) $$$

Lean4

/-- The morphism `X ⟶ nerveFunctor₂.obj (Cat.of C)` of 2-truncated simplicial sets that is
constructed from a refl prefunctor `F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of C` assuming
`∀ (φ : : X _⦋2⦌₂), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)`. -/
@[simps!]
def mk : X ⟶ nerveFunctor₂.obj (Cat.of C)
    where
  app n := toNerve₂.mk.app F n.unop
  naturality _ _ f := MorphismProperty.of_eq_top (toNerve₂.mk_naturality F hyp) f.unop

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