Documentation

Mathlib.Algebra.Homology.Single

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

Similarly single₀ V : V ⥤ ChainComplex V ℕ is the special case for -indexed chain complexes, with the object supported in degree 0, but with better definitional properties.

In 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.)

@[simp]
theorem HomologicalComplex.single_map_f (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) :
∀ {X Y : V} (f : X Y) (i : ι), HomologicalComplex.Hom.f ((HomologicalComplex.single V c j).map f) i = if h : i = j then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : HomologicalComplex.X ((fun A => HomologicalComplex.mk (fun i => if i = j then A else 0) fun i j => 0) X) i = X)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom (_ : Y = HomologicalComplex.X ((fun A => HomologicalComplex.mk (fun i => if i = j then A else 0) fun i j => 0) Y) i))) else 0

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

See also ChainComplex.single₀ : V ⥤ ChainComplex V ℕ, which has better definitional properties, if you are working with -indexed complexes.

Instances For

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

    Instances For

      ChainComplex.single₀ V is the embedding of V into ChainComplex V ℕ as chain complexes supported in degree 0.

      This is naturally isomorphic to single V _ 0, but has better definitional properties.

      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.

        Instances For

          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.

          Instances For

            CochainComplex.single₀ V is the embedding of V into CochainComplex V ℕ as cochain complexes supported in degree 0.

            This is naturally isomorphic to single V _ 0, but has better definitional properties.

            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.

              Instances For