Documentation

Mathlib.Algebra.Homology.Embedding.Connect

Connecting a chain complex and a cochain complex #

Given a chain complex K: ... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0, a cochain complex L: L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ..., a morphism d₀ : K.X 0 ⟶ L.X 0 satisfying the identifies K.d 1 0 ≫ d₀ = 0 and d₀ ≫ L.d 0 1 = 0, we construct a cochain complex indexed by of the form ... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0 ⟶ L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ..., where K.X 0 lies in degree -1 and L.X 0 in degree 0.

Main definitions #

Say K : ChainComplex C ℕ and L : CochainComplex C ℕ, so ... ⟶ K₂ ⟶ K₁ ⟶ K₀ and L⁰ ⟶ L¹ ⟶ L² ⟶ ....

Now say h : ConnectData K L.

TODO #

Given K : ChainComplex C ℕ and L : CochainComplex C ℕ, this data allows to connect K and L in order to get a cochain complex indexed by , see ConnectData.cochainComplex.

Instances For

    Auxiliary definition for ConnectData.cochainComplex.

    Equations
    Instances For

      Given h : ConnectData K L where K : ChainComplex C ℕ and L : CochainComplex C ℕ, this is the cochain complex indexed by obtained by connecting K and L: ... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0 ⟶ L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ....

      Equations
      Instances For

        Given h : ConnectData K L and n : ℕ, the homology of h.cochainComplex in degree n + 1 identifies to the homology of L in degree n + 1.

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

          Given h : ConnectData K L and n : ℕ, the homology of h.cochainComplex in degree -(n + 2) identifies to the homology of K in degree n + 1.

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