Documentation

Mathlib.Algebra.Homology.AlternatingConst

The alternating constant complex #

In this file we define the chain complex X ←0- X ←𝟙- X ←0- X ←𝟙- X ⋯, and calculate its homology.

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