A Lean Companion to Conceptual Mathematics

Session 26: Distributive categories and linear categoriesπŸ”—

2. Matrix multiplication in linear categoriesπŸ”—

Definition: Linear category (p. 279)

A category with zero maps in which every 'identity matrix'... f = \begin{bmatrix} 1_{X} & 0_{XY} \\ 0_{YX} & 1_{Y} \end{bmatrix} : X + Y \rightarrow X \times Y is an isomorphism is called a linear category.

Linear categories can be formalised in Lean using a combination of the HasZeroMorphisms and HasBinaryBiproducts type classes, which we print below for reference.

class CategoryTheory.Limits.HasZeroMorphisms.{v, u} (C : Type u) [Category.{v, u} C] : Type (max u v) number of parameters: 2 fields: CategoryTheory.Limits.HasZeroMorphisms.zero : (X Y : C) β†’ Zero (X ⟢ Y) CategoryTheory.Limits.HasZeroMorphisms.comp_zero : βˆ€ {X Y : C} (f : X ⟢ Y) (Z : C), 0 ⊚ f = 0 := by cat_disch CategoryTheory.Limits.HasZeroMorphisms.zero_comp : βˆ€ (X : C) {Y Z : C} (f : Y ⟢ Z), f ⊚ 0 = 0 := by cat_disch constructor: CategoryTheory.Limits.HasZeroMorphisms.mk.{v, u} {C : Type u} [Category.{v, u} C] [zero : (X Y : C) β†’ Zero (X ⟢ Y)] (comp_zero : βˆ€ {X Y : C} (f : X ⟢ Y) (Z : C), 0 ⊚ f = 0 := by cat_disch) (zero_comp : βˆ€ (X : C) {Y Z : C} (f : Y ⟢ Z), f ⊚ 0 = 0 := by cat_disch) : HasZeroMorphisms C#print HasZeroMorphisms 
class CategoryTheory.Limits.HasZeroMorphisms.{v, u} (C : Type u) [Category.{v, u} C] : Type (max u v)
number of parameters: 2
fields:
  CategoryTheory.Limits.HasZeroMorphisms.zero : (X Y : C) β†’ Zero (X ⟢ Y)
  CategoryTheory.Limits.HasZeroMorphisms.comp_zero : βˆ€ {X Y : C} (f : X ⟢ Y) (Z : C), 0 ⊚ f = 0 := by
    cat_disch
  CategoryTheory.Limits.HasZeroMorphisms.zero_comp : βˆ€ (X : C) {Y Z : C} (f : Y ⟢ Z), f ⊚ 0 = 0 := by
    cat_disch
constructor:
  CategoryTheory.Limits.HasZeroMorphisms.mk.{v, u} {C : Type u} [Category.{v, u} C] [zero : (X Y : C) β†’ Zero (X ⟢ Y)]
    (comp_zero : βˆ€ {X Y : C} (f : X ⟢ Y) (Z : C), 0 ⊚ f = 0 := by cat_disch)
    (zero_comp : βˆ€ (X : C) {Y Z : C} (f : Y ⟢ Z), f ⊚ 0 = 0 := by cat_disch) : HasZeroMorphisms C
class CategoryTheory.Limits.HasBinaryBiproducts.{uC', uC} (C : Type uC) [Category.{uC', uC} C] [HasZeroMorphisms C] : Prop number of parameters: 3 fields: CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct : βˆ€ (P Q : C), HasBinaryBiproduct P Q constructor: CategoryTheory.Limits.HasBinaryBiproducts.mk.{uC', uC} {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (has_binary_biproduct : βˆ€ (P Q : C), HasBinaryBiproduct P Q) : HasBinaryBiproducts C#print HasBinaryBiproducts 
class CategoryTheory.Limits.HasBinaryBiproducts.{uC', uC} (C : Type uC) [Category.{uC', uC} C] [HasZeroMorphisms C] :
  Prop
number of parameters: 3
fields:
  CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct : βˆ€ (P Q : C), HasBinaryBiproduct P Q
constructor:
  CategoryTheory.Limits.HasBinaryBiproducts.mk.{uC', uC} {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C]
    (has_binary_biproduct : βˆ€ (P Q : C), HasBinaryBiproduct P Q) : HasBinaryBiproducts C

In a category with zero morphisms, a binary biproduct is a BinaryBicone whose cone is a limit cone and whose cocone is a colimit cocone. We print the definition of BinaryBicone below for reference.

structure CategoryTheory.Limits.BinaryBicone.{uC', uC} {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) : Type (max uC uC') number of parameters: 5 fields: CategoryTheory.Limits.BinaryBicone.pt : C CategoryTheory.Limits.BinaryBicone.fst : self.pt ⟢ P CategoryTheory.Limits.BinaryBicone.snd : self.pt ⟢ Q CategoryTheory.Limits.BinaryBicone.inl : P ⟢ self.pt CategoryTheory.Limits.BinaryBicone.inr : Q ⟢ self.pt CategoryTheory.Limits.BinaryBicone.inl_fst : self.fst ⊚ self.inl = πŸ™ P := by aesop CategoryTheory.Limits.BinaryBicone.inl_snd : self.snd ⊚ self.inl = 0 := by aesop CategoryTheory.Limits.BinaryBicone.inr_fst : self.fst ⊚ self.inr = 0 := by aesop CategoryTheory.Limits.BinaryBicone.inr_snd : self.snd ⊚ self.inr = πŸ™ Q := by aesop constructor: CategoryTheory.Limits.BinaryBicone.mk.{uC', uC} {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (pt : C) (fst : pt ⟢ P) (snd : pt ⟢ Q) (inl : P ⟢ pt) (inr : Q ⟢ pt) (inl_fst : fst ⊚ inl = πŸ™ P := by aesop) (inl_snd : snd ⊚ inl = 0 := by aesop) (inr_fst : fst ⊚ inr = 0 := by aesop) (inr_snd : snd ⊚ inr = πŸ™ Q := by aesop) : BinaryBicone P Q#print BinaryBicone 
structure CategoryTheory.Limits.BinaryBicone.{uC', uC} {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C]
  (P Q : C) : Type (max uC uC')
number of parameters: 5
fields:
  CategoryTheory.Limits.BinaryBicone.pt : C
  CategoryTheory.Limits.BinaryBicone.fst : self.pt ⟢ P
  CategoryTheory.Limits.BinaryBicone.snd : self.pt ⟢ Q
  CategoryTheory.Limits.BinaryBicone.inl : P ⟢ self.pt
  CategoryTheory.Limits.BinaryBicone.inr : Q ⟢ self.pt
  CategoryTheory.Limits.BinaryBicone.inl_fst : self.fst ⊚ self.inl = πŸ™ P := by
    aesop
  CategoryTheory.Limits.BinaryBicone.inl_snd : self.snd ⊚ self.inl = 0 := by
    aesop
  CategoryTheory.Limits.BinaryBicone.inr_fst : self.fst ⊚ self.inr = 0 := by
    aesop
  CategoryTheory.Limits.BinaryBicone.inr_snd : self.snd ⊚ self.inr = πŸ™ Q := by
    aesop
constructor:
  CategoryTheory.Limits.BinaryBicone.mk.{uC', uC} {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C}
    (pt : C) (fst : pt ⟢ P) (snd : pt ⟢ Q) (inl : P ⟢ pt) (inr : Q ⟢ pt) (inl_fst : fst ⊚ inl = πŸ™ P := by aesop)
    (inl_snd : snd ⊚ inl = 0 := by aesop) (inr_fst : fst ⊚ inr = 0 := by aesop)
    (inr_snd : snd ⊚ inr = πŸ™ Q := by aesop) : BinaryBicone P Q

3. Sum of maps in a linear categoryπŸ”—

Exercise 1 (p. 280)

Using the [given] definitions of matrix multiplication and addition of maps, prove the following formula for matrix multiplication: \begin{bmatrix} f_{AX} & f_{AY} \\ f_{BX} & f_{BY} \end{bmatrix} \cdot \begin{bmatrix} g_{XU} & g_{XV} \\ g_{YU} & g_{YV} \end{bmatrix} = \begin{bmatrix} g_{XU} \circ f_{AX} + g_{YU} \circ f_{AY} & g_{XV} \circ f_{AX} + g_{YV} \circ f_{AY} \\ g_{XU} \circ f_{BX} + g_{YU} \circ f_{BY} & g_{XV} \circ f_{BX} + g_{YV} \circ f_{BY} \end{bmatrix}

Solution: Exercise 1

We start by defining the required 2Γ—2 matrix of morphisms in a linear category.

noncomputable def matrix2x2 {π’ž : Type u} [Category.{v, u} π’ž] [HasZeroMorphisms π’ž] [HasBinaryBiproducts π’ž] {C₁ Cβ‚‚ A B : π’ž} (f₁₁ : C₁ ⟢ A) (f₁₂ : C₁ ⟢ B) (f₂₁ : Cβ‚‚ ⟢ A) (fβ‚‚β‚‚ : Cβ‚‚ ⟢ B) : C₁ ⊞ Cβ‚‚ ⟢ A ⊞ B := biprod.lift (biprod.desc f₁₁ f₂₁) (biprod.desc f₁₂ fβ‚‚β‚‚)

In the solution below, we make our linear category Preadditive in order to have access to addition of morphisms. (We also use simp to discharge the last three of the four required equalities, since all four follow the same pattern.)

example {π’ž : Type u} [Category.{v, u} π’ž] [Preadditive π’ž] [HasBinaryBiproducts π’ž] {A B X Y U V : π’ž} (fAX : A ⟢ X) (fAY : A ⟢ Y) (fBX : B ⟢ X) (fBY : B ⟢ Y) (gXU : X ⟢ U) (gXV : X ⟢ V) (gYU : Y ⟢ U) (gYV : Y ⟢ V) : matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY = matrix2x2 ((gXU ⊚ fAX) + (gYU ⊚ fAY)) ((gXV ⊚ fAX) + (gYV ⊚ fAY)) ((gXU ⊚ fBX) + (gYU ⊚ fBY)) ((gXV ⊚ fBX) + (gYV ⊚ fBY)) := π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY = matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ biprod.fst ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY = biprod.fst ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ biprod.snd ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY = biprod.snd ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ biprod.fst ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY = biprod.fst ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ biprod.snd ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY = biprod.snd ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.snd ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY) ⊚ biprod.inl = (biprod.snd ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)) ⊚ biprod.inlπ’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.snd ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY) ⊚ biprod.inr = (biprod.snd ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)) ⊚ biprod.inr π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.fst ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY) ⊚ biprod.inl = (biprod.fst ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)) ⊚ biprod.inlπ’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.fst ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY) ⊚ biprod.inr = (biprod.fst ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)) ⊚ biprod.inrπ’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.snd ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY) ⊚ biprod.inl = (biprod.snd ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)) ⊚ biprod.inlπ’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.snd ⊚ matrix2x2 gXU gXV gYU gYV ⊚ matrix2x2 fAX fAY fBX fBY) ⊚ biprod.inr = (biprod.snd ⊚ matrix2x2 (gXU ⊚ fAX + gYU ⊚ fAY) (gXV ⊚ fAX + gYV ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) (gXV ⊚ fBX + gYV ⊚ fBY)) ⊚ biprod.inr π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.snd ⊚ biprod.lift (biprod.desc gXU gYU) (biprod.desc gXV gYV) ⊚ biprod.lift (biprod.desc fAX fBX) (biprod.desc fAY fBY)) ⊚ biprod.inr = (biprod.snd ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inr π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.fst ⊚ biprod.lift (biprod.desc gXU gYU) (biprod.desc gXV gYV) ⊚ biprod.lift (biprod.desc fAX fBX) (biprod.desc fAY fBY)) ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ ((biprod.fst ⊚ biprod.lift (biprod.desc gXU gYU) (biprod.desc gXV gYV)) ⊚ biprod.lift (biprod.desc fAX fBX) (biprod.desc fAY fBY)) ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.desc gXU gYU ⊚ biprod.lift (biprod.desc fAX fBX) (biprod.desc fAY fBY)) ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (gXU ⊚ biprod.desc fAX fBX + gYU ⊚ biprod.desc fAY fBY) ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (gXU ⊚ biprod.desc fAX fBX) ⊚ biprod.inl + (gYU ⊚ biprod.desc fAY fBY) ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ gXU ⊚ biprod.desc fAX fBX ⊚ biprod.inl + (gYU ⊚ biprod.desc fAY fBY) ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ gXU ⊚ fAX + (gYU ⊚ biprod.desc fAY fBY) ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ gXU ⊚ fAX + gYU ⊚ biprod.desc fAY fBY ⊚ biprod.inl = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ gXU ⊚ fAX + gYU ⊚ fAY = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ gXU ⊚ fAX + gYU ⊚ fAY = biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY) ⊚ biprod.inl All goals completed! πŸ™ π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.fst ⊚ biprod.lift (biprod.desc gXU gYU) (biprod.desc gXV gYV) ⊚ biprod.lift (biprod.desc fAX fBX) (biprod.desc fAY fBY)) ⊚ biprod.inr = (biprod.fst ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inr All goals completed! πŸ™ π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.snd ⊚ biprod.lift (biprod.desc gXU gYU) (biprod.desc gXV gYV) ⊚ biprod.lift (biprod.desc fAX fBX) (biprod.desc fAY fBY)) ⊚ biprod.inl = (biprod.snd ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inl All goals completed! πŸ™ π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:Preadditive π’žinst✝:HasBinaryBiproducts π’žA:π’žB:π’žX:π’žY:π’žU:π’žV:π’žfAX:A ⟢ XfAY:A ⟢ YfBX:B ⟢ XfBY:B ⟢ YgXU:X ⟢ UgXV:X ⟢ VgYU:Y ⟢ UgYV:Y ⟢ V⊒ (biprod.snd ⊚ biprod.lift (biprod.desc gXU gYU) (biprod.desc gXV gYV) ⊚ biprod.lift (biprod.desc fAX fBX) (biprod.desc fAY fBY)) ⊚ biprod.inr = (biprod.snd ⊚ biprod.lift (biprod.desc (gXU ⊚ fAX + gYU ⊚ fAY) (gXU ⊚ fBX + gYU ⊚ fBY)) (biprod.desc (gXV ⊚ fAX + gYV ⊚ fAY) (gXV ⊚ fBX + gYV ⊚ fBY))) ⊚ biprod.inr All goals completed! πŸ™
Exercise 2 (p. 280)

Prove that a category with initial and terminal objects has zero maps if and only if an initial object is isomorphic to a terminal object.

Solution: Exercise 2

The equivalence follows from the universal properties of initial and terminal objects.

example {π’ž : Type u} [Category.{v, u} π’ž] [HasInitial π’ž] [HasTerminal π’ž] : Nonempty (HasZeroMorphisms π’ž) ↔ Nonempty (βŠ₯_ π’ž β‰… ⊀_ π’ž) := π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žβŠ’ Nonempty (HasZeroMorphisms π’ž) ↔ Nonempty (βŠ₯_ π’ž β‰… ⊀_ π’ž) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žβŠ’ Nonempty (HasZeroMorphisms π’ž) β†’ Nonempty (βŠ₯_ π’ž β‰… ⊀_ π’ž)π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žβŠ’ Nonempty (βŠ₯_ π’ž β‰… ⊀_ π’ž) β†’ Nonempty (HasZeroMorphisms π’ž) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žβŠ’ Nonempty (HasZeroMorphisms π’ž) β†’ Nonempty (βŠ₯_ π’ž β‰… ⊀_ π’ž) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhZero:HasZeroMorphisms π’žβŠ’ Nonempty (βŠ₯_ π’ž β‰… ⊀_ π’ž) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhZero:HasZeroMorphisms π’žβŠ’ βŠ₯_ π’ž β‰… ⊀_ π’ž All goals completed! πŸ™ π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žβŠ’ Nonempty (βŠ₯_ π’ž β‰… ⊀_ π’ž) β†’ Nonempty (HasZeroMorphisms π’ž) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žβŠ’ Nonempty (HasZeroMorphisms π’ž) π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žβŠ’ HasZeroMorphisms π’ž exact { zero X Y := ⟨initial.to Y ⊚ hIso.inv ⊚ terminal.from X⟩ comp_zero := π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žβŠ’ βˆ€ {X Y : π’ž} (f : X ⟢ Y) (Z : π’ž), 0 ⊚ f = 0 π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žX:π’žY:π’žf:X ⟢ YZ:π’žβŠ’ 0 ⊚ f = 0 π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žX:π’žY:π’žf:X ⟢ YZ:π’žβŠ’ (initial.to Z ⊚ hIso.inv ⊚ terminal.from Y) ⊚ f = initial.to Z ⊚ hIso.inv ⊚ terminal.from X repeat π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žX:π’žY:π’žf:X ⟢ YZ:π’žβŠ’ initial.to Z ⊚ hIso.inv ⊚ terminal.from Y ⊚ f = initial.to Z ⊚ hIso.inv ⊚ terminal.from X All goals completed! πŸ™ zero_comp := π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žβŠ’ βˆ€ (X : π’ž) {Y Z : π’ž} (f : Y ⟢ Z), f ⊚ 0 = 0 π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žX:π’žY:π’žZ:π’žf:Y ⟢ Z⊒ f ⊚ 0 = 0 π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žX:π’žY:π’žZ:π’žf:Y ⟢ Z⊒ f ⊚ initial.to Y ⊚ hIso.inv ⊚ terminal.from X = initial.to Z ⊚ hIso.inv ⊚ terminal.from X π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasInitial π’žinst✝:HasTerminal π’žhIso:βŠ₯_ π’ž β‰… ⊀_ π’žX:π’žY:π’žZ:π’žf:Y ⟢ Z⊒ (f ⊚ initial.to Y) ⊚ hIso.inv ⊚ terminal.from X = initial.to Z ⊚ hIso.inv ⊚ terminal.from X All goals completed! πŸ™ }