Documentation

Mathlib.Algebra.Homology.Augment

Augmentation and truncation of -indexed (co)chain complexes. #

@[simp]
theorem ChainComplex.truncate_obj_X {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) (i : ) :
(ChainComplex.truncate.obj C).X i = C.X (i + 1)
@[simp]
theorem ChainComplex.truncate_obj_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) (i : ) (j : ) :
(ChainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
@[simp]
theorem ChainComplex.truncate_map_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
∀ {X Y : ChainComplex V } (f : X Y) (i : ), (ChainComplex.truncate.map f).f i = f.f (i + 1)

The truncation of an -indexed chain complex, deleting the object at 0 and shifting everything else down.

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

    There is a canonical chain map from the truncation of a chain map C to the "single object" chain complex consisting of the truncated object C.X 0 in degree 0. The components of this chain map are C.d 1 0 in degree 0, and zero otherwise.

    Equations
    • C.truncateTo = ((ChainComplex.truncate.obj C).toSingle₀Equiv (C.X 0)).symm C.d 1 0,
    Instances For

      We can "augment" a chain complex by inserting an arbitrary object in degree zero (shifting everything else up), along with a suitable differential.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem ChainComplex.augment_X_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :
        (C.augment f w).X 0 = X
        @[simp]
        theorem ChainComplex.augment_X_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) :
        (C.augment f w).X (i + 1) = C.X i
        @[simp]
        theorem ChainComplex.augment_d_one_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :
        (C.augment f w).d 1 0 = f
        @[simp]
        theorem ChainComplex.augment_d_succ_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) (j : ) :
        (C.augment f w).d (i + 1) (j + 1) = C.d i j
        def ChainComplex.truncateAugment {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :
        ChainComplex.truncate.obj (C.augment f w) C

        Truncating an augmented chain complex is isomorphic (with components the identity) to the original complex.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem ChainComplex.truncateAugment_hom_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) :
          (C.truncateAugment f w).hom.f i = CategoryTheory.CategoryStruct.id (C.X i)
          @[simp]
          theorem ChainComplex.truncateAugment_inv_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) :
          (C.truncateAugment f w).inv.f i = CategoryTheory.CategoryStruct.id ((ChainComplex.truncate.obj (C.augment f w)).X i)
          def ChainComplex.augmentTruncate {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ) :
          (ChainComplex.truncate.obj C).augment (C.d 1 0) C

          Augmenting a truncated complex with the original object and morphism is isomorphic (with components the identity) to the original complex.

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

            A chain map from a chain complex to a single object chain complex in degree zero can be reinterpreted as a chain complex.

            This is the inverse construction of truncateTo.

            Equations
            • C.toSingle₀AsComplex X f = match (C.toSingle₀Equiv X) f with | f, w => C.augment f w
            Instances For
              @[simp]
              theorem CochainComplex.truncate_obj_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) (i : ) (j : ) :
              (CochainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
              @[simp]
              theorem CochainComplex.truncate_obj_X {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) (i : ) :
              (CochainComplex.truncate.obj C).X i = C.X (i + 1)
              @[simp]
              theorem CochainComplex.truncate_map_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] :
              ∀ {X Y : CochainComplex V } (f : X Y) (i : ), (CochainComplex.truncate.map f).f i = f.f (i + 1)

              The truncation of an -indexed cochain complex, deleting the object at 0 and shifting everything else down.

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

                There is a canonical chain map from the truncation of a cochain complex C to the "single object" cochain complex consisting of the truncated object C.X 0 in degree 0. The components of this chain map are C.d 0 1 in degree 0, and zero otherwise.

                Equations
                • C.toTruncate = ((CochainComplex.truncate.obj C).fromSingle₀Equiv (C.X 0)).symm C.d 0 1,
                Instances For

                  We can "augment" a cochain complex by inserting an arbitrary object in degree zero (shifting everything else up), along with a suitable differential.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CochainComplex.augment_X_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :
                    (C.augment f w).X 0 = X
                    @[simp]
                    theorem CochainComplex.augment_X_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ) :
                    (C.augment f w).X (i + 1) = C.X i
                    @[simp]
                    theorem CochainComplex.augment_d_zero_one {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :
                    (C.augment f w).d 0 1 = f
                    @[simp]
                    theorem CochainComplex.augment_d_succ_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ) (j : ) :
                    (C.augment f w).d (i + 1) (j + 1) = C.d i j
                    def CochainComplex.truncateAugment {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :
                    CochainComplex.truncate.obj (C.augment f w) C

                    Truncating an augmented cochain complex is isomorphic (with components the identity) to the original complex.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      @[simp]
                      theorem CochainComplex.truncateAugment_inv_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ) :
                      (C.truncateAugment f w).inv.f i = CategoryTheory.CategoryStruct.id ((CochainComplex.truncate.obj (C.augment f w)).X i)
                      def CochainComplex.augmentTruncate {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ) :
                      (CochainComplex.truncate.obj C).augment (C.d 0 1) C

                      Augmenting a truncated complex with the original object and morphism is isomorphic (with components the identity) to the original complex.

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

                        A chain map from a single object cochain complex in degree zero to a cochain complex can be reinterpreted as a cochain complex.

                        This is the inverse construction of toTruncate.

                        Equations
                        • C.fromSingle₀AsComplex X f = match (C.fromSingle₀Equiv X) f with | f, w => C.augment f w
                        Instances For