Unique morphism between producs

Stream: new members

[Yakov Pechersky]

I am trying to learn the category theory library in mathlib, and am having difficulty understanding how to tackle the following exercise using mathlib. I have a proof using my own home-brewed category definitions.
image.png

lemma AProd.lift_square_aux {G H : C} (φ : G ⟶ H) :
    Nonempty (Unique ({fg : G ×_C G ⟶ H ×_C H // fg ≫ fstHom = fstHom ≫ φ ∧ fg ≫ sndHom = sndHom ≫ φ})) := by
  refine' ⟨⟨lift (fstHom ≫ φ) (sndHom ≫ φ), lift_comp_fst _ _, lift_comp_snd _ _⟩, _⟩
  intro ⟨h, hl, hr⟩
  exact Subtype.ext (lift_unique h hl hr)

[Yakov Pechersky]

The full code to make my proof work is here:

Full code

import Mathlib.CategoryTheory.Types

set_option autoImplicit false

open CategoryTheory

def Final {C : Type _} [Category C] (F : C) :=
    ∀ A : C, Unique (A ⟶ F)

instance example39_down {C : Type _} [hC : Category C] (A B : C) :
    Category (Σ (Z : C), hC.Hom Z A × hC.Hom Z B) where
  Hom := λ ⟨Z₁, f₁⟩ ⟨Z₂, f₂⟩ => {σ : Z₁ ⟶ Z₂ // σ ≫ f₂.fst = f₁.fst ∧ σ ≫ f₂.snd = f₁.snd}
  id  _ := ⟨𝟙 _, hC.id_comp _, hC.id_comp _⟩
  comp := λ ⟨f, hf⟩ ⟨g, hg⟩ => ⟨f ≫ g,
    by rw [hC.assoc, hg.left, hf.left],
    by rw [hC.assoc, hg.right, hf.right]⟩
  id_comp := by
    intros
    exact Subtype.ext (hC.id_comp _)
  comp_id := by
    intros
    exact Subtype.ext (hC.comp_id _)
  assoc := by
    intros
    exact Subtype.ext (hC.assoc _ _ _)

class HasFiniteProducts (C : Type _) [hC : Category C] : Prop where
  hasFinal : ∀ A B : C, ∃ F : (Σ (Z : C), hC.Hom Z A × hC.Hom Z B), Nonempty (Final F)

variable {C : Type _} [hC : Category C] [hp : HasFiniteProducts C]

noncomputable
def AProd (A B : C) : C :=
  (hp.hasFinal A B).choose.fst

local notation A:80 " ×_C " B:80 => AProd A B

noncomputable
def AProd.fstHom {A B : C} : A ×_C B ⟶ A :=
  (hp.hasFinal A B).choose.snd.fst

noncomputable
def AProd.sndHom {A B : C} : A ×_C B ⟶ B :=
  (hp.hasFinal A B).choose.snd.snd

lemma AProd_Final_sigma (A B : C) :
    Nonempty (Final (⟨A ×_C B, AProd.fstHom, AProd.sndHom⟩
      : (Σ (Z : C), hC.Hom Z A × hC.Hom Z B))) :=
  (hp.hasFinal A B).choose_spec

lemma AProd.lift_aux {A B X : C} (f : X ⟶ A) (g : X ⟶ B) :
    Nonempty (Unique ({fg : X ⟶ A ×_C B // fg ≫ fstHom = f ∧ fg ≫ sndHom = g})) := by
  obtain ⟨F⟩ := AProd_Final_sigma A B
  let ⟨⟨Z⟩, hZ⟩ := F ⟨X, f, g⟩
  refine' ⟨⟨Z⟩, λ w => _⟩
  exact hZ w

noncomputable
def AProd.lift {A B X : C} (f : X ⟶ A) (g : X ⟶ B) : X ⟶ A ×_C B :=
  (Classical.choice (AProd.lift_aux f g)).default

@[simp]
lemma AProd.lift_comp_fst  {A B X : C} (f : X ⟶ A) (g : X ⟶ B) : lift f g ≫ fstHom = f :=
  (Classical.choice (AProd.lift_aux f g)).default.prop.left

@[simp]
lemma AProd.lift_comp_snd {A B X : C} (f : X ⟶ A) (g : X ⟶ B) : lift f g ≫ sndHom = g :=
  (Classical.choice (AProd.lift_aux f g)).default.prop.right

lemma AProd.lift_unique {A B X : C} {f : X ⟶ A} {g : X ⟶ B} (h : X ⟶ A ×_C B)
    (hf : h ≫ fstHom = f) (hg : h ≫ sndHom = g) : h = lift f g := by
  have := (Classical.choice (AProd.lift_aux f g)).uniq
  exact congr_arg Subtype.val (this ⟨h, hf, hg⟩)

lemma AProd.lift_square_aux {G H : C} (φ : G ⟶ H) :
    Nonempty (Unique ({fg : G ×_C G ⟶ H ×_C H // fg ≫ fstHom = fstHom ≫ φ ∧ fg ≫ sndHom = sndHom ≫ φ})) := by
  refine' ⟨⟨lift (fstHom ≫ φ) (sndHom ≫ φ), lift_comp_fst _ _, lift_comp_snd _ _⟩, _⟩
  intro ⟨h, hl, hr⟩
  exact Subtype.ext (lift_unique h hl hr)

[Yakov Pechersky]

Where can I find some documentation/guide to understand how to reinterpret my proof in mathlib-style category theory defns?

[Adam Topaz]

This is a really poorly stated exercise imo.

[Adam Topaz]

It’s not true that there is a unique morphism. What is true is that there is a unique morphism such that the composition with the projections satisfies some commutative square involving phi.

[Adam Topaz]

That last point is left very implicit in the notation $(\phi,\phi)$.

[Yakov Pechersky]

Agreed. That's why I constrained the uniqueness to the subtype of homs such that composition equals composition with with phi.

[Yakov Pechersky]

Initially, I was stuck for a while because I didn't have that constraint. But then I realized that if there was another hom psi between G and H, that would induce another hom between the products.

[Adam Topaz]

The main definition you want to look at from mathlib would be docs#CategoryTheory.prod and the relevant api

[Adam Topaz]

we have docs#CategoryTheory.Limits.prod.map