equivProd — Mathlib

English

Let L: A → Discrete PUnit and R: B → Discrete PUnit be functors. Then the comma category Comma(L, R) is equivalent to the product category A × B.

Русский

Пусть L: A → Discrete PUnit и R: B → Discrete PUnit — функторы. Тогда категория запятой Comma(L, R) эквивалентна произведению категорий A × B.

LaTeX

$$$\\\\mathrm{Comma}(L,R) \\simeq A \\times B$$$

Lean4

/-- Taking the comma category of two functors into `Discrete PUnit` results in something
is equivalent to their product. -/
@[simps!]
def equivProd (L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : Comma L R ≌ A × B
    where
  functor := (fst L R).prod' (snd L R)
  inverse := fromProd L R
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Похожие утверждения