Exponential ideals

An exponential ideal of a Cartesian closed category C is a subcategory D ⊆ C such that for any B : D and A : C, the exponential A ⟹ B is in D: resembling ring-theoretic ideals. We define the notion here for inclusion functors i : D ⥤ C rather than explicit subcategories to preserve the principle of equivalence.

We additionally show that if C is Cartesian closed and i : D ⥤ C is a reflective functor, the following are equivalent.

• The left adjoint to i preserves binary (equivalently, finite) products.
• i is an exponential ideal.

class CategoryTheory.ExponentialIdeal {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [MonoidalClosed C] : Prop

The subcategory D of C expressed as an inclusion functor is an exponential ideal if B ∈ D implies A ⟹ B ∈ D for all A.

• exp_closed {B : C} : i.essImage B → ∀ (A : C), i.essImage (A ⟹ B)

theorem CategoryTheory.ExponentialIdeal.mk' {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [MonoidalClosed C] (h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)) : ExponentialIdeal i

To show i is an exponential ideal it suffices to show that A ⟹ iB is "in" D for any A in C and B in D.

instance CategoryTheory.instExponentialIdealId {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [MonoidalClosed C] : ExponentialIdeal (Functor.id C)

The entire category viewed as a subcategory is an exponential ideal.

instance CategoryTheory.instExponentialIdealSubterminalsSubterminalInclusion {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [MonoidalClosed C] : ExponentialIdeal (subterminalInclusion C)

The subcategory of subterminal objects is an exponential ideal.

def CategoryTheory.exponentialIdealReflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [MonoidalClosed C] (A : C) [Reflective i] [ExponentialIdeal i] : i.comp ((ihom A).comp ((reflector i).comp i)) ≅ i.comp (ihom A)

If D is a reflective subcategory, the property of being an exponential ideal is equivalent to the presence of a natural isomorphism i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A, that is: (A ⟹ iB) ≅ i L (A ⟹ iB), naturally in B. The converse is given in ExponentialIdeal.mk_of_iso.

theorem CategoryTheory.ExponentialIdeal.mk_of_iso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [MonoidalClosed C] [Reflective i] (h : (A : C) → i.comp ((ihom A).comp ((reflector i).comp i)) ≅ i.comp (ihom A)) : ExponentialIdeal i

Given a natural isomorphism i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A, we can show i is an exponential ideal.

theorem CategoryTheory.reflective_products {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [Limits.HasFiniteProducts C] [Reflective i] : Limits.HasFiniteProducts D

@[reducible, inline]

abbrev CategoryTheory.CartesianMonoidalCategory.ofReflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] : CartesianMonoidalCategory D

Given a reflective subcategory D of a category with chosen finite products C, D admits finite chosen products.

@[instance 10]

instance CategoryTheory.exponentialIdeal_of_preservesBinaryProducts {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)] : ExponentialIdeal i

If the reflector preserves binary products, the subcategory is an exponential ideal. This is the converse of preservesBinaryProductsOfExponentialIdeal.

def CategoryTheory.cartesianClosedOfReflective' {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] (l : Functor i.EssImageSubcategory D) (φ : l.comp i ≅ i.essImage.ι) : MonoidalClosed D

If i witnesses that D is a reflective subcategory and an exponential ideal, then D is itself Cartesian closed.

To allow for better control of definitional equality, this construction takes in an explicit choice of lift of the essential image of i to D, in the form of a functor l : i.EssImageSubcategory ⥤ D and natural isomorphism φ : l ⋙ i ≅ i.essImage.ι. When l ⋙ i is defeq to i.essImage.ι, images of exponential objects in D under i will be defeq to the respective exponential objects in C.

def CategoryTheory.cartesianClosedOfReflective {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] : MonoidalClosed D

If i witnesses that D is a reflective subcategory and an exponential ideal, then D is itself Cartesian closed.

Unlike cartesianClosedOfReflective' this construction lifts exponential objects in C to exponential objects in D by applying the reflector to them, even though they already lie in the essential image of i; if you need better control over definitional equality, use cartesianClosedOfReflective' instead.

noncomputable def CategoryTheory.bijection {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] [BraidedCategory C] (A B : C) (X : D) : ((reflector i).obj (MonoidalCategoryStruct.tensorObj A B) ⟶ X) ≃ (MonoidalCategoryStruct.tensorObj ((reflector i).obj A) ((reflector i).obj B) ⟶ X)

We construct a bijection between morphisms L(A ⊗ B) ⟶ X and morphisms LA ⊗ LB ⟶ X. This bijection has two key properties:

• It is natural in X: See bijection_natural.
• When X = LA ⨯ LB, then the backwards direction sends the identity morphism to the product comparison morphism: See bijection_symm_apply_id.

Together these help show that L preserves binary products. This should be considered internal implementation towards preservesBinaryProductsOfExponentialIdeal.

theorem CategoryTheory.bijection_symm_apply_id {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] [BraidedCategory C] (A B : C) : (bijection i A B (MonoidalCategoryStruct.tensorObj ((reflector i).obj A) ((reflector i).obj B))).symm (CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((reflector i).obj A) ((reflector i).obj B))) = CartesianMonoidalCategory.prodComparison (reflector i) A B

theorem CategoryTheory.bijection_natural {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] [BraidedCategory C] (A B : C) (X X' : D) (f : (reflector i).obj (MonoidalCategoryStruct.tensorObj A B) ⟶ X) (g : X ⟶ X') : (bijection i A B X') (CategoryStruct.comp f g) = CategoryStruct.comp ((bijection i A B X) f) g

theorem CategoryTheory.prodComparison_iso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] [BraidedCategory C] (A B : C) : IsIso (CartesianMonoidalCategory.prodComparison (reflector i) A B)

The bijection allows us to show that prodComparison L A B is an isomorphism, where the inverse is the forward map of the identity morphism.

theorem CategoryTheory.preservesBinaryProducts_of_exponentialIdeal {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] [BraidedCategory C] : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (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.

theorem CategoryTheory.Limits.PreservesFiniteProducts.of_exponentialIdeal {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₁, u₂} D] (i : Functor D C) [CartesianMonoidalCategory C] [Reflective i] [MonoidalClosed C] [CartesianMonoidalCategory D] [ExponentialIdeal i] [BraidedCategory C] : PreservesFiniteProducts (reflector i)

If a reflective subcategory is an exponential ideal, then the reflector preserves finite products.