English
The backward direction for the equivalence: from a functor F: A ⥤ B × C to a pair of functors (A ⥤ B) × (A ⥤ C) given by F ↦ ⟨F ∘ fst, F ∘ snd⟩ with morphisms mapped by whiskerRight.
Русский
Обратное направление эквивалентности: из функторa F: A ⥤ B × C в пару функторов (A ⥤ B) × (A ⥤ C) задается F ↦ ⟨F ∘ fst, F ∘ snd⟩, а отображения моров через whiskerRight.
LaTeX
$$$\\mathrm{functorProdToProdFunctor}: (A \\to B \\times C) \\to (A \\to B) \\times (A \\to C)$ with $\\mathrm{obj}F = \\langle F \\circ \\mathrm{fst}, F \\circ \\mathrm{snd} \\rangle$ and $\\mathrm{map}\\;\\alpha = \\langle \\mathrm{whiskerRight}\\;\\alpha\\;\\mathrm{fst}, \\mathrm{whiskerRight}\\;\\alpha\\;\\mathrm{snd} \\rangle$.$$
Lean4
/-- The backward direction for `functorProdFunctorEquiv` -/
@[simps]
def functorProdToProdFunctor : (A ⥤ B × C) ⥤ (A ⥤ B) × (A ⥤ C)
where
obj F := ⟨F ⋙ CategoryTheory.Prod.fst B C, F ⋙ CategoryTheory.Prod.snd B C⟩
map α := ⟨whiskerRight α _, whiskerRight α _⟩
