Documentation

Mathlib.CategoryTheory.Closed.Ideal

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 subcategory D of C expressed as an inclusion functor is an exponential ideal if B ∈ D implies A ⟹ B ∈ D for all A.

Instances

    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.

    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.

    Instances For

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

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

      Instances For