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] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] : 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_map_left {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] (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) ⋯

@[simp]

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

@[simp]

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

def CategoryTheory.Over.mapPullbackAdj {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] : 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_counit_app {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] (Y✝ : Over Y) : (mapPullbackAdj f).counit.app Y✝ = homMk (Limits.pullback.fst Y✝.hom f) ⋯

@[simp]

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

instance CategoryTheory.Over.faithful_pullback {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] [∀ (Z : C) (g : Z ⟶ Y), Epi (Limits.pullback.fst g f)] : (pullback f).Faithful

The pullback along an epi that's preserved under pullbacks is faithful.

This "preserved under pullbacks" condition is automatically satisfied in abelian categories:

example [Abelian C] [Epi f] : (pullback f).Faithful := inferInstance

def CategoryTheory.Over.pullbackId {C : Type u} [Category.{v, u} 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] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Limits.HasPullbacksAlong f] [Limits.HasPullbacksAlong g] : 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] {X Y : C} (f : X ⟶ Y) [Limits.HasPullbacksAlong f] : (pullback f).IsRightAdjoint

def CategoryTheory.Over.postAdjunctionLeft {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPullbacks C] {X : C} {F : Functor C D} {G : Functor D C} (a : F ⊣ G) : post F ⊣ (post G).comp (pullback (a.unit.app X))

If F is a left adjoint and its source category has pullbacks, then so is post F : Over Y ⥤ Over (G Y).

If the right adjoint of F is G, then the right adjoint of post F is given by (Y ⟶ F X) ↦ (G Y ⟶ X ×_{G F X} G Y ⟶ X).

Equations

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

@[simp]

theorem CategoryTheory.Over.postAdjunctionLeft_counit_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPullbacks C] {X : C} {F : Functor C D} {G : Functor D C} (a : F ⊣ G) (Y : Over ((Functor.id D).obj (F.obj X))) : ((postAdjunctionLeft a).counit.app Y).left = ((((mapPullbackAdj (a.unit.app X)).comp (postAdjunctionRight a)).homEquiv ((pullback (a.unit.app X)).obj (mk (G.map Y.hom))) Y).symm (CategoryStruct.id ((pullback (a.unit.app X)).obj (mk (G.map Y.hom))))).left

@[simp]

theorem CategoryTheory.Over.postAdjunctionLeft_unit_app_left {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPullbacks C] {X : C} {F : Functor C D} {G : Functor D C} (a : F ⊣ G) (X✝ : Over ((Functor.id C).obj X)) : ((postAdjunctionLeft a).unit.app X✝).left = CategoryStruct.comp (Limits.pullback.lift (CategoryStruct.id X✝.left) X✝.hom ⋯) (CategoryStruct.comp (Limits.pullback.lift (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp X✝.hom (a.unit.app X)) (a.unit.app X)) (a.unit.app X✝.left)) (Limits.pullback.snd (CategoryStruct.comp X✝.hom (a.unit.app X)) (a.unit.app X)) ⋯) (Limits.pullback.lift (CategoryStruct.comp (Limits.pullback.fst (G.map (CategoryStruct.comp (F.map (CategoryStruct.comp X✝.hom (a.unit.app X))) (a.counit.app (F.obj X)))) (a.unit.app X)) (G.map ((Adjunction.equivHomsetLeftOfNatIso (NatIso.ofComponents (fun (Y : Over X) => isoMk (Iso.refl (F.obj Y.left)) ⋯) ⋯).symm) (CategoryStruct.id (mk (F.map X✝.hom)))).left)) (Limits.pullback.snd (G.map (CategoryStruct.comp (F.map (CategoryStruct.comp X✝.hom (a.unit.app X))) (a.counit.app (F.obj X)))) (a.unit.app X)) ⋯))

instance CategoryTheory.Over.isLeftAdjoint_post {C : Type u} [Category.{v, u} C] (X : C) {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPullbacks C] {F : Functor C D} [F.IsLeftAdjoint] : (post F).IsLeftAdjoint

noncomputable def CategoryTheory.Over.forgetMapTerminal {C : Type u} [Category.{v, u} C] (X : C) {T : C} (hT : Limits.IsTerminal T) : forget X ≅ (map (hT.from X)).comp (equivalenceOfIsTerminal hT).functor

The category over any object X factors through the category over the terminal object T.

Equations

• CategoryTheory.Over.forgetMapTerminal X hT = CategoryTheory.NatIso.ofComponents (fun (X_1 : CategoryTheory.Over X) => CategoryTheory.Iso.refl ((CategoryTheory.Over.forget X).obj X_1)) ⋯

@[simp]

theorem CategoryTheory.Over.forgetMapTerminal_hom_app {C : Type u} [Category.{v, u} C] (X : C) {T : C} (hT : Limits.IsTerminal T) (X✝ : Over X) : (forgetMapTerminal X hT).hom.app X✝ = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.Over.forgetMapTerminal_inv_app {C : Type u} [Category.{v, u} C] (X : C) {T : C} (hT : Limits.IsTerminal T) (X✝ : Over X) : (forgetMapTerminal X hT).inv.app X✝ = CategoryStruct.id X✝.left

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_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_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_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.instIsRightAdjointStar {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] : (star X).IsRightAdjoint

instance CategoryTheory.Over.instIsLeftAdjointForget {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] {X Y : C} (f : X ⟶ Y) [Limits.HasPushoutsAlong f] : 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_obj {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPushoutsAlong f] (x : Under X) : (pushout f).obj x = mk (Limits.pushout.inr x.hom f)

@[simp]

theorem CategoryTheory.Under.pushout_map {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPushoutsAlong f] (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) ⋯) ⋯

def CategoryTheory.Under.mapPushoutAdj {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPushoutsAlong f] : 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_counit_app {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPushoutsAlong f] (Y✝ : Under Y) : (mapPushoutAdj f).counit.app Y✝ = homMk (Limits.pushout.desc (CategoryStruct.id Y✝.right) Y✝.hom ⋯) ⋯

@[simp]

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

instance CategoryTheory.Under.faithful_pushout {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Limits.HasPushoutsAlong f] [∀ (Z : C) (g : X ⟶ Z), Mono (Limits.pushout.inl g f)] : (pushout f).Faithful

The pushout along a mono that's preserved under pushouts is faithful.

This "preserved under pushouts" condition is automatically satisfied in abelian categories:

example [Abelian C] [Mono f] : (pushout f).Faithful := inferInstance

def CategoryTheory.Under.pushoutId {C : Type u} [Category.{v, u} 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.pushoutComp {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Limits.HasPushoutsAlong f] [Limits.HasPushoutsAlong g] : 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.

@[deprecated CategoryTheory.Under.pushoutComp (since := "2025-04-15")]

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

Alias of CategoryTheory.Under.pushoutComp.

---

pushout commutes with composition (up to natural isomorphism).

Equations

• @CategoryTheory.Under.pullbackComp = @CategoryTheory.Under.pushoutComp

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

def CategoryTheory.Under.postAdjunctionRight {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPushouts D] {Y : D} {F : Functor C D} {G : Functor D C} (a : F ⊣ G) : (post F).comp (pushout (a.counit.app Y)) ⊣ post G

If G is a right adjoint and its source category has pushouts, then so is post G : Under Y ⥤ Under (G Y).

If the left adjoint of G is F, then the left adjoint of post G is given by (G Y ⟶ X) ↦ (Y ⟶ Y ⨿_{F G Y} F X ⟶ F X).

Equations

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

@[simp]

theorem CategoryTheory.Under.postAdjunctionRight_unit_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPushouts D] {Y : D} {F : Functor C D} {G : Functor D C} (a : F ⊣ G) (X : Under ((Functor.id C).obj (G.1 Y))) : ((postAdjunctionRight a).unit.app X).right = ((((postAdjunctionLeft a).comp (mapPushoutAdj (a.counit.app Y))).homEquiv X (mk (Limits.pushout.inr (F.map X.hom) (a.counit.app Y)))) (CategoryStruct.id (mk (Limits.pushout.inr (F.map X.hom) (a.counit.app Y))))).right

@[simp]

theorem CategoryTheory.Under.postAdjunctionRight_counit_app_right {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPushouts D] {Y : D} {F : Functor C D} {G : Functor D C} (a : F ⊣ G) (Y✝ : Under ((Functor.id D).obj Y)) : ((postAdjunctionRight a).counit.app Y✝).right = CategoryStruct.comp (Limits.pushout.desc (CategoryStruct.comp (F.map ((Adjunction.equivHomsetRightOfNatIso (NatIso.ofComponents (fun (Y_1 : Under Y) => isoMk (Iso.refl (G.obj Y_1.right)) ⋯) ⋯)).symm (CategoryStruct.id (mk (G.map Y✝.hom)))).right) (Limits.pushout.inl (F.map (CategoryStruct.comp (a.unit.app (G.1 Y)) (G.map (CategoryStruct.comp (a.counit.app Y) Y✝.hom)))) (a.counit.app Y))) (Limits.pushout.inr (F.map (CategoryStruct.comp (a.unit.app (G.1 Y)) (G.map (CategoryStruct.comp (a.counit.app Y) Y✝.hom)))) (a.counit.app Y)) ⋯) (CategoryStruct.comp (Limits.pushout.desc (CategoryStruct.comp (a.counit.app Y✝.right) (Limits.pushout.inl (CategoryStruct.comp (a.counit.app Y) Y✝.hom) (a.counit.app Y))) (Limits.pushout.inr (CategoryStruct.comp (a.counit.app Y) Y✝.hom) (a.counit.app Y)) ⋯) (Limits.pushout.desc (CategoryStruct.id Y✝.right) Y✝.hom ⋯))

instance CategoryTheory.Under.isRightAdjoint_post {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPushouts D] {Y : D} {G : Functor D C} [G.IsRightAdjoint] : (post G).IsRightAdjoint

noncomputable def CategoryTheory.Under.forgetMapInitial {C : Type u} [Category.{v, u} C] (X : C) {I : C} (hI : Limits.IsInitial I) : forget X ≅ (map (hI.to X)).comp (equivalenceOfIsInitial hI).functor

The category under any object X factors through the category under the initial object I.

Equations

• CategoryTheory.Under.forgetMapInitial X hI = CategoryTheory.NatIso.ofComponents (fun (X_1 : CategoryTheory.Under X) => CategoryTheory.Iso.refl ((CategoryTheory.Under.forget X).obj X_1)) ⋯

@[simp]

theorem CategoryTheory.Under.forgetMapInitial_inv_app {C : Type u} [Category.{v, u} C] (X : C) {I : C} (hI : Limits.IsInitial I) (X✝ : Under X) : (forgetMapInitial X hI).inv.app X✝ = CategoryStruct.id X✝.right

@[simp]

theorem CategoryTheory.Under.forgetMapInitial_hom_app {C : Type u} [Category.{v, u} C] (X : C) {I : C} (hI : Limits.IsInitial I) (X✝ : Under X) : (forgetMapInitial X hI).hom.app X✝ = CategoryStruct.id X✝.right

def CategoryTheory.Under.costar {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] : Functor C (Under X)

The functor from C to Under X which sends Y : C to in₁ : X ⟶ X ⨿ Y.

Equations

• CategoryTheory.Under.costar X = (CategoryTheory.coprodMonad X).free.comp (CategoryTheory.algebraToUnder X)

@[simp]

theorem CategoryTheory.Under.costar_obj_hom {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (X✝ : C) : ((costar X).obj X✝).hom = Limits.coprod.inl

@[simp]

theorem CategoryTheory.Under.costar_obj_left {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (X✝ : C) : ((costar X).obj X✝).left = { as := PUnit.unit }

@[simp]

theorem CategoryTheory.Under.costar_map_left {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((costar X).map f).left = CategoryStruct.id (mk (CategoryStruct.comp Limits.coprod.inl (Limits.coprod.desc Limits.coprod.inl (CategoryStruct.id (X ⨿ X✝))))).left

def CategoryTheory.Under.costarAdjForget {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] : costar X ⊣ forget X

The functor Under.forget X : Under X ⥤ C has a left adjoint given by costar X.

Note that the binary coproducts assumption is necessary: the existence of a left adjoint to Under.forget X is equivalent to the existence of each binary coproduct X ⨿ -.

Equations

• CategoryTheory.Under.costarAdjForget X = (CategoryTheory.coprodMonad X).adj.comp (CategoryTheory.algebraEquivUnder X).toAdjunction

instance CategoryTheory.Under.instIsLeftAdjointCostar {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] : (costar X).IsLeftAdjoint

instance CategoryTheory.Under.instIsRightAdjointForget {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] : (forget X).IsRightAdjoint

Note that the binary coproducts assumption is necessary: the existence of a left adjoint to Under.forget X is equivalent to the existence of each binary coproduct X ⨿ -.