Homotopies in the arrow category

We define left and right homotopies between morphisms of Arrow V, where V is a preadditive category.

TODO: Define the preadditive categories LeftFreyd V (resp. RightFreyd V) obtained by taking the quotient of Arrow V by the left (resp. right) homotopy relation. If V has binary biproducts, this will have all kernels (resp. cokernels) and will be the category obtained by freely adjoining kernels (resp. cokernels) to V.

structure CategoryTheory.Arrow.LeftHomotopy {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f g : u ⟶ v) : Type v_1

A left homotopy on morphisms in the category of arrows of a preadditive category.

• hom : u.right ⟶ v.left

  A "diagonal" morphism from the right object of u to the left object of v.

• comm : Hom.left f - Hom.left g = CategoryStruct.comp u.hom self.hom

  The difference of the left morphisms factors through hom.

theorem CategoryTheory.Arrow.LeftHomotopy.ext {V : Type u_1} {inst✝ : Category.{v_1, u_1} V} {inst✝¹ : Preadditive V} {u v : Arrow V} {f g : u ⟶ v} {x y : LeftHomotopy f g} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.Arrow.LeftHomotopy.ext_iff {V : Type u_1} {inst✝ : Category.{v_1, u_1} V} {inst✝¹ : Preadditive V} {u v : Arrow V} {f g : u ⟶ v} {x y : LeftHomotopy f g} : x = y ↔ x.hom = y.hom

structure CategoryTheory.Arrow.RightHomotopy {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f g : u ⟶ v) : Type v_1

A right homotopy on morphisms in the category of arrows of a preadditive category.

• hom : u.right ⟶ v.left

  A "diagonal" morphism from the right object of u to the left object of v.

• comm : Hom.right f - Hom.right g = CategoryStruct.comp self.hom v.hom

  The difference of the right morphisms factors through hom.

theorem CategoryTheory.Arrow.RightHomotopy.ext_iff {V : Type u_1} {inst✝ : Category.{v_1, u_1} V} {inst✝¹ : Preadditive V} {u v : Arrow V} {f g : u ⟶ v} {x y : RightHomotopy f g} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.Arrow.RightHomotopy.ext {V : Type u_1} {inst✝ : Category.{v_1, u_1} V} {inst✝¹ : Preadditive V} {u v : Arrow V} {f g : u ⟶ v} {x y : RightHomotopy f g} (hom : x.hom = y.hom) : x = y

def CategoryTheory.Arrow.LeftHomotopy.equivSubZero {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} : LeftHomotopy f g ≃ LeftHomotopy (f - g) 0

f is left homotopic to g iff f - g is left homotopic to 0.

Equations

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

def CategoryTheory.Arrow.LeftHomotopy.ofEq {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : f = g) : LeftHomotopy f g

Equal maps of arrows are left homotopic.

Equations

• CategoryTheory.Arrow.LeftHomotopy.ofEq h = { hom := 0, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.ofEq_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : f = g) : (ofEq h).hom = 0

def CategoryTheory.Arrow.LeftHomotopy.refl {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f : u ⟶ v) : LeftHomotopy f f

Every map of arrows is left homotopic to itself.

Equations

• CategoryTheory.Arrow.LeftHomotopy.refl f = CategoryTheory.Arrow.LeftHomotopy.ofEq ⋯

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.refl_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f : u ⟶ v) : (refl f).hom = 0

def CategoryTheory.Arrow.LeftHomotopy.symm {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : LeftHomotopy f g) : LeftHomotopy g f

f is left homotopic to g iff g is left homotopic to f.

Equations

• h.symm = { hom := -h.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.symm_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : LeftHomotopy f g) : h.symm.hom = -h.hom

def CategoryTheory.Arrow.LeftHomotopy.trans {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {e f g : u ⟶ v} (h : LeftHomotopy e f) (k : LeftHomotopy f g) : LeftHomotopy e g

Left homotopy is a transitive relation.

Equations

• h.trans k = { hom := h.hom + k.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.trans_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {e f g : u ⟶ v} (h : LeftHomotopy e f) (k : LeftHomotopy f g) : (h.trans k).hom = h.hom + k.hom

def CategoryTheory.Arrow.LeftHomotopy.add {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f₁ g₁ f₂ g₂ : u ⟶ v} (h₁ : LeftHomotopy f₁ g₁) (h₂ : LeftHomotopy f₂ g₂) : LeftHomotopy (f₁ + f₂) (g₁ + g₂)

The sum of two left homotopies is a left homotopy between the sum of the respective morphisms.

Equations

• h₁.add h₂ = { hom := h₁.hom + h₂.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.add_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f₁ g₁ f₂ g₂ : u ⟶ v} (h₁ : LeftHomotopy f₁ g₁) (h₂ : LeftHomotopy f₂ g₂) : (h₁.add h₂).hom = h₁.hom + h₂.hom

def CategoryTheory.Arrow.LeftHomotopy.compRight {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {e f : u ⟶ v} (h : LeftHomotopy e f) (g : v ⟶ w) : LeftHomotopy (CategoryStruct.comp e g) (CategoryStruct.comp f g)

Left homotopy is closed under composition (on the right).

Equations

• h.compRight g = { hom := CategoryTheory.CategoryStruct.comp h.hom (CategoryTheory.Arrow.Hom.left g), comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.compRight_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {e f : u ⟶ v} (h : LeftHomotopy e f) (g : v ⟶ w) : (h.compRight g).hom = CategoryStruct.comp h.hom (Hom.left g)

def CategoryTheory.Arrow.LeftHomotopy.compLeft {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f g : v ⟶ w} (h : LeftHomotopy f g) (e : u ⟶ v) : LeftHomotopy (CategoryStruct.comp e f) (CategoryStruct.comp e g)

Left homotopy is closed under composition (on the left).

Equations

• h.compLeft e = { hom := CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e) h.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.compLeft_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f g : v ⟶ w} (h : LeftHomotopy f g) (e : u ⟶ v) : (h.compLeft e).hom = CategoryStruct.comp (Hom.right e) h.hom

def CategoryTheory.Arrow.LeftHomotopy.comp {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f₁ g₁ : u ⟶ v} {f₂ g₂ : v ⟶ w} (h₁ : LeftHomotopy f₁ g₁) (h₂ : LeftHomotopy f₂ g₂) : LeftHomotopy (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)

Left homotopy is closed under composition.

Equations

• h₁.comp h₂ = (h₁.compRight f₂).trans (h₂.compLeft g₁)

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.comp_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f₁ g₁ : u ⟶ v} {f₂ g₂ : v ⟶ w} (h₁ : LeftHomotopy f₁ g₁) (h₂ : LeftHomotopy f₂ g₂) : (h₁.comp h₂).hom = CategoryStruct.comp h₁.hom (Hom.left f₂) + CategoryStruct.comp (Hom.right g₁) h₂.hom

def CategoryTheory.Arrow.LeftHomotopy.compRightId {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : u ⟶ u} (h : LeftHomotopy f (CategoryStruct.id u)) (g : u ⟶ v) : LeftHomotopy (CategoryStruct.comp f g) g

A variant of LeftHomotopy.compRight useful for dealing with homotopy equivalences.

Equations

• h.compRightId g = (h.compRight g).trans (CategoryTheory.Arrow.LeftHomotopy.ofEq ⋯)

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.compRightId_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : u ⟶ u} (h : LeftHomotopy f (CategoryStruct.id u)) (g : u ⟶ v) : (h.compRightId g).hom = CategoryStruct.comp h.hom (Hom.left g)

def CategoryTheory.Arrow.LeftHomotopy.compLeftId {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : v ⟶ v} (h : LeftHomotopy f (CategoryStruct.id v)) (g : u ⟶ v) : LeftHomotopy (CategoryStruct.comp g f) g

A variant of LeftHomotopy.compLeft useful for dealing with homotopy equivalences.

Equations

• h.compLeftId g = (h.compLeft g).trans (CategoryTheory.Arrow.LeftHomotopy.ofEq ⋯)

@[simp]

theorem CategoryTheory.Arrow.LeftHomotopy.compLeftId_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : v ⟶ v} (h : LeftHomotopy f (CategoryStruct.id v)) (g : u ⟶ v) : (h.compLeftId g).hom = CategoryStruct.comp (Hom.right g) h.hom

def CategoryTheory.Arrow.RightHomotopy.equivSubZero {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} : RightHomotopy f g ≃ RightHomotopy (f - g) 0

f is right homotopic to g iff f - g is righthomotopic to 0.

Equations

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

def CategoryTheory.Arrow.RightHomotopy.ofEq {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : f = g) : RightHomotopy f g

Equal maps of arrows are right homotopic.

Equations

• CategoryTheory.Arrow.RightHomotopy.ofEq h = { hom := 0, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.ofEq_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : f = g) : (ofEq h).hom = 0

def CategoryTheory.Arrow.RightHomotopy.refl {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f : u ⟶ v) : RightHomotopy f f

Every map of arrows is right homotopic to itself.

Equations

• CategoryTheory.Arrow.RightHomotopy.refl f = CategoryTheory.Arrow.RightHomotopy.ofEq ⋯

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.refl_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f : u ⟶ v) : (refl f).hom = 0

def CategoryTheory.Arrow.RightHomotopy.symm {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : RightHomotopy f g) : RightHomotopy g f

f is right homotopic to g iff g is right homotopic to f.

Equations

• h.symm = { hom := -h.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.symm_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f g : u ⟶ v} (h : RightHomotopy f g) : h.symm.hom = -h.hom

def CategoryTheory.Arrow.RightHomotopy.trans {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {e f g : u ⟶ v} (h : RightHomotopy e f) (k : RightHomotopy f g) : RightHomotopy e g

Right homotopy is a transitive relation.

Equations

• h.trans k = { hom := h.hom + k.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.trans_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {e f g : u ⟶ v} (h : RightHomotopy e f) (k : RightHomotopy f g) : (h.trans k).hom = h.hom + k.hom

def CategoryTheory.Arrow.RightHomotopy.add {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f₁ g₁ f₂ g₂ : u ⟶ v} (h₁ : RightHomotopy f₁ g₁) (h₂ : RightHomotopy f₂ g₂) : RightHomotopy (f₁ + f₂) (g₁ + g₂)

The sum of two right homotopies is a right homotopy between the sum of the respective morphisms.

Equations

• h₁.add h₂ = { hom := h₁.hom + h₂.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.add_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f₁ g₁ f₂ g₂ : u ⟶ v} (h₁ : RightHomotopy f₁ g₁) (h₂ : RightHomotopy f₂ g₂) : (h₁.add h₂).hom = h₁.hom + h₂.hom

def CategoryTheory.Arrow.RightHomotopy.compRight {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {e f : u ⟶ v} (h : RightHomotopy e f) (g : v ⟶ w) : RightHomotopy (CategoryStruct.comp e g) (CategoryStruct.comp f g)

Right homotopy is closed under composition (on the right).

Equations

• h.compRight g = { hom := CategoryTheory.CategoryStruct.comp h.hom (CategoryTheory.Arrow.Hom.left g), comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.compRight_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {e f : u ⟶ v} (h : RightHomotopy e f) (g : v ⟶ w) : (h.compRight g).hom = CategoryStruct.comp h.hom (Hom.left g)

def CategoryTheory.Arrow.RightHomotopy.compLeft {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f g : v ⟶ w} (h : RightHomotopy f g) (e : u ⟶ v) : RightHomotopy (CategoryStruct.comp e f) (CategoryStruct.comp e g)

Right homotopy is closed under composition (on the left).

Equations

• h.compLeft e = { hom := CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e) h.hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.compLeft_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f g : v ⟶ w} (h : RightHomotopy f g) (e : u ⟶ v) : (h.compLeft e).hom = CategoryStruct.comp (Hom.right e) h.hom

def CategoryTheory.Arrow.RightHomotopy.comp {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f₁ g₁ : u ⟶ v} {f₂ g₂ : v ⟶ w} (h₁ : RightHomotopy f₁ g₁) (h₂ : RightHomotopy f₂ g₂) : RightHomotopy (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)

Right homotopy is closed under composition.

Equations

• h₁.comp h₂ = (h₁.compRight f₂).trans (h₂.compLeft g₁)

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.comp_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v w : Arrow V} {f₁ g₁ : u ⟶ v} {f₂ g₂ : v ⟶ w} (h₁ : RightHomotopy f₁ g₁) (h₂ : RightHomotopy f₂ g₂) : (h₁.comp h₂).hom = CategoryStruct.comp h₁.hom (Hom.left f₂) + CategoryStruct.comp (Hom.right g₁) h₂.hom

def CategoryTheory.Arrow.RightHomotopy.compRightId {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : u ⟶ u} (h : RightHomotopy f (CategoryStruct.id u)) (g : u ⟶ v) : RightHomotopy (CategoryStruct.comp f g) g

A variant of RightHomotopy.compRight useful for dealing with homotopy equivalences.

Equations

• h.compRightId g = (h.compRight g).trans (CategoryTheory.Arrow.RightHomotopy.ofEq ⋯)

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.compRightId_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : u ⟶ u} (h : RightHomotopy f (CategoryStruct.id u)) (g : u ⟶ v) : (h.compRightId g).hom = CategoryStruct.comp h.hom (Hom.left g)

def CategoryTheory.Arrow.RightHomotopy.compLeftId {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : v ⟶ v} (h : RightHomotopy f (CategoryStruct.id v)) (g : u ⟶ v) : RightHomotopy (CategoryStruct.comp g f) g

A variant of RightHomotopy.compLeft useful for dealing with homotopy equivalences.

Equations

• h.compLeftId g = (h.compLeft g).trans (CategoryTheory.Arrow.RightHomotopy.ofEq ⋯)

@[simp]

theorem CategoryTheory.Arrow.RightHomotopy.compLeftId_hom {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} {f : v ⟶ v} (h : RightHomotopy f (CategoryStruct.id v)) (g : u ⟶ v) : (h.compLeftId g).hom = CategoryStruct.comp (Hom.right g) h.hom

def CategoryTheory.Arrow.leftHomotopic (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : HomRel (Arrow V)

The left homotopy relation on morphisms of Arrow V.

Equations

• CategoryTheory.Arrow.leftHomotopic V f g = Nonempty (CategoryTheory.Arrow.LeftHomotopy f g)

instance CategoryTheory.Arrow.leftHomotopy_congruence (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : Congruence (leftHomotopic V)

def CategoryTheory.Arrow.rightHomotopic (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : HomRel (Arrow V)

The left homotopy relation on morphisms of Arrow V.

Equations

• CategoryTheory.Arrow.rightHomotopic V f g = Nonempty (CategoryTheory.Arrow.RightHomotopy f g)

instance CategoryTheory.Arrow.rightHomotopy_congruence (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : Congruence (rightHomotopic V)