English
If F reflects finite coproducts and J is finite, then F reflects the colimits of shape Discrete J.
Русский
Если F отражает конечные копроизведения и J конечен, то F отражает колимиты формы Discrete J.
LaTeX
$$$\mathrm{ReflectsFiniteCoproducts}(F) \land \mathrm{Finite}(J) \Rightarrow \mathrm{ReflectsColimitsOfShape}(\mathrm{Discrete} J, F)$$$
Lean4
instance (priority := 100) (F : C ⥤ D) [ReflectsFiniteCoproducts F] (J : Type u) [Finite J] :
ReflectsColimitsOfShape (Discrete J) F :=
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
have := ReflectsFiniteCoproducts.reflects (F := F) n
reflectsColimitsOfShape_of_equiv (Discrete.equivalence e.symm) _
