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.
The subcategory D
of C
expressed as an inclusion functor is an exponential ideal if
B ∈ D
implies A ⟹ B ∈ D
for all A
.
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
.
The entire category viewed as a subcategory is an exponential ideal.
The subcategory of subterminal objects is an exponential ideal.
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
- category_theory.exponential_ideal_reflective i A = (category_theory.nat_iso.of_components (λ (X : D), category_theory.as_iso ((category_theory.adjunction.of_right_adjoint i).unit.app ((category_theory.exp A).obj (i.obj X)))) _).symm
Given a natural isomorphism i ⋙ exp A ⋙ left_adjoint i ⋙ i ≅ i ⋙ exp A
, we can show i
is an exponential ideal.
If the reflector preserves binary products, the subcategory is an exponential ideal.
This is the converse of preserves_binary_products_of_exponential_ideal
.
If i
witnesses that D
is a reflective subcategory and an exponential ideal, then D
is
itself cartesian closed.
Equations
- category_theory.cartesian_closed_of_reflective i = {closed' := λ (B : D), {is_adj := {right := i ⋙ category_theory.exp (i.obj B) ⋙ category_theory.left_adjoint i, adj := category_theory.adjunction.restrict_fully_faithful i i (category_theory.exp.adjunction (i.obj B)) (category_theory.nat_iso.of_components (λ (X : D), category_theory.as_iso (category_theory.limits.prod_comparison i B X)) _).symm (category_theory.exponential_ideal_reflective i (i.obj B)).symm category_theory.reflective.to_faithful}}}
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
: Seebijection_natural
. - When
X = LA ⨯ LB
, then the backwards direction sends the identity morphism to the product comparison morphism: Seebijection_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
- category_theory.bijection i A B X = (((((((((((category_theory.adjunction.of_right_adjoint i).hom_equiv (A ⨯ B) X).trans ((category_theory.limits.prod.braiding A B).hom_congr (category_theory.iso.refl (i.obj X)))).trans ((category_theory.exp.adjunction B).hom_equiv A (i.obj X))).trans (category_theory.unit_comp_partial_bijective A _)).trans ((category_theory.exp.adjunction B).hom_equiv (i.obj ((category_theory.left_adjoint i).obj A)) (i.obj X)).symm).trans ((category_theory.limits.prod.braiding B (i.obj ((category_theory.left_adjoint i).obj A))).hom_congr (category_theory.iso.refl (i.obj X)))).trans ((category_theory.exp.adjunction (i.obj ((category_theory.left_adjoint i).obj A))).hom_equiv B (i.obj X))).trans (category_theory.unit_comp_partial_bijective B _)).trans ((category_theory.exp.adjunction (i.obj ((category_theory.left_adjoint i).obj A))).hom_equiv (i.obj ((category_theory.left_adjoint i).obj B)) (i.obj X)).symm).trans ((category_theory.limits.preserves_limit_pair.iso i ((category_theory.left_adjoint i).obj A) ((category_theory.left_adjoint i).obj B)).symm.hom_congr (category_theory.iso.refl (i.obj X)))).trans (category_theory.equiv_of_fully_faithful i).symm
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
- category_theory.preserves_finite_products_of_exponential_ideal i J = let _inst : category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) (category_theory.left_adjoint i) := category_theory.preserves_binary_products_of_exponential_ideal i, _inst_8 : category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) (category_theory.left_adjoint i) := category_theory.left_adjoint_preserves_terminal_of_reflective i in category_theory.preserves_finite_products_of_preserves_binary_and_terminal (category_theory.left_adjoint i) J