Locally cartesian closed categories

There are several equivalent definitions of locally cartesian closed categories. For instance the following two definitions are equivalent:

1. A locally cartesian closed category is a category C such that for every object I the slice category Over I is cartesian closed.

2. Equivalently, a locally cartesian closed category is a category with pullbacks where all morphisms f are exponentiable, that is the base change functor Over.pullback f has a right adjoint for every morphisms f : I ⟶ J. This latter condition is equivalent to exponentiability of Over.mk f in Over J. The right adjoint of Over.pullback f is called the pushforward functor.

In this file we prove the equivalence of these definitions.

Implementation notes

The type class LocallyCartesianClosed extends HasPushforwards with the extra data carrying the witness of cartesian closedness of the slice categories. HasPushforwards.cartesianClosedOver shows that the cartesian closed structure of the slices follows from existence of pushforwards along all morphisms. As such when instantiating a LocallyCartesianClosed structure, providing the the cartesian closed structure of the slices is not necessary and it will be filled in automatically. See LocallyCartesianClosed.mkOfHasPushforwards and LocallyCartesianClosed.mkOfCartesianClosedOver.

The advanatge we obtain from this implementation is that when using a LocallyCartesianClosed structure, both the pushforward functor and the cartesian closed structure of slices are automatically available.

Main results

• exponentiableOverMk shows that the exponentiable structure on a morphism f makes the object Over.mk f in the appropriate slice category exponentiable.
• ofOverExponentiable shows that an exponentiable object in a slice category gives rise to an exponentiable morphism.
• CartesianClosedOver.pushforward constructs, in a category with cartesian closed slices, the pushforward functor along a morphism f : I ⟶ J.
• CartesianClosedOver.pushforwardAdj shows that pushforward is right adjoint to the pullback functor.
• Conversely, HasPushforwards.cartesianClosedOver shows that, in a category with pushforwards along all morphisms, the slice categories are cartesian closed.
• LocallyCartesianClosed.cartesianClosed proves that a locally cartesian closed category with a terminal object is cartesian closed.
• LocallyCartesianClosed.overLocallyCartesianClosed shows that the slices of a locally cartesian closed category are locally cartesian closed.

@[reducible, inline]

abbrev CategoryTheory.ExponentiableMorphism {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] : MorphismProperty C

A morphism f : I ⟶ J is exponentiable if the pullback functor Over J ⥤ Over I has a right adjoint.

Equations

• CategoryTheory.ExponentiableMorphism f = (CategoryTheory.Over.pullback f).IsLeftAdjoint

@[reducible, inline]

abbrev CategoryTheory.ExponentiableMorphism.pushforward {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} (f : I ⟶ J) [ExponentiableMorphism f] : Functor (Over I) (Over J)

Equations

• CategoryTheory.ExponentiableMorphism.pushforward f = (CategoryTheory.Over.pullback f).rightAdjoint

def CategoryTheory.ExponentiableMorphism.adj {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} (f : I ⟶ J) [ExponentiableMorphism f] : Over.pullback f ⊣ (Over.pullback f).rightAdjoint

Equations

• CategoryTheory.ExponentiableMorphism.adj f = CategoryTheory.Adjunction.ofIsLeftAdjoint (CategoryTheory.Over.pullback f)

@[reducible, inline]

abbrev CategoryTheory.ExponentiableMorphism.ev {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} (f : I ⟶ J) [ExponentiableMorphism f] : (pushforward f).comp (Over.pullback f) ⟶ Functor.id (Over I)

The dependent evaluation natural transformation as the counit of the adjunction.

Equations

• CategoryTheory.ExponentiableMorphism.ev f = (CategoryTheory.ExponentiableMorphism.adj f).counit

@[reducible, inline]

abbrev CategoryTheory.ExponentiableMorphism.coev {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} (f : I ⟶ J) [ExponentiableMorphism f] : Functor.id (Over J) ⟶ (Over.pullback f).comp (pushforward f)

The dependent coevaluation natural transformation as the unit of the adjunction.

Equations

• CategoryTheory.ExponentiableMorphism.coev f = (CategoryTheory.ExponentiableMorphism.adj f).unit

theorem CategoryTheory.ExponentiableMorphism.ev_coev {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] (X : Over J) : CategoryStruct.comp ((Over.pullback f).map ((adj f).unit.app X)) ((adj f).counit.app ((Over.pullback f).obj X)) = CategoryStruct.id ((Over.pullback f).obj X)

The first triangle identity for the counit and unit of the adjunction.

theorem CategoryTheory.ExponentiableMorphism.ev_coev_assoc {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] (X : Over J) {Z : Over I} (h : (Over.pullback f).obj X ⟶ Z) : CategoryStruct.comp ((Over.pullback f).map ((adj f).unit.app X)) (CategoryStruct.comp ((adj f).counit.app ((Over.pullback f).obj X)) h) = h

theorem CategoryTheory.ExponentiableMorphism.coev_ev {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] (Y : Over I) : CategoryStruct.comp ((adj f).unit.app ((pushforward f).obj Y)) ((pushforward f).map ((adj f).counit.app Y)) = CategoryStruct.id ((pushforward f).obj Y)

The second triangle identity for the counit and unit of the adjunction.

theorem CategoryTheory.ExponentiableMorphism.coev_ev_assoc {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] (Y : Over I) {Z : Over J} (h : (pushforward f).obj Y ⟶ Z) : CategoryStruct.comp ((adj f).unit.app ((pushforward f).obj Y)) (CategoryStruct.comp ((pushforward f).map ((adj f).counit.app Y)) h) = h

def CategoryTheory.ExponentiableMorphism.pushforwardCurry {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] {X : Over I} {A : Over J} (u : (Over.pullback f).obj A ⟶ X) : A ⟶ (pushforward f).obj X

The currying of (Over.pullback f).obj A ⟶ X in Over I to a morphism A ⟶ (pushforward f).obj X in Over J.

Equations

• CategoryTheory.ExponentiableMorphism.pushforwardCurry u = ((CategoryTheory.ExponentiableMorphism.adj f).homEquiv A X) u

def CategoryTheory.ExponentiableMorphism.pushforwardUncurry {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] {X : Over I} {A : Over J} (v : A ⟶ (pushforward f).obj X) : (Over.pullback f).obj A ⟶ X

The uncurrying of A ⟶ (pushforward f).obj X in Over J to a morphism (Over.pullback f).obj A ⟶ X in Over I.

Equations

• CategoryTheory.ExponentiableMorphism.pushforwardUncurry v = ((CategoryTheory.ExponentiableMorphism.adj f).homEquiv A X).invFun v

theorem CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] {X : Over I} {A : Over J} (u : (Over.pullback f).obj A ⟶ X) : ((adj f).homEquiv A X) u = pushforwardCurry u

theorem CategoryTheory.ExponentiableMorphism.homEquiv_symm_apply_eq {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] {X : Over I} {A : Over J} (v : A ⟶ (pushforward f).obj X) : ((adj f).homEquiv A X).symm v = pushforwardUncurry v

theorem CategoryTheory.ExponentiableMorphism.pushforward_uncurry_curry {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] {X : Over I} {A : Over J} (u : (Over.pullback f).obj A ⟶ X) : pushforwardUncurry (pushforwardCurry u) = u

theorem CategoryTheory.ExponentiableMorphism.pushforward_curry_uncurry {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] {X : Over I} {A : Over J} (v : A ⟶ (pushforward f).obj X) : pushforwardCurry (pushforwardUncurry v) = v

instance CategoryTheory.ExponentiableMorphism.OverMkHom {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J : C} {f : I ⟶ J} [ExponentiableMorphism f] : ExponentiableMorphism (Over.mk f).hom

instance CategoryTheory.ExponentiableMorphism.id {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I : C} : ExponentiableMorphism (CategoryStruct.id I)

The identity morphisms 𝟙 are exponentiable.

def CategoryTheory.ExponentiableMorphism.pushforwardIdIso {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (I : C) : pushforward (CategoryStruct.id I) ≅ Functor.id (Over I)

The conjugate iso between the pushforward of the identity and the identity of the pushforward.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ExponentiableMorphism.comp {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K) [ExponentiableMorphism f] [ExponentiableMorphism g] : ExponentiableMorphism (CategoryStruct.comp f g)

The composition of exponentiable morphisms is exponentiable.

def CategoryTheory.ExponentiableMorphism.pushforwardCompIso {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K) [ExponentiableMorphism f] [ExponentiableMorphism g] : have x := ⋯; pushforward (CategoryStruct.comp f g) ≅ (pushforward f).comp (pushforward g)

The conjugate isomorphism between pushforward of the composition and the composition of pushforward functors.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ExponentiableMorphism.isMultiplicative {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] : ExponentiableMorphism.IsMultiplicative

def CategoryTheory.ExponentiableMorphism.exponentiableOverMk {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasFiniteWidePullbacks C] {X I : C} (f : X ⟶ I) [ExponentiableMorphism f] : Exponentiable (Over.mk f)

A morphism with a pushforward is an exponentiable object in the slice category.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.ExponentiableMorphism.ofOverExponentiable {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasFiniteWidePullbacks C] {I : C} (X : Over I) [Exponentiable X] : ExponentiableMorphism X.hom

An exponentibale object X in the slice category Over I gives rise to an exponentiable morphism X.hom. Here the pushforward functor along a morphism f : I ⟶ J is defined using the section functor Over (Over.mk f) ⥤ Over J.

Equations

• ⋯ = ⋯

class CategoryTheory.HasPushforwards (C : Type u) [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] : Prop

A category HasPushforwards if every morphism is exponentiable.

• exponentiable {I J : C} (f : I ⟶ J) : ExponentiableMorphism f

  A function assigning to every morphism f : I ⟶ J an exponentiable structure.

instance CategoryTheory.HasPushforwards.cartesianClosedOver {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [HasPushforwards C] (I : C) : CartesianClosed (Over I)

In a category where pushforwards exists along all morphisms, every slice category Over I is cartesian closed.

Equations

• CategoryTheory.HasPushforwards.cartesianClosedOver I = { closed := fun (X : CategoryTheory.Over I) => CategoryTheory.ExponentiableMorphism.exponentiableOverMk X.hom }

instance CategoryTheory.CartesianClosedOver.instExponentiableMorphism {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] {I J : C} [CartesianClosed (Over J)] (f : I ⟶ J) : ExponentiableMorphism f

instance CategoryTheory.CartesianClosedOver.hasPushforwards {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [(I : C) → CartesianClosed (Over I)] : HasPushforwards C

A category with cartesian closed slices has pushforwards along all morphisms.

class CategoryTheory.LocallyCartesianClosed (C : Type u) [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] extends CategoryTheory.HasPushforwards C : Type (max u v)

A category with FiniteWidePullbacks is locally cartesian closed if every morphism in it is exponentiable and all the slices are cartesian closed.

• exponentiable {I J : C} (f : I ⟶ J) : ExponentiableMorphism f
• cartesianClosedOver (I : C) : CartesianClosed (Over I)

  every slice category Over I is cartesian closed. This is filled in by default.

instance CategoryTheory.LocallyCartesianClosed.mkOfHasPushforwards {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [HasPushforwards C] : LocallyCartesianClosed C

A category with pushforwards along all morphisms is locally cartesian closed.

Equations

• CategoryTheory.LocallyCartesianClosed.mkOfHasPushforwards = { toHasPushforwards := inst✝, cartesianClosedOver := CategoryTheory.HasPushforwards.cartesianClosedOver }

instance CategoryTheory.LocallyCartesianClosed.mkOfCartesianClosedOver {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [(I : C) → CartesianClosed (Over I)] : LocallyCartesianClosed C

A category with cartesian closed slices is locally cartesian closed.

Equations

• CategoryTheory.LocallyCartesianClosed.mkOfCartesianClosedOver = { toHasPushforwards := ⋯, cartesianClosedOver := CategoryTheory.HasPushforwards.cartesianClosedOver }

instance CategoryTheory.LocallyCartesianClosed.instExponentiableMorphism {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] {I J : C} (f : I ⟶ J) : ExponentiableMorphism f

Every morphism in a locally cartesian closed category is exponentiable.

@[reducible, inline]

abbrev CategoryTheory.LocallyCartesianClosed.Pi {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] {I : C} (X : Over I) (Y : Over X.left) : Over I

Pi X Y is the dependent product of Y along X. This is analogous to the dependent function type Π x : X, Y x in type theory. See Over.Sigma and Over.Reindex for related constructions.

Equations

• CategoryTheory.LocallyCartesianClosed.Pi X Y = (CategoryTheory.ExponentiableMorphism.pushforward X.hom).obj Y

@[reducible, inline]

abbrev CategoryTheory.LocallyCartesianClosed.Pi' {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] {I X Y : C} (f : X ⟶ I) (u : Y ⟶ X) : (Pi (Over.mk f) (Over.mk u)).left ⟶ I

Pi' is a variant of Pi which takes as input morphisms and outputs morphisms.

Equations

• CategoryTheory.LocallyCartesianClosed.Pi' f u = (CategoryTheory.LocallyCartesianClosed.Pi (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk u)).hom

theorem CategoryTheory.LocallyCartesianClosed.Pi'_def {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] {I X Y : C} (f : X ⟶ I) (u : Y ⟶ X) : Pi' f u = ((ExponentiableMorphism.pushforward f).obj (Over.mk u)).hom

@[reducible, inline]

abbrev CategoryTheory.LocallyCartesianClosed.ev' {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] {I : C} (X : Over I) (Y : Over X.left) : X.Reindex (Pi X Y) ⟶ Y

The dependent evaluation morphisms.

Equations

• CategoryTheory.LocallyCartesianClosed.ev' X Y = (CategoryTheory.ExponentiableMorphism.adj X.hom).counit.app Y

def CategoryTheory.LocallyCartesianClosed.cartesianClosed {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] [Limits.HasTerminal C] : CartesianClosed C

A locally cartesian closed category with a terminal object is cartesian closed.

Equations

• CategoryTheory.LocallyCartesianClosed.cartesianClosed = CategoryTheory.cartesianClosedOfEquiv (CategoryTheory.equivOverTerminal C)

def CategoryTheory.LocallyCartesianClosed.overLocallyCartesianClosed {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] (I : C) : LocallyCartesianClosed (Over I)

The slices of a locally cartesian closed category are locally cartesian closed.

Equations

• CategoryTheory.LocallyCartesianClosed.overLocallyCartesianClosed I = CategoryTheory.LocallyCartesianClosed.mkOfCartesianClosedOver

def CategoryTheory.LocallyCartesianClosed.expIso {C : Type u} [Category.{v, u} C] [Limits.HasFiniteWidePullbacks C] [LocallyCartesianClosed C] {I : C} (A X : Over I) : Pi A (A.Reindex X) ≅ A ⟹ X

The exponential X^^A in the slice category Over I is isomorphic to the pushforward of the pullback of X along A.

Equations

• CategoryTheory.LocallyCartesianClosed.expIso A X = CategoryTheory.Iso.refl (CategoryTheory.LocallyCartesianClosed.Pi A (A.Reindex X))