English
To any arrow f: A → B in a category with wide pushouts, one assigns a cosimplicial object in C whose nth object is the wide pushout of the left and right legs of f with indices of size n+1, and whose coface and codegeneracy maps are induced by the universal properties of these pushouts.
Русский
Для стрелки f: A → B в категории с широкими сопряжениями присваивается косимплициальный объект в C, чьё n-е слагаемое есть широкий вытяж pushout левый и правый рёбра f с индексами размера n+1, а отображения сопряжения задаются через универсальные свойства этих pushout-объектов.
LaTeX
$$$$ \text{cechConerve}(f) : \mathrm{CosimplicialObject}\, C, \quad (\mathrm{cechConerve}(f))^n = \mathrm{widePushout}(f.left, (n.len+1 \mapsto f.right), f.hom). $$$$
Lean4
/-- The Čech conerve associated to an arrow. -/
@[simps]
def cechConerve : CosimplicialObject C
where
obj n := widePushout f.left (fun _ : Fin (n.len + 1) => f.right) fun _ => f.hom
map {x y}
g :=
by
refine
WidePushout.desc (WidePushout.head _) (fun i => (@WidePushout.ι _ _ _ _ _ (fun _ => f.hom) (_) (g.toOrderHom i)))
(fun j => ?_)
rw [← WidePushout.arrow_ι]
