Adjunctions related to the over category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}