A homological complex lying in two degrees #
Given c : ComplexShape ι, distinct indices i₀ and i₁ such that hi₀₁ : c.Rel i₀ i₁,
we construct a homological complex double f hi₀₁ for any morphism f : X₀ ⟶ X₁.
It consists of the objects X₀ and X₁ in degrees i₀ and i₁, respectively,
with the differential X₀ ⟶ X₁ given by f, and zero everywhere else.
noncomputable def
HomologicalComplex.double
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
(f : X₀ ⟶ X₁)
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
:
Given a complex shape c, two indices i₀ and i₁ such that c.Rel i₀ i₁,
and f : X₀ ⟶ X₁, this is the homological complex which, if i₀ ≠ i₁, only
consists of the map f in degrees i₀ and i₁, and zero everywhere else.
Equations
Instances For
theorem
HomologicalComplex.isZero_double_X
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
(f : X₀ ⟶ X₁)
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(k : ι)
(h₀ : k ≠ i₀)
(h₁ : k ≠ i₁)
:
CategoryTheory.Limits.IsZero ((double f hi₀₁).X k)
noncomputable def
HomologicalComplex.doubleXIso₀
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
(f : X₀ ⟶ X₁)
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
:
The isomorphism (double f hi₀₁).X i₀ ≅ X₀.
Equations
Instances For
noncomputable def
HomologicalComplex.doubleXIso₁
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
(f : X₀ ⟶ X₁)
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
:
The isomorphism (double f hi₀₁).X i₁ ≅ X₁.
Equations
Instances For
theorem
HomologicalComplex.double_d
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
(f : X₀ ⟶ X₁)
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
:
(double f hi₀₁).d i₀ i₁ = CategoryTheory.CategoryStruct.comp (doubleXIso₀ f hi₀₁).hom
(CategoryTheory.CategoryStruct.comp f (doubleXIso₁ f hi₀₁ h).inv)
theorem
HomologicalComplex.double_d_eq_zero₀
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
(f : X₀ ⟶ X₁)
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(a b : ι)
(ha : a ≠ i₀)
:
theorem
HomologicalComplex.double_d_eq_zero₁
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
(f : X₀ ⟶ X₁)
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(a b : ι)
(hb : b ≠ i₁)
:
theorem
HomologicalComplex.from_double_hom_ext
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
{hi₀₁ : c.Rel i₀ i₁}
{K : HomologicalComplex C c}
{φ φ' : double f hi₀₁ ⟶ K}
(h₀ : φ.f i₀ = φ'.f i₀)
(h₁ : φ.f i₁ = φ'.f i₁)
:
theorem
HomologicalComplex.from_double_hom_ext_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
{hi₀₁ : c.Rel i₀ i₁}
{K : HomologicalComplex C c}
{φ φ' : double f hi₀₁ ⟶ K}
:
theorem
HomologicalComplex.to_double_hom_ext
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
{hi₀₁ : c.Rel i₀ i₁}
{K : HomologicalComplex C c}
{φ φ' : K ⟶ double f hi₀₁}
(h₀ : φ.f i₀ = φ'.f i₀)
(h₁ : φ.f i₁ = φ'.f i₁)
:
theorem
HomologicalComplex.to_double_hom_ext_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
{hi₀₁ : c.Rel i₀ i₁}
{K : HomologicalComplex C c}
{φ φ' : K ⟶ double f hi₀₁}
:
noncomputable def
HomologicalComplex.mkHomFromDouble
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
{K : HomologicalComplex C c}
(φ₀ : X₀ ⟶ K.X i₀)
(φ₁ : X₁ ⟶ K.X i₁)
(comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
(hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0)
:
Constructor for morphisms from a homological complex double f hi₀₁.
Equations
Instances For
@[simp]
theorem
HomologicalComplex.mkHomFromDouble_f₀
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
{K : HomologicalComplex C c}
(φ₀ : X₀ ⟶ K.X i₀)
(φ₁ : X₁ ⟶ K.X i₁)
(comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
(hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0)
:
(mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀ = CategoryTheory.CategoryStruct.comp (doubleXIso₀ f hi₀₁).hom φ₀
theorem
HomologicalComplex.mkHomFromDouble_f₀_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
{K : HomologicalComplex C c}
(φ₀ : X₀ ⟶ K.X i₀)
(φ₁ : X₁ ⟶ K.X i₁)
(comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
(hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0)
{Z : C}
(h✝ : K.X i₀ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀) h✝ = CategoryTheory.CategoryStruct.comp (doubleXIso₀ f hi₀₁).hom (CategoryTheory.CategoryStruct.comp φ₀ h✝)
@[simp]
theorem
HomologicalComplex.mkHomFromDouble_f₁
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
{K : HomologicalComplex C c}
(φ₀ : X₀ ⟶ K.X i₀)
(φ₁ : X₁ ⟶ K.X i₁)
(comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
(hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0)
:
(mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₁ = CategoryTheory.CategoryStruct.comp (doubleXIso₁ f hi₀₁ h).hom φ₁
theorem
HomologicalComplex.mkHomFromDouble_f₁_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X₀ X₁ : C}
{f : X₀ ⟶ X₁}
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
{K : HomologicalComplex C c}
(φ₀ : X₀ ⟶ K.X i₀)
(φ₁ : X₁ ⟶ K.X i₁)
(comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
(hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0)
{Z : C}
(h✝ : K.X i₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₁) h✝ = CategoryTheory.CategoryStruct.comp (doubleXIso₁ f hi₀₁ h).hom (CategoryTheory.CategoryStruct.comp φ₁ h✝)
noncomputable def
HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
(X : C)
:
((eval C c i₀).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).CorepresentableBy
(double (CategoryTheory.CategoryStruct.id X) hi₀₁)
Let c : ComplexShape ι, and i₀ and i₁ be distinct indices such
that hi₀₁ : c.Rel i₀ i₁, then for any X : C, the functor which sends
K : HomologicalComplex C c to X ⟶ K.X i is corepresentable by double (𝟙 X) hi₀₁.
Equations
Instances For
theorem
HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
(X : C)
{K : HomologicalComplex C c}
(φ₀ : ((eval C c i₀).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj K)
:
(evalCompCoyonedaCorepresentableByDoubleId hi₀₁ h X).homEquiv.symm φ₀ = mkHomFromDouble hi₀₁ h φ₀ (CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁)) ⋯ ⋯
theorem
HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
{c : ComplexShape ι}
{i₀ i₁ : ι}
(hi₀₁ : c.Rel i₀ i₁)
(h : i₀ ≠ i₁)
(X : C)
{K : HomologicalComplex C c}
(g : double (CategoryTheory.CategoryStruct.id X) hi₀₁ ⟶ K)
:
(evalCompCoyonedaCorepresentableByDoubleId hi₀₁ h X).homEquiv g = CategoryTheory.CategoryStruct.comp (doubleXIso₀ (CategoryTheory.CategoryStruct.id X) hi₀₁).inv (g.f i₀)
noncomputable def
HomologicalComplex.evalCompCoyonedaCorepresentableBySingle
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
(c : ComplexShape ι)
(i : ι)
[DecidableEq ι]
(hi : ∀ (j : ι), ¬c.Rel i j)
(X : C)
:
((eval C c i).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).CorepresentableBy ((single C c i).obj X)
If i has no successor for the complex shape c,
then for any X : C, the functor which sends K : HomologicalComplex C c
to X ⟶ K.X i is corepresentable by (single C c i).obj X.
Equations
Instances For
theorem
HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_apply
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
(c : ComplexShape ι)
(i : ι)
[DecidableEq ι]
(hi : ∀ (j : ι), ¬c.Rel i j)
(X : C)
{K : HomologicalComplex C c}
(g : (single C c i).obj X ⟶ K)
:
(evalCompCoyonedaCorepresentableBySingle c i hi X).homEquiv g = CategoryTheory.CategoryStruct.comp (singleObjXSelf c i X).inv (g.f i)
theorem
HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
(c : ComplexShape ι)
(i : ι)
[DecidableEq ι]
(hi : ∀ (j : ι), ¬c.Rel i j)
(X : C)
{K : HomologicalComplex C c}
(f : ((eval C c i).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj K)
:
noncomputable def
HomologicalComplex.evalCompCoyonedaCorepresentative
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
(c : ComplexShape ι)
(X : C)
(j : ι)
:
Given a complex shape c : ComplexShape ι (with no loop), X : C and j : ι,
this is a quite explicit choice of corepresentative of the functor which sends
K : HomologicalComplex C c to X ⟶ K.X j.
Equations
Instances For
noncomputable def
HomologicalComplex.evalCompCoyonedaCorepresentable
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
(c : ComplexShape ι)
[c.HasNoLoop]
(X : C)
(j : ι)
:
((eval C c j).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).CorepresentableBy
(evalCompCoyonedaCorepresentative c X j)
If a complex shape c : ComplexShape ι has no loop,
then for any X : C and j : ι, the functor which sends K : HomologicalComplex C c
to X ⟶ K.X j is corepresentable.
Equations
Instances For
instance
HomologicalComplex.instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{ι : Type u_2}
(c : ComplexShape ι)
[c.HasNoLoop]
(X : C)
(j : ι)
:
((eval C c j).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).IsCorepresentable