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]
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)
noncomputable
def
homological_complex.single
(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 : ι) :
V ⥤ homological_complex V c
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
- homological_complex.single V c j = {obj := λ (A : V), {X := λ (i : ι), ite (i = j) A 0, d := λ (i j_1 : ι), 0, shape' := _, d_comp_d' := _}, map := λ (A B : V) (f : A ⟶ B), {f := λ (i : ι), dite (i = j) (λ (h : i = j), category_theory.eq_to_hom _ ≫ f ≫ category_theory.eq_to_hom _) (λ (h : ¬i = j), 0), comm' := _}, map_id' := _, map_comp' := _}
Instances for homological_complex.single
@[simp]
theorem
homological_complex.single_obj_d
(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 : V)
(i j_1 : ι) :
((homological_complex.single V c j).obj A).d i j_1 = 0
@[simp]
theorem
homological_complex.single_obj_X
(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 : V)
(i : ι) :
@[simp]
theorem
homological_complex.single_obj_X_self_hom
(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 : V) :
@[simp]
theorem
homological_complex.single_obj_X_self_inv
(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 : V) :
noncomputable
def
homological_complex.single_obj_X_self
(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 : V) :
((homological_complex.single V c 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)
[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) :
((homological_complex.single V c j).map f).f j = (homological_complex.single_obj_X_self V c j A).hom ≫ f ≫ (homological_complex.single_obj_X_self V c j B).inv
@[protected, instance]
def
homological_complex.single.category_theory.faithful
(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 : ι) :
@[protected, instance]
noncomputable
def
homological_complex.single.category_theory.full
(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 : ι) :
Equations
- homological_complex.single.category_theory.full V c j = {preimage := λ (X Y : V) (f : (homological_complex.single V c j).obj X ⟶ (homological_complex.single V c j).obj Y), category_theory.eq_to_hom _ ≫ f.f j ≫ category_theory.eq_to_hom _, witness' := _}
noncomputable
def
chain_complex.single₀
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V] :
V ⥤ chain_complex V ℕ
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.single₀_obj_X_0
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V) :
((chain_complex.single₀ V).obj X).X 0 = X
@[simp]
theorem
chain_complex.single₀_obj_X_succ
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(n : ℕ) :
((chain_complex.single₀ V).obj X).X (n + 1) = 0
@[simp]
theorem
chain_complex.single₀_obj_X_d
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(i j : ℕ) :
((chain_complex.single₀ V).obj X).d i j = 0
@[simp]
theorem
chain_complex.single₀_obj_X_d_to
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(j : ℕ) :
homological_complex.d_to ((chain_complex.single₀ V).obj X) j = 0
@[simp]
theorem
chain_complex.single₀_obj_X_d_from
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(i : ℕ) :
homological_complex.d_from ((chain_complex.single₀ V).obj X) i = 0
@[simp]
theorem
chain_complex.single₀_map_f_0
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
{X Y : V}
(f : X ⟶ Y) :
((chain_complex.single₀ V).map f).f 0 = f
@[simp]
theorem
chain_complex.single₀_map_f_succ
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
{X Y : V}
(f : X ⟶ Y)
(n : ℕ) :
((chain_complex.single₀ V).map f).f (n + 1) = 0
noncomputable
def
chain_complex.homology_functor_0_single₀
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V] :
chain_complex.single₀ V ⋙ homology_functor V (complex_shape.down ℕ) 0 ≅ 𝟭 V
Sending objects to chain complexes supported at 0 then taking 0-th homology
is the same as doing nothing.
Equations
- chain_complex.homology_functor_0_single₀ V = category_theory.nat_iso.of_components (λ (X : V), homology.congr _ _ _ _ ≪≫ homology_zero_zero) _
noncomputable
def
chain_complex.homology_functor_succ_single₀
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(n : ℕ) :
chain_complex.single₀ V ⋙ homology_functor V (complex_shape.down ℕ) (n + 1) ≅ 0
Sending objects to chain complexes supported at 0 then taking (n+1)-st homology
is the same as the zero functor.
Equations
- chain_complex.homology_functor_succ_single₀ V n = category_theory.nat_iso.of_components (λ (X : V), homology.congr _ _ _ _ ≪≫ homology_zero_zero ≪≫ _.iso_zero.symm) _
@[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
noncomputable
def
chain_complex.to_single₀_equiv
{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) :
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
- C.to_single₀_equiv X = {to_fun := λ (f : C ⟶ (chain_complex.single₀ V).obj 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
@[simp]
theorem
chain_complex.to_single₀_equiv_apply_coe
{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 : C ⟶ (chain_complex.single₀ V).obj X) :
↑(⇑(C.to_single₀_equiv X) f) = f.f 0
@[ext]
theorem
chain_complex.to_single₀_ext
{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 g : C ⟶ (chain_complex.single₀ V).obj X)
(h : f.f 0 = g.f 0) :
f = g
noncomputable
def
chain_complex.from_single₀_equiv
{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) :
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
- C.from_single₀_equiv X = {to_fun := λ (f : (chain_complex.single₀ V).obj X ⟶ C), f.f 0, inv_fun := λ (f : X ⟶ C.X 0), {f := λ (i : ℕ), chain_complex.from_single₀_equiv._match_1 C X f i, comm' := _}, left_inv := _, right_inv := _}
- chain_complex.from_single₀_equiv._match_1 C X f (n + 1) = 0
- chain_complex.from_single₀_equiv._match_1 C X f 0 = f
@[simp]
theorem
chain_complex.from_single₀_equiv_apply
{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 : (chain_complex.single₀ V).obj X ⟶ C) :
⇑(C.from_single₀_equiv X) f = f.f 0
@[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
noncomputable
def
chain_complex.single₀_iso_single
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V] :
single₀ is the same as single V _ 0.
Equations
- chain_complex.single₀_iso_single V = category_theory.nat_iso.of_components (λ (X : V), {hom := {f := λ (i : ℕ), i.cases_on (_.mpr (_.mp (𝟙 X))) (λ (i : ℕ), _.mpr (𝟙 0)), comm' := _}, inv := {f := λ (i : ℕ), i.cases_on (_.mpr (_.mp (𝟙 X))) (λ (i : ℕ), _.mpr (𝟙 0)), comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[protected, instance]
@[protected, instance]
noncomputable
def
chain_complex.single₀.category_theory.full
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V] :
noncomputable
def
cochain_complex.single₀
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V] :
V ⥤ cochain_complex V ℕ
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₀
@[simp]
theorem
cochain_complex.single₀_obj_X_0
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V) :
((cochain_complex.single₀ V).obj X).X 0 = X
@[simp]
theorem
cochain_complex.single₀_obj_X_succ
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(n : ℕ) :
((cochain_complex.single₀ V).obj X).X (n + 1) = 0
@[simp]
theorem
cochain_complex.single₀_obj_X_d
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(i j : ℕ) :
((cochain_complex.single₀ V).obj X).d i j = 0
@[simp]
theorem
cochain_complex.single₀_obj_X_d_from
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(j : ℕ) :
homological_complex.d_from ((cochain_complex.single₀ V).obj X) j = 0
@[simp]
theorem
cochain_complex.single₀_obj_X_d_to
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(X : V)
(i : ℕ) :
homological_complex.d_to ((cochain_complex.single₀ V).obj X) i = 0
@[simp]
theorem
cochain_complex.single₀_map_f_0
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
{X Y : V}
(f : X ⟶ Y) :
((cochain_complex.single₀ V).map f).f 0 = f
@[simp]
theorem
cochain_complex.single₀_map_f_succ
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
{X Y : V}
(f : X ⟶ Y)
(n : ℕ) :
((cochain_complex.single₀ V).map f).f (n + 1) = 0
noncomputable
def
cochain_complex.homology_functor_0_single₀
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V] :
cochain_complex.single₀ V ⋙ homology_functor V (complex_shape.up ℕ) 0 ≅ 𝟭 V
Sending objects to cochain complexes supported at 0 then taking 0-th homology
is the same as doing nothing.
Equations
- cochain_complex.homology_functor_0_single₀ V = category_theory.nat_iso.of_components (λ (X : V), homology.congr _ _ _ _ ≪≫ homology_zero_zero) _
noncomputable
def
cochain_complex.homology_functor_succ_single₀
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(n : ℕ) :
cochain_complex.single₀ V ⋙ homology_functor V (complex_shape.up ℕ) (n + 1) ≅ 0
Sending objects to cochain complexes supported at 0 then taking (n+1)-st homology
is the same as the zero functor.
Equations
- cochain_complex.homology_functor_succ_single₀ V n = category_theory.nat_iso.of_components (λ (X : V), homology.congr _ _ _ _ ≪≫ homology_zero_zero ≪≫ _.iso_zero.symm) _
noncomputable
def
cochain_complex.from_single₀_equiv
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
(C : cochain_complex V ℕ)
(X : V) :
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
- C.from_single₀_equiv X = {to_fun := λ (f : (cochain_complex.single₀ V).obj X ⟶ 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
noncomputable
def
cochain_complex.single₀_iso_single
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V] :
single₀ is the same as single V _ 0.
Equations
- cochain_complex.single₀_iso_single V = category_theory.nat_iso.of_components (λ (X : V), {hom := {f := λ (i : ℕ), i.cases_on (_.mpr (_.mp (𝟙 X))) (λ (i : ℕ), _.mpr (𝟙 0)), comm' := _}, inv := {f := λ (i : ℕ), i.cases_on (_.mpr (_.mp (𝟙 X))) (λ (i : ℕ), _.mpr (𝟙 0)), comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[protected, instance]
@[protected, instance]
noncomputable
def
cochain_complex.single₀.category_theory.full
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V] :