Documentation

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

The cochain complex of homomorphisms between cochain complexes

If F and G are cochain complexes (indexed by ) in a preadditive category, there is a cochain complex of abelian groups whose 0-cocycles identify to morphisms F ⟶ G. Informally, in degree n, this complex shall consist of cochains of degree n from F to G, i.e. arbitrary families for morphisms F.X p ⟶ G.X (p + n). This complex shall be denoted HomComplex F G.

In order to avoid type theoretic issues, a cochain of degree n : ℤ (i.e. a term of type of Cochain F G n) shall be defined here as the data of a morphism F.X p ⟶ G.X q for all triplets ⟨p, q, hpq⟩ where p and q are integers and hpq : p + n = q. If α : Cochain F G n, we shall define α.v p q hpq : F.X p ⟶ G.X q.

We follow the signs conventions appearing in the introduction of Brian Conrad's book Grothendieck duality and base change.

References #

A term of type HomComplex.Triplet n consists of two integers p and q such that p + n = q. (This type is introduced so that the instance AddCommGroup (Cochain F G n) defined below can be found automatically.)

  • p :

    a first integer

  • q :

    a second integer

  • hpq : self.p + n = self.q

    the condition on the two integers

Instances For

    the condition on the two integers

    A cochain of degree n : ℤ between to cochain complexes F and G consists of a family of morphisms F.X p ⟶ G.X q whenever p + n = q, i.e. for all triplets in HomComplex.Triplet n.

    Equations
    Instances For

      A practical constructor for cochains.

      Equations
      Instances For

        The value of a cochain on a triplet ⟨p, q, hpq⟩.

        Equations
        • γ.v p q hpq = γ { p := p, q := q, hpq := hpq }
        Instances For
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.mk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {n : } (v : (p q : ) → p + n = q(F.X p G.X q)) (p : ) (q : ) (hpq : p + n = q) :
          (CochainComplex.HomComplex.Cochain.mk v).v p q hpq = v p q hpq
          theorem CochainComplex.HomComplex.Cochain.congr_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {n : } {z₁ : CochainComplex.HomComplex.Cochain F G n} {z₂ : CochainComplex.HomComplex.Cochain F G n} (h : z₁ = z₂) (p : ) (q : ) (hpq : p + n = q) :
          z₁.v p q hpq = z₂.v p q hpq
          theorem CochainComplex.HomComplex.Cochain.ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {n : } {z₁ : CochainComplex.HomComplex.Cochain F G n} {z₂ : CochainComplex.HomComplex.Cochain F G n} :
          z₁ = z₂ ∀ (p q : ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
          theorem CochainComplex.HomComplex.Cochain.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {n : } (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) (h : ∀ (p q : ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq) :
          z₁ = z₂
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.add_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {n : } (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) (p : ) (q : ) (hpq : p + n = q) :
          (z₁ + z₂).v p q hpq = z₁.v p q hpq + z₂.v p q hpq
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.sub_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {n : } (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain F G n) (p : ) (q : ) (hpq : p + n = q) :
          (z₁ - z₂).v p q hpq = z₁.v p q hpq - z₂.v p q hpq
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.neg_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {n : } (z : CochainComplex.HomComplex.Cochain F G n) (p : ) (q : ) (hpq : p + n = q) :
          (-z).v p q hpq = -z.v p q hpq
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.smul_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F : CochainComplex C } {G : CochainComplex C } {n : } (k : R) (z : CochainComplex.HomComplex.Cochain F G n) (p : ) (q : ) (hpq : p + n = q) :
          (k z).v p q hpq = k z.v p q hpq
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.units_smul_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F : CochainComplex C } {G : CochainComplex C } {n : } (k : Rˣ) (z : CochainComplex.HomComplex.Cochain F G n) (p : ) (q : ) (hpq : p + n = q) :
          (k z).v p q hpq = k z.v p q hpq

          A cochain of degree 0 from F to G can be constructed from a family of morphisms F.X p ⟶ G.X p for all p : ℤ.

          Equations
          Instances For

            The cochain of degree -1 given by an homotopy between two morphism of complexes.

            Equations
            Instances For

              The composition of cochains.

              Equations
              Instances For

                If z₁ is a cochain of degree n₁ and z₂ is a cochain of degree n₂, and that we have a relation h : n₁ + n₂ = n₁₂, then z₁.comp z₂ h is a cochain of degree n₁₂. The following lemma comp_v computes the value of this composition z₁.comp z₂ h on a triplet ⟨p₁, p₃, _⟩ (with p₁ + n₁₂ = p₃). In order to use this lemma, we need to provide an intermediate integer p₂ such that p₁ + n₁ = p₂. It is advisable to use a p₂ that has good definitional properties (i.e. p₁ + n₁ is not always the best choice.)

                When z₁ or z₂ is a 0-cochain, there is a better choice of p₂, and this leads to the two simplification lemmas comp_zero_cochain_v and zero_cochain_comp_v.

                theorem CochainComplex.HomComplex.Cochain.comp_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (p₁ : ) (p₂ : ) (p₃ : ) (h₁ : p₁ + n₁ = p₂) (h₂ : p₂ + n₂ = p₃) :
                (z₁.comp z₂ h).v p₁ p₃ = CategoryTheory.CategoryStruct.comp (z₁.v p₁ p₂ h₁) (z₂.v p₂ p₃ h₂)
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_zero_cochain_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n : } (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain G K 0) (p : ) (q : ) (hpq : p + n = q) :
                (z₁.comp z₂ ).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p q hpq) (z₂.v q q )
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.zero_cochain_comp_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n : } (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n) (p : ) (q : ) (hpq : p + n = q) :
                (z₁.comp z₂ ).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p p ) (z₂.v p q hpq)
                theorem CochainComplex.HomComplex.Cochain.comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {L : CochainComplex C } {n₁ : } {n₂ : } {n₃ : } {n₁₂ : } {n₂₃ : } {n₁₂₃ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₁₂ : n₁ + n₂ = n₁₂) (h₂₃ : n₂ + n₃ = n₂₃) (h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃) :
                (z₁.comp z₂ h₁₂).comp z₃ = z₁.comp (z₂.comp z₃ h₂₃)

                The associativity of the composition of cochains.

                The formulation of the associativity of the composition of cochains given by the lemma comp_assoc often requires a careful selection of degrees with good definitional properties. In a few cases, like when one of the three cochains is a 0-cochain, there are better choices, which provides the following simplification lemmas.

                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {L : CochainComplex C } {n₂ : } {n₃ : } {n₂₃ : } (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₂₃ : n₂ + n₃ = n₂₃) :
                (z₁.comp z₂ ).comp z₃ h₂₃ = z₁.comp (z₂.comp z₃ h₂₃)
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {L : CochainComplex C } {n₁ : } {n₃ : } {n₁₃ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K 0) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₁₃ : n₁ + n₃ = n₁₃) :
                (z₁.comp z₂ ).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ ) h₁₃
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_third_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {L : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L 0) (h₁₂ : n₁ + n₂ = n₁₂) :
                (z₁.comp z₂ h₁₂).comp z₃ = z₁.comp (z₂.comp z₃ ) h₁₂
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_second_degree_eq_neg_third_degree {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {L : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K (-n₂)) (z₃ : CochainComplex.HomComplex.Cochain K L n₂) (h₁₂ : n₁ + -n₂ = n₁₂) :
                (z₁.comp z₂ h₁₂).comp z₃ = z₁.comp (z₂.comp z₃ )
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.add_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₁' : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                (z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.sub_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₁' : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                (z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.neg_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                (-z₁).comp z₂ h = -z₁.comp z₂ h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.smul_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (k : R) (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                (k z₁).comp z₂ h = k z₁.comp z₂ h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.units_smul_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (k : Rˣ) (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                (k z₁).comp z₂ h = k z₁.comp z₂ h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (h : n₁ + n₂ = n₁₂) :
                z₁.comp 0 h = 0
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                z₁.comp (-z₂) h = -z₁.comp z₂ h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (k : R) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                z₁.comp (k z₂) h = k z₁.comp z₂ h
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.comp_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (k : Rˣ) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                z₁.comp (k z₂) h = k z₁.comp z₂ h

                The differential on a cochain complex, as a cochain of degree 1.

                Equations
                Instances For

                  The differential on the complex of morphisms between cochain complexes.

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

                    Similarly as for the composition of cochains, if z : Cochain F G n, we usually need to carefully select intermediate indices with good definitional properties in order to obtain a suitable expansion of the morphisms which constitute δ n m z : Cochain F G m (when n + 1 = m, otherwise it shall be zero). The basic equational lemma is δ_v below.

                    theorem CochainComplex.HomComplex.δ_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (n : ) (m : ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) (p : ) (q : ) (hpq : p + m = q) (q₁ : ) (q₂ : ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂) :
                    (CochainComplex.HomComplex.δ n m z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p q₁ ) (G.d q₁ q) + m.negOnePow CategoryTheory.CategoryStruct.comp (F.d p q₂) (z.v q₂ q )

                    The differential on the complex of morphisms between cochain complexes, as a linear map.

                    Equations
                    Instances For
                      theorem CochainComplex.HomComplex.δ_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (m₁ : ) (m₂ : ) (m₁₂ : ) (h₁₂ : n₁₂ + 1 = m₁₂) (h₁ : n₁ + 1 = m₁) (h₂ : n₂ + 1 = m₂) :
                      CochainComplex.HomComplex.δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) + n₂.negOnePow (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂
                      theorem CochainComplex.HomComplex.δ_zero_cochain_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (m₂ : ) (h₂ : n₂ + 1 = m₂) :
                      CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ ) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) + n₂.negOnePow (CochainComplex.HomComplex.δ 0 1 z₁).comp z₂
                      theorem CochainComplex.HomComplex.δ_comp_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } {K : CochainComplex C } {n₁ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K 0) (m₁ : ) (h₁ : n₁ + 1 = m₁) :
                      CochainComplex.HomComplex.δ n₁ m₁ (z₁.comp z₂ ) = z₁.comp (CochainComplex.HomComplex.δ 0 1 z₂) h₁ + (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂

                      The cochain complex of homomorphisms between two cochain complexes F and G. In degree n : ℤ, it consists of the abelian group HomComplex.Cochain F G n.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        Equations
                        • CochainComplex.HomComplex.Cocycle.instModule = Module.mk

                        Constructor for Cocycle F G n, taking as inputs z : Cochain F G n, an integer m : ℤ such that n + 1 = m, and the relation δ n m z = 0.

                        Equations
                        Instances For

                          The morphism in CochainComplex C ℤ associated to a 0-cocycle.

                          Equations
                          • z.homOf = { f := fun (i : ) => (↑z).v i i , comm' := }
                          Instances For

                            The additive equivalence between morphisms in CochainComplex C ℤ and 0-cocycles.

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

                              Given two morphisms of complexes φ₁ φ₂ : F ⟶ G, the datum of an homotopy between φ₁ and φ₂ is equivalent to the datum of a 1-cochain z such that δ (-1) 0 z is the difference of the zero cochains associated to φ₂ and φ₁.

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

                                If Φ : C ⥤ D is an additive functor, a cochain z : Cochain K L n between cochain complexes in C can be mapped to a cochain between the cochain complexes in D obtained by applying the functor Φ.mapHomologicalComplex _ : CochainComplex C ℤ ⥤ CochainComplex D ℤ.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CochainComplex.HomComplex.Cochain.map_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C } {L : CochainComplex C } {n : } {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z : CochainComplex.HomComplex.Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] (p : ) (q : ) (hpq : p + n = q) :
                                  (z.map Φ).v p q hpq = Φ.map (z.v p q hpq)
                                  @[simp]
                                  theorem CochainComplex.HomComplex.Cochain.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (K : CochainComplex C ) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {n₁ : } {n₂ : } {n₁₂ : } (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (Φ : CategoryTheory.Functor C D) [Φ.Additive] :
                                  (z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h