Documentation

Mathlib.Algebra.Homology.Augment

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

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
    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

        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

          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
            Instances For

              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
                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

                    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

                      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
                        Instances For