nerveHomEquiv — Mathlib

English

There is a natural isomorphism between morphisms in the one-truncation nerve and arrows in the corresponding reflQuiver.

Русский

Существует естественная изоморфия между морфизмами в усечённом нерве и стрелами в соответствующем reflQuiver.

LaTeX

$$$$ \text{nerveHomEquiv} : \text{Hom}_{OneTruncation₂}(\text{nerve } C) \cong \text{Hom}_{ReflQuiv}(\ldots) $$$$

Lean4

/-- A hom equivalence over the function `OneTruncation₂.nerveEquiv`. -/
def nerveHomEquiv (X Y : OneTruncation₂ ((SSet.truncation 2).obj (nerve C))) : (X ⟶ Y) ≃ (nerveEquiv X ⟶ nerveEquiv Y)
    where
  toFun
    φ :=
    eqToHom (congr_arg ComposableArrows.left φ.src_eq.symm) ≫
      φ.edge.hom ≫ eqToHom (congr_arg ComposableArrows.left φ.tgt_eq)
  invFun
    f :=
    { edge := ComposableArrows.mk₁ f
      src_eq := ComposableArrows.ext₀ rfl
      tgt_eq := ComposableArrows.ext₀ rfl }
  left_inv
    φ := by
    ext
    exact
      ComposableArrows.ext₁ (congr_arg ComposableArrows.left φ.src_eq).symm
        (congr_arg ComposableArrows.left φ.tgt_eq).symm rfl
  right_inv f := by dsimp; simp only [comp_id, id_comp]; rfl

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