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₁) : HomologicalComplex C c

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

• One or more equations did not get rendered due to their size.

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₁) : (double f hi₀₁).X i₀ ≅ X₀

The isomorphism (double f hi₀₁).X i₀ ≅ X₀.

Equations

• HomologicalComplex.doubleXIso₀ f hi₀₁ = CategoryTheory.eqToIso ⋯

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₁) : (double f hi₀₁).X i₁ ≅ X₁

The isomorphism (double f hi₀₁).X i₁ ≅ X₁.

Equations

• HomologicalComplex.doubleXIso₁ f hi₀₁ h = CategoryTheory.eqToIso ⋯

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₀) : (double f hi₀₁).d a b = 0

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₁) : (double f hi₀₁).d a b = 0

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.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₁) : φ = φ'

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) : double f hi₀₁ ⟶ K

Constructor for morphisms from a homological complex double f hi₀₁.

Equations

• One or more equations did not get rendered due to their size.

@[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

• One or more equations did not get rendered due to their size.

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₀)

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₁)) ⋯ ⋯

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

• One or more equations did not get rendered due to their size.

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) : (evalCompCoyonedaCorepresentableBySingle c i hi X).homEquiv.symm f = mkHomFromSingle f ⋯