Documentation

Mathlib.Algebra.Homology.DifferentialObject

Homological complexes are differential graded objects. #

We verify that a HomologicalComplex indexed by an AddCommGroup is essentially the same thing as a differential graded object.

This equivalence is probably not particularly useful in practice; it's here to check that definitions match up as expected.

We first prove some results about differential graded objects.

Porting note: after the port, move these to their own file.

source
@[reducible, inline]
abbrev CategoryTheory.DifferentialObject.objEqToHom {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {i j : β} (h : i = j) :
X.obj i ⟶ X.obj j

Since eqToHom only preserves the fact that X.X i = X.X j but not i = j, this definition is used to aid the simplifier.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.DifferentialObject.objEqToHom_refl {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) (i : β) :
    X.objEqToHom ⋯ = CategoryStruct.id (X.obj i)
    source
    @[simp]
    theorem CategoryTheory.DifferentialObject.objEqToHom_d {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x y : β} (h : x = y) :
    CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)
    source
    @[simp]
    theorem CategoryTheory.DifferentialObject.objEqToHom_d_assoc {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x y : β} (h : x = y) {Z : V} (h✝ : (CategoryTheory.shiftFunctor (GradedObjectWithShift b V) 1).obj X.obj y ⟶ Z) :
    CategoryStruct.comp (X.objEqToHom h) (CategoryStruct.comp (X.d y) h✝) = CategoryStruct.comp (X.d x) (CategoryStruct.comp (X.objEqToHom ⋯) h✝)
    source
    @[simp]
    theorem CategoryTheory.DifferentialObject.d_squared_apply {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x : β} :
    CategoryStruct.comp (X.d x) (X.d ((fun (b_1 : β) => b_1 + { as := 1 }.as • b) x)) = 0
    source
    @[simp]
    theorem CategoryTheory.DifferentialObject.d_squared_apply_assoc {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x : β} {Z : V} (h : (CategoryTheory.shiftFunctor (GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z) :
    CategoryStruct.comp (X.d x) (CategoryStruct.comp (X.d (x + 1 • b)) h) = CategoryStruct.comp 0 h
    source
    @[simp]
    theorem CategoryTheory.DifferentialObject.eqToHom_f' {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) :
    CategoryStruct.comp (X.objEqToHom h) (f.f y) = CategoryStruct.comp (f.f x) (Y.objEqToHom h)
    source
    @[simp]
    theorem CategoryTheory.DifferentialObject.eqToHom_f'_assoc {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) {Z : V} (h✝ : Y.obj y ⟶ Z) :
    CategoryStruct.comp (X.objEqToHom h) (CategoryStruct.comp (f.f y) h✝) = CategoryStruct.comp (f.f x) (CategoryStruct.comp (Y.objEqToHom h) h✝)
    source
    @[simp]
    theorem HomologicalComplex.d_eqToHom {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) :
    CategoryTheory.CategoryStruct.comp (X.d x y) (CategoryTheory.eqToHom ⋯) = X.d x z
    source
    @[simp]
    theorem HomologicalComplex.d_eqToHom_assoc {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) {Z : V} (h✝ : X.X z ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (X.d x y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝) = CategoryTheory.CategoryStruct.comp (X.d x z) h✝
    source
    def HomologicalComplex.dgoToHomologicalComplex {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
    CategoryTheory.Functor (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (HomologicalComplex V (ComplexShape.up' b))

    The functor from differential graded objects to homological complexes.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HomologicalComplex.dgoToHomologicalComplex_obj_d {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i j : β) :
      ((dgoToHomologicalComplex b V).obj X).d i j = if h : i + b = j then CategoryTheory.CategoryStruct.comp (X.d i) (X.objEqToHom ⋯) else 0
      source
      @[simp]
      theorem HomologicalComplex.dgoToHomologicalComplex_obj_X {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) :
      ((dgoToHomologicalComplex b V).obj X).X i = X.obj i
      source
      @[simp]
      theorem HomologicalComplex.dgoToHomologicalComplex_map_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) (i : β) :
      ((dgoToHomologicalComplex b V).map f).f i = f.f i
      source
      def HomologicalComplex.homologicalComplexToDGO {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
      CategoryTheory.Functor (HomologicalComplex V (ComplexShape.up' b)) (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V))

      The functor from homological complexes to differential graded objects.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem HomologicalComplex.homologicalComplexToDGO_obj_obj {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) :
        ((homologicalComplexToDGO b V).obj X).obj i = X.X i
        source
        @[simp]
        theorem HomologicalComplex.homologicalComplexToDGO_obj_d {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) :
        ((homologicalComplexToDGO b V).obj X).d i = X.d i ((fun (b_1 : β) => b_1 + { as := 1 }.as • b) i)
        source
        @[simp]
        theorem HomologicalComplex.homologicalComplexToDGO_map_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V (ComplexShape.up' b)} (f : X ⟶ Y) (i : β) :
        ((homologicalComplexToDGO b V).map f).f i = f.f i
        source
        def HomologicalComplex.dgoEquivHomologicalComplexUnitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
        CategoryTheory.Functor.id (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) ≅ (dgoToHomologicalComplex b V).comp (homologicalComplexToDGO b V)

        The unit isomorphism for dgoEquivHomologicalComplex.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) :
          ((dgoEquivHomologicalComplexUnitIso b V).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.obj i)
          source
          @[simp]
          theorem HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) :
          ((dgoEquivHomologicalComplexUnitIso b V).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.obj i)
          source
          def HomologicalComplex.dgoEquivHomologicalComplexCounitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
          (homologicalComplexToDGO b V).comp (dgoToHomologicalComplex b V) ≅ CategoryTheory.Functor.id (HomologicalComplex V (ComplexShape.up' b))

          The counit isomorphism for dgoEquivHomologicalComplex.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) :
            ((dgoEquivHomologicalComplexCounitIso b V).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)
            source
            @[simp]
            theorem HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) :
            ((dgoEquivHomologicalComplexCounitIso b V).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)
            source
            def HomologicalComplex.dgoEquivHomologicalComplex {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
            CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V) ≌ HomologicalComplex V (ComplexShape.up' b)

            The category of differential graded objects in V is equivalent to the category of homological complexes in V.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem HomologicalComplex.dgoEquivHomologicalComplex_functor {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
              (dgoEquivHomologicalComplex b V).functor = dgoToHomologicalComplex b V
              source
              @[simp]
              theorem HomologicalComplex.dgoEquivHomologicalComplex_unitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
              (dgoEquivHomologicalComplex b V).unitIso = dgoEquivHomologicalComplexUnitIso b V
              source
              @[simp]
              theorem HomologicalComplex.dgoEquivHomologicalComplex_counitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
              (dgoEquivHomologicalComplex b V).counitIso = dgoEquivHomologicalComplexCounitIso b V
              source
              @[simp]
              theorem HomologicalComplex.dgoEquivHomologicalComplex_inverse {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
              (dgoEquivHomologicalComplex b V).inverse = homologicalComplexToDGO b V