Adjunctions related to the over category #

In a category with pullbacks, for any morphism f : X ⟶ Y, the functor Over.map f : Over X ⥤ Over Y has a right adjoint Over.pullback f.

In a category with binary products, for any object X the functor Over.forget X : Over X ⥤ C has a right adjoint Over.star X.

Main declarations #

• Over.pullback f : Over Y ⥤ Over X is the functor induced by a morphism f : X ⟶ Y.
• Over.mapPullbackAdj is the adjunction Over.map f ⊣ Over.pullback f.
• star : C ⥤ Over X is the functor induced by an object X.
• forgetAdjStar is the adjunction forget X ⊣ star X.

TODO #

Show star X itself has a right adjoint provided C is cartesian closed and has pullbacks.

@[simp]
theorem CategoryTheory.Over.pullback_obj_left {C : Type u} {X : C} {Y : C} (f : X Y) (g : ) :
(.obj g).left =
@[simp]
theorem CategoryTheory.Over.pullback_map_left {C : Type u} {X : C} {Y : C} (f : X Y) (g : ) {h : } {k : g h} :
(.map k).left =
@[simp]
theorem CategoryTheory.Over.pullback_obj_hom {C : Type u} {X : C} {Y : C} (f : X Y) (g : ) :
(.obj g).hom =
def CategoryTheory.Over.pullback {C : Type u} {X : C} {Y : C} (f : X Y) :

In a category with pullbacks, a morphism f : X ⟶ Y induces a functor Over Y ⥤ Over X, by pulling back a morphism along f.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[deprecated CategoryTheory.Over.pullback]
def CategoryTheory.Over.Limits.baseChange {C : Type u} {X : C} {Y : C} (f : X Y) :

Alias of CategoryTheory.Over.pullback.

In a category with pullbacks, a morphism f : X ⟶ Y induces a functor Over Y ⥤ Over X, by pulling back a morphism along f.

Equations
Instances For
@[deprecated CategoryTheory.Over.pullback]
def CategoryTheory.Over.baseChange {C : Type u} {X : C} {Y : C} (f : X Y) :

Alias of CategoryTheory.Over.pullback.

In a category with pullbacks, a morphism f : X ⟶ Y induces a functor Over Y ⥤ Over X, by pulling back a morphism along f.

Equations
Instances For
@[simp]
theorem CategoryTheory.Over.mapPullbackAdj_counit_app {C : Type u} {X : C} {Y : C} (f : X Y✝) (Y : ) :
.counit.app Y =
@[simp]
theorem CategoryTheory.Over.mapPullbackAdj_unit_app {C : Type u} {X : C} {Y : C} (f : X✝ Y) (X : ) :
.unit.app X =
def CategoryTheory.Over.mapPullbackAdj {C : Type u} {X : C} {Y : C} (f : X Y) :

Over.map f is left adjoint to Over.pullback f.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Over.mapAdjunction {C : Type u} {X : C} {Y : C} (f : X Y) :

Alias of CategoryTheory.Over.mapPullbackAdj.

Over.map f is left adjoint to Over.pullback f.

Equations
Instances For

pullback (𝟙 X) : Over X ⥤ Over X is the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Over.pullbackComp {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

pullback commutes with composition (up to natural isomorphism).

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Over.pullbackIsRightAdjoint {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
@[simp]
theorem CategoryTheory.Over.star_map_left {C : Type u} (X : C) :
∀ {X_1 Y : C} (f : X_1 Y), (.map f).left =
@[simp]
theorem CategoryTheory.Over.star_obj_left {C : Type u} (X : C) (X : C) :
(.obj X).left = (X✝ X)
@[simp]
theorem CategoryTheory.Over.star_obj_hom {C : Type u} (X : C) (X : C) :
(.obj X).hom = CategoryTheory.Limits.prod.fst
def CategoryTheory.Over.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
• = .cofree.comp
Instances For

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
Instances For

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
• =
@[deprecated CategoryTheory.Over.star]
def CategoryTheory.star {C : Type u} (X : C) :

Alias of CategoryTheory.Over.star.

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

Equations
Instances For

Alias of CategoryTheory.Over.forgetAdjStar.

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
Instances For
@[simp]
theorem CategoryTheory.Under.pushout_obj {C : Type u} {X : C} {Y : C} (f : X Y) (x : ) :
def CategoryTheory.Under.pushout {C : Type u} {X : C} {Y : C} (f : X Y) :

When C has pushouts, a morphism f : X ⟶ Y induces a functor Under X ⥤ Under Y, by pushing a morphism forward along f.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Under.mapPushoutAdj_unit_app {C : Type u} {X : C} {Y : C} (f : X✝ Y) (X : ) :
.unit.app X =
@[simp]
theorem CategoryTheory.Under.mapPushoutAdj_counit_app {C : Type u} {X : C} {Y : C} (f : X Y✝) (Y : ) :
.counit.app Y =
def CategoryTheory.Under.mapPushoutAdj {C : Type u} {X : C} {Y : C} (f : X Y) :

Under.pushout f is left adjoint to Under.map f.

Equations
• One or more equations did not get rendered due to their size.
Instances For

pushout (𝟙 X) : Under X ⥤ Under X is the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Under.pullbackComp {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

pushout commutes with composition (up to natural isomorphism).

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Under.pushoutIsLeftAdjoint {C : Type u} {X : C} {Y : C} (f : X Y) :