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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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 (_ : ((HomologicalComplex.single V c j).toPrefunctor.obj A).X i = A)
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).toPrefunctor.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 (_ : j = 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).toPrefunctor.obj A).d k l = 0
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 : V}
{B : V}
(f : A ⟶ B)
{Z : V}
(h : ((HomologicalComplex.single V c j).toPrefunctor.obj B).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single V c j).toPrefunctor.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))
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 : V}
{B : V}
(f : A ⟶ B)
:
((HomologicalComplex.single V c j).toPrefunctor.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.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 : (HomologicalComplex.single V c j).toPrefunctor.obj A ⟶ K}
{g : (HomologicalComplex.single V c j).toPrefunctor.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 : K ⟶ (HomologicalComplex.single V c j).toPrefunctor.obj A}
{g : K ⟶ (HomologicalComplex.single V c j).toPrefunctor.obj A}
(hfg : f.f j = g.f j)
:
f = g
instance
HomologicalComplex.instFaithfulHomologicalComplexInstCategoryHomologicalComplexSingle
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasZeroObject V]
{ι : Type u_1}
[DecidableEq ι]
(c : ComplexShape ι)
(j : ι)
:
Equations
- (_ : CategoryTheory.Faithful (HomologicalComplex.single V c j)) = (_ : CategoryTheory.Faithful (HomologicalComplex.single V c j))
noncomputable instance
HomologicalComplex.instFullHomologicalComplexInstCategoryHomologicalComplexSingle
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasZeroObject V]
{ι : Type u_1}
[DecidableEq ι]
(c : ComplexShape ι)
(j : ι)
:
Equations
- One or more equations did not get rendered due to their size.
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).toPrefunctor.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).toPrefunctor.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 φ
@[inline, reducible]
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).toPrefunctor.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 : V}
{B : V}
(f : A ⟶ B)
:
((ChainComplex.single₀ V).toPrefunctor.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).toPrefunctor.obj X).X 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 ⟶ (ChainComplex.single₀ V).toPrefunctor.obj X)
:
↑((ChainComplex.toSingle₀Equiv C X) φ) = φ.f 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).toPrefunctor.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}
[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)
:
((ChainComplex.toSingle₀Equiv C X).symm { val := f, property := hf }).f 0 = f
@[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).toPrefunctor.obj X ⟶ C)
:
(ChainComplex.fromSingle₀Equiv C X) f = f.f 0
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).toPrefunctor.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
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
((ChainComplex.fromSingle₀Equiv C 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 : ℕ)
:
((ChainComplex.fromSingle₀Equiv C X).symm f).f (n + 1) = 0
@[inline, reducible]
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).toPrefunctor.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 : V}
{B : V}
(f : A ⟶ B)
:
((CochainComplex.single₀ V).toPrefunctor.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).toPrefunctor.obj X).X 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)
(φ : (CochainComplex.single₀ V).toPrefunctor.obj X ⟶ C)
:
↑((CochainComplex.fromSingle₀Equiv C X) φ) = φ.f 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).toPrefunctor.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}
[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)
:
((CochainComplex.fromSingle₀Equiv C X).symm { val := f, property := hf }).f 0 = f
@[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).toPrefunctor.obj X)
:
(CochainComplex.toSingle₀Equiv C X) f = f.f 0
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).toPrefunctor.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
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
((CochainComplex.toSingle₀Equiv C 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 : ℕ)
:
((CochainComplex.toSingle₀Equiv C X).symm f).f (n + 1) = 0