English
The discrete category on a product J × K is equivalent to the product of the discrete categories Discrete J and Discrete K.
Русский
Дискретная категория над произведением J × K эквивалентна деконструированной продукции дискретных категорий Discrete J и Discrete K.
LaTeX
$$$\\mathrm{Discrete}(J \\times K) \\simeq \\mathrm{Discrete}(J) \\times \\mathrm{Discrete}(K)$$$
Lean4
/-- The discrete category on a product is equivalent to the product of the
discrete categories. -/
@[simps!]
def productEquiv {J K : Type*} : Discrete (J × K) ≌ Discrete J × Discrete K
where
functor := Discrete.functor <| fun ⟨j, k⟩ ↦ ⟨.mk j, .mk k⟩
inverse :=
{ obj := fun ⟨x, y⟩ ↦ .mk (⟨x.as, y.as⟩)
map := fun ⟨f₁, f₂⟩ ↦ eqToHom (by discrete_cases; dsimp; rw [f₁, f₂]) }
unitIso := NatIso.ofComponents (fun _ ↦ Iso.refl _)
counitIso := NatIso.ofComponents (fun _ ↦ Iso.refl _)
