English
The discrete category on a sum J ⊕ K is equivalent to the sum of the discrete categories Discrete J and Discrete K.
Русский
Дискретная категория над суммой J ⊕ K эквивалентна сумме дискретных категорий Discrete J и Discrete K.
LaTeX
$$$\\mathrm{Discrete}(J \\oplus K) \\simeq \\mathrm{Discrete}(J) \\oplus \\mathrm{Discrete}(K)$$$
Lean4
/-- The discrete category on a sum is equivalent to the sum of the
discrete categories. -/
@[simps!]
def sumEquiv {J K : Type*} : Discrete (J ⊕ K) ≌ Discrete J ⊕ Discrete K
where
functor :=
Discrete.functor <| fun t ↦
match t with
| .inl j => Sum.inl (Discrete.mk j)
| .inr k => Sum.inr (Discrete.mk k)
inverse :=
(Discrete.functor <| fun t ↦ Discrete.mk (Sum.inl t)).sum' (Discrete.functor <| fun t ↦ Discrete.mk (Sum.inr t))
unitIso :=
NatIso.ofComponents
(fun ⟨x⟩ ↦
match x with
| .inl x => Iso.refl _
| .inr x => Iso.refl _)
counitIso := Functor.sumIsoExt (Discrete.natIso <| fun _ ↦ Iso.refl _) (Discrete.natIso <| fun _ ↦ Iso.refl _)
