Documentation

Mathlib.Algebra.Homology.AlternatingConst

The alternating constant complex #

In this file we define the chain complex X ←0- X β†πŸ™- X ←0- X β†πŸ™- X β‹―, calculate its homology, and show that it is homotopy equivalent to the single complex where X is in degree 0.

source
def ChainComplex.alternatingConst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
CategoryTheory.Functor C (ChainComplex C β„•)

The chain complex X ←0- X β†πŸ™- X ←0- X β†πŸ™- X β‹―. It is exact away from 0 and has homology X at 0.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem ChainComplex.alternatingConst_obj_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (i j : β„•) :
    (alternatingConst.obj X).d i j = if Even i ∧ j + 1 = i then CategoryTheory.CategoryStruct.id X else 0
    source
    @[simp]
    theorem ChainComplex.alternatingConst_obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (x✝ : β„•) :
    (alternatingConst.obj X).X x✝ = X
    source
    @[simp]
    theorem ChainComplex.alternatingConst_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟢ Y) (x✝ : β„•) :
    (alternatingConst.map f).f x✝ = f
    source
    noncomputable def ChainComplex.alternatingConstHomologyDataEvenNEZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : β„•) (hn : Even n) (hβ‚€ : n β‰  0) :
    (HomologicalComplex.sc (alternatingConst.obj X) n).HomologyData

    The n-th homology of the alternating constant complex is zero for non-zero even n.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def ChainComplex.alternatingConstHomologyDataOdd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : β„•) (hn : Odd n) :
      (HomologicalComplex.sc (alternatingConst.obj X) n).HomologyData

      The n-th homology of the alternating constant complex is zero for odd n.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def ChainComplex.alternatingConstHomologyDataZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (n : β„•) (hn : n = 0) :
        (HomologicalComplex.sc (alternatingConst.obj X) n).HomologyData

        The n-th homology of the alternating constant complex is X for n = 0.

        Equations
        Instances For
          source
          instance ChainComplex.instHasHomologyNatObjAlternatingConst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : β„•) :
          HomologicalComplex.HasHomology (alternatingConst.obj X) n
          source
          theorem ChainComplex.alternatingConst_exactAt {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : β„•) (hn : n β‰  0) :
          HomologicalComplex.ExactAt (alternatingConst.obj X) n

          The n-th homology of the alternating constant complex is X for n β‰  0.

          source
          noncomputable def ChainComplex.alternatingConstHomologyZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) :
          HomologicalComplex.homology (alternatingConst.obj X) 0 β‰… X

          The n-th homology of the alternating constant complex is X for n = 0.

          Equations
          Instances For
            source
            def AlgebraicTopology.alternatingFaceMapComplexConst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
            (CategoryTheory.Functor.const SimplexCategoryα΅’α΅–).comp (alternatingFaceMapComplex C) β‰… ChainComplex.alternatingConst

            The alternating face complex of the constant complex is the alternating constant complex.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def ChainComplex.alternatingConstHomotopyEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) :
              HomotopyEquiv (alternatingConst.obj X) ((singleβ‚€ C).obj X)

              alternatingConst.obj X is homotopy equivalent to the chain complex (singleβ‚€ C).obj X.

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