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_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.
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.