# mathlib3documentation

category_theory.closed.ideal

# Exponential ideals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
structure category_theory.exponential_ideal {C : Type u₁} {D : Type u₂} (i : D 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.

Instances of this typeclass
theorem category_theory.exponential_ideal.mk' {C : Type u₁} {D : Type u₂} (i : D C) (h : (B : D) (A : C), (i.obj B) i.ess_image) :

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.

@[protected, instance]

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

@[protected, instance]

The subcategory of subterminal objects is an exponential ideal.

noncomputable def category_theory.exponential_ideal_reflective {C : Type u₁} {D : Type u₂} (i : D C) (A : C)  :

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 ⋙ left_adjoint i ⋙ i ≅ i ⋙ exp A, that is: (A ⟹ iB) ≅ i L (A ⟹ iB), naturally in B. The converse is given in exponential_ideal.mk_of_iso.

Equations
theorem category_theory.exponential_ideal.mk_of_iso {C : Type u₁} {D : Type u₂} (i : D C) (h : Π (A : C), ) :

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

theorem category_theory.reflective_products {C : Type u₁} {D : Type u₂} (i : D C)  :
@[protected, instance]

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

noncomputable def category_theory.cartesian_closed_of_reflective {C : Type u₁} {D : Type u₂} (i : D C)  :

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

Equations
noncomputable def category_theory.bijection {C : Type u₁} {D : Type u₂} (i : D C) (A B : C) (X : D) :
(A B) X) 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 preserves_binary_products_of_exponential_ideal.

Equations
theorem category_theory.bijection_symm_apply_id {C : Type u₁} {D : Type u₂} (i : D C) (A B : C) :
B B)).symm) (𝟙 B)) =
theorem category_theory.bijection_natural {C : Type u₁} {D : Type u₂} (i : D C) (A B : C) (X X' : D) (f : (A B) X) (g : X X') :
X') (f g) = X) f g
theorem category_theory.prod_comparison_iso {C : Type u₁} {D : Type u₂} (i : D C) (A B : C) :

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

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

Equations

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

Equations