Documentation

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

The short complexes attached to homological complexes #

In this file, we define a functor shortComplexFunctor C c i : HomologicalComplex C c ⥤ ShortComplex C. By definition, the image of a homological complex K by this functor is the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

The homology K.homology i of a homological complex K in degree i is defined as the homology of the short complex (shortComplexFunctor C c i).obj K, which can be abbreviated as K.sc i.

@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) :
∀ {X Y : HomologicalComplex C c} (f : X Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₁ = f.f i
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) :
∀ {X Y : HomologicalComplex C c} (f : X Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₃ = f.f k
@[simp]
theorem HomologicalComplex.shortComplexFunctor'_map_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) :
∀ {X Y : HomologicalComplex C c} (f : X Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₂ = f.f j

The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

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

    The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

    Equations
    Instances For
      @[simp]
      theorem HomologicalComplex.natIsoSc'_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₁ = (X.XIsoOfEq hi).hom
      @[simp]
      theorem HomologicalComplex.natIsoSc'_hom_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₂ = CategoryTheory.CategoryStruct.id (X.X j)
      @[simp]
      theorem HomologicalComplex.natIsoSc'_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₁ = (X.XIsoOfEq hi).inv
      @[simp]
      theorem HomologicalComplex.natIsoSc'_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₃ = (X.XIsoOfEq hk).hom
      @[simp]
      theorem HomologicalComplex.natIsoSc'_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₃ = (X.XIsoOfEq hk).inv
      @[simp]
      theorem HomologicalComplex.natIsoSc'_inv_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) :
      ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₂ = CategoryTheory.CategoryStruct.id (X.X j)
      noncomputable def HomologicalComplex.natIsoSc' (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) :

      The natural isomorphism shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k when c.prev j = i and c.next j = k.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible, inline]

        The short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

        Equations
        Instances For
          @[reducible, inline]

          The short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

          Equations
          Instances For
            @[reducible, inline]
            noncomputable abbrev HomologicalComplex.isoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) :
            K.sc j K.sc' i j k

            The canonical isomorphism K.sc j ≅ K.sc' i j k when c.prev j = i and c.next j = k.

            Equations
            Instances For
              @[reducible, inline]

              A homological complex K has homology in degree i if the associated short complex K.sc i has.

              Equations
              • K.HasHomology i = (K.sc i).HasHomology
              Instances For
                noncomputable def HomologicalComplex.homology {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] :
                C

                The homology in degree i of a homological complex.

                Equations
                • K.homology i = (K.sc i).homology
                Instances For
                  noncomputable def HomologicalComplex.cycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] :
                  C

                  The cycles in degree i of a homological complex.

                  Equations
                  • K.cycles i = (K.sc i).cycles
                  Instances For
                    noncomputable def HomologicalComplex.iCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] :
                    K.cycles i K.X i

                    The inclusion of the cycles of a homological complex.

                    Equations
                    • K.iCycles i = (K.sc i).iCycles
                    Instances For
                      noncomputable def HomologicalComplex.homologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] :
                      K.cycles i K.homology i

                      The homology class map from cycles to the homology of a homological complex.

                      Equations
                      • K.homologyπ i = (K.sc i).homologyπ
                      Instances For
                        noncomputable def HomologicalComplex.liftCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) :
                        A K.cycles i

                        The morphism to K.cycles i that is induced by a "cycle", i.e. a morphism to K.X i whose postcomposition with the differential is zero.

                        Equations
                        • K.liftCycles k j hj hk = (K.sc i).liftCycles k
                        Instances For
                          @[reducible, inline]
                          noncomputable abbrev HomologicalComplex.liftCycles' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.Rel i j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) :
                          A K.cycles i

                          The morphism to K.cycles i that is induced by a "cycle", i.e. a morphism to K.X i whose postcomposition with the differential is zero.

                          Equations
                          • K.liftCycles' k j hj hk = K.liftCycles k j hk
                          Instances For
                            @[simp]
                            theorem HomologicalComplex.liftCycles_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) {Z : C} (h : K.X i Z) :
                            @[simp]
                            theorem HomologicalComplex.liftCycles_i {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) :
                            CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (K.iCycles i) = k
                            noncomputable def HomologicalComplex.toCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] :
                            K.X i K.cycles j

                            The map K.X i ⟶ K.cycles j induced by the differential K.d i j.

                            Equations
                            • K.toCycles i j = K.liftCycles (K.d i j) (c.next j)
                            Instances For
                              @[simp]
                              theorem HomologicalComplex.iCycles_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] :
                              CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.d i j) = 0
                              noncomputable def HomologicalComplex.cyclesIsKernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] (hj : c.next i = j) :

                              K.cycles i is the kernel of K.d i j when c.next i = j.

                              Equations
                              • K.cyclesIsKernel i j hj = hj(K.sc i).cyclesIsKernel
                              Instances For
                                @[simp]
                                theorem HomologicalComplex.toCycles_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] {Z : C} (h : K.X j Z) :
                                @[simp]
                                theorem HomologicalComplex.toCycles_i {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] :
                                CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.iCycles j) = K.d i j
                                Equations
                                • =
                                Equations
                                • =
                                @[simp]
                                theorem HomologicalComplex.d_toCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology k] {Z : C} (h : K.cycles k Z) :
                                @[simp]
                                theorem HomologicalComplex.d_toCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology k] :
                                CategoryTheory.CategoryStruct.comp (K.d i j) (K.toCycles j k) = 0
                                theorem HomologicalComplex.comp_liftCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A' : C} {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' A) {Z : C} (h : K.cycles i Z) :
                                theorem HomologicalComplex.comp_liftCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A' : C} {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' A) :
                                CategoryTheory.CategoryStruct.comp α (K.liftCycles k j hj hk) = K.liftCycles (CategoryTheory.CategoryStruct.comp α k) j hj
                                theorem HomologicalComplex.liftCycles_homologyπ_eq_zero_of_boundary_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) {i' : ι} (x : A K.X i') (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)) {Z : C} (h : K.homology i Z) :
                                theorem HomologicalComplex.liftCycles_homologyπ_eq_zero_of_boundary {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) {i' : ι} (x : A K.X i') (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)) :
                                CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj ) (K.homologyπ i) = 0
                                @[simp]
                                @[simp]
                                theorem HomologicalComplex.toCycles_comp_homologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] :
                                CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.homologyπ j) = 0
                                noncomputable def HomologicalComplex.homologyIsCokernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] (hi : c.prev j = i) [K.HasHomology j] :

                                K.homology j is the cokernel of K.toCycles i j : K.X i ⟶ K.cycles j when c.prev j = i.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  noncomputable def HomologicalComplex.opcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] :
                                  C

                                  The opcycles in degree i of a homological complex.

                                  Equations
                                  • K.opcycles i = (K.sc i).opcycles
                                  Instances For
                                    noncomputable def HomologicalComplex.pOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] :
                                    K.X i K.opcycles i

                                    The projection to the opcycles of a homological complex.

                                    Equations
                                    • K.pOpcycles i = (K.sc i).pOpcycles
                                    Instances For
                                      noncomputable def HomologicalComplex.homologyι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] :
                                      K.homology i K.opcycles i

                                      The inclusion map of the homology of a homological complex into its opcycles.

                                      Equations
                                      • K.homologyι i = (K.sc i).homologyι
                                      Instances For
                                        noncomputable def HomologicalComplex.descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) :
                                        K.opcycles i A

                                        The morphism from K.opcycles i that is induced by an "opcycle", i.e. a morphism from K.X i whose precomposition with the differential is zero.

                                        Equations
                                        • K.descOpcycles k j hj hk = (K.sc i).descOpcycles k
                                        Instances For
                                          @[reducible, inline]
                                          noncomputable abbrev HomologicalComplex.descOpcycles' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i A) (j : ι) (hj : c.Rel j i) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) :
                                          K.opcycles i A

                                          The morphism from K.opcycles i that is induced by an "opcycle", i.e. a morphism from K.X i whose precomposition with the differential is zero.

                                          Equations
                                          • K.descOpcycles' k j hj hk = K.descOpcycles k j hk
                                          Instances For
                                            @[simp]
                                            theorem HomologicalComplex.p_descOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) {Z : C} (h : A Z) :
                                            @[simp]
                                            theorem HomologicalComplex.p_descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) :
                                            CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.descOpcycles k j hj hk) = k
                                            noncomputable def HomologicalComplex.fromOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] :
                                            K.opcycles i K.X j

                                            The map K.opcycles i ⟶ K.X j induced by the differential K.d i j.

                                            Equations
                                            • K.fromOpcycles i j = K.descOpcycles (K.d i j) (c.prev i)
                                            Instances For
                                              @[simp]
                                              theorem HomologicalComplex.d_pOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.opcycles j Z) :
                                              @[simp]
                                              theorem HomologicalComplex.d_pOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :
                                              CategoryTheory.CategoryStruct.comp (K.d i j) (K.pOpcycles j) = 0
                                              noncomputable def HomologicalComplex.opcyclesIsCokernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] (hi : c.prev j = i) [K.HasHomology j] :

                                              K.opcycles j is the cokernel of K.d i j when c.prev j = i.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem HomologicalComplex.p_fromOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] {Z : C} (h : K.X j Z) :
                                                @[simp]
                                                theorem HomologicalComplex.p_fromOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] :
                                                CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.fromOpcycles i j) = K.d i j
                                                Equations
                                                • =
                                                Equations
                                                • =
                                                @[simp]
                                                theorem HomologicalComplex.fromOpcycles_d_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology i] {Z : C} (h : K.X k Z) :
                                                @[simp]
                                                theorem HomologicalComplex.fromOpcycles_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology i] :
                                                CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) (K.d j k) = 0
                                                theorem HomologicalComplex.descOpcycles_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} {A' : C} (k : K.X i A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A A') {Z : C} (h : A' Z) :
                                                theorem HomologicalComplex.descOpcycles_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} {A' : C} (k : K.X i A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A A') :
                                                CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj hk) α = K.descOpcycles (CategoryTheory.CategoryStruct.comp k α) j hj
                                                theorem HomologicalComplex.homologyι_descOpcycles_eq_zero_of_boundary_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i A) (j : ι) (hj : c.prev i = j) {i' : ι} (x : K.X i' A) (hx : k = CategoryTheory.CategoryStruct.comp (K.d i i') x) {Z : C} (h : A Z) :
                                                theorem HomologicalComplex.homologyι_descOpcycles_eq_zero_of_boundary {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i A) (j : ι) (hj : c.prev i = j) {i' : ι} (x : K.X i' A) (hx : k = CategoryTheory.CategoryStruct.comp (K.d i i') x) :
                                                CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.descOpcycles k j hj ) = 0
                                                @[simp]
                                                theorem HomologicalComplex.homologyι_comp_fromOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] :
                                                CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.fromOpcycles i j) = 0
                                                noncomputable def HomologicalComplex.homologyIsKernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] (hi : c.next i = j) :

                                                K.homology i is the kernel of K.fromOpcycles i j : K.opcycles i ⟶ K.X j when c.next i = j.

                                                Equations
                                                • K.homologyIsKernel i j hi = hi(K.sc i).homologyIsKernel
                                                Instances For
                                                  noncomputable def HomologicalComplex.homologyMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                  K.homology i L.homology i

                                                  The map K.homology i ⟶ L.homology i induced by a morphism in HomologicalComplex.

                                                  Equations
                                                  Instances For
                                                    noncomputable def HomologicalComplex.cyclesMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                    K.cycles i L.cycles i

                                                    The map K.cycles i ⟶ L.cycles i induced by a morphism in HomologicalComplex.

                                                    Equations
                                                    Instances For
                                                      noncomputable def HomologicalComplex.opcyclesMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                      K.opcycles i L.opcycles i

                                                      The map K.opcycles i ⟶ L.opcycles i induced by a morphism in HomologicalComplex.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem HomologicalComplex.cyclesMap_i {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                        @[simp]
                                                        @[simp]
                                                        theorem HomologicalComplex.p_opcyclesMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                        Equations
                                                        • =
                                                        Equations
                                                        • =
                                                        @[simp]
                                                        @[simp]
                                                        theorem HomologicalComplex.cyclesMap_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (L : HomologicalComplex C c) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                        @[simp]
                                                        @[simp]
                                                        theorem HomologicalComplex.homology_π_ι_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} (i : ι) [K.HasHomology i] {Z : C} (h : K.opcycles i Z) :
                                                        @[simp]
                                                        theorem HomologicalComplex.homology_π_ι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} (i : ι) [K.HasHomology i] :
                                                        CategoryTheory.CategoryStruct.comp (K.homologyπ i) (K.homologyι i) = CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.pOpcycles i)
                                                        @[simp]
                                                        theorem HomologicalComplex.opcyclesMap_comp_descOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : L.X i A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (L.d j i) k = 0) (φ : K L) {Z : C} (h : A Z) :
                                                        @[simp]
                                                        theorem HomologicalComplex.opcyclesMap_comp_descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : L.X i A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (L.d j i) k = 0) (φ : K L) :
                                                        CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (L.descOpcycles k j hj hk) = K.descOpcycles (CategoryTheory.CategoryStruct.comp (φ.f i) k) j hj
                                                        @[simp]
                                                        theorem HomologicalComplex.liftCycles_comp_cyclesMap_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K L) {Z : C} (h : L.cycles i Z) :
                                                        @[simp]
                                                        theorem HomologicalComplex.liftCycles_comp_cyclesMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : A K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K L) :
                                                        CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (HomologicalComplex.cyclesMap φ i) = L.liftCycles (CategoryTheory.CategoryStruct.comp k (φ.f i)) j hj

                                                        The ith homology functor HomologicalComplex C c ⥤ C.

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

                                                          The homology functor to graded objects.

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

                                                            The ith cycles functor HomologicalComplex C c ⥤ C.

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

                                                              The ith opcycles functor HomologicalComplex C c ⥤ C.

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

                                                                The natural transformation K.homologyπ i : K.cycles i ⟶ K.homology i for all K : HomologicalComplex C c.

                                                                Equations
                                                                Instances For

                                                                  The natural transformation K.homologyι i : K.homology i ⟶ K.opcycles i for all K : HomologicalComplex C c.

                                                                  Equations
                                                                  Instances For

                                                                    The natural isomorphism K.homology j ≅ (K.sc' i j k).homology for all homological complexes K when c.prev j = i and c.next j = k.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      theorem HomologicalComplex.isIso_iCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                      CategoryTheory.IsIso (K.iCycles i)
                                                                      @[simp]
                                                                      theorem HomologicalComplex.iCyclesIso_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                      (K.iCyclesIso i j hj h).hom = K.iCycles i
                                                                      noncomputable def HomologicalComplex.iCyclesIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                      K.cycles i K.X i

                                                                      The canonical isomorphism K.cycles i ≅ K.X i when the differential from i is zero.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem HomologicalComplex.iCyclesIso_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.cycles i Z) :
                                                                        CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h✝).inv h) = h
                                                                        @[simp]
                                                                        theorem HomologicalComplex.iCyclesIso_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                        CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.iCyclesIso i j hj h).inv = CategoryTheory.CategoryStruct.id (K.cycles i)
                                                                        @[simp]
                                                                        theorem HomologicalComplex.iCyclesIso_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.X i Z) :
                                                                        CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h✝).inv (CategoryTheory.CategoryStruct.comp (K.iCycles i) h) = h
                                                                        @[simp]
                                                                        theorem HomologicalComplex.iCyclesIso_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                        CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h).inv (K.iCycles i) = CategoryTheory.CategoryStruct.id (K.X i)
                                                                        theorem HomologicalComplex.isIso_homologyι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                        CategoryTheory.IsIso (K.homologyι i)
                                                                        @[simp]
                                                                        theorem HomologicalComplex.isoHomologyι_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                        (K.isoHomologyι i j hj h).hom = K.homologyι i
                                                                        noncomputable def HomologicalComplex.isoHomologyι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                        K.homology i K.opcycles i

                                                                        The canonical isomorphism K.homology i ≅ K.opcycles i when the differential from i is zero.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem HomologicalComplex.isoHomologyι_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.homology i Z) :
                                                                          CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h✝).inv h) = h
                                                                          @[simp]
                                                                          theorem HomologicalComplex.isoHomologyι_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                          CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.isoHomologyι i j hj h).inv = CategoryTheory.CategoryStruct.id (K.homology i)
                                                                          @[simp]
                                                                          theorem HomologicalComplex.isoHomologyι_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.opcycles i Z) :
                                                                          CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h✝).inv (CategoryTheory.CategoryStruct.comp (K.homologyι i) h) = h
                                                                          @[simp]
                                                                          theorem HomologicalComplex.isoHomologyι_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] :
                                                                          CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h).inv (K.homologyι i) = CategoryTheory.CategoryStruct.id (K.opcycles i)
                                                                          theorem HomologicalComplex.isIso_pOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                          CategoryTheory.IsIso (K.pOpcycles j)
                                                                          @[simp]
                                                                          theorem HomologicalComplex.pOpcyclesIso_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                          (K.pOpcyclesIso i j hi h).hom = K.pOpcycles j
                                                                          noncomputable def HomologicalComplex.pOpcyclesIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                          K.X j K.opcycles j

                                                                          The canonical isomorphism K.X j ≅ K.opCycles j when the differential to j is zero.

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem HomologicalComplex.pOpcyclesIso_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.X j Z) :
                                                                            CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h✝).inv h) = h
                                                                            @[simp]
                                                                            theorem HomologicalComplex.pOpcyclesIso_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                            CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.pOpcyclesIso i j hi h).inv = CategoryTheory.CategoryStruct.id (K.X j)
                                                                            @[simp]
                                                                            theorem HomologicalComplex.pOpcyclesIso_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.opcycles j Z) :
                                                                            CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h✝).inv (CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h) = h
                                                                            @[simp]
                                                                            theorem HomologicalComplex.pOpcyclesIso_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                            CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h).inv (K.pOpcycles j) = CategoryTheory.CategoryStruct.id (K.opcycles j)
                                                                            theorem HomologicalComplex.isIso_homologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                            CategoryTheory.IsIso (K.homologyπ j)
                                                                            @[simp]
                                                                            theorem HomologicalComplex.isoHomologyπ_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                            (K.isoHomologyπ i j hi h).hom = K.homologyπ j
                                                                            noncomputable def HomologicalComplex.isoHomologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                            K.cycles j K.homology j

                                                                            The canonical isomorphism K.cycles j ≅ K.homology j when the differential to j is zero.

                                                                            Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem HomologicalComplex.isoHomologyπ_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.cycles j Z) :
                                                                              CategoryTheory.CategoryStruct.comp (K.homologyπ j) (CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h✝).inv h) = h
                                                                              @[simp]
                                                                              theorem HomologicalComplex.isoHomologyπ_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                              CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.isoHomologyπ i j hi h).inv = CategoryTheory.CategoryStruct.id (K.cycles j)
                                                                              @[simp]
                                                                              theorem HomologicalComplex.isoHomologyπ_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.homology j Z) :
                                                                              CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h✝).inv (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h) = h
                                                                              @[simp]
                                                                              theorem HomologicalComplex.isoHomologyπ_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] :
                                                                              CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h).inv (K.homologyπ j) = CategoryTheory.CategoryStruct.id (K.homology j)
                                                                              theorem HomologicalComplex.epi_homologyMap_of_epi_of_not_rel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [CategoryTheory.Epi (φ.f i)] (hi : ∀ (j : ι), ¬c.Rel i j) :
                                                                              theorem HomologicalComplex.mono_homologyMap_of_mono_of_not_rel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (j : ι) [K.HasHomology j] [L.HasHomology j] [CategoryTheory.Mono (φ.f j)] (hj : ∀ (i : ι), ¬c.Rel i j) :

                                                                              A homological complex K is exact at i if the short complex K.sc i is exact.

                                                                              Equations
                                                                              • K.ExactAt i = (K.sc i).Exact
                                                                              Instances For
                                                                                theorem HomologicalComplex.exactAt_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) :
                                                                                K.ExactAt i (K.sc i).Exact
                                                                                theorem HomologicalComplex.ExactAt.of_iso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι} (hK : K.ExactAt i) {L : HomologicalComplex C c} (e : K L) :
                                                                                L.ExactAt i
                                                                                theorem HomologicalComplex.exactAt_iff' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) :
                                                                                K.ExactAt j (K.sc' i j k).Exact
                                                                                @[reducible, inline]

                                                                                The canonical isomorphism K.homology 0 ≅ K.opcycles 0 for a chain complex K indexed by .

                                                                                Equations
                                                                                Instances For
                                                                                  @[reducible, inline]

                                                                                  The canonical isomorphism K.cycles 0 ≅ K.homology 0 for a cochain complex K indexed by .

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem HomologicalComplex.homologyMap_neg {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                                                    @[simp]
                                                                                    theorem HomologicalComplex.homologyMap_add {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (ψ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                                                    @[simp]
                                                                                    theorem HomologicalComplex.homologyMap_sub {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (ψ : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                                                    noncomputable def HomologicalComplex.cyclesIsoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                    K.cycles j (K.sc' i j k).cycles

                                                                                    The cycles of a homological complex in degree j can be computed by specifying a choice of c.prev j and c.next j.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem HomologicalComplex.cyclesIsoSc'_hom_iCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).X₂ Z) :
                                                                                      CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (K.sc' i j k).iCycles h) = CategoryTheory.CategoryStruct.comp (K.iCycles j) h
                                                                                      @[simp]
                                                                                      theorem HomologicalComplex.cyclesIsoSc'_hom_iCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                      CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (K.sc' i j k).iCycles = K.iCycles j
                                                                                      @[simp]
                                                                                      theorem HomologicalComplex.cyclesIsoSc'_inv_iCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.X j Z) :
                                                                                      CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).iCycles h
                                                                                      @[simp]
                                                                                      theorem HomologicalComplex.cyclesIsoSc'_inv_iCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                      CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (K.iCycles j) = (K.sc' i j k).iCycles
                                                                                      @[simp]
                                                                                      theorem HomologicalComplex.toCycles_cyclesIsoSc'_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).cycles Z) :
                                                                                      CategoryTheory.CategoryStruct.comp (K.toCycles i j) (CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).toCycles h
                                                                                      @[simp]
                                                                                      theorem HomologicalComplex.toCycles_cyclesIsoSc'_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                      CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles
                                                                                      noncomputable def HomologicalComplex.opcyclesIsoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                      K.opcycles j (K.sc' i j k).opcycles

                                                                                      The homology of a homological complex in degree j can be computed by specifying a choice of c.prev j and c.next j.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.opcycles j Z) :
                                                                                        CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv h) = CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h
                                                                                        @[simp]
                                                                                        theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                        CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles (K.opcyclesIsoSc' i j k hi hk).inv = K.pOpcycles j
                                                                                        @[simp]
                                                                                        theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).opcycles Z) :
                                                                                        CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles h
                                                                                        @[simp]
                                                                                        theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                        CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles
                                                                                        @[simp]
                                                                                        theorem HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.X k Z) :
                                                                                        CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.fromOpcycles j k) h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).fromOpcycles h
                                                                                        @[simp]
                                                                                        theorem HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                        CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv (K.fromOpcycles j k) = (K.sc' i j k).fromOpcycles
                                                                                        noncomputable def HomologicalComplex.homologyIsoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                        K.homology j (K.sc' i j k).homology

                                                                                        The opcycles of a homological complex in degree j can be computed by specifying a choice of c.prev j and c.next j.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.π_homologyIsoSc'_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).homology Z) :
                                                                                          CategoryTheory.CategoryStruct.comp (K.homologyπ j) (CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ h)
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.π_homologyIsoSc'_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                          CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.homologyIsoSc' i j k hi hk).hom = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (K.sc' i j k).homologyπ
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.π_homologyIsoSc'_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.homology j Z) :
                                                                                          CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ (CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv h) = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h)
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.π_homologyIsoSc'_inv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                          CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ (K.homologyIsoSc' i j k hi hk).inv = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (K.homologyπ j)
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.homologyIsoSc'_hom_ι_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).opcycles Z) :
                                                                                          CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι h) = CategoryTheory.CategoryStruct.comp (K.homologyι j) (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).hom h)
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.homologyIsoSc'_hom_ι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                          CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom (K.sc' i j k).homologyι = CategoryTheory.CategoryStruct.comp (K.homologyι j) (K.opcyclesIsoSc' i j k hi hk).hom
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.homologyIsoSc'_inv_ι_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.opcycles j Z) :
                                                                                          CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.homologyι j) h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv h)
                                                                                          @[simp]
                                                                                          theorem HomologicalComplex.homologyIsoSc'_inv_ι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] :
                                                                                          CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv (K.homologyι j) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι (K.opcyclesIsoSc' i j k hi hk).inv