mathlib documentation

category_theory.adjunction.over

Adjunctions related to the over category #

Construct the left adjoint star X to over.forget X : over X ⥤ C.

TODO #

Show star X itself has a left adjoint provided C is locally cartesian closed.

The functor from C to over X which sends Y : C to π₁ : X ⨯ Y ⟶ X, sometimes denoted X*.

Equations

The functor over.forget X : over X ⥤ C has a right adjoint given by star X.

Note that the binary products assumption is necessary: the existence of a right adjoint to over.forget X is equivalent to the existence of each binary product X ⨯ -.

Equations
@[protected, instance]

Note that the binary products assumption is necessary: the existence of a right adjoint to over.forget X is equivalent to the existence of each binary product X ⨯ -.

Equations