The homotopy fiber of a morphism of homological complexes

In this file, we construct the homotopy fiber of a morphism φ : F ⟶ G between homological complexes. Moreover, we dualise the definition of the cylinder (which is a particular case of a homotopy cofiber) in order to define the path object of a homological complex.

class HomologicalComplex.HasHomotopyFiber {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F G : HomologicalComplex C c} (φ : F ⟶ G) : Prop

A morphism of homological complexes φ : F ⟶ G has a homotopy fiber if for all indices i and j such that c.Rel i j, the binary biproduct F.X i ⊞ G.X j exists.

• hasBinaryBiproduct (i j : α) (hij : c.Rel i j) : CategoryTheory.Limits.HasBinaryBiproduct (G.X i) (F.X j)

instance HomologicalComplex.instHasHomotopyFiberOfHasBinaryBiproducts {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F G : HomologicalComplex C c} (φ : F ⟶ G) [CategoryTheory.Limits.HasBinaryBiproducts C] : HasHomotopyFiber φ

instance HomologicalComplex.instHasHomotopyCofiberOppositeMapSymmOpFunctorOp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F G : HomologicalComplex C c} (φ : F ⟶ G) [HasHomotopyFiber φ] : HasHomotopyCofiber ((opFunctor C c).map φ.op)

noncomputable def HomologicalComplex.homotopyFiber {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F G : HomologicalComplex C c} (φ : F ⟶ G) [HasHomotopyFiber φ] [DecidableRel c.Rel] : HomologicalComplex C c

The homotopy fiber of a morphism between homological complexes.

Equations

• HomologicalComplex.homotopyFiber φ = (HomologicalComplex.unopFunctor C c.symm).obj (Opposite.op (HomologicalComplex.homotopyCofiber ((HomologicalComplex.opFunctor C c).map φ.op)))

instance HomologicalComplex.instHasBinaryBiproductOppositeXOp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] (i : α) : CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)

@[reducible, inline]

abbrev HomologicalComplex.HasPathObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] : Prop

The property that a homological complex K has a path object, i.e. that the morphism K ⟶ K ⊞ K induced by 𝟙 K and -𝟙 K has a homotopy fiber.

Equations

• K.HasPathObject = HomologicalComplex.HasHomotopyFiber (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))

instance HomologicalComplex.instHasHomotopyCofiberOppositeLiftSymmIdOpNegHomOfHasPathObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] : HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op) (-CategoryTheory.CategoryStruct.id K.op))

noncomputable def HomologicalComplex.pathObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] : HomologicalComplex C c.symm.symm

The path object of a homological complex is defined here by dualizing the cylinder object of K.op.

Equations

• K.pathObject = (HomologicalComplex.unopFunctor C c.symm).obj (Opposite.op K.op.cylinder)

theorem HomologicalComplex.pathObject.isZero_X {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (i : α) (h₁ : CategoryTheory.Limits.IsZero (K.X i)) (h₂ : ∀ (j : α), c.Rel j i → CategoryTheory.Limits.IsZero (K.X j)) : CategoryTheory.Limits.IsZero (K.pathObject.X i)

noncomputable def HomologicalComplex.pathObject.π₀ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] : K.pathObject ⟶ K

The first projection K.pathObject ⟶ K.

Equations

• HomologicalComplex.pathObject.π₀ K = (HomologicalComplex.unopFunctor C c.symm).map (HomologicalComplex.cylinder.ι₀ K.op).op

noncomputable def HomologicalComplex.pathObject.π₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] : K.pathObject ⟶ K

The second projection K.pathObject ⟶ K.

Equations

• HomologicalComplex.pathObject.π₁ K = (HomologicalComplex.unopFunctor C c.symm).map (HomologicalComplex.cylinder.ι₁ K.op).op

noncomputable def HomologicalComplex.pathObject.ι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] : K ⟶ K.pathObject

The inclusion K ⟶ K.pathObject.

Equations

• HomologicalComplex.pathObject.ι K = (HomologicalComplex.unopFunctor C c.symm).map (HomologicalComplex.cylinder.π K.op).op

@[simp]

theorem HomologicalComplex.pathObject.π₀_ι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] : CategoryTheory.CategoryStruct.comp (ι K) (π₀ K) = CategoryTheory.CategoryStruct.id K

@[simp]

theorem HomologicalComplex.pathObject.π₀_ι_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] {Z : HomologicalComplex C c} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι K) (CategoryTheory.CategoryStruct.comp (π₀ K) h) = h

@[simp]

theorem HomologicalComplex.pathObject.π₁_ι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] : CategoryTheory.CategoryStruct.comp (ι K) (π₁ K) = CategoryTheory.CategoryStruct.id K

@[simp]

theorem HomologicalComplex.pathObject.π₁_ι_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] {Z : HomologicalComplex C c} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι K) (CategoryTheory.CategoryStruct.comp (π₁ K) h) = h

noncomputable def HomologicalComplex.pathObject.π₀CompιHomotopy {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (hc : ∀ (i : α), ∃ (j : α), c.Rel i j) : Homotopy (CategoryTheory.CategoryStruct.comp (π₀ K) (ι K)) (CategoryTheory.CategoryStruct.id K.pathObject)

The homotopy between π₀ K ≫ ι K and 𝟙 K.pathObject.

Equations

• HomologicalComplex.pathObject.π₀CompιHomotopy K hc = (HomologicalComplex.cylinder.πCompι₀Homotopy K.op hc).unop

noncomputable def HomologicalComplex.pathObject.homotopyEquiv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (hc : ∀ (i : α), ∃ (j : α), c.Rel i j) : HomotopyEquiv K K.pathObject

The homotopy equivalence between K and K.pathObject.

Equations

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

@[simp]

theorem HomologicalComplex.pathObject.homotopyEquiv_inv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (hc : ∀ (i : α), ∃ (j : α), c.Rel i j) : (homotopyEquiv K hc).inv = π₀ K

@[simp]

theorem HomologicalComplex.pathObject.homotopyEquiv_homotopyHomInvId {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (hc : ∀ (i : α), ∃ (j : α), c.Rel i j) : (homotopyEquiv K hc).homotopyHomInvId = Homotopy.ofEq ⋯

@[simp]

theorem HomologicalComplex.pathObject.homotopyEquiv_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (hc : ∀ (i : α), ∃ (j : α), c.Rel i j) : (homotopyEquiv K hc).hom = ι K

@[simp]

theorem HomologicalComplex.pathObject.homotopyEquiv_homotopyInvHomId {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (hc : ∀ (i : α), ∃ (j : α), c.Rel i j) : (homotopyEquiv K hc).homotopyInvHomId = π₀CompιHomotopy K hc

noncomputable def HomologicalComplex.pathObject.homotopy₀₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (hc : ∀ (i : α), ∃ (j : α), c.Rel i j) : Homotopy (π₀ K) (π₁ K)

The homotopy between pathObject.ι₀ K and pathObject.ι₁ K.

Equations

• HomologicalComplex.pathObject.homotopy₀₁ K hc = (HomologicalComplex.cylinder.homotopy₀₁ K.op hc).unop

noncomputable def HomologicalComplex.pathObject.lift {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) : F ⟶ K.pathObject

The morphism F ⟶ K.pathObject that is induced by two morphisms φ₀ φ₁ : F ⟶ K and a homotopy h : Homotopy φ₀ φ₁.

Equations

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

@[simp]

theorem HomologicalComplex.pathObject.lift_π₀ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) : CategoryTheory.CategoryStruct.comp (lift φ₀ φ₁ h) (π₀ K) = φ₀

@[simp]

theorem HomologicalComplex.pathObject.lift_π₀_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h✝ : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (lift φ₀ φ₁ h) (CategoryTheory.CategoryStruct.comp (π₀ K) h✝) = CategoryTheory.CategoryStruct.comp φ₀ h✝

@[simp]

theorem HomologicalComplex.pathObject.lift_π₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) : CategoryTheory.CategoryStruct.comp (lift φ₀ φ₁ h) (π₁ K) = φ₁

@[simp]

theorem HomologicalComplex.pathObject.lift_π₁_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {α : Type u_2} {c : ComplexShape α} {F K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h✝ : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (lift φ₀ φ₁ h) (CategoryTheory.CategoryStruct.comp (π₁ K) h✝) = CategoryTheory.CategoryStruct.comp φ₁ h✝