Products in precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-13.
Last modified on 2024-04-11.

module category-theory.products-in-precategories where
Imports 
open import category-theory.precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.uniqueness-quantification
open import foundation.universe-levels

Idea

A product of two objects x and x in a category C consists of:

  • an object p
  • morphisms l : hom p x and r : hom p y such that for every object z and morphisms f : hom z x and g : hom z y there exists a unique morphism h : hom z p such that
  • l ∘ h = f
  • r ∘ h = g.

We say that C has all binary products if there is a choice of a product for each pair of objects in C.

Definition

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  where

  is-product-obj-Precategory :
    (x y p : obj-Precategory C) →
    hom-Precategory C p x →
    hom-Precategory C p y →
    UU (l1 ⊔ l2)
  is-product-obj-Precategory x y p l r =
    (z : obj-Precategory C)
    (f : hom-Precategory C z x) →
    (g : hom-Precategory C z y) →
    ( uniquely-exists-structure
      ( hom-Precategory C z p)
      ( λ h →
        ( comp-hom-Precategory C l h ＝ f) ×
        ( comp-hom-Precategory C r h ＝ g)))

  product-obj-Precategory : obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
  product-obj-Precategory x y =
    Σ (obj-Precategory C) λ p →
    Σ (hom-Precategory C p x) λ l →
    Σ (hom-Precategory C p y) λ r →
      is-product-obj-Precategory x y p l r

  has-all-binary-products-Precategory : UU (l1 ⊔ l2)
  has-all-binary-products-Precategory =
    (x y : obj-Precategory C) → product-obj-Precategory x y

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  (t : has-all-binary-products-Precategory C)
  where

  object-product-obj-Precategory :
    obj-Precategory C → obj-Precategory C → obj-Precategory C
  object-product-obj-Precategory x y = pr1 (t x y)

  pr1-product-obj-Precategory :
    (x y : obj-Precategory C) →
    hom-Precategory C (object-product-obj-Precategory x y) x
  pr1-product-obj-Precategory x y = pr1 (pr2 (t x y))

  pr2-product-obj-Precategory :
    (x y : obj-Precategory C) →
    hom-Precategory C (object-product-obj-Precategory x y) y
  pr2-product-obj-Precategory x y = pr1 (pr2 (pr2 (t x y)))

  module _
    (x y z : obj-Precategory C)
    (f : hom-Precategory C z x)
    (g : hom-Precategory C z y)
    where

    morphism-into-product-obj-Precategory :
      hom-Precategory C z (object-product-obj-Precategory x y)
    morphism-into-product-obj-Precategory =
      pr1 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g))

    morphism-into-product-obj-Precategory-comm-pr1 :
      comp-hom-Precategory C
        ( pr1-product-obj-Precategory x y)
        ( morphism-into-product-obj-Precategory) ＝ f
    morphism-into-product-obj-Precategory-comm-pr1 =
      pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g)))

    morphism-into-product-obj-Precategory-comm-pr2 :
      comp-hom-Precategory C
        ( pr2-product-obj-Precategory x y)
        ( morphism-into-product-obj-Precategory) ＝ g
    morphism-into-product-obj-Precategory-comm-pr2 =
      pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g)))

    is-unique-morphism-into-product-obj-Precategory :
      (h : hom-Precategory C z (object-product-obj-Precategory x y)) →
      comp-hom-Precategory C (pr1-product-obj-Precategory x y) h ＝ f →
      comp-hom-Precategory C (pr2-product-obj-Precategory x y) h ＝ g →
      morphism-into-product-obj-Precategory ＝ h
    is-unique-morphism-into-product-obj-Precategory h comm1 comm2 =
      ap pr1 ((pr2 (pr2 (pr2 (pr2 (t x y))) z f g)) (h , (comm1 , comm2)))

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  (x y p : obj-Precategory C)
  (l : hom-Precategory C p x)
  (r : hom-Precategory C p y)
  where

  is-prop-is-product-obj-Precategory :
    is-prop (is-product-obj-Precategory C x y p l r)
  is-prop-is-product-obj-Precategory =
    is-prop-iterated-Π 3 (λ z f g → is-property-is-contr)

  is-product-prop-Precategory : Prop (l1 ⊔ l2)
  pr1 is-product-prop-Precategory = is-product-obj-Precategory C x y p l r
  pr2 is-product-prop-Precategory = is-prop-is-product-obj-Precategory

Properties

Products of morphisms

If C has all binary products then for any pair of morphisms f : hom x₁ y₁ and g : hom x₂ y₂ we can construct a morphism f × g : hom (x₁ × x₂) (y₁ × y₂).

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  (t : has-all-binary-products-Precategory C)
  {x₁ x₂ y₁ y₂ : obj-Precategory C}
  (f : hom-Precategory C x₁ y₁)
  (g : hom-Precategory C x₂ y₂)
  where

  map-product-obj-Precategory :
    hom-Precategory C
      (object-product-obj-Precategory C t x₁ x₂)
      (object-product-obj-Precategory C t y₁ y₂)
  map-product-obj-Precategory =
    morphism-into-product-obj-Precategory C t _ _ _
      (comp-hom-Precategory C f (pr1-product-obj-Precategory C t x₁ x₂))
      (comp-hom-Precategory C g (pr2-product-obj-Precategory C t x₁ x₂))

Recent changes