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.

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

The Čech nerve associated to an arrow.

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] {X✝ Y✝ : SimplexCategoryᵒᵖ} (g : X✝ ⟶ Y✝) : f.cechNerve.map g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun (x : Fin ((Opposite.unop X✝).len + 1)) => f.hom) (fun (i : Fin ((Opposite.unop Y✝).len + 1)) => CategoryTheory.Limits.WidePullback.π (fun (x : Fin ((Opposite.unop X✝).len + 1)) => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (n : SimplexCategoryᵒᵖ) : f.cechNerve.obj n = CategoryTheory.Limits.widePullback f.right (fun (x : Fin ((Opposite.unop n).len + 1)) => f.left) fun (x : Fin ((Opposite.unop n).len + 1)) => f.hom

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Arrow.mapCechNerve_app {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => 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 : Fin ((Opposite.unop n).len + 1)) => f.hom) F.right) (fun (i : Fin ((Opposite.unop n).len + 1)) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun (x : Fin ((Opposite.unop n).len + 1)) => f.hom) i) F.left) ⋯

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

The augmented Čech nerve associated to an arrow.

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] : f.augmentedCechNerve.right = f.right

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] : f.augmentedCechNerve.left = f.cechNerve

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (x✝ : SimplexCategoryᵒᵖ) : f.augmentedCechNerve.hom.app x✝ = CategoryTheory.Limits.WidePullback.base fun (x : Fin ((Opposite.unop x✝).len + 1)) => f.hom

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

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

Equations

• CategoryTheory.Arrow.mapAugmentedCechNerve F = { left := CategoryTheory.Arrow.mapCechNerve F, right := F.right, w := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.mapAugmentedCechNerve_left {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => 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 g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechNerve F).right = F.right

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] {X✝ Y✝ : CategoryTheory.Arrow C} (F : X✝ ⟶ Y✝) : CategoryTheory.SimplicialObject.cechNerve.map F = CategoryTheory.Arrow.mapCechNerve F

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (f : CategoryTheory.Arrow C) : CategoryTheory.SimplicialObject.cechNerve.obj f = f.cechNerve

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (f : CategoryTheory.Arrow C) (x✝ : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).hom.app x✝ = CategoryTheory.Limits.WidePullback.base fun (x : Fin ((Opposite.unop x✝).len + 1)) => 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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => 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 : Fin ((Opposite.unop X✝).len + 1)) => f.hom) (fun (i : Fin ((Opposite.unop Y✝).len + 1)) => CategoryTheory.Limits.WidePullback.π (fun (x : Fin ((Opposite.unop X✝).len + 1)) => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => 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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => 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 : Fin ((Opposite.unop n).len + 1)) => X✝.hom) F.right) (fun (i : Fin ((Opposite.unop n).len + 1)) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun (x : Fin ((Opposite.unop n).len + 1)) => X✝.hom) i) F.left) ⋯

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] {X✝ Y✝ : CategoryTheory.Arrow C} (F : X✝ ⟶ Y✝) : (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).right = F.right

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (f : CategoryTheory.Arrow C) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.obj n = CategoryTheory.Limits.widePullback f.right (fun (x : Fin ((Opposite.unop n).len + 1)) => f.left) fun (x : Fin ((Opposite.unop n).len + 1)) => f.hom

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

A helper function used in defining the Čech adjunction.

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve) : (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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve) : (CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).left = CategoryTheory.CategoryStruct.comp (G.left.app (Opposite.op (SimplexCategory.mk 0))) (CategoryTheory.Limits.WidePullback.π (fun (x : Fin ((Opposite.unop (Opposite.op (SimplexCategory.mk 0))).len + 1)) => F.hom) 0)

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

A helper function used in defining the Čech adjunction.

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => 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 : Fin ((Opposite.unop x).len + 1)) => CategoryTheory.CategoryStruct.comp (X.left.map ((SimplexCategory.mk 0).const (Opposite.unop x) i).op) G.left) ⋯

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => 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

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

A helper function used in defining the Čech adjunction.

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve) : (CategoryTheory.SimplicialObject.cechNerveEquiv X F).symm G = CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G

@[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 : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => 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

@[reducible, inline]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The Čech conerve associated to an arrow.

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] {x y : SimplexCategory} (g : x ⟶ y) : f.cechConerve.map g = CategoryTheory.Limits.WidePushout.desc (CategoryTheory.Limits.WidePushout.head fun (x : Fin (y.len + 1)) => f.hom) (fun (i : Fin (x.len + 1)) => CategoryTheory.Limits.WidePushout.ι (fun (x : Fin (y.len + 1)) => f.hom) ((SimplexCategory.Hom.toOrderHom g) i)) ⋯

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (n : SimplexCategory) : f.cechConerve.obj n = CategoryTheory.Limits.widePushout f.left (fun (x : Fin (n.len + 1)) => f.right) fun (x : Fin (n.len + 1)) => f.hom

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Arrow.mapCechConerve_app {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun (x : Fin (n + 1)) => g.right) fun (x : Fin (n + 1)) => 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 : Fin (n.len + 1)) => g.hom)) (fun (i : Fin (n.len + 1)) => CategoryTheory.CategoryStruct.comp F.right (CategoryTheory.Limits.WidePushout.ι (fun (x : Fin (n.len + 1)) => g.hom) i)) ⋯

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

The augmented Čech conerve associated to an arrow.

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (x✝ : SimplexCategory) : f.augmentedCechConerve.hom.app x✝ = CategoryTheory.Limits.WidePushout.head fun (x : Fin (x✝.len + 1)) => f.hom

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] : f.augmentedCechConerve.left = f.left

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] : f.augmentedCechConerve.right = f.cechConerve

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

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

Equations

• CategoryTheory.Arrow.mapAugmentedCechConerve F = { left := F.left, right := CategoryTheory.Arrow.mapCechConerve F, w := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.mapAugmentedCechConerve_right {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun (x : Fin (n + 1)) => g.right) fun (x : Fin (n + 1)) => 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 g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun (x : Fin (n + 1)) => g.right) fun (x : Fin (n + 1)) => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechConerve F).left = F.left

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (f : CategoryTheory.Arrow C) : CategoryTheory.CosimplicialObject.cechConerve.obj f = f.cechConerve

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] {X✝ Y✝ : CategoryTheory.Arrow C} (F : X✝ ⟶ Y✝) : CategoryTheory.CosimplicialObject.cechConerve.map F = CategoryTheory.Arrow.mapCechConerve 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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.CosimplicialObject.Augmented C)

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (f : CategoryTheory.Arrow C) : CategoryTheory.CosimplicialObject.augmentedCechConerve.obj f = f.augmentedCechConerve

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] {X✝ Y✝ : CategoryTheory.Arrow C} (F : X✝ ⟶ Y✝) : CategoryTheory.CosimplicialObject.augmentedCechConerve.map F = CategoryTheory.Arrow.mapAugmentedCechConerve F

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F.augmentedCechConerve ⟶ X) : (CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).right = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι (fun (x : Fin ((SimplexCategory.mk 0).len + 1)) => 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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F.augmentedCechConerve ⟶ X) : (CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).left = G.left

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => 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 : Fin (x.len + 1)) => CategoryTheory.CategoryStruct.comp G.right (X.right.map ((SimplexCategory.mk 0).const x i))) ⋯

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => 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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => 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 : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F.augmentedCechConerve ⟶ X) : (CategoryTheory.CosimplicialObject.cechConerveEquiv F X) G = CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G

@[reducible, inline]

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

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

Equations

• One or more equations did not get rendered due to their size.

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ⁿ⁺¹.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CategoryTheory.CechNerveTerminalFrom.wideCospan ι X = CategoryTheory.Limits.WidePullbackShape.wideCospan (⊤_ C) (fun (x : ι) => X) fun (x : ι) => CategoryTheory.Limits.terminal.from X

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

Equations

• CategoryTheory.CechNerveTerminalFrom.uniqueToWideCospanNone ι X Y = id inferInstance

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

@[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_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_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

@[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

def CategoryTheory.CechNerveTerminalFrom.iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasFiniteProducts C] (X : C) : (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).cechNerve ≅ 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.

Equations

• One or more equations did not get rendered due to their size.