English
Let C be a category where for every arrow f there exist wide pullbacks of its right leg with its left leg and the arrow hom. The augmented Čech nerve construction is right adjoint to the arrow functor that sends an object X to its underlying arrow. In particular, for every augmented object X and arrow Y there is a natural bijection between morphisms from Augmented.toArrow(X) to Y and morphisms from X to augmentedCechNerve(Y).
Русский
Пусть C — категория, в которой для любого стрелки f существуют широкие обратные пределы справа и стрелке f. Раскладка дополненного Čech-нерва образует правую сопряженность к функтору toArrow, который преобразует объект в стрелку. Для любой дополненной фигуры X и стрелки Y существует естественная биекция между гомоморфизмами от Augmented.toArrow(X) к Y и гомоморфизмами от X к augmentedCechNerve(Y).
LaTeX
$$$$ \mathrm{Hom}\big((\mathrm{Augmented.toArrow})X, Y\big) \cong \mathrm{Hom}\big(X, \mathrm{augmentedCechNerve}(Y)\big). $$$$
Lean4
/-- The augmented Čech nerve construction is right adjoint to the `toArrow` functor. -/
abbrev cechNerveAdjunction : (Augmented.toArrow : _ ⥤ Arrow C) ⊣ augmentedCechNerve :=
Adjunction.mkOfHomEquiv
{ homEquiv := cechNerveEquiv
homEquiv_naturality_left_symm := by dsimp [cechNerveEquiv]; cat_disch
homEquiv_naturality_right :=
by
dsimp [cechNerveEquiv]
-- The next three lines were not needed before https://github.com/leanprover/lean4/pull/2644
intro X Y Y' f g
change equivalenceLeftToRight X Y' (f ≫ g) = equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g
cat_disch }
