English
There is an equivalence between the Pi-category over Option J and the binary product of the none-indexed and some-indexed components.
Русский
Существует эквивалентность между Pi-категорией над Option J и бинарным произведением none-направленного и some-направленного компонентов.
LaTeX
$$$(\\forall i:Option J)\\; C'(i) \\simeq C'(\\mathrm{none}) \\times (\\forall j: J, C'(\\mathrm{some}(j)))$$$
Lean4
/-- A product of categories indexed by `Option J` identifies to a binary product. -/
@[simps]
def optionEquivalence (C' : Option J → Type u₁) [∀ i, Category.{v₁} (C' i)] :
(∀ i, C' i) ≌ C' none × (∀ (j : J), C' (some j))
where
functor := Functor.prod' (Pi.eval C' none) (Functor.pi' (fun i => (Pi.eval _ (some i))))
inverse :=
Functor.pi'
(fun i =>
match i with
| none => Prod.fst _ _
| some i => Prod.snd _ _ ⋙ (Pi.eval _ i))
unitIso :=
NatIso.pi'
(fun i =>
match i with
| none => Iso.refl _
| some _ => Iso.refl _)
counitIso := by exact Iso.refl _
