mathlib documentation

algebra.homology.single

Chain complexes supported in a single degree #

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

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

In to_single₀_equiv we characterize chain maps to a -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 homological_complex.single_map_f (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_zero_object V] {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) (A B : V) (f : A B) (i : ι) :
((homological_complex.single V c j).map f).f i = dite (i = j) (λ (h : i = j), category_theory.eq_to_hom _ f category_theory.eq_to_hom _) (λ (h : ¬i = j), 0)

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

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

Equations
@[simp]
@[simp]

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

Equations

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

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

Equations
  • chain_complex.single₀ V = {obj := λ (X : V), {X := λ (n : ), chain_complex.single₀._match_1 V X n, d := λ (i j : ), 0, shape' := _, d_comp_d' := _}, map := λ (X Y : V) (f : X Y), {f := λ (n : ), chain_complex.single₀._match_2 V X Y f n, comm' := _}, map_id' := _, map_comp' := _}
  • chain_complex.single₀._match_1 V X (n + 1) = 0
  • chain_complex.single₀._match_1 V X 0 = X
  • chain_complex.single₀._match_2 V X Y f (n + 1) = 0
  • chain_complex.single₀._match_2 V X Y f 0 = f

Morphisms from a -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

single₀ is the same as single V _ 0.

Equations

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

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

Equations
  • cochain_complex.single₀ V = {obj := λ (X : V), {X := λ (n : ), cochain_complex.single₀._match_1 V X n, d := λ (i j : ), 0, shape' := _, d_comp_d' := _}, map := λ (X Y : V) (f : X Y), {f := λ (n : ), cochain_complex.single₀._match_2 V X Y f n, comm' := _}, map_id' := _, map_comp' := _}
  • cochain_complex.single₀._match_1 V X (n + 1) = 0
  • cochain_complex.single₀._match_1 V X 0 = X
  • cochain_complex.single₀._match_2 V X Y f (n + 1) = 0
  • cochain_complex.single₀._match_2 V X Y f 0 = f

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

Equations

single₀ is the same as single V _ 0.

Equations