Mathlib.CategoryTheory.Comma.Over.Pullback

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.

source

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.

Instances For

source

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

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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

source

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.

Instances For

source

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.

Instances For

source

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

(pullback f).IsRightAdjoint

source

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.

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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)

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

(star X).IsRightAdjoint

source

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

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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

source

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.

Instances For

source

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.

Instances For

source

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

Instances For

source

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

(pushout f).IsLeftAdjoint

source

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.

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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)

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

(costar X).IsLeftAdjoint

source

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

Adjunctions related to the over category #

Main declarations #

TODO #