Cartesian closed categories
Given a category with finite products, the cartesian monoidal structure is provided by the local
instance monoidal_of_has_finite_products.
We define exponentiable objects to be closed objects with respect to this monoidal structure,
i.e. (X × -) is a left adjoint.
We say a category is cartesian closed if every object is exponentiable (equivalently, that the category equipped with the cartesian monoidal structure is closed monoidal).
Show that exponential forms a difunctor and define the exponential comparison morphisms.
TODO
Some of the results here are true more generally for closed objects and for closed monoidal categories, and these could be generalised.
def
category_theory.exponentiable
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C] :
C → Type (max u v)
An object X is exponentiable if (X × -) is a left adjoint.
We define this as being closed in the cartesian monoidal structure.
def
category_theory.binary_product_exponentiable
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
{X Y : C} :
If X and Y are exponentiable then X ⨯ Y is.
This isn't an instance because it's not usually how we want to construct exponentials, we'll usually
prove all objects are exponential uniformly.
Equations
- category_theory.binary_product_exponentiable hX hY = {is_adj := category_theory.adjunction.left_adjoint_of_nat_iso (category_theory.monoidal_category.tensor_left_tensor X Y).symm (category_theory.adjunction.left_adjoint_of_comp (category_theory.monoidal_category.tensor_left Y) (category_theory.monoidal_category.tensor_left X))}
def
category_theory.terminal_exponentiable
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C] :
The terminal object is always exponentiable. This isn't an instance because most of the time we'll prove cartesian closed for all objects at once, rather than just for this one.
def
category_theory.cartesian_closed
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_finite_products C] :
Type (max u v)
A category C is cartesian closed if it has finite products and every object is exponentiable.
We define this as monoidal_closed with respect to the cartesian monoidal structure.
def
category_theory.exp
{C : Type u}
[category_theory.category C]
(A : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
C ⥤ C
This is (-)^A.
def
category_theory.exp.adjunction
{C : Type u}
[category_theory.category C]
(A : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
The adjunction between A ⨯ - and (-)^A.
def
category_theory.ev
{C : Type u}
[category_theory.category C]
(A : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
The evaluation natural transformation.
Equations
def
category_theory.coev
{C : Type u}
[category_theory.category C]
(A : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
The coevaluation natural transformation.
Equations
@[simp]
theorem
category_theory.ev_coev
{C : Type u}
[category_theory.category C]
(A B : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
category_theory.limits.prod.map (𝟙 A) ((category_theory.coev A).app B) ≫ (category_theory.ev A).app (A ⨯ B) = 𝟙 (A ⨯ B)
@[simp]
theorem
category_theory.ev_coev_assoc
{C : Type u}
[category_theory.category C]
(A B : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
{X' : C}
(f' : (𝟭 C).obj ((category_theory.limits.prod_functor.obj A).obj B) ⟶ X') :
category_theory.limits.prod.map (𝟙 A) ((category_theory.coev A).app B) ≫ (category_theory.ev A).app (A ⨯ B) ≫ f' = f'
@[simp]
theorem
category_theory.coev_ev
{C : Type u}
[category_theory.category C]
(A B : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
(category_theory.coev A).app ((category_theory.exp A).obj B) ≫ (category_theory.exp A).map ((category_theory.ev A).app B) = 𝟙 ((category_theory.exp A).obj B)
@[simp]
theorem
category_theory.coev_ev_assoc
{C : Type u}
[category_theory.category C]
(A B : C)
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
{X' : C}
(f' : (category_theory.exp A).obj ((𝟭 C).obj B) ⟶ X') :
(category_theory.coev A).app ((category_theory.exp A).obj B) ≫ (category_theory.exp A).map ((category_theory.ev A).app B) ≫ f' = f'
def
category_theory.cartesian_closed.curry
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
(A ⨯ Y ⟶ X) → (Y ⟶ (category_theory.exp A).obj X)
Currying in a cartesian closed category.
def
category_theory.cartesian_closed.uncurry
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
(Y ⟶ (category_theory.exp A).obj X) → (A ⨯ Y ⟶ X)
Uncurrying in a cartesian closed category.
theorem
category_theory.curry_natural_left_assoc
{C : Type u}
[category_theory.category C]
{A X X' Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : X ⟶ X')
(g : A ⨯ X' ⟶ Y)
{X'_1 : C}
(f' : (category_theory.exp A).obj Y ⟶ X'_1) :
theorem
category_theory.curry_natural_left
{C : Type u}
[category_theory.category C]
{A X X' Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : X ⟶ X')
(g : A ⨯ X' ⟶ Y) :
theorem
category_theory.curry_natural_right
{C : Type u}
[category_theory.category C]
{A X Y Y' : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : A ⨯ X ⟶ Y)
(g : Y ⟶ Y') :
theorem
category_theory.curry_natural_right_assoc
{C : Type u}
[category_theory.category C]
{A X Y Y' : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : A ⨯ X ⟶ Y)
(g : Y ⟶ Y')
{X' : C}
(f' : (category_theory.exp A).obj Y' ⟶ X') :
category_theory.cartesian_closed.curry (f ≫ g) ≫ f' = category_theory.cartesian_closed.curry f ≫ (category_theory.exp A).map g ≫ f'
theorem
category_theory.uncurry_natural_right
{C : Type u}
[category_theory.category C]
{A X Y Y' : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : X ⟶ (category_theory.exp A).obj Y)
(g : Y ⟶ Y') :
theorem
category_theory.uncurry_natural_right_assoc
{C : Type u}
[category_theory.category C]
{A X Y Y' : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : X ⟶ (category_theory.exp A).obj Y)
(g : Y ⟶ Y')
{X' : C}
(f' : Y' ⟶ X') :
category_theory.cartesian_closed.uncurry (f ≫ (category_theory.exp A).map g) ≫ f' = category_theory.cartesian_closed.uncurry f ≫ g ≫ f'
theorem
category_theory.uncurry_natural_left_assoc
{C : Type u}
[category_theory.category C]
{A X X' Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : X ⟶ X')
(g : X' ⟶ (category_theory.exp A).obj Y)
{X'_1 : C}
(f' : Y ⟶ X'_1) :
theorem
category_theory.uncurry_natural_left
{C : Type u}
[category_theory.category C]
{A X X' Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : X ⟶ X')
(g : X' ⟶ (category_theory.exp A).obj Y) :
@[simp]
theorem
category_theory.uncurry_curry
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : A ⨯ X ⟶ Y) :
@[simp]
theorem
category_theory.curry_uncurry
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : X ⟶ (category_theory.exp A).obj Y) :
theorem
category_theory.curry_eq_iff
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : A ⨯ Y ⟶ X)
(g : Y ⟶ (category_theory.exp A).obj X) :
theorem
category_theory.eq_curry_iff
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(f : A ⨯ Y ⟶ X)
(g : Y ⟶ (category_theory.exp A).obj X) :
theorem
category_theory.uncurry_eq
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(g : Y ⟶ (category_theory.exp A).obj X) :
theorem
category_theory.curry_eq
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(g : A ⨯ Y ⟶ X) :
theorem
category_theory.uncurry_id_eq_ev
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
(A X : C)
[category_theory.exponentiable A] :
category_theory.cartesian_closed.uncurry (𝟙 ((category_theory.exp A).obj X)) = (category_theory.ev A).app X
theorem
category_theory.curry_id_eq_coev
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
(A X : C)
[category_theory.exponentiable A] :
category_theory.cartesian_closed.curry (𝟙 (A ⨯ (𝟭 C).obj X)) = (category_theory.coev A).app X
theorem
category_theory.curry_injective
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
theorem
category_theory.uncurry_injective
{C : Type u}
[category_theory.category C]
{A X Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
def
category_theory.exp_terminal_iso_self
{C : Type u}
[category_theory.category C]
{X : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable (⊤_C)] :
(category_theory.exp (⊤_C)).obj X ≅ X
Show that the exponential of the terminal object is isomorphic to itself, i.e. X^1 ≅ X.
The typeclass argument is explicit: any instance can be used.
Equations
- category_theory.exp_terminal_iso_self = category_theory.yoneda.ext ((category_theory.exp (⊤_C)).obj X) X (λ (Y : C) (f : Y ⟶ (category_theory.exp (⊤_C)).obj X), (category_theory.limits.prod.left_unitor Y).inv ≫ category_theory.cartesian_closed.uncurry f) (λ (Y : C) (f : Y ⟶ X), category_theory.cartesian_closed.curry ((category_theory.limits.prod.left_unitor Y).hom ≫ f)) category_theory.exp_terminal_iso_self._proof_1 category_theory.exp_terminal_iso_self._proof_2 category_theory.exp_terminal_iso_self._proof_3
def
category_theory.internalize_hom
{C : Type u}
[category_theory.category C]
{A Y : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A] :
(A ⟶ Y) → (⊤_C ⟶ (category_theory.exp A).obj Y)
The internal element which points at the given morphism.
def
category_theory.pre
{C : Type u}
[category_theory.category C]
{A B : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
(X : C)
(f : B ⟶ A)
[category_theory.exponentiable B] :
(category_theory.exp A).obj X ⟶ (category_theory.exp B).obj X
Pre-compose an internal hom with an external hom.
Equations
theorem
category_theory.pre_id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
(A X : C)
[category_theory.exponentiable A] :
category_theory.pre X (𝟙 A) = 𝟙 ((category_theory.exp A).obj X)
theorem
category_theory.pre_map
{C : Type u}
[category_theory.category C]
{A B X : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
[category_theory.exponentiable B]
{D : C}
[category_theory.exponentiable D]
(f : A ⟶ B)
(g : B ⟶ D) :
category_theory.pre X (f ≫ g) = category_theory.pre X g ≫ category_theory.pre X f
Precomposition is contrafunctorial.
theorem
category_theory.pre_post_comm
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
[category_theory.cartesian_closed C]
{A B : C}
{X Y : Cᵒᵖ}
(f : A ⟶ B)
(g : X ⟶ Y) :
category_theory.pre A g.unop ≫ (category_theory.exp (opposite.unop Y)).map f = (category_theory.exp (opposite.unop X)).map f ≫ category_theory.pre B g.unop
def
category_theory.internal_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
[category_theory.cartesian_closed C] :
The internal hom functor given by the cartesian closed structure.
Equations
- category_theory.internal_hom = {obj := λ (X : C), {obj := λ (Y : Cᵒᵖ), (category_theory.exp (opposite.unop Y)).obj X, map := λ (Y Y' : Cᵒᵖ) (f : Y ⟶ Y'), category_theory.pre X f.unop, map_id' := _, map_comp' := _}, map := λ (A B : C) (f : A ⟶ B), {app := λ (X : Cᵒᵖ), (category_theory.exp (opposite.unop X)).map f, naturality' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.zero_mul_inv
{C : Type u}
[category_theory.category C]
{A : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
[category_theory.limits.has_initial C] :
category_theory.zero_mul.inv = inhabited.default (⊥_C ⟶ A ⨯ ⊥_C)
@[simp]
theorem
category_theory.zero_mul_hom
{C : Type u}
[category_theory.category C]
{A : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
[category_theory.limits.has_initial C] :
def
category_theory.zero_mul
{C : Type u}
[category_theory.category C]
{A : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
[category_theory.limits.has_initial C] :
If an initial object 0 exists in a CCC, then A ⨯ 0 ≅ 0.
Equations
def
category_theory.mul_zero
{C : Type u}
[category_theory.category C]
{A : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
[category_theory.limits.has_initial C] :
If an initial object 0 exists in a CCC, then 0 ⨯ A ≅ 0.
def
category_theory.pow_zero
{C : Type u}
[category_theory.category C]
(B : C)
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_initial C]
[category_theory.cartesian_closed C] :
(category_theory.exp (⊥_C)).obj B ≅ ⊤_C
If an initial object 0 exists in a CCC then 0^B ≅ 1 for any B.
Equations
- category_theory.pow_zero B = {hom := inhabited.default ((category_theory.exp (⊥_C)).obj B ⟶ ⊤_C) unique.inhabited, inv := category_theory.cartesian_closed.curry (category_theory.mul_zero.hom ≫ inhabited.default (⊥_C ⟶ B)), hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.prod_coprod_distrib
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.cartesian_closed C]
(X Y Z : C) :
In a CCC with binary coproducts, the distribution morphism is an isomorphism.
Equations
- category_theory.prod_coprod_distrib X Y Z = {hom := category_theory.limits.coprod.desc (category_theory.limits.prod.map (𝟙 Z) category_theory.limits.coprod.inl) (category_theory.limits.prod.map (𝟙 Z) category_theory.limits.coprod.inr), inv := category_theory.cartesian_closed.uncurry (category_theory.limits.coprod.desc (category_theory.cartesian_closed.curry category_theory.limits.coprod.inl) (category_theory.cartesian_closed.curry category_theory.limits.coprod.inr)), hom_inv_id' := _, inv_hom_id' := _}
@[instance]
def
category_theory.strict_initial
{C : Type u}
[category_theory.category C]
{A : C}
[category_theory.limits.has_finite_products C]
[category_theory.exponentiable A]
[category_theory.limits.has_initial C]
{f : A ⟶ ⊥_C} :
If an initial object 0 exists in a CCC then it is a strict initial object,
i.e. any morphism to 0 is an iso.
@[instance]
def
category_theory.initial_mono
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
(B : C)
[category_theory.limits.has_initial C]
[category_theory.cartesian_closed C] :
If an initial object 0 exists in a CCC then every morphism from it is monic.
Equations
- _ = _
def
category_theory.cartesian_closed_of_equiv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_finite_products D]
(e : C ≌ D)
[h : category_theory.cartesian_closed C] :
Transport the property of being cartesian closed across an equivalence of categories.
Note we didn't require any coherence between the choice of finite products here, since we transport
along the prod_comparison isomorphism.
Equations
- category_theory.cartesian_closed_of_equiv e = {closed := λ (X : D), {is_adj := category_theory.adjunction.left_adjoint_of_nat_iso (category_theory.iso_whisker_right e.counit_iso (category_theory.limits.prod_functor.obj X ⋙ e.inverse ⋙ e.functor) ≪≫ id (category_theory.iso_whisker_left (category_theory.limits.prod_functor.obj X) e.counit_iso)) (category_theory.adjunction.left_adjoint_of_comp (e.inverse ⋙ e.functor ⋙ category_theory.limits.prod_functor.obj X ⋙ e.inverse) e.functor)}}
def
category_theory.exp_comparison
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_finite_products D]
[category_theory.cartesian_closed C]
[category_theory.cartesian_closed D]
(F : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F]
(A B : C) :
F.obj ((category_theory.exp A).obj B) ⟶ (category_theory.exp (F.obj A)).obj (F.obj B)
The exponential comparison map.
F is a cartesian closed functor if this is an iso for all A,B.
Equations
theorem
category_theory.exp_comparison_natural_left
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_finite_products D]
[category_theory.cartesian_closed C]
[category_theory.cartesian_closed D]
(F : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F]
(A A' B : C)
(f : A' ⟶ A) :
category_theory.exp_comparison F A B ≫ category_theory.pre (F.obj B) (F.map f) = F.map (category_theory.pre B f) ≫ category_theory.exp_comparison F A' B
The exponential comparison map is natural in its left argument.
theorem
category_theory.exp_comparison_natural_right
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_finite_products D]
[category_theory.cartesian_closed C]
[category_theory.cartesian_closed D]
(F : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F]
(A B B' : C)
(f : B ⟶ B') :
category_theory.exp_comparison F A B ≫ (category_theory.exp (F.obj A)).map (F.map f) = F.map ((category_theory.exp A).map f) ≫ category_theory.exp_comparison F A B'
The exponential comparison map is natural in its right argument.