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 : ι)
:
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}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasZeroObject V]
{ι : Type u_1}
[DecidableEq ι]
(c : ComplexShape ι)
(j : ι)
(A : V)
:
((HomologicalComplex.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 (((HomologicalComplex.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)
:
((HomologicalComplex.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.
Equations
- HomologicalComplex.singleObjXIsoOfEq c j A i hi = CategoryTheory.eqToIso ⋯
Instances For
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)
:
((HomologicalComplex.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
- HomologicalComplex.singleObjXSelf c j A = HomologicalComplex.singleObjXIsoOfEq c j A j ⋯
Instances For
@[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 : ι)
:
((HomologicalComplex.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)
:
((HomologicalComplex.single V c j).map f).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom
(CategoryTheory.CategoryStruct.comp f (HomologicalComplex.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 : ((HomologicalComplex.single V c j).obj B).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single V c j).map f).f j) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom
(CategoryTheory.CategoryStruct.comp f
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.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 : ι)
:
(HomologicalComplex.single V c j).comp (HomologicalComplex.eval V c j) ≅ CategoryTheory.Functor.id V
The natural isomorphism single V c j ⋙ eval V c j ≅ 𝟭 V.
Equations
Instances For
@[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)
:
(HomologicalComplex.singleCompEvalIsoSelf V c j).inv.app X = (HomologicalComplex.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)
:
(HomologicalComplex.singleCompEvalIsoSelf V c j).hom.app X = (HomologicalComplex.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 ((HomologicalComplex.single V c j).comp (HomologicalComplex.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 : (HomologicalComplex.single V c j).obj A ⟶ K}
(hfg : f.f j = g.f j)
:
f = g
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 ⟶ (HomologicalComplex.single V c j).obj A}
(hfg : f.f j = g.f j)
:
f = g
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 : ι)
:
(HomologicalComplex.single V c j).Faithful
Equations
- ⋯ = ⋯
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 : ι)
:
(HomologicalComplex.single V c j).Full
Equations
- ⋯ = ⋯
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 ⟶ (HomologicalComplex.single V c j).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}
[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)
:
(HomologicalComplex.mkHomToSingle φ hφ).f j = CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.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)
:
(HomologicalComplex.single V c j).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}
[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)
:
(HomologicalComplex.mkHomFromSingle φ hφ).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.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 : ι)
:
(HomologicalComplex.single V c j).PreservesZeroMorphisms
Equations
- ⋯ = ⋯
@[reducible, inline]
noncomputable abbrev
ChainComplex.single₀
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasZeroObject V]
:
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}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasZeroObject V]
(A : V)
:
((ChainComplex.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)
:
((ChainComplex.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 ⟶ (ChainComplex.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 ⟶ (ChainComplex.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)
:
((ChainComplex.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.
Equations
- C.fromSingle₀Equiv X = { toFun := fun (f : (ChainComplex.single₀ V).obj X ⟶ C) => f.f 0, invFun := fun (f : X ⟶ C.X 0) => HomologicalComplex.mkHomFromSingle f ⋯, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[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 : (ChainComplex.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 : ℕ)
:
@[reducible, inline]
noncomputable abbrev
CochainComplex.single₀
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasZeroObject V]
:
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}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasZeroObject V]
(A : V)
:
((CochainComplex.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)
:
((CochainComplex.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)
:
((CochainComplex.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
(φ : (CochainComplex.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 ⟶ (CochainComplex.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.
Equations
- C.toSingle₀Equiv X = { toFun := fun (f : C ⟶ (CochainComplex.single₀ V).obj X) => f.f 0, invFun := fun (f : C.X 0 ⟶ X) => HomologicalComplex.mkHomToSingle f ⋯, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[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 ⟶ (CochainComplex.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 : ℕ)
: