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:

1. f.cechNerve is the Čech nerve, considered as a simplicial object in C.
2. f.augmentedCechNerve is the augmented Čech nerve, considered as an augmented simplicial object in C.
3. SimplicialObject.cechNerve and SimplicialObject.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.

@[simp]

theorem CategoryTheory.Arrow.cechNerve_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (n : SimplexCategoryᵒᵖ) : (CategoryTheory.Arrow.cechNerve f).obj n = CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom

@[simp]

theorem CategoryTheory.Arrow.cechNerve_map {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : ∀ {X Y : SimplexCategoryᵒᵖ} (g : X ⟶ Y), (CategoryTheory.Arrow.cechNerve f).map g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g.unop) i)) (_ : ∀ (j : Fin (SimplexCategory.len Y.unop + 1)), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g.unop) j)) f.hom = CategoryTheory.Limits.WidePullback.base fun x => f.hom)

def CategoryTheory.Arrow.cechNerve {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.SimplicialObject C

The Čech nerve associated to an arrow.

@[simp]

theorem CategoryTheory.Arrow.mapCechNerve_app {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.Arrow.mapCechNerve F).app n = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) F.right) (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i) F.left) (_ : ∀ (j : Fin (SimplexCategory.len n.unop + 1)), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) j) F.left) g.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) F.right)

def CategoryTheory.Arrow.mapCechNerve {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : CategoryTheory.Arrow.cechNerve f ⟶ CategoryTheory.Arrow.cechNerve g

The morphism between Čech nerves associated to a morphism of arrows.

@[simp]

theorem CategoryTheory.Arrow.augmentedCechNerve_left {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : (CategoryTheory.Arrow.augmentedCechNerve f).left = CategoryTheory.Arrow.cechNerve f

@[simp]

theorem CategoryTheory.Arrow.augmentedCechNerve_right {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : (CategoryTheory.Arrow.augmentedCechNerve f).right = f.right

@[simp]

theorem CategoryTheory.Arrow.augmentedCechNerve_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (i : SimplexCategoryᵒᵖ) : (CategoryTheory.Arrow.augmentedCechNerve f).hom.app i = CategoryTheory.Limits.WidePullback.base fun x => f.hom

def CategoryTheory.Arrow.augmentedCechNerve {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.SimplicialObject.Augmented C

The augmented Čech nerve associated to an arrow.

@[simp]

theorem CategoryTheory.Arrow.mapAugmentedCechNerve_left {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechNerve F).left = CategoryTheory.Arrow.mapCechNerve F

@[simp]

theorem CategoryTheory.Arrow.mapAugmentedCechNerve_right {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechNerve F).right = F.right

def CategoryTheory.Arrow.mapAugmentedCechNerve {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : CategoryTheory.Arrow.augmentedCechNerve f ⟶ CategoryTheory.Arrow.augmentedCechNerve g

The morphism between augmented Čech nerve associated to a morphism of arrows.

@[simp]

theorem CategoryTheory.SimplicialObject.cechNerve_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) : CategoryTheory.SimplicialObject.cechNerve.obj f = CategoryTheory.Arrow.cechNerve f

@[simp]

theorem CategoryTheory.SimplicialObject.cechNerve_map {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : ∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), CategoryTheory.SimplicialObject.cechNerve.map F = CategoryTheory.Arrow.mapCechNerve F

def CategoryTheory.SimplicialObject.cechNerve {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.SimplicialObject C)

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

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_map_right {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : ∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).right = F.right

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) (i : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).hom.app i = CategoryTheory.Limits.WidePullback.base fun x => f.hom

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) : ∀ {X Y : SimplexCategoryᵒᵖ} (g : X ⟶ Y), (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.map g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g.unop) i)) (_ : ∀ (j : Fin (SimplexCategory.len Y.unop + 1)), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g.unop) j)) f.hom = CategoryTheory.Limits.WidePullback.base fun x => f.hom)

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.obj n = CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).right = f.right

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : ∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y) (n : SimplexCategoryᵒᵖ), (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).left.app n = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => X.hom) F.right) (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => X.hom) i) F.left) (_ : ∀ (j : Fin (SimplexCategory.len n.unop + 1)), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => X.hom) j) F.left) Y.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => X.hom) F.right)

def CategoryTheory.SimplicialObject.augmentedCechNerve {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.SimplicialObject.Augmented C)

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

@[simp]

theorem CategoryTheory.SimplicialObject.equivalenceRightToLeft_right {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ CategoryTheory.Arrow.augmentedCechNerve F) : (CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).right = G.right

@[simp]

theorem CategoryTheory.SimplicialObject.equivalenceRightToLeft_left {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ CategoryTheory.Arrow.augmentedCechNerve F) : (CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).left = CategoryTheory.CategoryStruct.comp (G.left.app (Opposite.op (SimplexCategory.mk 0))) (CategoryTheory.Limits.WidePullback.π (fun x => F.hom) 0)

def CategoryTheory.SimplicialObject.equivalenceRightToLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ CategoryTheory.Arrow.augmentedCechNerve F) : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F

A helper function used in defining the Čech adjunction.

@[simp]

theorem CategoryTheory.SimplicialObject.equivalenceLeftToRight_right {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) : (CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).right = G.right

@[simp]

theorem CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) (x : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).left.app x = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp (X.hom.app x) G.right) (fun i => CategoryTheory.CategoryStruct.comp (X.left.map (SimplexCategory.const x.unop i).op) G.left) (_ : ∀ (i : Fin (SimplexCategory.len x.unop + 1)), CategoryTheory.CategoryStruct.comp ((fun i => CategoryTheory.CategoryStruct.comp (X.left.map (SimplexCategory.const x.unop i).op) G.left) i) F.hom = CategoryTheory.CategoryStruct.comp (X.hom.app x) G.right)

def CategoryTheory.SimplicialObject.equivalenceLeftToRight {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) : X ⟶ CategoryTheory.Arrow.augmentedCechNerve F

A helper function used in defining the Čech adjunction.

@[simp]

theorem CategoryTheory.SimplicialObject.cechNerveEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) : ↑(CategoryTheory.SimplicialObject.cechNerveEquiv X F) G = CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G

@[simp]

theorem CategoryTheory.SimplicialObject.cechNerveEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ CategoryTheory.Arrow.augmentedCechNerve F) : ↑(CategoryTheory.SimplicialObject.cechNerveEquiv X F).symm G = CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G

def CategoryTheory.SimplicialObject.cechNerveEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) : (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) ≃ (X ⟶ CategoryTheory.Arrow.augmentedCechNerve F)

A helper function used in defining the Čech adjunction.

@[inline, reducible]

abbrev CategoryTheory.SimplicialObject.cechNerveAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.SimplicialObject.Augmented.toArrow ⊣ CategoryTheory.SimplicialObject.augmentedCechNerve

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

@[simp]

theorem CategoryTheory.Arrow.cechConerve_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (n : SimplexCategory) : (CategoryTheory.Arrow.cechConerve f).obj n = CategoryTheory.Limits.widePushout f.left (fun x => f.right) fun x => f.hom

@[simp]

theorem CategoryTheory.Arrow.cechConerve_map {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] {x : SimplexCategory} {y : SimplexCategory} (g : x ⟶ y) : (CategoryTheory.Arrow.cechConerve f).map g = CategoryTheory.Limits.WidePushout.desc (CategoryTheory.Limits.WidePushout.head fun x => f.hom) (fun i => CategoryTheory.Limits.WidePushout.ι (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g) i)) (_ : ∀ (j : Fin (SimplexCategory.len x + 1)), CategoryTheory.CategoryStruct.comp f.hom ((fun i => CategoryTheory.Limits.WidePushout.ι (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g) i)) j) = CategoryTheory.Limits.WidePushout.head fun x => f.hom)

def CategoryTheory.Arrow.cechConerve {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : CategoryTheory.CosimplicialObject C

The Čech conerve associated to an arrow.

@[simp]

theorem CategoryTheory.Arrow.mapCechConerve_app {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g) (n : SimplexCategory) : (CategoryTheory.Arrow.mapCechConerve F).app n = CategoryTheory.Limits.WidePushout.desc (CategoryTheory.CategoryStruct.comp F.left (CategoryTheory.Limits.WidePushout.head fun x => g.hom)) (fun i => CategoryTheory.CategoryStruct.comp F.right (CategoryTheory.Limits.WidePushout.ι (fun x => g.hom) i)) (_ : ∀ (i : Fin (SimplexCategory.len n + 1)), CategoryTheory.CategoryStruct.comp f.hom ((fun i => CategoryTheory.CategoryStruct.comp F.right (CategoryTheory.Limits.WidePushout.ι (fun x => g.hom) i)) i) = CategoryTheory.CategoryStruct.comp F.left (CategoryTheory.Limits.WidePushout.head fun x => g.hom))

def CategoryTheory.Arrow.mapCechConerve {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g) : CategoryTheory.Arrow.cechConerve f ⟶ CategoryTheory.Arrow.cechConerve g

The morphism between Čech conerves associated to a morphism of arrows.

@[simp]

theorem CategoryTheory.Arrow.augmentedCechConerve_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (i : SimplexCategory) : (CategoryTheory.Arrow.augmentedCechConerve f).hom.app i = CategoryTheory.Limits.WidePushout.head fun x => f.hom

@[simp]

theorem CategoryTheory.Arrow.augmentedCechConerve_right {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : (CategoryTheory.Arrow.augmentedCechConerve f).right = CategoryTheory.Arrow.cechConerve f

@[simp]

theorem CategoryTheory.Arrow.augmentedCechConerve_left {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : (CategoryTheory.Arrow.augmentedCechConerve f).left = f.left

def CategoryTheory.Arrow.augmentedCechConerve {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : CategoryTheory.CosimplicialObject.Augmented C

The augmented Čech conerve associated to an arrow.

@[simp]

theorem CategoryTheory.Arrow.mapAugmentedCechConerve_right {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechConerve F).right = CategoryTheory.Arrow.mapCechConerve F

@[simp]

theorem CategoryTheory.Arrow.mapAugmentedCechConerve_left {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechConerve F).left = F.left

def CategoryTheory.Arrow.mapAugmentedCechConerve {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g) : CategoryTheory.Arrow.augmentedCechConerve f ⟶ CategoryTheory.Arrow.augmentedCechConerve g

The morphism between augmented Čech conerves associated to a morphism of arrows.

@[simp]

theorem CategoryTheory.CosimplicialObject.cechConerve_map {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : ∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), CategoryTheory.CosimplicialObject.cechConerve.map F = CategoryTheory.Arrow.mapCechConerve F

@[simp]

theorem CategoryTheory.CosimplicialObject.cechConerve_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (f : CategoryTheory.Arrow C) : CategoryTheory.CosimplicialObject.cechConerve.obj f = CategoryTheory.Arrow.cechConerve f

def CategoryTheory.CosimplicialObject.cechConerve {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.CosimplicialObject C)

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

@[simp]

theorem CategoryTheory.CosimplicialObject.augmentedCechConerve_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (f : CategoryTheory.Arrow C) : CategoryTheory.CosimplicialObject.augmentedCechConerve.obj f = CategoryTheory.Arrow.augmentedCechConerve f

@[simp]

theorem CategoryTheory.CosimplicialObject.augmentedCechConerve_map {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : ∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), CategoryTheory.CosimplicialObject.augmentedCechConerve.map F = CategoryTheory.Arrow.mapAugmentedCechConerve F

def CategoryTheory.CosimplicialObject.augmentedCechConerve {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.CosimplicialObject.Augmented C)

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

@[simp]

theorem CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : CategoryTheory.Arrow.augmentedCechConerve F ⟶ X) : (CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).right = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι (fun x => F.hom) 0) (G.right.app (SimplexCategory.mk 0))

@[simp]

theorem CategoryTheory.CosimplicialObject.equivalenceLeftToRight_left {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : CategoryTheory.Arrow.augmentedCechConerve F ⟶ X) : (CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).left = G.left

def CategoryTheory.CosimplicialObject.equivalenceLeftToRight {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : CategoryTheory.Arrow.augmentedCechConerve F ⟶ X) : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X

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

@[simp]

theorem CategoryTheory.CosimplicialObject.equivalenceRightToLeft_left {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X) : (CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G).left = G.left

@[simp]

theorem CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X) (x : SimplexCategory) : (CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G).right.app x = CategoryTheory.Limits.WidePushout.desc (CategoryTheory.CategoryStruct.comp G.left (X.hom.app x)) (fun i => CategoryTheory.CategoryStruct.comp G.right (X.right.map (SimplexCategory.const x i))) (_ : ∀ (j : Fin (SimplexCategory.len x + 1)), CategoryTheory.CategoryStruct.comp F.hom ((fun i => CategoryTheory.CategoryStruct.comp G.right (X.right.map (SimplexCategory.const x i))) j) = CategoryTheory.CategoryStruct.comp G.left (X.hom.app x))

def CategoryTheory.CosimplicialObject.equivalenceRightToLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X) : CategoryTheory.Arrow.augmentedCechConerve F ⟶ X

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

@[simp]

theorem CategoryTheory.CosimplicialObject.cechConerveEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X) : ↑(CategoryTheory.CosimplicialObject.cechConerveEquiv F X).symm G = CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G

@[simp]

theorem CategoryTheory.CosimplicialObject.cechConerveEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : CategoryTheory.Arrow.augmentedCechConerve F ⟶ X) : ↑(CategoryTheory.CosimplicialObject.cechConerveEquiv F X) G = CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G

def CategoryTheory.CosimplicialObject.cechConerveEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) : (CategoryTheory.Arrow.augmentedCechConerve F ⟶ X) ≃ (F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X)

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

@[inline, reducible]

abbrev CategoryTheory.CosimplicialObject.cechConerveAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] : CategoryTheory.CosimplicialObject.augmentedCechConerve ⊣ CategoryTheory.CosimplicialObject.Augmented.toArrow

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

def CategoryTheory.cechNerveTerminalFrom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (X : C) : CategoryTheory.SimplicialObject C

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

def CategoryTheory.CechNerveTerminalFrom.wideCospan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) (X : C) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C

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

instance CategoryTheory.CechNerveTerminalFrom.uniqueToWideCospanNone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) (X : C) (Y : C) : Unique (Y ⟶ (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X).obj none)

def CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.LimitCone (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)

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

instance CategoryTheory.CechNerveTerminalFrom.hasWidePullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasWidePullback (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).right (fun x => (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).left) fun x => (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).hom

instance CategoryTheory.CechNerveTerminalFrom.hasWidePullback' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasWidePullback (⊤_ C) (fun x => X) fun x => CategoryTheory.Limits.terminal.from X

instance CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasLimit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)

def CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.limit (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X) ≅ ∏ fun x => X

the isomorphism to the product induced by the limit cone wideCospan ι X

@[simp]

theorem CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h

@[simp]

theorem CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) = CategoryTheory.Limits.Pi.π (fun x => X) j

@[simp]

theorem CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h

@[simp]

theorem CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_hom_comp_pi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom (CategoryTheory.Limits.Pi.π (fun x => X) j) = CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j

def CategoryTheory.CechNerveTerminalFrom.iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasFiniteProducts C] (X : C) : CategoryTheory.Arrow.cechNerve (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)) ≅ CategoryTheory.cechNerveTerminalFrom X

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.