# mathlibdocumentation

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) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) (A B : V) (f : A B) (i : ι) :
j).map f).f i = dite (i = j) (λ (h : i = j), (λ (h : ¬i = j), 0)
def homological_complex.single (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) :
V

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]
theorem homological_complex.single_obj_d (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) (A : V) (i j_1 : ι) :
j).obj A).d i j_1 = 0
@[simp]
theorem homological_complex.single_obj_X (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) (A : V) (i : ι) :
j).obj A).X i = ite (i = j) A 0
@[simp]
theorem homological_complex.single_obj_X_self_hom (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) (A : V) :
@[simp]
theorem homological_complex.single_obj_X_self_inv (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) (A : V) :
def homological_complex.single_obj_X_self (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) (A : V) :
j).obj A).X j A

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

Equations
@[simp]
theorem homological_complex.single_map_f_self (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) {A B : V} (f : A B) :
j).map f).f j = .hom f .inv
@[protected, instance]
def homological_complex.single.category_theory.faithful (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) :
@[protected, instance]
def homological_complex.single.category_theory.full (V : Type u) {ι : Type u_1} [decidable_eq ι] (c : complex_shape ι) (j : ι) :
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
• = {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
@[simp]
theorem chain_complex.single₀_obj_X_0 (V : Type u) (X : V) :
.obj X).X 0 = X
@[simp]
theorem chain_complex.single₀_obj_X_succ (V : Type u) (X : V) (n : ) :
.obj X).X (n + 1) = 0
@[simp]
theorem chain_complex.single₀_obj_X_d (V : Type u) (X : V) (i j : ) :
.obj X).d i j = 0
@[simp]
theorem chain_complex.single₀_obj_X_d_to (V : Type u) (X : V) (j : ) :
= 0
@[simp]
theorem chain_complex.single₀_obj_X_d_from (V : Type u) (X : V) (i : ) :
= 0
@[simp]
theorem chain_complex.single₀_map_f_0 (V : Type u) {X Y : V} (f : X Y) :
.map f).f 0 = f
@[simp]
theorem chain_complex.single₀_map_f_succ (V : Type u) {X Y : V} (f : X Y) (n : ) :
.map f).f (n + 1) = 0

Sending objects to chain complexes supported at 0 then taking 0-th homology is the same as doing nothing.

Equations

Sending objects to chain complexes supported at 0 then taking (n+1)-st homology is the same as the zero functor.

Equations
def chain_complex.to_single₀_equiv {V : Type u} (C : ) (X : V) :
(C X) {f // C.d 1 0 f = 0}

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
• = {to_fun := λ (f : C X), f.f 0, _⟩, inv_fun := λ (f : {f // C.d 1 0 f = 0}), {f := λ (i : ), chain_complex.to_single₀_equiv._match_1 C X f i, comm' := _}, left_inv := _, right_inv := _}
• chain_complex.to_single₀_equiv._match_1 C X f (n + 1) = 0
• chain_complex.to_single₀_equiv._match_1 C X f 0 = f.val

single₀ is the same as single V _ 0.

Equations
@[protected, instance]
@[protected, instance]
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
• = {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
@[simp]
theorem cochain_complex.single₀_obj_X_0 (V : Type u) (X : V) :
X).X 0 = X
@[simp]
theorem cochain_complex.single₀_obj_X_succ (V : Type u) (X : V) (n : ) :
X).X (n + 1) = 0
@[simp]
theorem cochain_complex.single₀_obj_X_d (V : Type u) (X : V) (i j : ) :
X).d i j = 0
@[simp]
theorem cochain_complex.single₀_obj_X_d_from (V : Type u) (X : V) (j : ) :
@[simp]
theorem cochain_complex.single₀_obj_X_d_to (V : Type u) (X : V) (i : ) :
= 0
@[simp]
theorem cochain_complex.single₀_map_f_0 (V : Type u) {X Y : V} (f : X Y) :
f).f 0 = f
@[simp]
theorem cochain_complex.single₀_map_f_succ (V : Type u) {X Y : V} (f : X Y) (n : ) :
f).f (n + 1) = 0

Sending objects to cochain complexes supported at 0 then taking 0-th homology is the same as doing nothing.

Equations

Sending objects to cochain complexes supported at 0 then taking (n+1)-st homology is the same as the zero functor.

Equations
def cochain_complex.from_single₀_equiv {V : Type u} (C : ) (X : V) :
X C) {f // f C.d 0 1 = 0}

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
• = {to_fun := λ (f : C), f.f 0, _⟩, inv_fun := λ (f : {f // f C.d 0 1 = 0}), {f := λ (i : ), cochain_complex.from_single₀_equiv._match_1 C X f i, comm' := _}, left_inv := _, right_inv := _}
• cochain_complex.from_single₀_equiv._match_1 C X f (n + 1) = 0
• cochain_complex.from_single₀_equiv._match_1 C X f 0 = f.val

single₀ is the same as single V _ 0.

Equations
@[protected, instance]
@[protected, instance]
Equations