unitor for product of categories?

Stream: new members

[Shanghe Chen]

Hi I saw there is no unitors for the product of two categories? An adhoc implementation seems not hard, yet Associator.lean#L56 still marks it as TODO, any reason for this?

import Mathlib.CategoryTheory.Products.Basic
import Mathlib.CategoryTheory.DiscreteCategory

/-!
The unitors for product of categories
see also Mathlib/CategoryTheory/Products/Associator.lean
-/

universe v u

open CategoryTheory

namespace CategoryTheory.prod

variable (C : Type u) [Category.{v} C]

@[simps]
def leftUnitor : Discrete PUnit.{1} × C ⥤ C where
  obj X := X.2
  map := @fun _ _ f => f.2

@[simps]
def rightUnitor : C × Discrete PUnit.{1} ⥤ C where
  obj X := X.1
  map := @fun _ _ f => f.1

@[simps]
def leftUnitor_inverse : C ⥤ Discrete PUnit.{1} × C where
  obj X := ⟨⟨PUnit.unit⟩, X⟩
  map := @fun _ _ f =>  ⟨𝟙 _, f⟩

@[simps]
def rightUnitor_inverse : C ⥤ C × Discrete PUnit.{1} where
  obj X := ⟨X, ⟨PUnit.unit⟩⟩
  map := @fun _ _ f =>  ⟨f, 𝟙 _⟩

def leftUnity : Discrete PUnit.{1} × C ≌ C :=
  Equivalence.mk (leftUnitor C) (leftUnitor_inverse C)
    (NatIso.ofComponents fun X => eqToIso (by simp))
    (NatIso.ofComponents fun X => eqToIso (by simp))

def rightUnity : C × Discrete PUnit.{1} ≌ C :=
  Equivalence.mk (rightUnitor C) (rightUnitor_inverse C)
    (NatIso.ofComponents fun X => eqToIso (by simp))
    (NatIso.ofComponents fun X => eqToIso (by simp))

end CategoryTheory.prod

[Kevin Buzzard]

TODO might just mean "perfectly doable but nobody did it yet". You can find out by making a PR. Do you have push access to non master branches?

[Shanghe Chen]

Thank you very much Kevin. I have no push access yet. Yeah let me ask for it in the related thread

[Shanghe Chen]

#13663 PR created :tada: