Documentation

Poly.Exponentiable

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:

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

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

The conjugate isomorphism between pushforward functors.

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

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

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