Theorems · Theorem · category theory

CategoryTheory.preservesBinaryProducts_of_exponentialIdeal

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.ExponentialIdeal i] [CategoryTheory.BraidedCategory C],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
    (CategoryTheory.reflector i)

If a reflective subcategory is an exponential ideal, then the reflector preserves binary products. This is the converse of exponentialIdeal_of_preserves_binary_products.

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Cited by

1 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.ReflectiveCategoryTheory.MonoidalClosedCategoryTheory.CartesianMonoidalCategoryCategoryTheory.ExponentialIdealCategoryTheory.BraidedCategory