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_1 Y : C} (f : X_1 ⟶ 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*.

Equations

• CategoryTheory.star X = CategoryTheory.Functor.comp (CategoryTheory.Comonad.cofree (CategoryTheory.prodComonad X)) (CategoryTheory.coalgebraToOver 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 ⨯ -.

Equations

• CategoryTheory.forgetAdjStar X = CategoryTheory.Adjunction.comp (CategoryTheory.coalgebraEquivOver X).symm.toAdjunction (CategoryTheory.Comonad.adj (CategoryTheory.prodComonad 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 ⨯ -.

Equations

• CategoryTheory.instIsLeftAdjointOverInstCategoryOverForget X = { right := CategoryTheory.star X, adj := CategoryTheory.forgetAdjStar X }