Documentation

Mathlib.Algebra.Homology.Monoidal

The monoidal category structure on homological complexes #

Let c : ComplexShape I with I an additive monoid. If c is equipped with the data and axioms c.TensorSigns, then the category HomologicalComplex C c can be equipped with a monoidal category structure if C is a monoidal category such that C has certain coproducts and both left/right tensoring commute with these.

In particular, we obtain a monoidal category structure on ChainComplex C ℕ when C is an additive monoidal category.

@[reducible, inline]

If K₁ and K₂ are two homological complexes, this is the property that for all j, the coproduct of K₁ i₁ ⊗ K₂ i₂ for i₁ + i₂ = j exists.

Equations
Instances For
    @[reducible, inline]

    The tensor product of two homological complexes.

    Equations
    Instances For
      @[reducible, inline]

      The inclusion K₁.X i₁ ⊗ K₂.X i₂ ⟶ (tensorObj K₁ K₂).X j of a summand in the tensor product of the homological complexes.

      Equations
      Instances For
        @[reducible, inline]

        The tensor product of two morphisms of homological complexes.

        Equations
        Instances For
          @[reducible, inline]

          Given three homological complexes K₁, K₂, and K₃, this asserts that for all j, the functor - ⊗ K₃.X i₃ commutes with the coproduct of the K₁.X i₁ ⊗ K₂.X i₂ such that i₁ + i₂ = j.

          Equations
          Instances For
            @[reducible, inline]

            Given three homological complexes K₁, K₂, and K₃, this asserts that for all j, the functor K₁.X i₁ commutes with the coproduct of the K₂.X i₂ ⊗ K₃.X i₃ such that i₂ + i₃ = j.

            Equations
            Instances For
              @[reducible, inline]

              The associator isomorphism for the tensor product of homological complexes.

              Equations
              Instances For
                @[reducible, inline]

                The unit of the tensor product of homological complexes.

                Equations
                Instances For

                  As a graded object, the single complex (single C c 0).obj (𝟙_ C) identifies to the unit (GradedObject.single₀ I).obj (𝟙_ C) of the tensor product of graded objects.

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

                    The structure which allows to construct the monoidal category structure on HomologicalComplex C c from the monoidal category structure on graded objects.

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