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 CategoryTheory.star_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : ((CategoryTheory.star X).obj X).left = (X ⨯ X)

@[simp]

theorem CategoryTheory.star_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.star X).map f).left = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.star_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : ((CategoryTheory.star X).obj X).hom = CategoryTheory.Limits.prod.fst

def CategoryTheory.star {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor C (CategoryTheory.Over X)

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

def CategoryTheory.forgetAdjStar {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Over.forget X ⊣ CategoryTheory.star X

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 ⨯ -.

instance CategoryTheory.instIsLeftAdjointOverInstCategoryOverForget {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.IsLeftAdjoint (CategoryTheory.Over.forget 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 ⨯ -.