preservesBinaryProducts_of_exponentialIdeal

English

If an exponential ideal i is preserved by binary products, then i is such that the reflector preserves binary products (hence finite products).

Русский

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

LaTeX

$$$ \\mathrm{PreservesBinaryProducts}\\ i $$

Lean4

/-- If a reflective subcategory is an exponential ideal, then the reflector preserves binary products.
This is the converse of `exponentialIdeal_of_preserves_binary_products`.
-/
theorem preservesBinaryProducts_of_exponentialIdeal : PreservesLimitsOfShape (Discrete WalkingPair) (reflector i) where
  preservesLimit
    {K} :=
    letI :=
      preservesLimit_pair_of_isIso_prodComparison (reflector i) (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)
    Limits.preservesLimit_of_iso_diagram _ (diagramIsoPair K).symm

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