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:
f.cech_nerveis the Čech nerve, considered as a simplicial object inC.f.augmented_cech_nerveis the augmented Čech nerve, considered as an augmented simplicial object inC.simplicial_object.cech_nerveandsimplicial_object.augmented_cech_nerveare 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}
[category_theory.category C]
(f : 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)] :
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' := _}
@[simp]
theorem
category_theory.arrow.cech_nerve_map
{C : Type u}
[category_theory.category C]
(f : 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)]
(m n : simplex_categoryᵒᵖ)
(g : m ⟶ n) :
f.cech_nerve.map g = 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)) _
@[simp]
theorem
category_theory.arrow.cech_nerve_obj
{C : Type u}
[category_theory.category C]
(f : 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 : simplex_categoryᵒᵖ) :
f.cech_nerve.obj n = 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)
@[simp]
theorem
category_theory.arrow.map_cech_nerve_app
{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)
(n : simplex_categoryᵒᵖ) :
(category_theory.arrow.map_cech_nerve F).app n = 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) _
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) :
f.cech_nerve ⟶ g.cech_nerve
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' := _}
@[simp]
theorem
category_theory.arrow.augmented_cech_nerve_hom_app
{C : Type u}
[category_theory.category C]
(f : 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)]
(i : simplex_categoryᵒᵖ) :
f.augmented_cech_nerve.hom.app i = category_theory.limits.wide_pullback.base (λ (i : fin ((opposite.unop i).len + 1)), f.hom)
noncomputable
def
category_theory.arrow.augmented_cech_nerve
{C : Type u}
[category_theory.category C]
(f : 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)] :
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' := _}}
@[simp]
theorem
category_theory.arrow.augmented_cech_nerve_left
{C : Type u}
[category_theory.category C]
(f : 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)] :
@[simp]
theorem
category_theory.arrow.augmented_cech_nerve_right
{C : Type u}
[category_theory.category C]
(f : 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)] :
@[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 : 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) :
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
- category_theory.arrow.map_augmented_cech_nerve F = {left := category_theory.arrow.map_cech_nerve F, right := F.right, w' := _}
@[simp]
theorem
category_theory.arrow.map_augmented_cech_nerve_left
{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) :
noncomputable
def
category_theory.simplicial_object.cech_nerve
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :
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' := _}
@[simp]
theorem
category_theory.simplicial_object.cech_nerve_map
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)] :
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' := _}
@[simp]
theorem
category_theory.simplicial_object.augmented_cech_nerve_map
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : X ⟶ F.augmented_cech_nerve) :
(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
@[simp]
theorem
category_theory.simplicial_object.equivalence_right_to_left_right
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : X ⟶ F.augmented_cech_nerve) :
noncomputable
def
category_theory.simplicial_object.equivalence_right_to_left
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : X ⟶ F.augmented_cech_nerve) :
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' := _}
@[simp]
theorem
category_theory.simplicial_object.equivalence_left_to_right_right
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : category_theory.simplicial_object.augmented.to_arrow.obj X ⟶ F) :
noncomputable
def
category_theory.simplicial_object.equivalence_left_to_right
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : category_theory.simplicial_object.augmented.to_arrow.obj X ⟶ F) :
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' := _}
@[simp]
theorem
category_theory.simplicial_object.equivalence_left_to_right_left_app
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : category_theory.simplicial_object.augmented.to_arrow.obj X ⟶ F)
(x : simplex_categoryᵒᵖ) :
(category_theory.simplicial_object.equivalence_left_to_right X F G).left.app x = 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) _
@[simp]
theorem
category_theory.simplicial_object.cech_nerve_equiv_apply
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : category_theory.simplicial_object.augmented.to_arrow.obj X ⟶ F) :
@[simp]
theorem
category_theory.simplicial_object.cech_nerve_equiv_symm_apply
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C)
(G : X ⟶ F.augmented_cech_nerve) :
noncomputable
def
category_theory.simplicial_object.cech_nerve_equiv
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (i : fin (n + 1)), f.left) (λ (i : fin (n + 1)), f.hom)]
(X : category_theory.simplicial_object.augmented C)
(F : category_theory.arrow C) :
A helper function used in defining the Čech adjunction.
@[reducible]
noncomputable
def
category_theory.simplicial_object.cech_nerve_adjunction
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pullback f.right (λ (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}
[category_theory.category C]
(f : 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 : simplex_category) :
noncomputable
def
category_theory.arrow.cech_conerve
{C : Type u}
[category_theory.category C]
(f : 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)] :
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' := _}
@[simp]
theorem
category_theory.arrow.cech_conerve_map
{C : Type u}
[category_theory.category C]
(f : 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)]
(m n : simplex_category)
(g : m ⟶ n) :
f.cech_conerve.map g = 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)) _
@[simp]
theorem
category_theory.arrow.map_cech_conerve_app
{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)
(n : simplex_category) :
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
- 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' := _}
noncomputable
def
category_theory.arrow.augmented_cech_conerve
{C : Type u}
[category_theory.category C]
(f : 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)] :
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' := _}}
@[simp]
theorem
category_theory.arrow.augmented_cech_conerve_hom_app
{C : Type u}
[category_theory.category C]
(f : 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)]
(i : simplex_category) :
f.augmented_cech_conerve.hom.app i = category_theory.limits.wide_pushout.head (λ (i : fin (i.len + 1)), f.hom)
@[simp]
theorem
category_theory.arrow.augmented_cech_conerve_right
{C : Type u}
[category_theory.category C]
(f : 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)] :
@[simp]
theorem
category_theory.arrow.augmented_cech_conerve_left
{C : Type u}
[category_theory.category C]
(f : 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)] :
@[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 : 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) :
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
- category_theory.arrow.map_augmented_cech_conerve F = {left := F.left, right := category_theory.arrow.map_cech_conerve F, w' := _}
@[simp]
theorem
category_theory.arrow.map_augmented_cech_conerve_right
{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) :
@[simp]
theorem
category_theory.cosimplicial_object.cech_conerve_obj
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :
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' := _}
@[simp]
theorem
category_theory.cosimplicial_object.augmented_cech_conerve_map
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (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}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)] :
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' := _}
@[simp]
theorem
category_theory.cosimplicial_object.equivalence_left_to_right_right
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F.augmented_cech_conerve ⟶ X) :
(category_theory.cosimplicial_object.equivalence_left_to_right F X G).right = category_theory.limits.wide_pushout.ι (λ (i : fin ((simplex_category.mk 0).len + 1)), F.hom) 0 ≫ G.right.app (simplex_category.mk 0)
@[simp]
theorem
category_theory.cosimplicial_object.equivalence_left_to_right_left
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F.augmented_cech_conerve ⟶ X) :
noncomputable
def
category_theory.cosimplicial_object.equivalence_left_to_right
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F.augmented_cech_conerve ⟶ X) :
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' := _}
noncomputable
def
category_theory.cosimplicial_object.equivalence_right_to_left
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F ⟶ category_theory.cosimplicial_object.augmented.to_arrow.obj X) :
A helper function used in defining the Čech conerve adjunction.
@[simp]
theorem
category_theory.cosimplicial_object.equivalence_right_to_left_right_app
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F ⟶ category_theory.cosimplicial_object.augmented.to_arrow.obj X)
(x : simplex_category) :
@[simp]
theorem
category_theory.cosimplicial_object.equivalence_right_to_left_left
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F ⟶ category_theory.cosimplicial_object.augmented.to_arrow.obj X) :
@[simp]
theorem
category_theory.cosimplicial_object.cech_conerve_equiv_apply
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F.augmented_cech_conerve ⟶ X) :
noncomputable
def
category_theory.cosimplicial_object.cech_conerve_equiv
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C) :
A helper function used in defining the Čech conerve adjunction.
@[simp]
theorem
category_theory.cosimplicial_object.cech_conerve_equiv_symm_apply
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (i : fin (n + 1)), f.right) (λ (i : fin (n + 1)), f.hom)]
(F : category_theory.arrow C)
(X : category_theory.cosimplicial_object.augmented C)
(G : F ⟶ category_theory.cosimplicial_object.augmented.to_arrow.obj X) :
@[reducible]
noncomputable
def
category_theory.cosimplicial_object.cech_conerve_adjunction
{C : Type u}
[category_theory.category C]
[∀ (n : ℕ) (f : category_theory.arrow C), category_theory.limits.has_wide_pushout f.left (λ (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}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
(X : C) :
Given an object X : C, the natural simplicial object sending [n] to Xⁿ⁺¹.
Equations
- category_theory.cech_nerve_terminal_from X = {obj := λ (n : simplex_categoryᵒᵖ), ∏ λ (i : fin ((opposite.unop n).len + 1)), X, map := λ (m n : simplex_categoryᵒᵖ) (f : m ⟶ n), category_theory.limits.pi.lift (λ (i : fin ((opposite.unop n).len + 1)), category_theory.limits.pi.π (λ (i : fin ((opposite.unop m).len + 1)), X) (⇑(simplex_category.hom.to_order_hom f.unop) i)), map_id' := _, map_comp' := _}
noncomputable
def
category_theory.cech_nerve_terminal_from.wide_cospan
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(ι : Type w)
(X : C) :
The diagram option ι ⥤ C sending none to the terminal object and some j to X.
Equations
- category_theory.cech_nerve_terminal_from.wide_cospan ι X = category_theory.limits.wide_pullback_shape.wide_cospan (⊤_ C) (λ (i : ι), X) (λ (i : ι), category_theory.limits.terminal.from X)
@[protected, instance]
noncomputable
def
category_theory.cech_nerve_terminal_from.unique_to_wide_cospan_none
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(ι : Type w)
(X Y : C) :
noncomputable
def
category_theory.cech_nerve_terminal_from.wide_cospan.limit_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(ι : Type w)
[category_theory.limits.has_finite_products C]
[fintype ι]
(X : C) :
The product Xᶥ is the vertex of a limit cone on wide_cospan ι X.
Equations
- category_theory.cech_nerve_terminal_from.wide_cospan.limit_cone ι X = {cone := {X := ∏ λ (i : ι), X, π := {app := λ (X_1 : category_theory.limits.wide_pullback_shape ι), option.cases_on X_1 (category_theory.limits.terminal.from (((category_theory.functor.const (category_theory.limits.wide_pullback_shape ι)).obj (∏ λ (i : ι), X)).obj option.none)) (λ (i : ι), category_theory.limits.limit.π (category_theory.discrete.functor (λ (i : ι), X)) {as := i}), naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.cech_nerve_terminal_from.wide_cospan ι X)), category_theory.limits.pi.lift (λ (j : ι), s.π.app (option.some j)), fac' := _, uniq' := _}}
@[protected, instance]
def
category_theory.cech_nerve_terminal_from.has_wide_pullback
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(ι : Type w)
[category_theory.limits.has_finite_products C]
[finite ι]
(X : C) :
noncomputable
def
category_theory.cech_nerve_terminal_from.iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_finite_products C]
(X : C) :
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
- category_theory.cech_nerve_terminal_from.iso X = (category_theory.nat_iso.of_components (λ (m : simplex_categoryᵒᵖ), ((category_theory.limits.limit.is_limit (category_theory.cech_nerve_terminal_from.wide_cospan (fin ((opposite.unop m).len + 1)) X)).cone_point_unique_up_to_iso (category_theory.cech_nerve_terminal_from.wide_cospan.limit_cone (fin ((opposite.unop m).len + 1)) X).is_limit).symm) _).symm