# Homological 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.

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

noncomputable def HomologicalComplex.single (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.single_obj_X_self {V : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : V) :
(.obj A).X j = A
theorem HomologicalComplex.isZero_single_obj_X {V : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : V) (i : ι) (hi : i j) :
noncomputable def HomologicalComplex.singleObjXIsoOfEq {V : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : V) (i : ι) (hi : i = j) :
(.obj A).X i A

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

Equations
Instances For
noncomputable def HomologicalComplex.singleObjXSelf {V : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : V) :
(.obj A).X j A

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

Equations
Instances For
@[simp]
theorem HomologicalComplex.single_obj_d {V : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : V) (k : ι) (l : ι) :
(.obj A).d k l = 0
theorem HomologicalComplex.single_map_f_self_assoc {V : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : V} {B : V} (f : A B) {Z : V} (h : (.obj B).X j Z) :
theorem HomologicalComplex.single_map_f_self {V : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : V} {B : V} (f : A B) :
(.map f).f j =
@[simp]
theorem HomologicalComplex.singleCompEvalIsoSelf_hom_app (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) (X : V) :
.hom.app X = .hom
@[simp]
theorem HomologicalComplex.singleCompEvalIsoSelf_inv_app (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) (X : V) :
.inv.app X = .inv
noncomputable def HomologicalComplex.singleCompEvalIsoSelf (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) :
.comp

The natural isomorphism single V c j ⋙ eval V c j ≅ 𝟭 V.

Equations
Instances For
theorem HomologicalComplex.isZero_single_comp_eval (V : Type u) {ι : Type u_1} [] (c : ) (j : ι) (i : ι) (hi : i j) :
theorem HomologicalComplex.from_single_hom_ext_iff {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} {f : .obj A K} {g : .obj A K} :
f = g f.f j = g.f j
theorem HomologicalComplex.from_single_hom_ext {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} {f : .obj A K} {g : .obj A K} (hfg : f.f j = g.f j) :
f = g
theorem HomologicalComplex.to_single_hom_ext_iff {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} {f : K .obj A} {g : K .obj A} :
f = g f.f j = g.f j
theorem HomologicalComplex.to_single_hom_ext {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} {f : K .obj A} {g : K .obj A} (hfg : f.f j = g.f j) :
f = g
instance HomologicalComplex.instFaithfulSingle {V : Type u} {ι : Type u_1} [] {c : } (j : ι) :
.Faithful
Equations
• =
instance HomologicalComplex.instFullSingle {V : Type u} {ι : Type u_1} [] {c : } (j : ι) :
.Full
Equations
• =
noncomputable def HomologicalComplex.mkHomToSingle {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} (φ : K.X j A) (hφ : ∀ (i : ι), c.Rel i jCategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) :
K .obj A

Constructor for morphisms to a single homological complex.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.mkHomToSingle_f {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} (φ : K.X j A) (hφ : ∀ (i : ι), c.Rel i jCategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) :
.f j =
noncomputable def HomologicalComplex.mkHomFromSingle {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} (φ : A K.X j) (hφ : ∀ (k : ι), c.Rel j kCategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) :
.obj A K

Constructor for morphisms from a single homological complex.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.mkHomFromSingle_f {V : Type u} {ι : Type u_1} [] {c : } {K : } {j : ι} {A : V} (φ : A K.X j) (hφ : ∀ (k : ι), c.Rel j kCategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) :
.f j =
instance HomologicalComplex.instPreservesZeroMorphismsSingle {V : Type u} {ι : Type u_1} [] {c : } (j : ι) :
.PreservesZeroMorphisms
Equations
• =
@[reducible, inline]
noncomputable abbrev ChainComplex.single₀ (V : Type u) :

The functor V ⥤ ChainComplex V ℕ creating a chain complex supported in degree zero.

Equations
Instances For
@[simp]
theorem ChainComplex.single₀_obj_zero {V : Type u} (A : V) :
(.obj A).X 0 = A
@[simp]
theorem ChainComplex.single₀_map_f_zero {V : Type u} {A : V} {B : V} (f : A B) :
(.map f).f 0 = f
@[simp]
theorem ChainComplex.single₀ObjXSelf {V : Type u} (X : V) :
= CategoryTheory.Iso.refl ((.obj X).X 0)
@[simp]
theorem ChainComplex.toSingle₀Equiv_apply_coe {V : Type u} (C : ) (X : V) (φ : C .obj X) :
((C.toSingle₀Equiv X) φ) = φ.f 0
noncomputable def ChainComplex.toSingle₀Equiv {V : Type u} (C : ) (X : V) :
(C .obj X) { f : C.X 0 X // CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0 }

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ChainComplex.toSingle₀Equiv_symm_apply_f_zero {V : Type u} {C : } {X : V} (f : C.X 0 X) (hf : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :
((C.toSingle₀Equiv X).symm f, hf).f 0 = f
@[simp]
theorem ChainComplex.fromSingle₀Equiv_apply {V : Type u} (C : ) (X : V) (f : .obj X C) :
(C.fromSingle₀Equiv X) f = f.f 0
noncomputable def ChainComplex.fromSingle₀Equiv {V : Type u} (C : ) (X : V) :
(.obj X C) (X C.X 0)

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

Equations
• C.fromSingle₀Equiv X = { toFun := fun (f : .obj X C) => f.f 0, invFun := fun (f : X C.X 0) => , left_inv := , right_inv := }
Instances For
@[simp]
theorem ChainComplex.fromSingle₀Equiv_symm_apply_f_zero {V : Type u} {C : } {X : V} (f : X C.X 0) :
((C.fromSingle₀Equiv X).symm f).f 0 = f
@[simp]
theorem ChainComplex.fromSingle₀Equiv_symm_apply_f_succ {V : Type u} {C : } {X : V} (f : X C.X 0) (n : ) :
((C.fromSingle₀Equiv X).symm f).f (n + 1) = 0
@[reducible, inline]
noncomputable abbrev CochainComplex.single₀ (V : Type u) :

The functor V ⥤ CochainComplex V ℕ creating a cochain complex supported in degree zero.

Equations
Instances For
@[simp]
theorem CochainComplex.single₀_obj_zero {V : Type u} (A : V) :
(.obj A).X 0 = A
@[simp]
theorem CochainComplex.single₀_map_f_zero {V : Type u} {A : V} {B : V} (f : A B) :
(.map f).f 0 = f
@[simp]
theorem CochainComplex.single₀ObjXSelf {V : Type u} (X : V) :
= CategoryTheory.Iso.refl ((.obj X).X 0)
@[simp]
theorem CochainComplex.fromSingle₀Equiv_apply_coe {V : Type u} (C : ) (X : V) (φ : .obj X C) :
((C.fromSingle₀Equiv X) φ) = φ.f 0
noncomputable def CochainComplex.fromSingle₀Equiv {V : Type u} (C : ) (X : V) :
(.obj X C) { f : X C.X 0 // CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0 }

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CochainComplex.fromSingle₀Equiv_symm_apply_f_zero {V : Type u} {C : } {X : V} (f : X C.X 0) (hf : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :
((C.fromSingle₀Equiv X).symm f, hf).f 0 = f
@[simp]
theorem CochainComplex.toSingle₀Equiv_apply {V : Type u} (C : ) (X : V) (f : C .obj X) :
(C.toSingle₀Equiv X) f = f.f 0
noncomputable def CochainComplex.toSingle₀Equiv {V : Type u} (C : ) (X : V) :
(C .obj X) (C.X 0 X)

Morphisms to a single object cochain complex with X concentrated in degree 0 to an ℕ-indexed cochain complex C are the same as morphisms f : C.X 0 ⟶ X.

Equations
• C.toSingle₀Equiv X = { toFun := fun (f : C .obj X) => f.f 0, invFun := fun (f : C.X 0 X) => , left_inv := , right_inv := }
Instances For
@[simp]
theorem CochainComplex.toSingle₀Equiv_symm_apply_f_zero {V : Type u} {C : } {X : V} (f : C.X 0 X) :
((C.toSingle₀Equiv X).symm f).f 0 = f
@[simp]
theorem CochainComplex.toSingle₀Equiv_symm_apply_f_succ {V : Type u} {C : } {X : V} (f : C.X 0 X) (n : ) :
((C.toSingle₀Equiv X).symm f).f (n + 1) = 0