Documentation

Mathlib.Algebra.Homology.Augment

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

@[simp]

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

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.

    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.

      Instances For

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

        Instances For

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

          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.

            Instances For

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

              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.

                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.

                  Instances For

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

                    Instances For

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

                      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.

                        Instances For