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.cech_nerve
is the Čech nerve, considered as a simplicial object inC
.f.augmented_cech_nerve
is the augmented Čech nerve, considered as an augmented simplicial object inC
.simplicial_object.cech_nerve
andsimplicial_object.augmented_cech_nerve
are functorial versions of 1 resp. 2.
The Čech nerve associated to an arrow.
Equations
- f.cech_nerve = {obj := λ (n : simplex_categoryᵒᵖ), category_theory.limits.wide_pullback f.right (λ (i : fin ((opposite.unop n).len + 1)), f.left) (λ (i : fin ((opposite.unop n).len + 1)), f.hom), map := λ (m n : simplex_categoryᵒᵖ) (g : m ⟶ n), category_theory.limits.wide_pullback.lift (category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop m).len + 1)), f.hom)) (λ (i : fin ((opposite.unop n).len + 1)), category_theory.limits.wide_pullback.π (λ (i : fin ((opposite.unop m).len + 1)), f.hom) (⇑(simplex_category.hom.to_order_hom g.unop) i)) _, map_id' := _, map_comp' := _}
The morphism between Čech nerves associated to a morphism of arrows.
Equations
- category_theory.arrow.map_cech_nerve F = {app := λ (n : simplex_categoryᵒᵖ), category_theory.limits.wide_pullback.lift (category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop n).len + 1)), f.hom) ≫ F.right) (λ (i : fin ((opposite.unop n).len + 1)), category_theory.limits.wide_pullback.π (λ (i : fin ((opposite.unop n).len + 1)), f.hom) i ≫ F.left) _, naturality' := _}
The augmented Čech nerve associated to an arrow.
Equations
- f.augmented_cech_nerve = {left := f.cech_nerve _, right := f.right, hom := {app := λ (i : simplex_categoryᵒᵖ), category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop i).len + 1)), f.hom), naturality' := _}}
The morphism between augmented Čech nerve associated to a morphism of arrows.
Equations
- category_theory.arrow.map_augmented_cech_nerve F = {left := category_theory.arrow.map_cech_nerve F, right := F.right, w' := _}
The Čech nerve construction, as a functor from arrow C
.
Equations
- category_theory.simplicial_object.cech_nerve = {obj := λ (f : category_theory.arrow C), f.cech_nerve, map := λ (f g : category_theory.arrow C) (F : f ⟶ g), category_theory.arrow.map_cech_nerve F, map_id' := _, map_comp' := _}
The augmented Čech nerve construction, as a functor from arrow C
.
Equations
- category_theory.simplicial_object.augmented_cech_nerve = {obj := λ (f : category_theory.arrow C), f.augmented_cech_nerve, map := λ (f g : category_theory.arrow C) (F : f ⟶ g), category_theory.arrow.map_augmented_cech_nerve F, map_id' := _, map_comp' := _}
A helper function used in defining the Čech adjunction.
Equations
- category_theory.simplicial_object.equivalence_right_to_left X F G = {left := G.left.app (opposite.op (simplex_category.mk 0)) ≫ category_theory.limits.wide_pullback.π (λ (i : fin ((opposite.unop (opposite.op (simplex_category.mk 0))).len + 1)), F.hom) 0, right := G.right, w' := _}
A helper function used in defining the Čech adjunction.
Equations
- category_theory.simplicial_object.equivalence_left_to_right X F G = {left := {app := λ (x : simplex_categoryᵒᵖ), category_theory.limits.wide_pullback.lift (X.hom.app x ≫ G.right) (λ (i : fin ((opposite.unop x).len + 1)), X.left.map ((opposite.unop x).const i).op ≫ G.left) _, naturality' := _}, right := G.right, w' := _}
A helper function used in defining the Čech adjunction.
The augmented Čech nerve construction is right adjoint to the to_arrow
functor.
The Čech conerve associated to an arrow.
Equations
- f.cech_conerve = {obj := λ (n : simplex_category), category_theory.limits.wide_pushout f.left (λ (i : fin (n.len + 1)), f.right) (λ (i : fin (n.len + 1)), f.hom), map := λ (m n : simplex_category) (g : m ⟶ n), category_theory.limits.wide_pushout.desc (category_theory.limits.wide_pushout.head (λ (i : fin (n.len + 1)), f.hom)) (λ (i : fin (m.len + 1)), category_theory.limits.wide_pushout.ι (λ (i : fin (n.len + 1)), f.hom) (⇑(simplex_category.hom.to_order_hom g) i)) _, map_id' := _, map_comp' := _}
The morphism between Čech conerves associated to a morphism of arrows.
Equations
- category_theory.arrow.map_cech_conerve F = {app := λ (n : simplex_category), category_theory.limits.wide_pushout.desc (F.left ≫ category_theory.limits.wide_pushout.head (λ (i : fin (n.len + 1)), g.hom)) (λ (i : fin (n.len + 1)), F.right ≫ category_theory.limits.wide_pushout.ι (λ (i : fin (n.len + 1)), g.hom) i) _, naturality' := _}
The augmented Čech conerve associated to an arrow.
Equations
- f.augmented_cech_conerve = {left := f.left, right := f.cech_conerve _, hom := {app := λ (i : simplex_category), category_theory.limits.wide_pushout.head (λ (i : fin (i.len + 1)), f.hom), naturality' := _}}
The morphism between augmented Čech conerves associated to a morphism of arrows.
Equations
- category_theory.arrow.map_augmented_cech_conerve F = {left := F.left, right := category_theory.arrow.map_cech_conerve F, w' := _}
The Čech conerve construction, as a functor from arrow C
.
Equations
- category_theory.cosimplicial_object.cech_conerve = {obj := λ (f : category_theory.arrow C), f.cech_conerve, map := λ (f g : category_theory.arrow C) (F : f ⟶ g), category_theory.arrow.map_cech_conerve F, map_id' := _, map_comp' := _}
The augmented Čech conerve construction, as a functor from arrow C
.
Equations
- category_theory.cosimplicial_object.augmented_cech_conerve = {obj := λ (f : category_theory.arrow C), f.augmented_cech_conerve, map := λ (f g : category_theory.arrow C) (F : f ⟶ g), category_theory.arrow.map_augmented_cech_conerve F, map_id' := _, map_comp' := _}
A helper function used in defining the Čech conerve adjunction.
Equations
- category_theory.cosimplicial_object.equivalence_left_to_right F X G = {left := G.left, right := category_theory.limits.wide_pushout.ι (λ (i : fin ((simplex_category.mk 0).len + 1)), F.hom) 0 ≫ G.right.app (simplex_category.mk 0), w' := _}
A helper function used in defining the Čech conerve adjunction.
A helper function used in defining the Čech conerve adjunction.
The augmented Čech conerve construction is left adjoint to the to_arrow
functor.