counit — Mathlib

English

The counit of the 2-truncated nerve adjunction is a natural transformation from the nerve functor composed with ho-functor to the identity on Cat, realized levelwise by the appropriate component maps.

Русский

Контра-единица 2-уровня нервной adjunction является натуральной трансформацией от композиции нерва с ho-функтором к тождественному функтору на категорию Cat, реализованной на каждом уровне компонентами.

LaTeX

$$$\varepsilon: \mathrm{nerveFunctor}_2 \circ \mathrm{hoFunctor}_2 \Rightarrow \mathrm{Id}_{\mathrm{Cat}}$$$

Lean4

/-- The counit of `nerve₂Adj.` -/
@[simps]
def counit : nerveFunctor₂ ⋙ hoFunctor₂.{u} ⟶ 𝟭 Cat
    where
  app _ := nerve₂Adj.counit.app _
  naturality _ _ _ := nerve₂Adj.counit.naturality _

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