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_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) (g : CategoryTheory.Over Y) : ((CategoryTheory.Over.pullback f).obj g).hom = CategoryTheory.Limits.pullback.snd g.hom f

@[simp]

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

@[simp]

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

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

@[deprecated CategoryTheory.Over.pullback]

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

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

• @CategoryTheory.Over.Limits.baseChange = @CategoryTheory.Over.pullback

@[deprecated CategoryTheory.Over.pullback]

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

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

• @CategoryTheory.Over.baseChange = @CategoryTheory.Over.pullback

@[simp]

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

@[simp]

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

def CategoryTheory.Over.mapPullbackAdj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Over.map f ⊣ CategoryTheory.Over.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.

@[deprecated CategoryTheory.Over.mapPullbackAdj]

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

Alias of CategoryTheory.Over.mapPullbackAdj.

---

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

Equations

• @CategoryTheory.Over.mapAdjunction = @CategoryTheory.Over.mapPullbackAdj

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Over.star {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor C (CategoryTheory.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)

def CategoryTheory.Over.forgetAdjStar {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Over.forget X ⊣ CategoryTheory.Over.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} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.Over.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 ⨯ -.

Equations

• ⋯ = ⋯

@[deprecated CategoryTheory.Over.star]

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

Alias of CategoryTheory.Over.star.

---

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

Equations

• @CategoryTheory.star = @CategoryTheory.Over.star

@[deprecated CategoryTheory.Over.forgetAdjStar]

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

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

• @CategoryTheory.forgetAdjStar = @CategoryTheory.Over.forgetAdjStar

@[simp]

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

@[simp]

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

def CategoryTheory.Under.pushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.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.mapPushoutAdj_unit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] {X : C} {Y : C} (f : X✝ ⟶ Y) (X : CategoryTheory.Under X✝) : (CategoryTheory.Under.mapPushoutAdj f).unit.app X = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.inl X.hom f) ⋯

@[simp]

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

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

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

Equations

• ⋯ = ⋯