Documentation

Mathlib.AlgebraicTopology.CechNerve

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

The Čech nerve associated to an arrow.

Instances For

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

    Instances For

      The augmented Čech nerve associated to an arrow.

      Instances For
        @[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) :

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

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

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

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

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

            Instances For
              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.

              Instances For
                @[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) :
                @[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ᵒᵖ) :
                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) :

                A helper function used in defining the Čech adjunction.

                Instances For
                  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.

                  Instances For
                    @[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.

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

                      The Čech conerve associated to an arrow.

                      Instances For

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

                        Instances For

                          The augmented Čech conerve associated to an arrow.

                          Instances For
                            @[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) :

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

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

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

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

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

                                Instances For
                                  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.

                                  Instances For
                                    @[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) :
                                    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) :

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

                                    Instances For
                                      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.

                                      Instances For
                                        @[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.

                                        Instances For

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

                                          Instances For

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

                                            Instances For

                                              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.

                                              Instances For