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]
noncomputable def category_theory.arrow.map_cech_nerve {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [∀ (n : ), category_theory.limits.has_wide_pullback f.right (λ (i : ulift (fin (n + 1))), f.left) (λ (i : ulift (fin (n + 1))), f.hom)] [∀ (n : ), category_theory.limits.has_wide_pullback g.right (λ (i : ulift (fin (n + 1))), g.left) (λ (i : ulift (fin (n + 1))), g.hom)] (F : f g) :

The morphism between Čech nerves associated to a morphism of arrows.

Equations

The augmented Čech nerve associated to an arrow.

Equations
@[simp]
theorem category_theory.arrow.map_augmented_cech_nerve_right {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [∀ (n : ), category_theory.limits.has_wide_pullback f.right (λ (i : ulift (fin (n + 1))), f.left) (λ (i : ulift (fin (n + 1))), f.hom)] [∀ (n : ), category_theory.limits.has_wide_pullback g.right (λ (i : ulift (fin (n + 1))), g.left) (λ (i : ulift (fin (n + 1))), g.hom)] (F : f g) :
noncomputable def category_theory.arrow.map_augmented_cech_nerve {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [∀ (n : ), category_theory.limits.has_wide_pullback f.right (λ (i : ulift (fin (n + 1))), f.left) (λ (i : ulift (fin (n + 1))), f.hom)] [∀ (n : ), category_theory.limits.has_wide_pullback g.right (λ (i : ulift (fin (n + 1))), g.left) (λ (i : ulift (fin (n + 1))), g.hom)] (F : f g) :

The morphism between augmented Čech nerve associated to a morphism of arrows.

Equations

The Čech nerve construction, as a functor from arrow C.

Equations

The augmented Čech nerve construction is right adjoint to the to_arrow functor.

@[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
noncomputable def category_theory.arrow.map_cech_conerve {C : Type u} [category_theory.category C] {f g : 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 : ), category_theory.limits.has_wide_pushout g.left (λ (i : ulift (fin (n + 1))), g.right) (λ (i : ulift (fin (n + 1))), g.hom)] (F : f g) :

The morphism between Čech conerves associated to a morphism of arrows.

Equations

The augmented Čech conerve associated to an arrow.

Equations
@[simp]
theorem category_theory.arrow.map_augmented_cech_conerve_left {C : Type u} [category_theory.category C] {f g : 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 : ), category_theory.limits.has_wide_pushout g.left (λ (i : ulift (fin (n + 1))), g.right) (λ (i : ulift (fin (n + 1))), g.hom)] (F : f g) :
noncomputable def category_theory.arrow.map_augmented_cech_conerve {C : Type u} [category_theory.category C] {f g : 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 : ), category_theory.limits.has_wide_pushout g.left (λ (i : ulift (fin (n + 1))), g.right) (λ (i : ulift (fin (n + 1))), g.hom)] (F : f g) :

The morphism between augmented Čech conerves associated to a morphism of arrows.

Equations

The Čech conerve construction, as a functor from arrow C.

Equations

The augmented Čech conerve construction is left adjoint to the to_arrow functor.