of_exponentialIdeal — Mathlib

English

If i is an exponential ideal, then the reflector preserves finite products.

Русский

Если i является экспоненциальным идеалом, то рефлектор сохраняет конечные произведения.

LaTeX

$$$ \\mathrm{PreservesFiniteProducts}(\\mathrm{reflector}\, i) $$$

Lean4

/-- If a reflective subcategory is an exponential ideal, then the reflector preserves finite products.
-/
theorem of_exponentialIdeal : PreservesFiniteProducts (reflector i) :=
  have := preservesBinaryProducts_of_exponentialIdeal i
  have : PreservesLimitsOfShape _ (reflector i) := leftAdjoint_preservesTerminal_of_reflective.{0} i
  .of_preserves_binary_and_terminal _

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