English
The canonical functor from A × B to Comma L R maps (a,b) to the comma object with left arrow a and right arrow b and unique morphism between them.
Русский
Канонический функтор из A × B в Comma L R отправляет пару (a,b) в объект комма с левым компонентом a и правым компонентом b и единственным морфизмом между ними.
LaTeX
$$$\mathrm{fromProd} : A \times B \to \mathrm{Comma}(L,R),\quad \mathrm{fromProd}(a,b) = (a,b,\ast)$.$$
Lean4
/-- The canonical functor from the product of two categories to the comma category of their
respective functors into `Discrete PUnit`. -/
@[simps]
def fromProd (L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : A × B ⥤ Comma L R
where
obj
X :=
{ left := X.1
right := X.2
hom := Discrete.eqToHom rfl }
map {X} {Y}
f :=
{ left := f.1
right := f.2 }
