Documentation

Mathlib.Algebra.Homology.AlternatingConst

The alternating constant complex #

Given an object X : C and endomorphisms φ, ψ : X ⟶ X such that φ ∘ ψ = ψ ∘ φ = 0, this file defines the periodic chain and cochain complexes ... ⟶ X --φ--> X --ψ--> X --φ--> X --ψ--> 0 and 0 ⟶ X --ψ--> X --φ--> X --ψ--> X --φ--> ... (or more generally for any complex shape c on where c.Rel i j implies i and j have different parity). We calculate the homology of these periodic complexes.

In particular, we show ... ⟶ X --𝟙--> X --0--> X --𝟙--> X --0--> X ⟶ 0 is homotopy equivalent to the single complex where X is in degree 0.

theorem ComplexShape.up_nat_odd_add {i j : } (h : (up ).Rel i j) :
Odd (i + j)
theorem ComplexShape.down_nat_odd_add {i j : } (h : (down ).Rel i j) :
Odd (i + j)

Let c : ComplexShape be such that i j : ℕ have opposite parity if they are related by c. Let φ, ψ : A ⟶ A be such that φ ∘ ψ = ψ ∘ φ = 0. This is a complex of shape c whose objects are all A. For all i, j related by c, dᵢⱼ = φ when i is even, and dᵢⱼ = ψ when i is odd.

Equations
Instances For
    @[simp]
    theorem HomologicalComplex.alternatingConst_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) (n : ) :
    (alternatingConst A hOdd hEven hc).X n = A
    @[simp]
    theorem HomologicalComplex.alternatingConst_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) (i j : ) :
    (alternatingConst A hOdd hEven hc).d i j = if c.Rel i j then if Even i then φ else ψ else 0
    noncomputable def HomologicalComplex.alternatingConstScIsoEven {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) {i j k : } (hij : c.Rel i j) (hjk : c.Rel j k) (h : Even j) :
    (alternatingConst A hOdd hEven hc).sc' i j k { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }

    The i, j, kth short complex associated to the alternating constant complex on φ, ψ : A ⟶ A is A --ψ--> A --φ--> A when i ~ j, j ~ k and j is even.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def HomologicalComplex.alternatingConstScIsoOdd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) {i j k : } (hij : c.Rel i j) (hjk : c.Rel j k) (h : Odd j) :
      (alternatingConst A hOdd hEven hc).sc' i j k { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }

      The i, j, kth short complex associated to the alternating constant complex on φ, ψ : A ⟶ A is A --φ--> A --ψ--> A when i ~ j, j ~ k and j is even.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem HomologicalComplex.alternatingConst_iCycles_even_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : } (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) :
        @[simp]
        theorem HomologicalComplex.alternatingConst_iCycles_even_comp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : } (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) {F : CCType uF} {carrier : CType w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : CategoryTheory.ToType ((alternatingConst A hOdd hEven hc).cycles j)) :
        @[simp]
        theorem HomologicalComplex.alternatingConst_iCycles_odd_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : } (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) :
        @[simp]
        theorem HomologicalComplex.alternatingConst_iCycles_odd_comp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : } (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) {F : CCType uF} {carrier : CType w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : CategoryTheory.ToType ((alternatingConst A hOdd hEven hc).cycles j)) :
        noncomputable def HomologicalComplex.alternatingConstHomologyIsoEven {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : } (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Even j) :
        (alternatingConst A hOdd hEven hc).homology j { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.homology

        The jth homology of the alternating constant complex on φ, ψ : A ⟶ A is the homology of A --ψ--> A --φ--> A when prev(j) ~ j, j ~ next(j) and j is even.

        Equations
        Instances For
          noncomputable def HomologicalComplex.alternatingConstHomologyIsoOdd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A : C) {φ ψ : A A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape } [DecidableRel c.Rel] (hc : ∀ (i j : ), c.Rel i jOdd (i + j)) [CategoryTheory.CategoryWithHomology C] {j : } (hpj : c.Rel (c.prev j) j) (hnj : c.Rel j (c.next j)) (h : Odd j) :
          (alternatingConst A hOdd hEven hc).homology j { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.homology

          The jth homology of the alternating constant complex on φ, ψ : A ⟶ A is the homology of A --φ--> A --ψ--> A when prev(j) ~ j, j ~ next(j) and j is odd.

          Equations
          Instances For

            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

              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

                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

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

                  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

                    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