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.

@[simp]
theorem category_theory.star_map_right_down_down {C : Type u} [category_theory.category C] (X : C) [category_theory.limits.has_binary_products C] (_x _x_1 : C) (f : _x _x_1) :
_ = _

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
@[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