Documentation

Mathlib.Algebra.Homology.Single

Homological complexes supported in a single degree #

We define single V j c : V ⥤ HomologicalComplex V c, which constructs complexes in V of shape c, supported in degree j.

In ChainComplex.toSingle₀Equiv we characterize chain maps to an -indexed complex concentrated in degree 0; they are equivalent to { f : C.X 0 ⟶ X // C.d 1 0 ≫ f = 0 }. (This is useful translating between a projective resolution and an augmented exact complex of projectives.)

The functor V ⥤ HomologicalComplex V c creating a chain complex supported in a single degree.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable def HomologicalComplex.singleObjXIsoOfEq {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) (hi : i = j) :
    ((HomologicalComplex.single V c j).obj A).X i A

    The object in degree i of (single V c h).obj A is just A when i = j.

    Equations
    Instances For

      The object in degree j of (single V c h).obj A is just A.

      Equations
      Instances For
        noncomputable def HomologicalComplex.mkHomToSingle {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j A) (hφ : ∀ (i : ι), c.Rel i jCategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) :

        Constructor for morphisms to a single homological complex.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def HomologicalComplex.mkHomFromSingle {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A K.X j) (hφ : ∀ (k : ι), c.Rel j kCategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) :

          Constructor for morphisms from a single homological complex.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible, inline]

            The functor V ⥤ ChainComplex V ℕ creating a chain complex supported in degree zero.

            Equations
            Instances For

              Morphisms from an -indexed chain complex C to a single object chain complex with X concentrated in degree 0 are the same as morphisms f : C.X 0 ⟶ X such that C.d 1 0 ≫ f = 0.

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

                Morphisms from a single object chain complex with X concentrated in degree 0 to an -indexed chain complex C are the same as morphisms f : X → C.X 0.

                Equations
                Instances For
                  @[simp]
                  @[reducible, inline]

                  The functor V ⥤ CochainComplex V ℕ creating a cochain complex supported in degree zero.

                  Equations
                  Instances For

                    Morphisms from a single object cochain complex with X concentrated in degree 0 to an -indexed cochain complex C are the same as morphisms f : X ⟶ C.X 0 such that f ≫ C.d 0 1 = 0.

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

                      Morphisms to a single object cochain complex with X concentrated in degree 0 to an -indexed cochain complex C are the same as morphisms f : C.X 0 ⟶ X.

                      Equations
                      Instances For
                        @[simp]