cechConerve — Mathlib

English

The Čech conerve construction defines a functor from Arrow C to CosimplicialObject C; on objects f it sends f to f.cechConerve and on morphisms F it sends F to Arrow.mapCechConerve F.

Русский

Конструкция Čech-конвервы задаёт функтор от Arrow C к CosimplicialObject C; на объектах f она отправляет f в f.cechConerve, а на стрелках F — F в Arrow.mapCechConerve F.

LaTeX

$$$\\mathrm{cechConerve} : \\mathrm{Arrow}(C) \\to \\mathrm{CosimplicialObject}(C),\\quad \\mathrm{cechConerve}(f) = f.a\\n\\;\\;\\mathrm{cechConerve}(F) = \\mathrm{Arrow.mapCechConerve}(F)$$$

Lean4

/-- The Čech conerve construction, as a functor from `Arrow C`. -/
@[simps]
def cechConerve : Arrow C ⥤ CosimplicialObject C
    where
  obj f := f.cechConerve
  map F := Arrow.mapCechConerve F

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