reflective_products — Mathlib

English

If the ambient category C has finite products and i: D ⥤ C is reflective, then D also has finite products.

Русский

Если в каталоге C существуют конечные произведения и i: D ⥤ C является отражающим, то и D имеет конечные произведения.

LaTeX

$$$ \\text{HasFiniteProducts}(C) \\Rightarrow (\\text{Reflective } i) \\Rightarrow \\text{HasFiniteProducts}(D) $$$

Lean4

theorem reflective_products [Limits.HasFiniteProducts C] [Reflective i] : Limits.HasFiniteProducts D :=
  ⟨fun _ => hasLimitsOfShape_of_reflective i⟩

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