Exponentiable morphisms in a category

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

Notation

We provide the following notations:

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

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

A morphism f : X ⟶ Y in a category C is cartesian exponentiable if there is a right adjoint to the base-change functor along f.

• 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_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} : CartesianExponentiable (CategoryTheory.CategoryStruct.id I)

The identity morphisms 𝟙 are cartesian 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_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y 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_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y 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_1} [CategoryTheory.Category.{u_2, u_1} 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.