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}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(X_1 : C) :
((category_theory.star X).obj X_1).left = (X ⨯ X_1)
@[simp]
theorem
category_theory.star_obj_hom
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(X_1 : C) :
noncomputable
def
category_theory.star
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products 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}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(_x _x_1 : C)
(f : _x ⟶ _x_1) :
((category_theory.star X).map f).left = category_theory.limits.prod.map (𝟙 X) f
noncomputable
def
category_theory.forget_adj_star
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products 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 ⨯ -
.
@[protected, instance]
noncomputable
def
category_theory.over.forget.is_left_adjoint
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products 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
- category_theory.over.forget.is_left_adjoint X = {right := category_theory.star X _inst_2, adj := category_theory.forget_adj_star X _inst_2}