Exponentiable morphisms in a category

We say that a morphism f : X ⟶ Y in a category C has pushforward if there is a right adjoint to the base-change functor along f. The type Pushforward f is a structure containing functor : Over X ⥤ Over Y and a witness adj : baseChange f ⊣ functor.

We prove that if a morphism f : X ⟶ Y has pushforwards then f is exponentiable in the slice category Over Y. In particular, for a morphism g : X ⟶ I the exponential f^* g is the functor composition (baseChange g) ⋙ (Over.map g).

Notation

We provide the following notations:

• Π_ f is the functor pushforward f : Over J ⥤ Over I. As such, for an object X : Over J, we have Π_f X : Over I

class CartesianExponentiable {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) : Type (max u_1 u_2)

• functor : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)

  A functor C/X ⥤ C/Y right adjoint to f*.

• adj : Δ_ f ⊣ Π_ f

def «termΠ__» : Lean.ParserDescr

A functor C/X ⥤ C/Y right adjoint to f*.

Equations

• «termΠ__» = Lean.ParserDescr.node `«termΠ__» 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Π_ ") (Lean.ParserDescr.cat `term 90))

instance CartesianExponentiable.id {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} : CartesianExponentiable (CategoryTheory.CategoryStruct.id I)

The identity morphisms 𝟙 are exponentiable.

Equations

• CartesianExponentiable.id = { functor := CategoryTheory.Functor.id (CategoryTheory.Over I), adj := CategoryTheory.Adjunction.id.ofNatIsoLeft (CategoryTheory.baseChange.id I).symm }

instance CartesianExponentiable.comp {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [fexp : CartesianExponentiable f] [gexp : CartesianExponentiable g] : CartesianExponentiable (CategoryTheory.CategoryStruct.comp f g)

Equations

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

def CartesianExponentiable.pushforwardCompIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [fexp : CartesianExponentiable f] [gexp : CartesianExponentiable g] : (Π_ f).comp (Π_ g) ≅ Π_ CategoryTheory.CategoryStruct.comp f g

The conjugate isomorphism between pushforward functors.

Equations

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

instance CartesianExponentiable.exponentiableOverMk {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} [CategoryTheory.Limits.HasFiniteWidePullbacks C] {I : C} (f : X ⟶ I) [CartesianExponentiable f] : CategoryTheory.Exponentiable (CategoryTheory.Over.mk f)

An arrow with a pushforward is exponentiable in the slice category.

Equations

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