Documentation

Mathlib.Algebra.Homology.Homology

The homology of a complex #

Given C : HomologicalComplex V c, we have C.cycles' i and C.boundaries i, both defined as subobjects of C.X i.

We show these are functorial with respect to chain maps, as cyclesMap' f i and boundariesMap f i.

As a consequence we construct homologyFunctor' i : HomologicalComplex V c ⥤ V, computing the i-th homology.

Note: Some definitions (specifically, names containing components homology, cycles) in this file have the suffix ' so as to allow the development of the new homology API of homological complex (starting from Algebra.Homology.ShortComplex.HomologicalComplex). It is planned that these definitions shall be removed and replaced by the new API.

@[reducible, inline]

The cycles at index i, as a subobject.

Equations
Instances For
    def HomologicalComplex.cycles'IsoKernel {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i : ι} {j : ι} (r : c.Rel i j) :
    CategoryTheory.Subobject.underlying.obj (C.cycles' i) CategoryTheory.Limits.kernel (C.d i j)

    The underlying object of C.cycles' i is isomorphic to kernel (C.d i j), for any j such that Rel i j.

    Equations
    Instances For
      @[reducible, inline]

      The boundaries at index i, as a subobject.

      Equations
      Instances For
        def HomologicalComplex.boundariesIsoImage {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i : ι} {j : ι} (r : c.Rel i j) :
        CategoryTheory.Subobject.underlying.obj (C.boundaries j) CategoryTheory.Limits.image (C.d i j)

        The underlying object of C.boundaries j is isomorphic to image (C.d i j), for any i such that Rel i j.

        Equations
        Instances For
          @[reducible, inline]
          abbrev HomologicalComplex.boundariesToCycles' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (C : HomologicalComplex V c) (i : ι) :
          CategoryTheory.Subobject.underlying.obj (C.boundaries i) CategoryTheory.Subobject.underlying.obj (C.cycles' i)

          The canonical map from boundaries i to cycles' i.

          Equations
          Instances For
            @[simp]
            theorem HomologicalComplex.imageToKernel_as_boundariesToCycles' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (C : HomologicalComplex V c) (i : ι) (h : C.boundaries i C.cycles' i) :
            (C.boundaries i).ofLE (C.cycles' i) h = C.boundariesToCycles' i

            Prefer boundariesToCycles'.

            @[reducible, inline]

            The homology of a complex at index i.

            Equations
            • C.homology' i = homology' (C.dTo i) (C.dFrom i)
            Instances For
              def HomologicalComplex.homology'Iso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasCokernels V] (C : HomologicalComplex V c) {i : ι} {j : ι} {k : ι} (hij : c.Rel i j) (hjk : c.Rel j k) :
              C.homology' j homology' (C.d i j) (C.d j k)

              The jth homology of a homological complex (as kernel of 'the differential from Cⱼ' modulo the image of 'the differential to Cⱼ') is isomorphic to the kernel of d : Cⱼ → Cₖ modulo the image of d : Cᵢ → Cⱼ when Rel i j and Rel j k.

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

                The 0th homology of a chain complex is isomorphic to the cokernel of d : C₁ ⟶ C₀.

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

                  The 0th cohomology of a cochain complex is isomorphic to the kernel of d : C₀ → C₁.

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

                    The n + 1th homology of a chain complex (as kernel of 'the differential from Cₙ₊₁' modulo the image of 'the differential to Cₙ₊₁') is isomorphic to the kernel of d : Cₙ₊₁ → Cₙ modulo the image of d : Cₙ₊₂ → Cₙ₊₁.

                    Equations
                    Instances For

                      The n + 1th cohomology of a cochain complex (as kernel of 'the differential from Cₙ₊₁' modulo the image of 'the differential to Cₙ₊₁') is isomorphic to the kernel of d : Cₙ₊₁ → Cₙ₊₂ modulo the image of d : Cₙ → Cₙ₊₁.

                      Equations
                      Instances For

                        Computing the cycles is functorial.

                        @[reducible, inline]
                        abbrev cycles'Map {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ C₂) (i : ι) :
                        CategoryTheory.Subobject.underlying.obj (C₁.cycles' i) CategoryTheory.Subobject.underlying.obj (C₂.cycles' i)

                        The morphism between cycles induced by a chain map.

                        Equations
                        Instances For
                          @[simp]
                          theorem cycles'Map_arrow_apply {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ C₂) (i : ι) [inst : CategoryTheory.ConcreteCategory V] (x : (CategoryTheory.forget V).obj (CategoryTheory.Subobject.underlying.obj (C₁.cycles' i))) :
                          (C₂.cycles' i).arrow (((C₂.cycles' i).factorThru (CategoryTheory.CategoryStruct.comp (C₁.cycles' i).arrow (f.f i)) ) x) = (f.f i) ((C₁.cycles' i).arrow x)
                          @[simp]
                          @[simp]
                          theorem cycles'Functor_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasKernels V] (i : ι) (C : HomologicalComplex V c) :
                          (cycles'Functor V c i).obj C = CategoryTheory.Subobject.underlying.obj (C.cycles' i)

                          Cycles as a functor.

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

                            Computing the boundaries is functorial.

                            @[reducible, inline]
                            abbrev boundariesMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ C₂) (i : ι) :
                            CategoryTheory.Subobject.underlying.obj (C₁.boundaries i) CategoryTheory.Subobject.underlying.obj (C₂.boundaries i)

                            The morphism between boundaries induced by a chain map.

                            Equations
                            Instances For
                              @[simp]
                              theorem boundariesFunctor_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (i : ι) (C : HomologicalComplex V c) :
                              (boundariesFunctor V c i).obj C = CategoryTheory.Subobject.underlying.obj (C.boundaries i)

                              Boundaries as a functor.

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

                                The boundariesToCycles morphisms are natural.

                                The natural transformation from the boundaries functor to the cycles functor.

                                Equations
                                Instances For

                                  The i-th homology, as a functor to V.

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

                                    The homology functor from ι-indexed complexes to ι-graded objects in V.

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