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_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) ⋯

@[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 ⋯) ⋯

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

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_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

@[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✝)

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] [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_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)

@[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) ⋯) ⋯

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_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 ⋯) ⋯

@[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) ⋯

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.pushoutComp {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.

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

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)

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] [Limits.HasPushouts C] {X Y : C} (f : X ⟶ Y) : (pushout f).IsLeftAdjoint

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_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

@[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

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