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.

def CategoryTheory.Over.pullback {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : Functor (Over Y) (Over X)

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.

@[simp]

theorem CategoryTheory.Over.pullback_obj_hom {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (g : Over Y) : ((pullback f).obj g).hom = Limits.pullback.snd g.hom f

@[simp]

theorem CategoryTheory.Over.pullback_obj_left {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (g : Over Y) : ((pullback f).obj g).left = Limits.pullback g.hom f

@[simp]

theorem CategoryTheory.Over.pullback_map_left {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (g : Over Y) {h : Over Y} {k : g ⟶ h} : ((pullback f).map k).left = Limits.pullback.lift (CategoryStruct.comp (Limits.pullback.fst g.hom f) k.left) (Limits.pullback.snd g.hom f) ⋯

def CategoryTheory.Over.mapPullbackAdj {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : map f ⊣ pullback f

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

Equations

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

@[simp]

theorem CategoryTheory.Over.mapPullbackAdj_unit_app {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (X✝ : Over X) : (mapPullbackAdj f).unit.app X✝ = homMk (Limits.pullback.lift (CategoryStruct.id X✝.left) X✝.hom ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.mapPullbackAdj_counit_app {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) (Y✝ : Over Y) : (mapPullbackAdj f).counit.app Y✝ = homMk (Limits.pullback.fst Y✝.hom f) ⋯

def CategoryTheory.Over.pullbackId {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X : C} : pullback (CategoryStruct.id X) ≅ Functor.id (Over X)

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

Equations

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

def CategoryTheory.Over.pullbackComp {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : pullback (CategoryStruct.comp f g) ≅ (pullback g).comp (pullback f)

pullback commutes with composition (up to natural isomorphism).

Equations

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

instance CategoryTheory.Over.pullbackIsRightAdjoint {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : (pullback f).IsRightAdjoint

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

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

Equations

• CategoryTheory.Over.star X = (CategoryTheory.prodComonad X).cofree.comp (CategoryTheory.coalgebraToOver X)

@[simp]

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

@[simp]

theorem CategoryTheory.Over.star_obj_left {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (X✝ : C) : ((star X).obj X✝).left = (X ⨯ X✝)

@[simp]

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

def CategoryTheory.Over.forgetAdjStar {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] : forget X ⊣ 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.Over.forgetAdjStar X = (CategoryTheory.coalgebraEquivOver X).symm.toAdjunction.comp (CategoryTheory.prodComonad X).adj

instance CategoryTheory.Over.instIsLeftAdjointForgetOfHasBinaryProducts {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] : (forget X).IsLeftAdjoint

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

def CategoryTheory.Under.pushout {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) : Functor (Under X) (Under 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.

@[simp]

theorem CategoryTheory.Under.pushout_map {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) (x : Under X) {x' : Under X} {u : x ⟶ x'} : (pushout f).map u = homMk (Limits.pushout.desc (CategoryStruct.comp u.right (Limits.pushout.inl x'.hom f)) (Limits.pushout.inr x'.hom f) ⋯) ⋯

@[simp]

theorem CategoryTheory.Under.pushout_obj {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) (x : Under X) : (pushout f).obj x = mk (Limits.pushout.inr x.hom f)

def CategoryTheory.Under.mapPushoutAdj {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) : pushout f ⊣ map f

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

Equations

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

@[simp]

theorem CategoryTheory.Under.mapPushoutAdj_unit_app {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) (X✝ : Under X) : (mapPushoutAdj f).unit.app X✝ = homMk (Limits.pushout.inl X✝.hom f) ⋯

@[simp]

theorem CategoryTheory.Under.mapPushoutAdj_counit_app {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) (Y✝ : Under Y) : (mapPushoutAdj f).counit.app Y✝ = homMk (Limits.pushout.desc (CategoryStruct.id Y✝.right) Y✝.hom ⋯) ⋯

def CategoryTheory.Under.pushoutId {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X : C} : pushout (CategoryStruct.id X) ≅ Functor.id (Under X)

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

Equations

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

def CategoryTheory.Under.pullbackComp {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : pushout (CategoryStruct.comp f g) ≅ (pushout f).comp (pushout g)

pushout commutes with composition (up to natural isomorphism).

Equations

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

instance CategoryTheory.Under.pushoutIsLeftAdjoint {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) : (pushout f).IsLeftAdjoint

def CategoryTheory.Under.equivalenceOfIsInitial {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsInitial X) : Under X ≌ C

If X : C is initial, then the under category of X is equivalent to C.

Equations

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