mathlib3 documentation

algebraic_topology.cech_nerve

The Čech Nerve #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

We end the file with a description of the Čech nerve of an arrow X ⟶ ⊤_ C to a terminal object, when C has finite products. We call this cech_nerve_terminal_from. When C is G-Set this gives us EG (the universal cover of the classifying space of G) as a simplicial G-set, which is useful for group cohomology.

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 : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] [ (n : ), category_theory.limits.has_wide_pullback g.right (λ (i : fin (n + 1)), g.left) (λ (i : 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
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 : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] [ (n : ), category_theory.limits.has_wide_pullback g.right (λ (i : fin (n + 1)), g.left) (λ (i : fin (n + 1)), g.hom)] (F : f g) :

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

Equations
@[reducible]

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

@[simp]

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 : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] [ (n : ), category_theory.limits.has_wide_pushout g.left (λ (i : fin (n + 1)), g.right) (λ (i : 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
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 : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] [ (n : ), category_theory.limits.has_wide_pushout g.left (λ (i : fin (n + 1)), g.right) (λ (i : fin (n + 1)), g.hom)] (F : f g) :

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

Equations
@[reducible]

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

Given an object X : C, the natural simplicial object sending [n] to Xⁿ⁺¹.

Equations