# mathlibdocumentation

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.cech_nerve {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :

The Čech nerve associated to an arrow.

Equations
@[simp]
theorem category_theory.arrow.cech_nerve_obj {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (n : simplex_categoryᵒᵖ) :
f.cech_nerve.obj n = (λ (i : fin ((opposite.unop n).len + 1)), f.left) (λ (i : fin ((opposite.unop n).len + 1)), f.hom)
@[simp]
theorem category_theory.arrow.map_cech_nerve_app {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (i : fin (n + 1)), g.left) (λ (i : fin (n + 1)), g.hom)] (F : f g) (n : simplex_categoryᵒᵖ) :
noncomputable def category_theory.arrow.map_cech_nerve {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (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
@[simp]
theorem category_theory.arrow.augmented_cech_nerve_hom_app {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (i : simplex_categoryᵒᵖ) :
noncomputable def category_theory.arrow.augmented_cech_nerve {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :

The augmented Čech nerve associated to an arrow.

Equations
@[simp]
theorem category_theory.arrow.augmented_cech_nerve_left {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :
@[simp]
theorem category_theory.arrow.augmented_cech_nerve_right {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :
@[simp]
theorem category_theory.arrow.map_augmented_cech_nerve_right {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (i : fin (n + 1)), g.left) (λ (i : fin (n + 1)), g.hom)] (F : f g) :
noncomputable def category_theory.arrow.map_augmented_cech_nerve {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (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
@[simp]
theorem category_theory.arrow.map_augmented_cech_nerve_left {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (i : fin (n + 1)), g.left) (λ (i : fin (n + 1)), g.hom)] (F : f g) :
noncomputable def category_theory.simplicial_object.cech_nerve {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :

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

Equations
@[simp]
theorem category_theory.simplicial_object.cech_nerve_map {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (f g : category_theory.arrow C) (F : f g) :
@[simp]
theorem category_theory.simplicial_object.cech_nerve_obj {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (f : category_theory.arrow C) :
noncomputable def category_theory.simplicial_object.augmented_cech_nerve {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :

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

Equations
@[simp]
theorem category_theory.simplicial_object.augmented_cech_nerve_map {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (f g : category_theory.arrow C) (F : f g) :
@[simp]
theorem category_theory.simplicial_object.augmented_cech_nerve_obj {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (f : category_theory.arrow C) :
@[simp]
theorem category_theory.simplicial_object.equivalence_right_to_left_left {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : X F.augmented_cech_nerve) :
@[simp]
theorem category_theory.simplicial_object.equivalence_right_to_left_right {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : X F.augmented_cech_nerve) :
noncomputable def category_theory.simplicial_object.equivalence_right_to_left {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : X F.augmented_cech_nerve) :

A helper function used in defining the Čech adjunction.

Equations
@[simp]
theorem category_theory.simplicial_object.equivalence_left_to_right_right {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C)  :
noncomputable def category_theory.simplicial_object.equivalence_left_to_right {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C)  :

A helper function used in defining the Čech adjunction.

Equations
@[simp]
theorem category_theory.simplicial_object.equivalence_left_to_right_left_app {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (x : simplex_categoryᵒᵖ) :
= (λ (i : fin ((opposite.unop x).len + 1)), X.left.map ((opposite.unop x).const i).op G.left) _
@[simp]
theorem category_theory.simplicial_object.cech_nerve_equiv_apply {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C)  :
@[simp]
theorem category_theory.simplicial_object.cech_nerve_equiv_symm_apply {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : X F.augmented_cech_nerve) :
noncomputable def category_theory.simplicial_object.cech_nerve_equiv {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) :

A helper function used in defining the Čech adjunction.

Equations
@[reducible]
noncomputable def category_theory.simplicial_object.cech_nerve_adjunction {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :

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

@[simp]
theorem category_theory.arrow.cech_conerve_obj {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (n : simplex_category) :
f.cech_conerve.obj n = (λ (i : fin (n.len + 1)), f.right) (λ (i : fin (n.len + 1)), f.hom)
noncomputable def category_theory.arrow.cech_conerve {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :

The Čech conerve associated to an arrow.

Equations
@[simp]
theorem category_theory.arrow.cech_conerve_map {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (m n : simplex_category) (g : m n) :
@[simp]
theorem category_theory.arrow.map_cech_conerve_app {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (i : fin (n + 1)), g.right) (λ (i : fin (n + 1)), g.hom)] (F : f g) (n : simplex_category) :
noncomputable def category_theory.arrow.map_cech_conerve {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (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
noncomputable def category_theory.arrow.augmented_cech_conerve {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :

The augmented Čech conerve associated to an arrow.

Equations
@[simp]
theorem category_theory.arrow.augmented_cech_conerve_hom_app {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (i : simplex_category) :
@[simp]
theorem category_theory.arrow.augmented_cech_conerve_right {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :
@[simp]
theorem category_theory.arrow.augmented_cech_conerve_left {C : Type u} (f : category_theory.arrow C) [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :
@[simp]
theorem category_theory.arrow.map_augmented_cech_conerve_left {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (i : fin (n + 1)), g.right) (λ (i : fin (n + 1)), g.hom)] (F : f g) :
noncomputable def category_theory.arrow.map_augmented_cech_conerve {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (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
@[simp]
theorem category_theory.arrow.map_augmented_cech_conerve_right {C : Type u} {f g : category_theory.arrow C} [ (n : ), (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] [ (n : ), (λ (i : fin (n + 1)), g.right) (λ (i : fin (n + 1)), g.hom)] (F : f g) :
@[simp]
theorem category_theory.cosimplicial_object.cech_conerve_obj {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (f : category_theory.arrow C) :
@[simp]
theorem category_theory.cosimplicial_object.cech_conerve_map {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (f g : category_theory.arrow C) (F : f g) :
noncomputable def category_theory.cosimplicial_object.cech_conerve {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :

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

Equations
@[simp]
theorem category_theory.cosimplicial_object.augmented_cech_conerve_map {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (f g : category_theory.arrow C) (F : f g) :
@[simp]
theorem category_theory.cosimplicial_object.augmented_cech_conerve_obj {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (f : category_theory.arrow C) :
noncomputable def category_theory.cosimplicial_object.augmented_cech_conerve {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :

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

Equations
@[simp]
theorem category_theory.cosimplicial_object.equivalence_left_to_right_right {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : F.augmented_cech_conerve X) :
@[simp]
theorem category_theory.cosimplicial_object.equivalence_left_to_right_left {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : F.augmented_cech_conerve X) :
noncomputable def category_theory.cosimplicial_object.equivalence_left_to_right {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : F.augmented_cech_conerve X) :

A helper function used in defining the Čech conerve adjunction.

Equations
noncomputable def category_theory.cosimplicial_object.equivalence_right_to_left {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C)  :

A helper function used in defining the Čech conerve adjunction.

Equations
@[simp]
theorem category_theory.cosimplicial_object.equivalence_right_to_left_right_app {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (x : simplex_category) :
= (λ (i : fin (x.len + 1)), G.right X.right.map (x.const i)) _
@[simp]
theorem category_theory.cosimplicial_object.equivalence_right_to_left_left {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C)  :
@[simp]
theorem category_theory.cosimplicial_object.cech_conerve_equiv_apply {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C) (G : F.augmented_cech_conerve X) :
noncomputable def category_theory.cosimplicial_object.cech_conerve_equiv {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C)  :

A helper function used in defining the Čech conerve adjunction.

Equations
@[simp]
theorem category_theory.cosimplicial_object.cech_conerve_equiv_symm_apply {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] (F : category_theory.arrow C)  :
@[reducible]
noncomputable def category_theory.cosimplicial_object.cech_conerve_adjunction {C : Type u} [ (n : ) (f : , (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :

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

noncomputable def category_theory.cech_nerve_terminal_from {C : Type u} (X : C) :

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

Equations
noncomputable def category_theory.cech_nerve_terminal_from.wide_cospan {C : Type u} (ι : Type w) (X : C) :

The diagram `option ι ⥤ C` sending `none` to the terminal object and `some j` to `X`.

Equations
• = (λ (i : ι), X) (λ (i : ι),
@[protected, instance]
noncomputable def category_theory.cech_nerve_terminal_from.unique_to_wide_cospan_none {C : Type u} (ι : Type w) (X Y : C) :
Equations

The product `Xᶥ` is the vertex of a limit cone on `wide_cospan ι X`.

Equations
@[protected, instance]

Given an object `X : C`, the Čech nerve of the hom to the terminal object `X ⟶ ⊤_ C` is naturally isomorphic to a simplicial object sending `[n]` to `Xⁿ⁺¹` (when `C` is `G-Set`, this is `EG`, the universal cover of the classifying space of `G`.

Equations