Cartesian closed categories #
Given a category with finite products, the cartesian monoidal structure is provided by the local
instance monoidalOfHasFiniteProducts
.
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.
An object X
is exponentiable if (X × -)
is a left adjoint.
We define this as being Closed
in the cartesian monoidal structure.
Equations
Instances For
Constructor for Exponentiable X
which takes as an input an adjunction
MonoidalCategory.tensorLeft X ⊣ exp
for some functor exp : C ⥤ C
.
Equations
- CategoryTheory.Exponentiable.mk X exp adj = { rightAdj := exp, adj := adj }
Instances For
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
Instances For
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.
Equations
- CategoryTheory.terminalExponentiable = CategoryTheory.unitClosed
Instances For
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.
Equations
Instances For
Constructor for CartesianClosed C
.
Equations
- CategoryTheory.CartesianClosed.mk C exp = { closed := fun (X : C) => exp X }
Instances For
This is (-)^A.
Equations
Instances For
The adjunction between A ⨯ - and (-)^A.
Equations
Instances For
The evaluation natural transformation.
Equations
Instances For
The coevaluation natural transformation.
Equations
Instances For
Morphisms obtained using an exponentiable object.
Equations
- CategoryTheory.exp.«term_⟹_» = Lean.ParserDescr.trailingNode `CategoryTheory.exp.term_⟹_ 20 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 19))
Instances For
Delaborator for Prefunctor.obj
Equations
- One or more equations did not get rendered due to their size.
Instances For
Morphisms from an exponentiable object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.instPreservesColimitsObjFunctorFunctor A = (CategoryTheory.ihom.adjunction A).leftAdjointPreservesColimits
Currying in a cartesian closed category.
Equations
- CategoryTheory.CartesianClosed.curry = ⇑((CategoryTheory.exp.adjunction A).homEquiv Y X)
Instances For
Uncurrying in a cartesian closed category.
Equations
- CategoryTheory.CartesianClosed.uncurry = ⇑((CategoryTheory.exp.adjunction A).homEquiv Y X).symm
Instances For
The exponential with the terminal object is naturally isomorphic to the identity. The typeclass argument is explicit: any instance can be used.
Equations
- CategoryTheory.expTerminalNatIso = CategoryTheory.MonoidalClosed.unitNatIso
Instances For
The exponential of any object with the terminal object is isomorphic to itself, i.e. X^1 ≅ X
.
The typeclass argument is explicit: any instance can be used.
Equations
- CategoryTheory.expTerminalIsoSelf = (CategoryTheory.expTerminalNatIso.app X).symm
Instances For
The internal element which points at the given morphism.
Equations
- CategoryTheory.internalizeHom f = CategoryTheory.CartesianClosed.curry (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)
Instances For
Pre-compose an internal hom with an external hom.
Equations
- CategoryTheory.pre f = (CategoryTheory.conjugateEquiv (CategoryTheory.exp.adjunction A) (CategoryTheory.exp.adjunction B)) (CategoryTheory.Limits.prod.functor.map f)
Instances For
The internal hom functor given by the cartesian closed structure.
Equations
- CategoryTheory.internalHom = { obj := fun (X : Cᵒᵖ) => CategoryTheory.exp (Opposite.unop X), map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => CategoryTheory.pre f.unop, map_id := ⋯, map_comp := ⋯ }
Instances For
If an initial object I
exists in a CCC, then A ⨯ I ≅ I
.
Equations
- CategoryTheory.zeroMul t = { hom := CategoryTheory.Limits.prod.snd, inv := t.to (A ⨯ I), hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
If an initial object 0
exists in a CCC, then 0 ⨯ A ≅ 0
.
Equations
Instances For
If an initial object 0
exists in a CCC then 0^B ≅ 1
for any B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
In a CCC with binary coproducts, the distribution morphism is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If an initial object I
exists in a CCC then it is a strict initial object,
i.e. any morphism to I
is an iso.
This actually shows a slightly stronger version: any morphism to an initial object from an
exponentiable object is an isomorphism.
Equations
- ⋯ = ⋯
If an initial object 0
exists in a CCC then every morphism from it is monic.
Equations
- ⋯ = ⋯
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 prodComparison
isomorphism.
Equations
- CategoryTheory.cartesianClosedOfEquiv e = CategoryTheory.MonoidalClosed.ofEquiv e.inverse.toMonoidalFunctorOfHasFiniteProducts e.symm.toAdjunction