English
The inverse composed with the i-th sigma injection equals the i-th projection.
Русский
Обратное композиции с i-й инъекцией в копродукте эквивалентно i-й проекции.
LaTeX
$$$(\mathrm{opProductIsoCoproduct Z).inv} \circ (\Sigma.ι Z i)^{\mathrm{op}} = \Pi.π (\cdot) i$$$
Lean4
/-- If a `Fan` is limit, then its opposite is colimit. -/
-- noncomputability is just for performance (compilation takes a while)
noncomputable def op {f : Fan Z} (hf : IsLimit f) : IsColimit f.op :=
by
let e : Discrete.functor (Opposite.op <| Z ·) ≅ (Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op :=
Discrete.natIso (fun _ ↦ Iso.refl _)
refine
IsColimit.ofIsoColimit
((IsColimit.precomposeHomEquiv e _).2 (IsColimit.whiskerEquivalence hf.op (Discrete.opposite α).symm))
(Cocones.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))
dsimp
erw [Category.id_comp, Category.comp_id]
rfl
