CategoryTheory.Limits.IsBinaryProduct

Stream: Is there code for X?

[William Sørensen]

HI is there code like this in mathlib? Ive not been able to find it and its quite surprising

import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

namespace CategoryTheory.Limits

universe u

variable {𝓒 : Type u} [Category 𝓒] {X Y P : 𝓒} (fst : P ⟶ X) (snd : P ⟶ Y)

def IsBinaryProduct :=
  Limits.IsLimit (Limits.BinaryFan.mk fst snd)

def IsBinaryProduct.ofUniqueHom {fst snd}
    (lift : {T : 𝓒} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ P))
    (hl₁ : ∀ {T} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ fst = f)
    (hl₂ : ∀ {T} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ snd = g)
    (uniq : ∀ {T} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ P), m ≫ fst = f → m ≫ snd = g → m = lift f g)
    : IsBinaryProduct fst snd :=
  Limits.BinaryFan.IsLimit.mk _ lift hl₁ hl₂ uniq

theorem IsBinaryProduct.hasBinaryProduct (h : IsBinaryProduct fst snd) : HasBinaryProduct X Y :=
  ⟨⟨{ cone := BinaryFan.mk fst snd, isLimit := h }⟩⟩

noncomputable def productIsBinaryProduct [HasBinaryProduct X Y]
    : IsBinaryProduct (prod.fst : X ⨯ Y ⟶ X) prod.snd :=
  IsBinaryProduct.ofUniqueHom
    prod.lift
    prod.lift_fst
    prod.lift_snd
    (fun {T} f g m hf hg => by
      dsimp
      ext
      · rw [hf, prod.lift_fst f g]
      · rw [hg, prod.lift_snd f g])

end CategoryTheory.Limits

[Joël Riou]

Your definition IsBinaryProduct.ofUniqueHom essentially duplicates BinaryFan.IsLimit.mk which you are using. The last one productIsBinaryProduct is prodIsProd (which I found by doing apply?).

[William Sørensen]

Hmm fair enough. I just really like the is-/hasterminal interface for code discovery but this might just be because I’m trying to formalise my course as I learn it