mathlib3 documentation

algebra.homology.single

Chain complexes supported in a single degree #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

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
Instances for homological_complex.single

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
Instances for chain_complex.single₀
@[simp]
theorem chain_complex.to_single₀_equiv_symm_apply_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_zero_object V] (C : chain_complex V ) (X : V) (f : {f // C.d 1 0 f = 0}) (i : ) :
(((C.to_single₀_equiv X).symm) f).f i = chain_complex.to_single₀_equiv._match_1 C X f i

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

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

Equations
@[simp]
theorem chain_complex.from_single₀_equiv_symm_apply_f {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_zero_object V] (C : chain_complex V ) (X : V) (f : X C.X 0) (i : ) :
(((C.from_single₀_equiv X).symm) f).f i = chain_complex.from_single₀_equiv._match_1 C X f i

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
Instances for cochain_complex.single₀

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