The right Freyd category

Let V be a preadditive category. The right Freyd category of V is the quotient of Arrow V by the right homotopy relation. (This is simply called "Freyd category" in the reference.) This is a preadditive category with a fully faithful additive functor RightFreyd.functor : V ⥤ RightFreyd V.

We also show that, if V has binary biproducts, then RightFreyd V has cokernels. In fact we construct, given a morphism f : u ⟶ v in Arrow V, a morphism Candidate.π f : v ⟶ Candidate.cokernel f in Arrow V such that f ≫ Candidate.π f is right homotopic to 0 (see Candidate.condition). This allows us to define a cokernel cofork for (quotient V).map f (see Candidate.cokernelCofork), and we show in Candidate.isColimitCokernelCofork that this is a cokernel cofork.

References

• Posur, S., A constructive approach to Freyd categories

def CategoryTheory.Preadditive.RightFreyd (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : Type (max u_1 v_1)

If V is a preadditive category, then RightFreyd V is the category of arrows in V, with morphisms identified when they are right homotopic.

Equations

• CategoryTheory.Preadditive.RightFreyd V = CategoryTheory.Quotient (CategoryTheory.Arrow.rightHomotopic V)

@[implicit_reducible]

instance CategoryTheory.Preadditive.instCategoryRightFreyd (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : Category.{v_1, max u_1 v_1} (RightFreyd V)

Equations

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

@[implicit_reducible]

instance CategoryTheory.Preadditive.instRightFreyd (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : Preadditive (RightFreyd V)

The category RightFreyd V is preadditive.

Equations

• CategoryTheory.Preadditive.instRightFreyd V = CategoryTheory.Quotient.preadditive (CategoryTheory.Arrow.rightHomotopic V) ⋯

def CategoryTheory.Preadditive.RightFreyd.quotient (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : Functor (Arrow V) (RightFreyd V)

The quotient functor from Arrow V to RightFreyd V.

Equations

• CategoryTheory.Preadditive.RightFreyd.quotient V = CategoryTheory.Quotient.functor (CategoryTheory.Arrow.rightHomotopic V)

instance CategoryTheory.Preadditive.RightFreyd.instFullArrowQuotient (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : (quotient V).Full

instance CategoryTheory.Preadditive.RightFreyd.instEssSurjArrowQuotient (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : (quotient V).EssSurj

instance CategoryTheory.Preadditive.RightFreyd.instAdditiveArrowQuotient (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] : (quotient V).Additive

theorem CategoryTheory.Preadditive.RightFreyd.eq_of_rightHomotopy {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f g : u ⟶ v) (h : Arrow.RightHomotopy f g) : (quotient V).map f = (quotient V).map g

If two morphisms in Arrow V are right homotopic, then they become equal in the right Freyd category.

noncomputable def CategoryTheory.Preadditive.RightFreyd.homotopyOfEq {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f g : u ⟶ v) (w : (quotient V).map f = (quotient V).map g) : Arrow.RightHomotopy f g

If two morphisms of Arrow V become equal in the right Freyd category, then they are right homotopic.

Equations

• CategoryTheory.Preadditive.RightFreyd.homotopyOfEq f g w = Nonempty.some ⋯

theorem CategoryTheory.Preadditive.RightFreyd.quotient_map_eq_iff {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f g : u ⟶ v) : (quotient V).map f = (quotient V).map g ↔ Nonempty (Arrow.RightHomotopy f g)

Two morphisms in Arrow V have the same image in RightFreyd V if and only if there exists a right homotopy between them.

theorem CategoryTheory.Preadditive.RightFreyd.quotient_map_eq_zero_iff {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f : u ⟶ v) : (quotient V).map f = 0 ↔ Nonempty (Arrow.RightHomotopy f 0)

A morphism f in Arrow V is sent to 0 in RightFreyd V if and only if there exists a right homotopy between f and 0.

theorem CategoryTheory.Preadditive.RightFreyd.epi_of_isIso_right {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] {u v : Arrow V} (f : u ⟶ v) [IsIso (Arrow.Hom.right f)] : Epi ((quotient V).map f)

If f is a morphism of Arrow V such that f.right is an isomorphism, then the image of f in the right Freyd category is an epimorphism.

noncomputable def CategoryTheory.Preadditive.RightFreyd.rightFunctor (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] : Functor V (Arrow V)

If V has a zero object, this is the functor from V to Arrow V that sends an object X to the arrow 0 ⟶ X.

Equations

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

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.rightFunctor_obj (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] (X : V) : (rightFunctor V).obj X = Arrow.mk 0

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.rightFunctor_map (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) : (rightFunctor V).map f = Arrow.homMk 0 f ⋯

instance CategoryTheory.Preadditive.RightFreyd.instAdditiveArrowRightFunctor (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] : (rightFunctor V).Additive

@[reducible, inline]

noncomputable abbrev CategoryTheory.Preadditive.RightFreyd.functor (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] : Functor V (RightFreyd V)

The fully faithful additive functor from V to RightFreyd V sending an object X of V to the class of the arrow 0 ⟶ X.

Equations

• CategoryTheory.Preadditive.RightFreyd.functor V = (CategoryTheory.Preadditive.RightFreyd.rightFunctor V).comp (CategoryTheory.Preadditive.RightFreyd.quotient V)

instance CategoryTheory.Preadditive.RightFreyd.instAdditiveFunctor (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] : (functor V).Additive

instance CategoryTheory.Preadditive.RightFreyd.instFullFunctor (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] : (functor V).Full

instance CategoryTheory.Preadditive.RightFreyd.instFaithfulFunctor (V : Type u_1) [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasZeroObject V] : (functor V).Faithful

@[reducible, inline]

noncomputable abbrev CategoryTheory.Preadditive.RightFreyd.Candidate.cokernel {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) : Arrow V

If f is a morphism of Arrow V, this is a "candidate cokernel" of f, i.e. an object in Arrow V whose image in RightFreyd V will be a cokernel of the image of f.

Equations

• CategoryTheory.Preadditive.RightFreyd.Candidate.cokernel f = CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc v.hom (CategoryTheory.Arrow.Hom.right f))

noncomputable def CategoryTheory.Preadditive.RightFreyd.Candidate.π {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) : v ⟶ cokernel f

For f : u ⟶ v a morphism in Arrow V, this is the morphism v ⟶ cokernel f from v to the "candidate cokernel" of f, whose image in RightFreyd V will be the projection to the cokernel of the image of f.

Equations

• CategoryTheory.Preadditive.RightFreyd.Candidate.π f = CategoryTheory.Arrow.homMk CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.id v.right) ⋯

noncomputable def CategoryTheory.Preadditive.RightFreyd.Candidate.condition {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) : Arrow.RightHomotopy (CategoryStruct.comp f (π f)) 0

The right homotopy expressing that f ≫ π f is sent to 0 in RightFreyd V.

Equations

• CategoryTheory.Preadditive.RightFreyd.Candidate.condition f = { hom := CategoryTheory.Limits.biprod.inr, comm := ⋯ }

instance CategoryTheory.Preadditive.RightFreyd.Candidate.instEpiMapArrowQuotientπ {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) : Epi ((quotient V).map (π f))

noncomputable def CategoryTheory.Preadditive.RightFreyd.Candidate.desc {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) {w : Arrow V} (g : v ⟶ w) (h : Arrow.RightHomotopy (CategoryStruct.comp f g) 0) : cokernel f ⟶ w

If f : u ⟶ v and g : v ⟶ w are morphisms in Arrow V such that f ≫ g is right homotopic to 0, this is the morphism from the "candidate cokernel" of f to w defined from the right homotopy.

Equations

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

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.Candidate.π_desc {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) {w : Arrow V} (g : v ⟶ w) (h : Arrow.RightHomotopy (CategoryStruct.comp f g) 0) : CategoryStruct.comp (π f) (desc f g h) = g

@[simp]

theorem CategoryTheory.Preadditive.RightFreyd.Candidate.π_desc_assoc {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) {w : Arrow V} (g : v ⟶ w) (h : Arrow.RightHomotopy (CategoryStruct.comp f g) 0) {Z : Arrow V} (h✝ : w ⟶ Z) : CategoryStruct.comp (π f) (CategoryStruct.comp (desc f g h) h✝) = CategoryStruct.comp g h✝

noncomputable def CategoryTheory.Preadditive.RightFreyd.Candidate.cokernelCofork {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) : Limits.CokernelCofork ((quotient V).map f)

For f a morphism in Arrow V, this is a cokernel cofork of (quotient V).map f.

Equations

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

noncomputable def CategoryTheory.Preadditive.RightFreyd.Candidate.isColimitCokernelCofork {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] {u v : Arrow V} (f : u ⟶ v) : Limits.IsColimit (cokernelCofork f)

For f a morphism in Arrow V, the cokernel cofork of (quotient V).map f constructed in cokernelCofork is a colimit cofork.

Equations

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

instance CategoryTheory.Preadditive.RightFreyd.instHasCokernels {V : Type u_1} [Category.{v_1, u_1} V] [Preadditive V] [Limits.HasBinaryBiproducts V] : Limits.HasCokernels (RightFreyd V)

The category RightFreyd V has all cokernels if V has binary biproducts.