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 #

source
structure CochainComplex.HomComplex.Triplet (n : ℤ) :
Type

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
    source
    def CochainComplex.HomComplex.Cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (n : ℤ) :
    Type v

    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
      source
      instance CochainComplex.HomComplex.instAddCommGroupCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (n : ℤ) :
      AddCommGroup (CochainComplex.HomComplex.Cochain F G n)
      Equations
      source
      instance CochainComplex.HomComplex.instModuleCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n : ℤ) :
      Module R (CochainComplex.HomComplex.Cochain F G n)
      Equations
      source
      def CochainComplex.HomComplex.Cochain.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)) :
      CochainComplex.HomComplex.Cochain F G n

      A practical constructor for cochains.

      Equations
      Instances For
        source
        def CochainComplex.HomComplex.Cochain.v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q) :
        F.X p ⟶ G.X q

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

        Equations
        • γ.v p q hpq = γ { p := p, q := q, hpq := hpq }
        Instances For
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.mk_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F 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
          source
          theorem CochainComplex.HomComplex.Cochain.congr_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} {z₁ 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
          source
          theorem CochainComplex.HomComplex.Cochain.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ 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₂
          source
          theorem CochainComplex.HomComplex.Cochain.ext₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G 0) (h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯) :
          z₁ = z₂
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.zero_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (p q : ℤ) (hpq : p + n = q) :
          CochainComplex.HomComplex.Cochain.v 0 p q hpq = 0
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.add_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ 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
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.sub_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ 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
          source
          @[simp]
          theorem CochainComplex.HomComplex.Cochain.neg_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F 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
          source
          @[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 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
          source
          @[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 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
          source
          def CochainComplex.HomComplex.Cochain.ofHoms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) :
          CochainComplex.HomComplex.Cochain F G 0

          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
            source
            @[simp]
            theorem CochainComplex.HomComplex.Cochain.ofHoms_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p : ℤ) :
            (CochainComplex.HomComplex.Cochain.ofHoms ψ).v p p ⋯ = ψ p
            source
            @[simp]
            theorem CochainComplex.HomComplex.Cochain.ofHoms_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} :
            (CochainComplex.HomComplex.Cochain.ofHoms fun (p : ℤ) => 0) = 0
            source
            @[simp]
            theorem CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p q q' : ℤ) (hpq : p + 0 = q) :
            CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) (G.d q q') = CategoryTheory.CategoryStruct.comp (ψ p) (G.d p q')
            source
            @[simp]
            theorem CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p' p q : ℤ) (hpq : p + 0 = q) :
            CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) = CategoryTheory.CategoryStruct.comp (F.d p' q) (ψ q)
            source
            def CochainComplex.HomComplex.Cochain.ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) :
            CochainComplex.HomComplex.Cochain F G 0

            The 0-cochain attached to a morphism of cochain complexes.

            Equations
            Instances For
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cochain.ofHom_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) :
              CochainComplex.HomComplex.Cochain.ofHom 0 = 0
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cochain.ofHom_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p : ℤ) :
              (CochainComplex.HomComplex.Cochain.ofHom φ).v p p ⋯ = φ.f p
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cochain.ofHom_v_comp_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p q q' : ℤ) (hpq : p + 0 = q) :
              CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) (G.d q q') = CategoryTheory.CategoryStruct.comp (φ.f p) (G.d p q')
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cochain.d_comp_ofHom_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p' p q : ℤ) (hpq : p + 0 = q) :
              CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) = CategoryTheory.CategoryStruct.comp (F.d p' q) (φ.f q)
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cochain.ofHom_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) :
              CochainComplex.HomComplex.Cochain.ofHom (φ₁ + φ₂) = CochainComplex.HomComplex.Cochain.ofHom φ₁ + CochainComplex.HomComplex.Cochain.ofHom φ₂
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cochain.ofHom_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) :
              CochainComplex.HomComplex.Cochain.ofHom (φ₁ - φ₂) = CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂
              source
              @[simp]
              theorem CochainComplex.HomComplex.Cochain.ofHom_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) :
              CochainComplex.HomComplex.Cochain.ofHom (-φ) = -CochainComplex.HomComplex.Cochain.ofHom φ
              source
              def CochainComplex.HomComplex.Cochain.ofHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (ho : Homotopy φ₁ φ₂) :
              CochainComplex.HomComplex.Cochain F G (-1)

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

              Equations
              Instances For
                source
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (h : φ₁ = φ₂) :
                CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.ofEq h) = 0
                source
                @[simp]
                theorem CochainComplex.HomComplex.Cochain.ofHomotopy_refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) :
                CochainComplex.HomComplex.Cochain.ofHomotopy (Homotopy.refl φ) = 0
                source
                theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q = q') :
                CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯
                source
                theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q = q') {Z : C} (h : G.X q' ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').hom h) = CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h
                source
                theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q' = q) :
                CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯
                source
                theorem CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q' = q) {Z : C} (h : G.X q' ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').inv h) = CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h
                source
                def CochainComplex.HomComplex.Cochain.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                CochainComplex.HomComplex.Cochain F K n₁₂

                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.

                  source
                  theorem CochainComplex.HomComplex.Cochain.comp_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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₂)
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_zero_cochain_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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 ⋯)
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.zero_cochain_comp_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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)
                  source
                  theorem CochainComplex.HomComplex.Cochain.comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K 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.

                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K 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₂₃) ⋯
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K 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₁₃
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_assoc_of_third_is_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K 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₁₂
                  source
                  @[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 G K 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₃ ⋯) ⋯
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.zero_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                  CochainComplex.HomComplex.Cochain.comp 0 z₂ h = 0
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.add_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ 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
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.sub_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ 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
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.neg_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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
                  source
                  @[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 G 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
                  source
                  @[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 G 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
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.id_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₂ : CochainComplex.HomComplex.Cochain F G n) :
                  (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)).comp z₂ ⋯ = z₂
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (h : n₁ + n₂ = n₁₂) :
                  z₁.comp 0 h = 0
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                  z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
                  z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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
                  source
                  @[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 G 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
                  source
                  @[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 G 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
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.comp_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) :
                  z₁.comp (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id G)) ⋯ = z₁
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.ofHoms_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} (φ : (p : ℤ) → F.X p ⟶ G.X p) (ψ : (p : ℤ) → G.X p ⟶ K.X p) :
                  (CochainComplex.HomComplex.Cochain.ofHoms φ).comp (CochainComplex.HomComplex.Cochain.ofHoms ψ) ⋯ = CochainComplex.HomComplex.Cochain.ofHoms fun (p : ℤ) => CategoryTheory.CategoryStruct.comp (φ p) (ψ p)
                  source
                  @[simp]
                  theorem CochainComplex.HomComplex.Cochain.ofHom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} (f : F ⟶ G) (g : G ⟶ K) :
                  CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp f g) = (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.Cochain.ofHom g) ⋯
                  source
                  def CochainComplex.HomComplex.Cochain.diff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) :
                  CochainComplex.HomComplex.Cochain K K 1

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

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem CochainComplex.HomComplex.Cochain.diff_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p + 1 = q) :
                    (CochainComplex.HomComplex.Cochain.diff K).v p q hpq = K.d p q
                    source
                    def CochainComplex.HomComplex.δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (z : CochainComplex.HomComplex.Cochain F G n) :
                    CochainComplex.HomComplex.Cochain F G m

                    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.

                      source
                      theorem CochainComplex.HomComplex.δ_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F 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 ⋯)
                      source
                      theorem CochainComplex.HomComplex.δ_shape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (hnm : ¬n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) :
                      CochainComplex.HomComplex.δ n m z = 0
                      source
                      def CochainComplex.HomComplex.δ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n m : ℤ) :
                      CochainComplex.HomComplex.Cochain F G n →ₗ[R] CochainComplex.HomComplex.Cochain F G m

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

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n m : ℤ) (z : CochainComplex.HomComplex.Cochain F G n) :
                        (CochainComplex.HomComplex.δ_hom R F G n m) z = CochainComplex.HomComplex.δ n m z
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n) :
                        CochainComplex.HomComplex.δ n m (z₁ + z₂) = CochainComplex.HomComplex.δ n m z₁ + CochainComplex.HomComplex.δ n m z₂
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n) :
                        CochainComplex.HomComplex.δ n m (z₁ - z₂) = CochainComplex.HomComplex.δ n m z₁ - CochainComplex.HomComplex.δ n m z₂
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) :
                        CochainComplex.HomComplex.δ n m 0 = 0
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (z : CochainComplex.HomComplex.Cochain F G n) :
                        CochainComplex.HomComplex.δ n m (-z) = -CochainComplex.HomComplex.δ n m z
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (n m : ℤ) (k : R) (z : CochainComplex.HomComplex.Cochain F G n) :
                        CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (n m : ℤ) (k : Rˣ) (z : CochainComplex.HomComplex.Cochain F G n) :
                        CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
                        source
                        theorem CochainComplex.HomComplex.δ_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n₀ n₁ n₂ : ℤ) (z : CochainComplex.HomComplex.Cochain F G n₀) :
                        CochainComplex.HomComplex.δ n₁ n₂ (CochainComplex.HomComplex.δ n₀ n₁ z) = 0
                        source
                        theorem CochainComplex.HomComplex.δ_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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₂ ⋯
                        source
                        theorem CochainComplex.HomComplex.δ_zero_cochain_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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₂ ⋯
                        source
                        theorem CochainComplex.HomComplex.δ_comp_zero_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G 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₂ ⋯
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_zero_cochain_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G 0) (p q : ℤ) (hpq : p + 1 = q) :
                        (CochainComplex.HomComplex.δ 0 1 z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p p ⋯) (G.d p q) - CategoryTheory.CategoryStruct.comp (F.d p q) (z.v q q ⋯)
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {p : ℤ} (φ : F ⟶ G) :
                        CochainComplex.HomComplex.δ 0 p (CochainComplex.HomComplex.Cochain.ofHom φ) = 0
                        source
                        @[simp]
                        theorem CochainComplex.HomComplex.δ_ofHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) :
                        CochainComplex.HomComplex.δ (-1) 0 (CochainComplex.HomComplex.Cochain.ofHomotopy h) = CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂
                        source
                        theorem CochainComplex.HomComplex.δ_neg_one_cochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G (-1)) :
                        CochainComplex.HomComplex.δ (-1) 0 z = CochainComplex.HomComplex.Cochain.ofHom (Homotopy.nullHomotopicMap' fun (i j : ℤ) (hij : (ComplexShape.up ℤ).Rel j i) => z.v i j ⋯)
                        source
                        def CochainComplex.HomComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) :
                        CochainComplex AddCommGrp ℤ

                        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
                          source
                          @[simp]
                          theorem CochainComplex.HomComplex_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (i : ℤ) :
                          (F.HomComplex G).X i = AddCommGrp.of (CochainComplex.HomComplex.Cochain F G i)
                          source
                          def CochainComplex.HomComplex.cocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (n : ℤ) :
                          AddSubgroup (CochainComplex.HomComplex.Cochain F G n)

                          The subgroup of cocycles in Cochain F G n.

                          Equations
                          Instances For
                            source
                            def CochainComplex.HomComplex.Cocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (n : ℤ) :
                            Type v

                            The type of n-cocycles, as a subtype of Cochain F G n.

                            Equations
                            Instances For
                              source
                              instance CochainComplex.HomComplex.instAddCommGroupCocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (n : ℤ) :
                              AddCommGroup (CochainComplex.HomComplex.Cocycle F G n)
                              Equations
                              source
                              theorem CochainComplex.HomComplex.Cocycle.mem_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) :
                              z ∈ CochainComplex.HomComplex.cocycle F G n ↔ CochainComplex.HomComplex.δ n m z = 0
                              source
                              instance CochainComplex.HomComplex.Cocycle.instCoeCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} :
                              Coe (CochainComplex.HomComplex.Cocycle F G n) (CochainComplex.HomComplex.Cochain F G n)
                              Equations
                              source
                              theorem CochainComplex.HomComplex.Cocycle.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n) (h : ↑z₁ = ↑z₂) :
                              z₁ = z₂
                              source
                              instance CochainComplex.HomComplex.Cocycle.instSMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} :
                              SMul R (CochainComplex.HomComplex.Cocycle F G n)
                              Equations
                              source
                              @[simp]
                              theorem CochainComplex.HomComplex.Cocycle.coe_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (n : ℤ) :
                              ↑0 = 0
                              source
                              @[simp]
                              theorem CochainComplex.HomComplex.Cocycle.coe_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n) :
                              ↑(z₁ + z₂) = ↑z₁ + ↑z₂
                              source
                              @[simp]
                              theorem CochainComplex.HomComplex.Cocycle.coe_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) :
                              ↑(-z) = -↑z
                              source
                              @[simp]
                              theorem CochainComplex.HomComplex.Cocycle.coe_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) (x : R) :
                              ↑(x • z) = x • ↑z
                              source
                              @[simp]
                              theorem CochainComplex.HomComplex.Cocycle.coe_units_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) (x : Rˣ) :
                              ↑(x • z) = x • ↑z
                              source
                              @[simp]
                              theorem CochainComplex.HomComplex.Cocycle.coe_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n) :
                              ↑(z₁ - z₂) = ↑z₁ - ↑z₂
                              source
                              instance CochainComplex.HomComplex.Cocycle.instModule {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} :
                              Module R (CochainComplex.HomComplex.Cocycle F G n)
                              Equations
                              • CochainComplex.HomComplex.Cocycle.instModule = Module.mk ⋯ ⋯
                              source
                              def CochainComplex.HomComplex.Cocycle.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (m : ℤ) (hnm : n + 1 = m) (h : CochainComplex.HomComplex.δ n m z = 0) :
                              CochainComplex.HomComplex.Cocycle F G n

                              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
                                source
                                @[simp]
                                theorem CochainComplex.HomComplex.Cocycle.mk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (m : ℤ) (hnm : n + 1 = m) (h : CochainComplex.HomComplex.δ n m z = 0) :
                                ↑(CochainComplex.HomComplex.Cocycle.mk z m hnm h) = z
                                source
                                @[simp]
                                theorem CochainComplex.HomComplex.Cocycle.δ_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) (m : ℤ) :
                                CochainComplex.HomComplex.δ n m ↑z = 0
                                source
                                def CochainComplex.HomComplex.Cocycle.ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) :
                                CochainComplex.HomComplex.Cocycle F G 0

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

                                Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem CochainComplex.HomComplex.Cocycle.ofHom_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) :
                                  ↑(CochainComplex.HomComplex.Cocycle.ofHom φ) = CochainComplex.HomComplex.Cochain.ofHom φ
                                  source
                                  def CochainComplex.HomComplex.Cocycle.homOf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) :
                                  F ⟶ G

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

                                  Equations
                                  • z.homOf = { f := fun (i : ℤ) => (↑z).v i i ⋯, comm' := ⋯ }
                                  Instances For
                                    source
                                    @[simp]
                                    theorem CochainComplex.HomComplex.Cocycle.homOf_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) (i : ℤ) :
                                    z.homOf.f i = (↑z).v i i ⋯
                                    source
                                    @[simp]
                                    theorem CochainComplex.HomComplex.Cocycle.homOf_ofHom_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) :
                                    (CochainComplex.HomComplex.Cocycle.ofHom φ).homOf = φ
                                    source
                                    @[simp]
                                    theorem CochainComplex.HomComplex.Cocycle.ofHom_homOf_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) :
                                    CochainComplex.HomComplex.Cocycle.ofHom z.homOf = z
                                    source
                                    @[simp]
                                    theorem CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) :
                                    CochainComplex.HomComplex.Cochain.ofHom z.homOf = ↑z
                                    source
                                    def CochainComplex.HomComplex.Cocycle.equivHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) :
                                    (F ⟶ G) ≃+ CochainComplex.HomComplex.Cocycle F G 0

                                    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
                                      source
                                      @[simp]
                                      theorem CochainComplex.HomComplex.Cocycle.equivHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (φ : F ⟶ G) :
                                      (CochainComplex.HomComplex.Cocycle.equivHom F G) φ = CochainComplex.HomComplex.Cocycle.ofHom φ
                                      source
                                      @[simp]
                                      theorem CochainComplex.HomComplex.Cocycle.equivHom_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F G : CochainComplex C ℤ) (z : CochainComplex.HomComplex.Cocycle F G 0) :
                                      (CochainComplex.HomComplex.Cocycle.equivHom F G).symm z = z.homOf
                                      source
                                      def CochainComplex.HomComplex.Cocycle.diff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) :
                                      CochainComplex.HomComplex.Cocycle K K 1

                                      The 1-cocycle given by the differential on a cochain complex.

                                      Equations
                                      Instances For
                                        source
                                        @[simp]
                                        theorem CochainComplex.HomComplex.Cocycle.diff_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) :
                                        ↑(CochainComplex.HomComplex.Cocycle.diff K) = CochainComplex.HomComplex.Cochain.diff K
                                        source
                                        @[simp]
                                        theorem CochainComplex.HomComplex.δ_comp_zero_cocycle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cocycle G K 0) (m : ℤ) :
                                        CochainComplex.HomComplex.δ n m (z₁.comp ↑z₂ ⋯) = (CochainComplex.HomComplex.δ n m z₁).comp ↑z₂ ⋯
                                        source
                                        @[simp]
                                        theorem CochainComplex.HomComplex.δ_comp_ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (f : G ⟶ K) (m : ℤ) :
                                        CochainComplex.HomComplex.δ n m (z₁.comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯) = (CochainComplex.HomComplex.δ n m z₁).comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯
                                        source
                                        @[simp]
                                        theorem CochainComplex.HomComplex.δ_zero_cocycle_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cocycle F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n) (m : ℤ) :
                                        CochainComplex.HomComplex.δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (CochainComplex.HomComplex.δ n m z₂) ⋯
                                        source
                                        @[simp]
                                        theorem CochainComplex.HomComplex.δ_ofHom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (f : F ⟶ G) (z : CochainComplex.HomComplex.Cochain G K n) (m : ℤ) :
                                        CochainComplex.HomComplex.δ n m ((CochainComplex.HomComplex.Cochain.ofHom f).comp z ⋯) = (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.δ n m z) ⋯
                                        source
                                        def CochainComplex.HomComplex.Cochain.equivHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) :
                                        Homotopy φ₁ φ₂ ≃ { z : CochainComplex.HomComplex.Cochain F G (-1) // CochainComplex.HomComplex.Cochain.ofHom φ₁ = CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ }

                                        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
                                          source
                                          @[simp]
                                          theorem CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) (ho : Homotopy φ₁ φ₂) :
                                          ↑((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂) ho) = CochainComplex.HomComplex.Cochain.ofHomotopy ho
                                          source
                                          @[simp]
                                          theorem CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) (z : { z : CochainComplex.HomComplex.Cochain F G (-1) // CochainComplex.HomComplex.Cochain.ofHom φ₁ = CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ }) (i j : ℤ) :
                                          ((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂).symm z).hom i j = if hij : i + -1 = j then (↑z).v i j hij else 0
                                          source
                                          @[simp]
                                          theorem CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (h : φ₁ = φ₂) :
                                          ↑((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂) (Homotopy.ofEq h)) = 0
                                          source
                                          theorem CochainComplex.HomComplex.Cochain.ofHom_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {f₁ f₂ : F ⟶ G} (h : CochainComplex.HomComplex.Cochain.ofHom f₁ = CochainComplex.HomComplex.Cochain.ofHom f₂) :
                                          f₁ = f₂
                                          source
                                          def CochainComplex.HomComplex.Cochain.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K 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] :
                                          CochainComplex.HomComplex.Cochain ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) n

                                          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
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.Cochain.map_v {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K 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)
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.Cochain.map_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z z' : CochainComplex.HomComplex.Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] :
                                            (z + z').map Φ = z.map Φ + z'.map Φ
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.Cochain.map_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K 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] :
                                            (-z).map Φ = -z.map Φ
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.Cochain.map_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (z z' : CochainComplex.HomComplex.Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] :
                                            (z - z').map Φ = z.map Φ - z'.map Φ
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.Cochain.map_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (Φ : CategoryTheory.Functor C D) [Φ.Additive] :
                                            CochainComplex.HomComplex.Cochain.map 0 Φ = 0
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.Cochain.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F 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
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.Cochain.map_ofHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (f : K ⟶ L) (Φ : CategoryTheory.Functor C D) [Φ.Additive] :
                                            (CochainComplex.HomComplex.Cochain.ofHom f).map Φ = CochainComplex.HomComplex.Cochain.ofHom ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).map f)
                                            source
                                            @[simp]
                                            theorem CochainComplex.HomComplex.δ_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (n m : ℤ) {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] :
                                            CochainComplex.HomComplex.δ n m (z.map Φ) = (CochainComplex.HomComplex.δ n m z).map Φ