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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] : 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), 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 = Limits.WidePullback.lift (Limits.WidePullback.base fun (x : Fin ((Opposite.unop X✝).len + 1)) => f.hom) (fun (i : Fin ((Opposite.unop Y✝).len + 1)) => 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (n : SimplexCategoryᵒᵖ) : f.cechNerve.obj n = 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} [Category.{v, u} C] {f g : Arrow C} [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), 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} [Category.{v, u} C] {f g : Arrow C} [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => g.hom] (F : f ⟶ g) (n : SimplexCategoryᵒᵖ) : (mapCechNerve F).app n = Limits.WidePullback.lift (CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin ((Opposite.unop n).len + 1)) => f.hom) F.right) (fun (i : Fin ((Opposite.unop n).len + 1)) => CategoryStruct.comp (Limits.WidePullback.π (fun (x : Fin ((Opposite.unop n).len + 1)) => f.hom) i) F.left) ⋯

def CategoryTheory.Arrow.augmentedCechNerve {C : Type u} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] : 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), 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✝ = Limits.WidePullback.base fun (x : Fin ((Opposite.unop x✝).len + 1)) => f.hom

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

@[simp]

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

def CategoryTheory.SimplicialObject.cechNerve {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] : Functor (Arrow C) (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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] {X✝ Y✝ : Arrow C} (F : X✝ ⟶ Y✝) : cechNerve.map F = Arrow.mapCechNerve F

@[simp]

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

def CategoryTheory.SimplicialObject.augmentedCechNerve {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] : Functor (Arrow C) (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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (f : Arrow C) (x✝ : SimplexCategoryᵒᵖ) : (augmentedCechNerve.obj f).hom.app x✝ = Limits.WidePullback.base fun (x : Fin ((Opposite.unop x✝).len + 1)) => f.hom

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (f : Arrow C) {X✝ Y✝ : SimplexCategoryᵒᵖ} (g : X✝ ⟶ Y✝) : (augmentedCechNerve.obj f).left.map g = Limits.WidePullback.lift (Limits.WidePullback.base fun (x : Fin ((Opposite.unop X✝).len + 1)) => f.hom) (fun (i : Fin ((Opposite.unop Y✝).len + 1)) => 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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (f : Arrow C) : (augmentedCechNerve.obj f).right = f.right

@[simp]

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

@[simp]

theorem CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (f : Arrow C) (n : SimplexCategoryᵒᵖ) : (augmentedCechNerve.obj f).left.obj n = 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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : Augmented C) (F : Arrow C) (G : X ⟶ F.augmentedCechNerve) : 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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : Augmented C) (F : Arrow C) (G : X ⟶ F.augmentedCechNerve) : (equivalenceRightToLeft X F G).right = G.right

@[simp]

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

def CategoryTheory.SimplicialObject.equivalenceLeftToRight {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : Augmented C) (F : Arrow C) (G : 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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : Augmented C) (F : Arrow C) (G : Augmented.toArrow.obj X ⟶ F) (x : SimplexCategoryᵒᵖ) : (equivalenceLeftToRight X F G).left.app x = Limits.WidePullback.lift (CategoryStruct.comp (X.hom.app x) G.right) (fun (i : Fin ((Opposite.unop x).len + 1)) => 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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : Augmented C) (F : Arrow C) (G : Augmented.toArrow.obj X ⟶ F) : (equivalenceLeftToRight X F G).right = G.right

def CategoryTheory.SimplicialObject.cechNerveEquiv {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : Augmented C) (F : Arrow C) : (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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (X : Augmented C) (F : Arrow C) (G : X ⟶ F.augmentedCechNerve) : (cechNerveEquiv X F).symm G = equivalenceRightToLeft X F G

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.SimplicialObject.cechNerveAdjunction {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] : Augmented.toArrow ⊣ 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] : 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), 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 = Limits.WidePushout.desc (Limits.WidePushout.head fun (x : Fin (y.len + 1)) => f.hom) (fun (i : Fin (x.len + 1)) => Limits.WidePushout.ι (fun (x : Fin (y.len + 1)) => f.hom) ((SimplexCategory.Hom.toOrderHom g) i)) ⋯

@[simp]

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

def CategoryTheory.Arrow.augmentedCechConerve {C : Type u} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] : 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} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), 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✝ = Limits.WidePushout.head fun (x : Fin (x✝.len + 1)) => f.hom

@[simp]

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

@[simp]

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

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

@[simp]

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

def CategoryTheory.CosimplicialObject.augmentedCechConerve {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] : Functor (Arrow C) (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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (f : Arrow C) : augmentedCechConerve.obj f = f.augmentedCechConerve

@[simp]

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

def CategoryTheory.CosimplicialObject.equivalenceLeftToRight {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : Arrow C) (X : Augmented C) (G : F.augmentedCechConerve ⟶ X) : F ⟶ 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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : Arrow C) (X : Augmented C) (G : F.augmentedCechConerve ⟶ X) : (equivalenceLeftToRight F X G).right = CategoryStruct.comp (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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : Arrow C) (X : Augmented C) (G : F.augmentedCechConerve ⟶ X) : (equivalenceLeftToRight F X G).left = G.left

def CategoryTheory.CosimplicialObject.equivalenceRightToLeft {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : Arrow C) (X : Augmented C) (G : F ⟶ 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} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] (F : Arrow C) (X : Augmented C) (G : F ⟶ Augmented.toArrow.obj X) (x : SimplexCategory) : (equivalenceRightToLeft F X G).right.app x = Limits.WidePushout.desc (CategoryStruct.comp G.left (X.hom.app x)) (fun (i : Fin (x.len + 1)) => CategoryStruct.comp G.right (X.right.map ((SimplexCategory.mk 0).const x i))) ⋯

@[simp]

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

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

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.CosimplicialObject.cechConerveAdjunction {C : Type u} [Category.{v, u} C] [∀ (n : ℕ) (f : Arrow C), Limits.HasWidePushout f.left (fun (x : Fin (n + 1)) => f.right) fun (x : Fin (n + 1)) => f.hom] : augmentedCechConerve ⊣ 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} [Category.{v, u} C] [Limits.HasFiniteProducts C] (X : C) : 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} [Category.{v, u} C] [Limits.HasTerminal C] (ι : Type w) (X : C) : Functor (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} [Category.{v, u} C] [Limits.HasTerminal C] (ι : Type w) (X Y : C) : Unique (Y ⟶ (wideCospan ι X).obj none)

Equations

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

def CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] (ι : Type w) [Limits.HasFiniteProducts C] [Finite ι] (X : C) : Limits.LimitCone (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} [Category.{v, u} C] [Limits.HasTerminal C] (ι : Type w) [Limits.HasFiniteProducts C] [Finite ι] (X : C) : Limits.HasWidePullback (Arrow.mk (Limits.terminal.from X)).right (fun (x : ι) => (Arrow.mk (Limits.terminal.from X)).left) fun (x : ι) => (Arrow.mk (Limits.terminal.from X)).hom

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

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

def CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] (ι : Type w) [Limits.HasFiniteProducts C] [Finite ι] (X : C) : Limits.limit (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} [Category.{v, u} C] [Limits.HasTerminal C] (ι : Type w) [Limits.HasFiniteProducts C] [Finite ι] (X : C) (j : ι) : CategoryStruct.comp (limitIsoPi ι X).inv (Limits.WidePullback.π (fun (x : ι) => Limits.terminal.from X) j) = Limits.Pi.π (fun (x : ι) => X) j

@[simp]

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

@[simp]

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

@[simp]

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

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