Documentation

Mathlib.Algebra.Homology.Precylinder

Precylinder and pre-path objects in the category of homological complexes #

In this file, we upgrade the definitions HomologicalComplex.cylinder and HomologicalComplex.pathObject to pre-cylinder objects and pre-path objects in the sense of homotopical algebra.

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

HomotopicalAlgebra.Precylinder K

The precylinder object of a homological complex that is given by HomologicalComplex.cylinder.

Equations

K.precylinder = { I := K.cylinder, i₀ := HomologicalComplex.cylinder.ι₀ K, i₁ := HomologicalComplex.cylinder.ι₁ K, π := HomologicalComplex.cylinder.π K, i₀_π := ⋯, i₁_π := ⋯ }

Instances For

@[simp]

theorem HomologicalComplex.precylinder_π {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} [DecidableRel c.Rel] (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasCylinder] :

K.precylinder.π = cylinder.π K

@[simp]

theorem HomologicalComplex.precylinder_I {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} [DecidableRel c.Rel] (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasCylinder] :

K.precylinder.I = K.cylinder

@[simp]

theorem HomologicalComplex.precylinder_i₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} [DecidableRel c.Rel] (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasCylinder] :

K.precylinder.i₁ = cylinder.ι₁ K

@[simp]

theorem HomologicalComplex.precylinder_i₀ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} [DecidableRel c.Rel] (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasCylinder] :

K.precylinder.i₀ = cylinder.ι₀ K

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

HomotopicalAlgebra.PrepathObject K

The pre-path object of a homological complex that is given by HomologicalComplex.pathObject.

Equations

K.prepathObject = { P := K.pathObject, p₀ := HomologicalComplex.pathObject.π₀ K, p₁ := HomologicalComplex.pathObject.π₁ K, ι := HomologicalComplex.pathObject.ι K, ι_p₀ := ⋯, ι_p₁ := ⋯ }

Instances For

@[simp]

theorem HomologicalComplex.prepathObject_p₀ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} [DecidableRel c.Rel] (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] :

K.prepathObject.p₀ = pathObject.π₀ K

@[simp]

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

K.prepathObject.P = K.pathObject

@[simp]

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

K.prepathObject.ι = pathObject.ι K

@[simp]

theorem HomologicalComplex.prepathObject_p₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} [DecidableRel c.Rel] (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject] :

K.prepathObject.p₁ = pathObject.π₁ K