English
If F reflects isomorphisms, has finite coproducts in C, and preserves finite coproducts, then F reflects finite coproducts.
Русский
Если F отражает изоморфизмы, есть конечные копроизведения в C и F сохраняет конечные копроизведения, тогда F отражает конечные копроизведения.
LaTeX
$$$\mathrm{ReflectsIsomorphisms}(F) \land \mathrm{HasFiniteCoproducts}(C) \land \mathrm{PreservesFiniteCoproducts}(F) \Rightarrow \mathrm{ReflectsFiniteCoproducts}(F)$$$
Lean4
instance (priority := 100) (F : C ⥤ D) (J : Type u) [Finite J] [PreservesFiniteCoproducts F] :
PreservesColimitsOfShape (Discrete J) F :=
let ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
have := PreservesFiniteCoproducts.preserves (F := F) n
preservesColimitsOfShape_of_equiv (Discrete.equivalence e.symm) F
