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
:
f.cechNerve
is the Čech nerve, considered as a simplicial object inC
.f.augmentedCechNerve
is the augmented Čech nerve, considered as an augmented simplicial object inC
.SimplicialObject.cechNerve
andSimplicialObject.augmentedCechNerve
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 cechNerveTerminalFrom
. 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.
The Čech nerve associated to an arrow.
Instances For
The morphism between Čech nerves associated to a morphism of arrows.
Instances For
The augmented Čech nerve associated to an arrow.
Instances For
The morphism between augmented Čech nerve associated to a morphism of arrows.
Instances For
The Čech nerve construction, as a functor from Arrow C
.
Instances For
The augmented Čech nerve construction, as a functor from Arrow C
.
Instances For
A helper function used in defining the Čech adjunction.
Instances For
A helper function used in defining the Čech adjunction.
Instances For
A helper function used in defining the Čech adjunction.
Instances For
The augmented Čech nerve construction is right adjoint to the toArrow
functor.
Instances For
The Čech conerve associated to an arrow.
Instances For
The morphism between Čech conerves associated to a morphism of arrows.
Instances For
The augmented Čech conerve associated to an arrow.
Instances For
The morphism between augmented Čech conerves associated to a morphism of arrows.
Instances For
The Čech conerve construction, as a functor from Arrow C
.
Instances For
The augmented Čech conerve construction, as a functor from Arrow C
.
Instances For
A helper function used in defining the Čech conerve adjunction.
Instances For
A helper function used in defining the Čech conerve adjunction.
Instances For
A helper function used in defining the Čech conerve adjunction.
Instances For
The augmented Čech conerve construction is left adjoint to the toArrow
functor.
Instances For
Given an object X : C
, the natural simplicial object sending [n]
to Xⁿ⁺¹
.
Instances For
The diagram Option ι ⥤ C
sending none
to the terminal object and some j
to X
.
Instances For
The product Xᶥ
is the vertex of a limit cone on wideCospan ι X
.
Instances For
the isomorphism to the product induced by the limit cone wideCospan ι X
Instances For
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
.