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) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : CategoryTheory.Functor V (HomologicalComplex V c)

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

@[simp]

theorem HomologicalComplex.single_obj_X_self {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) : ((single V c j).obj A).X j = A

theorem HomologicalComplex.isZero_single_obj_X {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) (hi : i ≠ j) : CategoryTheory.Limits.IsZero (((single V c j).obj A).X i)

noncomputable def HomologicalComplex.singleObjXIsoOfEq {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) (hi : i = j) : ((single V c j).obj A).X i ≅ A

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

noncomputable def HomologicalComplex.singleObjXSelf {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) : ((single V c j).obj A).X j ≅ A

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

@[simp]

theorem HomologicalComplex.single_obj_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (k l : ι) : ((single V c j).obj A).d k l = 0

theorem HomologicalComplex.single_map_f_self {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : V} (f : A ⟶ B) : ((single V c j).map f).f j = CategoryTheory.CategoryStruct.comp (singleObjXSelf c j A).hom (CategoryTheory.CategoryStruct.comp f (singleObjXSelf c j B).inv)

theorem HomologicalComplex.single_map_f_self_assoc {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : V} (f : A ⟶ B) {Z : V} (h : ((single V c j).obj B).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (((single V c j).map f).f j) h = CategoryTheory.CategoryStruct.comp (singleObjXSelf c j A).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (singleObjXSelf c j B).inv h))

noncomputable def HomologicalComplex.singleCompEvalIsoSelf (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) : (single V c j).comp (eval V c j) ≅ CategoryTheory.Functor.id V

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

@[simp]

theorem HomologicalComplex.singleCompEvalIsoSelf_inv_app (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (X : V) : (singleCompEvalIsoSelf V c j).inv.app X = (singleObjXSelf c j X).inv

@[simp]

theorem HomologicalComplex.singleCompEvalIsoSelf_hom_app (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (X : V) : (singleCompEvalIsoSelf V c j).hom.app X = (singleObjXSelf c j X).hom

theorem HomologicalComplex.isZero_single_comp_eval (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j i : ι) (hi : i ≠ j) : CategoryTheory.Limits.IsZero ((single V c j).comp (eval V c i))

theorem HomologicalComplex.from_single_hom_ext {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : (single V c j).obj A ⟶ K} (hfg : f.f j = g.f j) : f = g

theorem HomologicalComplex.from_single_hom_ext_iff {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : (single V c j).obj A ⟶ K} : f = g ↔ f.f j = g.f j

theorem HomologicalComplex.to_single_hom_ext {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (single V c j).obj A} (hfg : f.f j = g.f j) : f = g

theorem HomologicalComplex.to_single_hom_ext_iff {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (single V c j).obj A} : f = g ↔ f.f j = g.f j

instance HomologicalComplex.instFaithfulSingle {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} (j : ι) : (single V c j).Faithful

instance HomologicalComplex.instFullSingle {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} (j : ι) : (single V c j).Full

noncomputable def HomologicalComplex.mkHomToSingle {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A) (hφ : ∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) : K ⟶ (single V c j).obj A

Constructor for morphisms to a single homological complex.

@[simp]

theorem HomologicalComplex.mkHomToSingle_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A) (hφ : ∀ (i : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0) : (mkHomToSingle φ hφ).f j = CategoryTheory.CategoryStruct.comp φ (singleObjXSelf c j A).inv

noncomputable def HomologicalComplex.mkHomFromSingle {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j) (hφ : ∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) : (single V c j).obj A ⟶ K

Constructor for morphisms from a single homological complex.

@[simp]

theorem HomologicalComplex.mkHomFromSingle_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j) (hφ : ∀ (k : ι), c.Rel j k → CategoryTheory.CategoryStruct.comp φ (K.d j k) = 0) : (mkHomFromSingle φ hφ).f j = CategoryTheory.CategoryStruct.comp (singleObjXSelf c j A).hom φ

instance HomologicalComplex.instPreservesZeroMorphismsSingle {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] {c : ComplexShape ι} (j : ι) : (single V c j).PreservesZeroMorphisms

@[reducible, inline]

noncomputable abbrev ChainComplex.single₀ (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Functor V (ChainComplex V ℕ)

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

@[simp]

theorem ChainComplex.single₀_obj_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (A : V) : ((single₀ V).obj A).X 0 = A

@[simp]

theorem ChainComplex.single₀_map_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {A B : V} (f : A ⟶ B) : ((single₀ V).map f).f 0 = f

@[simp]

theorem ChainComplex.single₀ObjXSelf {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) : HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X = CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.down ℕ) 0).obj X).X 0)

noncomputable def ChainComplex.toSingle₀Equiv {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) : (C ⟶ (single₀ V).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.

@[simp]

theorem ChainComplex.toSingle₀Equiv_apply_coe {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (φ : C ⟶ (single₀ V).obj X) : ↑((C.toSingle₀Equiv X) φ) = φ.f 0

@[simp]

theorem ChainComplex.toSingle₀Equiv_symm_apply_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : ChainComplex V ℕ} {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

noncomputable def ChainComplex.fromSingle₀Equiv {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) : ((single₀ 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.

@[simp]

theorem ChainComplex.fromSingle₀Equiv_apply {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (f : (single₀ V).obj X ⟶ C) : (C.fromSingle₀Equiv X) f = f.f 0

@[simp]

theorem ChainComplex.fromSingle₀Equiv_symm_apply_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : ChainComplex V ℕ} {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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : ChainComplex V ℕ} {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) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Functor V (CochainComplex V ℕ)

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

@[simp]

theorem CochainComplex.single₀_obj_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (A : V) : ((single₀ V).obj A).X 0 = A

@[simp]

theorem CochainComplex.single₀_map_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {A B : V} (f : A ⟶ B) : ((single₀ V).map f).f 0 = f

@[simp]

theorem CochainComplex.single₀ObjXSelf {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (X : V) : HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X = CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.up ℕ) 0).obj X).X 0)

noncomputable def CochainComplex.fromSingle₀Equiv {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V) : ((single₀ 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.

@[simp]

theorem CochainComplex.fromSingle₀Equiv_apply_coe {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V) (φ : (single₀ V).obj X ⟶ C) : ↑((C.fromSingle₀Equiv X) φ) = φ.f 0

@[simp]

theorem CochainComplex.fromSingle₀Equiv_symm_apply_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : CochainComplex V ℕ} {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

noncomputable def CochainComplex.toSingle₀Equiv {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V) : (C ⟶ (single₀ V).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.

@[simp]

theorem CochainComplex.toSingle₀Equiv_apply {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V) (f : C ⟶ (single₀ V).obj X) : (C.toSingle₀Equiv X) f = f.f 0

@[simp]

theorem CochainComplex.toSingle₀Equiv_symm_apply_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : CochainComplex V ℕ} {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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {C : CochainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X) (n : ℕ) : ((C.toSingle₀Equiv X).symm f).f (n + 1) = 0