# 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_obj_left {C : Type u} (X : C) (X_1 : C) :
.obj X_1).left = (X X_1)
@[simp]
theorem category_theory.star_map_right_down_down {C : Type u} (X : C) (_x _x_1 : C) (f : _x _x_1) :
_ = _
@[simp]
theorem category_theory.star_obj_hom {C : Type u} (X : C) (X_1 : C) :
@[simp]
theorem category_theory.star_obj_right {C : Type u} (X : C) (X_1 : C) :
noncomputable def category_theory.star {C : Type u} (X : C)  :

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

Equations
@[simp]
theorem category_theory.star_map_left {C : Type u} (X : C) (_x _x_1 : C) (f : _x _x_1) :
.map f).left =
noncomputable def category_theory.forget_adj_star {C : Type u} (X : C)  :

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]
noncomputable def category_theory.over.forget.is_left_adjoint {C : Type u} (X : C)  :

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