reflectsFiniteProducts_of_reflectsIsomorphisms

English

If F reflects isomorphisms and has finite limits, and preserves finite limits, then F reflects finite limits.

Русский

Если F отражает изоморфизмы и имеет конечные пределы, и сохраняет конечные пределы, то F отражает конечные пределы.

LaTeX

$$ReflectsFiniteLimits F from F reflects isomorphisms and HasFiniteLimits and PreservesFiniteLimits F$$

Lean4

instance reflectsFiniteProducts_of_reflectsIsomorphisms (F : C ⥤ D) [F.ReflectsIsomorphisms] [HasFiniteProducts C]
    [PreservesFiniteProducts F] : ReflectsFiniteProducts F where
  reflects _ := reflectsLimitsOfShape_of_reflectsIsomorphisms

Похожие утверждения