Documentation

Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

The alternating face map complex of a simplicial object in a preadditive category #

We construct the alternating face map complex, as a functor alternatingFaceMapComplex : SimplicialObject C ⥤ ChainComplex C ℕ for any preadditive category C. For any simplicial object X in C, this is the homological complex ... → X_2 → X_1 → X_0 where the differentials are alternating sums of faces.

The dual version alternatingCofaceMapComplex : CosimplicialObject C ⥤ CochainComplex C ℕ is also constructed.

We also construct the natural transformation inclusionOfMooreComplex : normalizedMooreComplex A ⟶ alternatingFaceMapComplex A when A is an abelian category.

References #

Construction of the alternating face map complex #

source
def AlgebraicTopology.AlternatingFaceMapComplex.objD {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))

The differential on the alternating face map complex is the alternate sum of the face maps

Equations
Instances For
    source
    theorem AlgebraicTopology.AlternatingFaceMapComplex.d_squared {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingFaceMapComplex.objD X (n + 1)) (AlgebraicTopology.AlternatingFaceMapComplex.objD X n) = 0

    The chain complex relation d ≫ d #

    Construction of the alternating face map complex functor #

    source
    def AlgebraicTopology.AlternatingFaceMapComplex.obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) :
    ChainComplex C ℕ

    The alternating face map complex, on objects

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
      (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n = X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))
      source
      @[simp]
      theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
      (AlgebraicTopology.AlternatingFaceMapComplex.obj X).d (n + 1) n = Finset.sum Finset.univ fun (i : Fin (n + 2)) => (-1) ^ ↑i • CategoryTheory.SimplicialObject.δ X i
      source
      def AlgebraicTopology.AlternatingFaceMapComplex.map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) :
      AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj Y

      The alternating face map complex, on morphisms

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AlgebraicTopology.AlternatingFaceMapComplex.map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ) :
        (AlgebraicTopology.AlternatingFaceMapComplex.map f).f n = f.app (Opposite.op (SimplexCategory.mk n))
        source
        def AlgebraicTopology.alternatingFaceMapComplex (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
        CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex C ℕ)

        The alternating face map complex, as a functor

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem AlgebraicTopology.alternatingFaceMapComplex_obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
          ((AlgebraicTopology.alternatingFaceMapComplex C).toPrefunctor.obj X).X n = X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))
          source
          @[simp]
          theorem AlgebraicTopology.alternatingFaceMapComplex_obj_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
          ((AlgebraicTopology.alternatingFaceMapComplex C).toPrefunctor.obj X).d (n + 1) n = AlgebraicTopology.AlternatingFaceMapComplex.objD X n
          source
          @[simp]
          theorem AlgebraicTopology.alternatingFaceMapComplex_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ) :
          ((AlgebraicTopology.alternatingFaceMapComplex C).toPrefunctor.map f).f n = f.app (Opposite.op (SimplexCategory.mk n))
          source
          theorem AlgebraicTopology.map_alternatingFaceMapComplex {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] :
          CategoryTheory.Functor.comp (AlgebraicTopology.alternatingFaceMapComplex C) (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) = CategoryTheory.Functor.comp ((CategoryTheory.SimplicialObject.whiskering C D).toPrefunctor.obj F) (AlgebraicTopology.alternatingFaceMapComplex D)
          source
          theorem AlgebraicTopology.karoubi_alternatingFaceMapComplex_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (n : ℕ) :
          ((AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f = CategoryTheory.CategoryStruct.comp (P.p.app (Opposite.op (SimplexCategory.mk (n + 1)))) ((AlgebraicTopology.AlternatingFaceMapComplex.obj P.X).d (n + 1) n)
          source
          def AlgebraicTopology.AlternatingFaceMapComplex.ε {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] :
          CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented.drop (AlgebraicTopology.alternatingFaceMapComplex C) ⟶ CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented.point (ChainComplex.single₀ C)

          The natural transformation which gives the augmentation of the alternating face map complex attached to an augmented simplicial object.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : CategoryTheory.SimplicialObject.Augmented C) :
            (AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f 0 = X.hom.app (Opposite.op (SimplexCategory.mk 0))
            source
            @[simp]
            theorem AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : CategoryTheory.SimplicialObject.Augmented C) (n : ℕ) :
            (AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f (n + 1) = 0

            Construction of the natural inclusion of the normalized Moore complex #

            source
            def AlgebraicTopology.inclusionOfMooreComplexMap {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) :
            (AlgebraicTopology.normalizedMooreComplex A).toPrefunctor.obj X ⟶ (AlgebraicTopology.alternatingFaceMapComplex A).toPrefunctor.obj X

            The inclusion map of the Moore complex in the alternating face map complex

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem AlgebraicTopology.inclusionOfMooreComplexMap_f {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) (n : ℕ) :
              (AlgebraicTopology.inclusionOfMooreComplexMap X).f n = CategoryTheory.Subobject.arrow (AlgebraicTopology.NormalizedMooreComplex.objX X n)
              source
              @[simp]
              theorem AlgebraicTopology.inclusionOfMooreComplex_app (A : Type u_2) [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) :
              (AlgebraicTopology.inclusionOfMooreComplex A).app X = AlgebraicTopology.inclusionOfMooreComplexMap X
              source
              def AlgebraicTopology.inclusionOfMooreComplex (A : Type u_2) [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] :
              AlgebraicTopology.normalizedMooreComplex A ⟶ AlgebraicTopology.alternatingFaceMapComplex A

              The inclusion map of the Moore complex in the alternating face map complex, as a natural transformation

              Equations
              Instances For
                source
                def AlgebraicTopology.AlternatingCofaceMapComplex.objD {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) (n : ℕ) :
                X.toPrefunctor.obj (SimplexCategory.mk n) ⟶ X.toPrefunctor.obj (SimplexCategory.mk (n + 1))

                The differential on the alternating coface map complex is the alternate sum of the coface maps

                Equations
                Instances For
                  source
                  theorem AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) (n : ℕ) :
                  AlgebraicTopology.AlternatingCofaceMapComplex.objD X n = (AlgebraicTopology.AlternatingFaceMapComplex.objD ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.toPrefunctor.obj (Opposite.op X)) n).unop
                  source
                  theorem AlgebraicTopology.AlternatingCofaceMapComplex.d_squared {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) (n : ℕ) :
                  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingCofaceMapComplex.objD X n) (AlgebraicTopology.AlternatingCofaceMapComplex.objD X (n + 1)) = 0
                  source
                  def AlgebraicTopology.AlternatingCofaceMapComplex.obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) :
                  CochainComplex C ℕ

                  The alternating coface map complex, on objects

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def AlgebraicTopology.AlternatingCofaceMapComplex.map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.CosimplicialObject C} {Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y) :
                    AlgebraicTopology.AlternatingCofaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingCofaceMapComplex.obj Y

                    The alternating face map complex, on morphisms

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem AlgebraicTopology.alternatingCofaceMapComplex_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] :
                      ∀ {X Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y), (AlgebraicTopology.alternatingCofaceMapComplex C).toPrefunctor.map f = AlgebraicTopology.AlternatingCofaceMapComplex.map f
                      source
                      @[simp]
                      theorem AlgebraicTopology.alternatingCofaceMapComplex_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) :
                      (AlgebraicTopology.alternatingCofaceMapComplex C).toPrefunctor.obj X = AlgebraicTopology.AlternatingCofaceMapComplex.obj X
                      source
                      def AlgebraicTopology.alternatingCofaceMapComplex (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] :
                      CategoryTheory.Functor (CategoryTheory.CosimplicialObject C) (CochainComplex C ℕ)

                      The alternating coface map complex, as a functor

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