mathlib documentation

algebraic_topology.cech_nerve

The Čech Nerve #

This file provides a definition of the Čech nerve associated to an arrow, provided the base category has the correct wide pullbacks.

Several variants are provided, given f : arrow C:

  1. f.cech_nerve is the Čech nerve, considered as a simplicial object in C.
  2. f.augmented_cech_nerve is the augmented Čech nerve, considered as an augmented simplicial object in C.
  3. simplicial_object.cech_nerve and simplicial_object.augmented_cech_nerve are functorial versions of 1 resp. 2.
@[simp]

The augmented Čech nerve associated to an arrow.

Equations
@[simp]
theorem category_theory.arrow.cech_conerve_obj {C : Type u} [category_theory.category C] (f : category_theory.arrow C) [∀ (n : ), category_theory.limits.has_wide_pushout f.left (λ (i : ulift (fin (n + 1))), f.right) (λ (i : ulift (fin (n + 1))), f.hom)] (n : simplex_category) :
f.cech_conerve.obj n = category_theory.limits.wide_pushout f.left (λ (i : ulift (fin (n.len + 1))), f.right) (λ (i : ulift (fin (n.len + 1))), f.hom)

The Čech conerve associated to an arrow.

Equations

The augmented Čech conerve associated to an arrow.

Equations