nerve₂Adj — Mathlib

English

There is an adjunction between the 2-truncated nerve functor and the 2-truncated homotopy-category functor; equivalently, the 2-truncated nerve functor has a left adjoint giving a natural pair of adjoint functors.

Русский

Существуют соответствующая пара взаимной вложенности (адъюнкция) между 2‑уровневым функтором нерва и функтором 2‑уровневой гомотопии; другими словами, существует левый соседний функтор, образующий с функтором нерва пару, обладающую свойствами адъюнкции.

LaTeX

$$$ hoFunctor_2 \dashv nerveFunctor_2 $$$

Lean4

/-- The adjunction between the 2-truncated nerve functor and the 2-truncated homotopy category
functor. -/
nonrec def nerve₂Adj : hoFunctor₂.{u} ⊣ nerveFunctor₂ :=
  Adjunction.mkOfUnitCounit
    { unit := nerve₂Adj.unit
      counit := nerve₂Adj.counit
      left_triangle := by
        ext X
        apply HomotopyCategory.lift_unique'
        dsimp
        rw [Cat.comp_eq_comp, ← Functor.assoc]
        dsimp only [hoFunctor₂]
        rw [← hoFunctor₂_naturality (nerve₂Adj.unit.app X)]
        dsimp
        rw [nerve₂Adj.unit.map_app_eq X, Functor.assoc, id_comp]
        change _ ⋙ (HomotopyCategory.quotientFunctor _ ⋙ nerve₂Adj.counit.app (hoFunctor₂.obj X)) = _
        rw [nerve₂Adj.counit.app_eq]
        dsimp
        rw [← Cat.comp_eq_comp, ← assoc, ← Cat.freeRefl.map_comp, ReflQuiv.comp_eq_comp, ReflPrefunctor.comp_assoc]
        dsimp
        rw [← ReflQuiv.comp_eq_comp, Iso.inv_hom_id_app, ReflQuiv.id_eq_id]
        dsimp
        rw [ReflPrefunctor.comp_id (V := hoFunctor₂.obj X), ← ReflQuiv.comp_eq_comp (Z := .of _), Cat.freeRefl.map_comp,
          assoc]
        have :=
          ReflQuiv.adj.counit.naturality (X := Cat.freeRefl.obj (ReflQuiv.of (OneTruncation₂ X))) (Y :=
            hoFunctor₂.obj X) (SSet.Truncated.HomotopyCategory.quotientFunctor X)
        dsimp at this
        rw [this]
        apply Adjunction.left_triangle_components_assoc
      right_triangle := by
        refine NatTrans.ext (funext fun C ↦ ?_)
        apply toNerve₂.ext
        dsimp
        simp only [id_comp, map_comp, oneTruncation₂_obj, map_id]
        rw [nerve₂Adj.unit.map_app_eq, ReflPrefunctor.comp_assoc]
        rw [← ReflQuiv.comp_eq_comp, ← ReflQuiv.comp_eq_comp (X := ReflQuiv.of _) (Y := ReflQuiv.of _), assoc, assoc, ←
          Functor.comp_map, ← OneTruncation₂.ofNerve₂.natIso.inv.naturality]
        conv => lhs; rhs; rw [← assoc]
        change _ ≫ (ReflQuiv.forget.map _ ≫ ReflQuiv.forget.map _) ≫ _ = _
        rw [← ReflQuiv.forget.map_comp]
        dsimp
        conv => lhs; rhs; lhs; rw [Cat.comp_eq_comp]
        have : HomotopyCategory.quotientFunctor (nerveFunctor₂.obj C) ⋙ _ = _ := nerve₂Adj.counit.app_eq C
        rw [this]
        dsimp
        rw [← assoc, Cat.comp_eq_comp, toReflPrefunctor.map_comp]
        rw [← ReflQuiv.comp_eq_comp (X := ReflQuiv.of _) (Y := ReflQuiv.of _) (Z := ReflQuiv.of _)]
        have := ReflQuiv.adj.unit.naturality (OneTruncation₂.ofNerve₂.natIso.hom.app C)
        dsimp at this ⊢
        rw [← assoc, ← this]
        have := ReflQuiv.adj.right_triangle_components C
        dsimp [ReflQuiv.forget] at this
        simp [reassoc_of% this] }

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