module Cat.Diagram.Product {o h} (C : Precategory o h) where
Productsπ
The product of two objects and , if it exists, is the smallest object equipped with βprojectionβ maps and . This situation can be visualised by putting the data of a product into a commutative diagram, as the one below: To express that is the smallest object with projections to and , we ask that any other object with projections through and factors uniquely through :
In the sense that (univalent) categories generalise posets, the product of and β if it exists β generalises the binary meet . Since products are unique when they exist, we may safely denote any product of and by .
For a diagram to be a product diagram, it must be able to cough up an arrow given the data of another span , which must not only fit into the diagram above but be unique among the arrows that do so.
This factoring is called the pairing of the arrows and , since in the special case where is the terminal object (hence the two arrows are global elements of resp. ), the pairing is a global element of the product .
record is-product {A B P} (Οβ : Hom P A) (Οβ : Hom P B) : Type (o β h) where field β¨_,_β© : β {Q} (p1 : Hom Q A) (p2 : Hom Q B) β Hom Q P Οββfactor : β {Q} {p1 : Hom Q _} {p2} β Οβ β β¨ p1 , p2 β© β‘ p1 Οββfactor : β {Q} {p1 : Hom Q _} {p2} β Οβ β β¨ p1 , p2 β© β‘ p2 unique : β {Q} {p1 : Hom Q A} {p2} β (other : Hom Q P) β Οβ β other β‘ p1 β Οβ β other β‘ p2 β other β‘ β¨ p1 , p2 β© uniqueβ : β {Q} {pr1 : Hom Q A} {pr2} β β {o1} (p1 : Οβ β o1 β‘ pr1) (q1 : Οβ β o1 β‘ pr2) β β {o2} (p2 : Οβ β o2 β‘ pr1) (q2 : Οβ β o2 β‘ pr2) β o1 β‘ o2 uniqueβ p1 q1 p2 q2 = unique _ p1 q1 β sym (unique _ p2 q2) β¨β©β : β {Q R} {p1 : Hom Q A} {p2 : Hom Q B} (f : Hom R Q) β β¨ p1 , p2 β© β f β‘ β¨ p1 β f , p2 β f β© β¨β©β f = unique _ (pulll Οββfactor) (pulll Οββfactor) β¨β©-Ξ· : β¨ Οβ , Οβ β© β‘ id β¨β©-Ξ· = sym $ unique id (idr _) (idr _)
A product of and is an explicit choice of product diagram:
record Product (A B : Ob) : Type (o β h) where no-eta-equality field apex : Ob Οβ : Hom apex A Οβ : Hom apex B has-is-product : is-product Οβ Οβ open is-product has-is-product public
Uniquenessπ
Products, when they exist, are unique. Itβs easiest to see this with a diagrammatic argument: If we have product diagrams and , we can fit them into a βcommutative diamondβ like the one below:
Since both and are products, we know that the dashed arrows in the diagram below exist, so the overall diagram commutes: hence we have an isomorphism .
We construct the map as the pairing of the projections from , and symmetrically for .
Γ-Unique : (p1 p2 : Product A B) β apex p1 β apex p2 Γ-Unique p1 p2 = make-iso p1βp2 p2βp1 p1βp2βp1 p2βp1βp2 where module p1 = Product p1 module p2 = Product p2 p1βp2 : Hom (apex p1) (apex p2) p1βp2 = p2.β¨ p1.Οβ , p1.Οβ β©p2. p2βp1 : Hom (apex p2) (apex p1) p2βp1 = p1.β¨ p2.Οβ , p2.Οβ β©p1.
These are unique because they are maps into products which commute with the projections.
p1βp2βp1 : p1βp2 β p2βp1 β‘ id p1βp2βp1 = p2.uniqueβ (assoc _ _ _ Β·Β· ap (_β _) p2.Οββfactor Β·Β· p1.Οββfactor) (assoc _ _ _ Β·Β· ap (_β _) p2.Οββfactor Β·Β· p1.Οββfactor) (idr _) (idr _) p2βp1βp2 : p2βp1 β p1βp2 β‘ id p2βp1βp2 = p1.uniqueβ (assoc _ _ _ Β·Β· ap (_β _) p1.Οββfactor Β·Β· p2.Οββfactor) (assoc _ _ _ Β·Β· ap (_β _) p1.Οββfactor Β·Β· p2.Οββfactor) (idr _) (idr _) is-product-iso : β {A Aβ² B Bβ² P} {Οβ : Hom P A} {Οβ : Hom P B} {f : Hom A Aβ²} {g : Hom B Bβ²} β is-invertible f β is-invertible g β is-product Οβ Οβ β is-product (f β Οβ) (g β Οβ) is-product-iso f-iso g-iso prod = prodβ² where module fi = is-invertible f-iso module gi = is-invertible g-iso open is-product prodβ² : is-product _ _ prodβ² .β¨_,_β© qa qb = prod .β¨_,_β© (fi.inv β qa) (gi.inv β qb) prodβ² .Οββfactor = pullr (prod .Οββfactor) β cancell fi.invl prodβ² .Οββfactor = pullr (prod .Οββfactor) β cancell gi.invl prodβ² .unique other p q = prod .unique other (sym (ap (_ β_) (sym p) β pulll (cancell fi.invr))) (sym (ap (_ β_) (sym q) β pulll (cancell gi.invr)))
Categories with all binary productsπ
Categories with all binary products are quite common, so we define a module for working with them.
has-products : Type _ has-products = β a b β Product a b module Binary-products (all-products : has-products) where module product {a} {b} = Product (all-products a b) open product renaming (unique to β¨β©-unique; Οββfactor to Οβββ¨β©; Οββfactor to Οβββ¨β©) public open Functor infixr 7 _ββ_ infix 50 _ββ_
We start by defining a βglobalβ product-assigning operation.
_ββ_ : Ob β Ob β Ob a ββ b = product.apex {a} {b}
This operation extends to a bifunctor .
_ββ_ : β {a b x y} β Hom a x β Hom b y β Hom (a ββ b) (x ββ y) f ββ g = β¨ f β Οβ , g β Οβ β© Γ-functor : Functor (C ΓαΆ C) C Γ-functor .Fβ (a , b) = a ββ b Γ-functor .Fβ (f , g) = f ββ g Γ-functor .F-id = sym $ β¨β©-unique id id-comm id-comm Γ-functor .F-β (f , g) (h , i) = sym $ β¨β©-unique (f ββ g β h ββ i) (pulll Οβββ¨β© β extendr Οβββ¨β©) (pulll Οβββ¨β© β extendr Οβββ¨β©)
We also define a handful of common morphisms.
Ξ΄ : Hom a (a ββ a) Ξ΄ = β¨ id , id β© swap : Hom (a ββ b) (b ββ a) swap = β¨ Οβ , Οβ β©
swap-is-iso : β {a b} β is-invertible (swap {a} {b}) swap-is-iso = make-invertible swap (uniqueβ (pulll Οβββ¨β© β Οβββ¨β©) ((pulll Οβββ¨β© β Οβββ¨β©)) (idr _) (idr _)) (uniqueβ (pulll Οβββ¨β© β Οβββ¨β©) ((pulll Οβββ¨β© β Οβββ¨β©)) (idr _) (idr _)) by-Οβ : β {f f' : Hom a b} {g g' : Hom a c} β β¨ f , g β© β‘ β¨ f' , g' β© β f β‘ f' by-Οβ p = sym Οβββ¨β© β ap (Οβ β_) p β Οβββ¨β© extend-Οβ : β {f : Hom a b} {g : Hom a c} {h} β β¨ f , g β© β‘ h β f β‘ Οβ β h extend-Οβ p = sym Οβββ¨β© β ap (Οβ β_) p by-Οβ : β {f f' : Hom a b} {g g' : Hom a c} β β¨ f , g β© β‘ β¨ f' , g' β© β g β‘ g' by-Οβ p = sym Οβββ¨β© β ap (Οβ β_) p β Οβββ¨β© extend-Οβ : β {f : Hom a b} {g : Hom a c} {h} β β¨ f , g β© β‘ h β g β‘ Οβ β h extend-Οβ p = sym Οβββ¨β© β ap (Οβ β_) p Οβ-inv : β {f : Hom (a ββ b) c} {g : Hom (a ββ b) d} β (β¨β©-inv : is-invertible β¨ f , g β©) β f β is-invertible.inv β¨β©-inv β‘ Οβ Οβ-inv {f = f} {g = g} β¨β©-inv = pushl (sym Οβββ¨β©) β elimr (is-invertible.invl β¨β©-inv) Οβ-inv : β {f : Hom (a ββ b) c} {g : Hom (a ββ b) d} β (β¨β©-inv : is-invertible β¨ f , g β©) β g β is-invertible.inv β¨β©-inv β‘ Οβ Οβ-inv {f = f} {g = g} β¨β©-inv = pushl (sym Οβββ¨β©) β elimr (is-invertible.invl β¨β©-inv)
Representability of productsπ
The collection of maps into a product is equivalent to the collection of pairs of maps into and . The forward direction of the equivalence is given by postcomposition of the projections, and the reverse direction by the universal property of products.
product-repr : β {a b} β (prod : Product a b) β (x : Ob) β Hom x (Product.apex prod) β (Hom x a Γ Hom x b) product-repr prod x = IsoβEquiv Ξ» where .fst f β Οβ β f , Οβ β f .snd .is-iso.inv (f , g) β β¨ f , g β© .snd .is-iso.rinv (f , g) β Οββfactor ,β Οββfactor .snd .is-iso.linv f β sym (β¨β©β f) β eliml β¨β©-Ξ· where open Product prod