Adjunctions and limits

A left adjoint preserves colimits (CategoryTheory.Adjunction.leftAdjointPreservesColimits), and a right adjoint preserves limits (CategoryTheory.Adjunction.rightAdjointPreservesLimits).

Equivalences create and reflect (co)limits. (CategoryTheory.Adjunction.isEquivalenceCreatesLimits, CategoryTheory.Adjunction.isEquivalenceCreatesColimits, CategoryTheory.Adjunction.isEquivalenceReflectsLimits, CategoryTheory.Adjunction.isEquivalenceReflectsColimits,)

In CategoryTheory.Adjunction.coconesIso we show that when F ⊣ G, the functor associating to each Y the cocones over K ⋙ F with cone point Y is naturally isomorphic to the functor associating to each Y the cocones over K with cone point G.obj Y.

def CategoryTheory.Adjunction.functorialityRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp K F)) (CategoryTheory.Limits.Cocone K)

The right adjoint of Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F).

Auxiliary definition for functorialityIsLeftAdjoint.

@[simp]

theorem CategoryTheory.Adjunction.functorialityUnit_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone K) : ((CategoryTheory.Adjunction.functorialityUnit adj K).app c).hom = adj.unit.app c.pt

def CategoryTheory.Adjunction.functorialityUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) : CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone K) ⟶ CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocones.functoriality K F) (CategoryTheory.Adjunction.functorialityRightAdjoint adj K)

The unit for the adjunction for Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F).

Auxiliary definition for functorialityIsLeftAdjoint.

@[simp]

theorem CategoryTheory.Adjunction.functorialityCounit_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp K F)) : ((CategoryTheory.Adjunction.functorialityCounit adj K).app c).hom = adj.counit.app c.pt

def CategoryTheory.Adjunction.functorialityCounit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) : CategoryTheory.Functor.comp (CategoryTheory.Adjunction.functorialityRightAdjoint adj K) (CategoryTheory.Limits.Cocones.functoriality K F) ⟶ CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp K F))

The counit for the adjunction for Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F).

Auxiliary definition for functorialityIsLeftAdjoint.

def CategoryTheory.Adjunction.functorialityIsLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) : CategoryTheory.IsLeftAdjoint (CategoryTheory.Limits.Cocones.functoriality K F)

The functor Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F) is a left adjoint.

def CategoryTheory.Adjunction.leftAdjointPreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} F

A left adjoint preserves colimits.

See https://stacks.math.columbia.edu/tag/0038.

instance CategoryTheory.Adjunction.isEquivalencePreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence E] : CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} E

instance CategoryTheory.Adjunction.isEquivalenceReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence E] : CategoryTheory.Limits.ReflectsColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E

instance CategoryTheory.Adjunction.isEquivalenceCreatesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (H : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence H] : CategoryTheory.CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H

theorem CategoryTheory.Adjunction.hasColimit_comp_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (E : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasColimit K] : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp K E)

theorem CategoryTheory.Adjunction.hasColimit_of_comp_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (E : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp K E)] : CategoryTheory.Limits.HasColimit K

theorem CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (E : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasColimitsOfShape J D] : CategoryTheory.Limits.HasColimitsOfShape J C

Transport a HasColimitsOfShape instance across an equivalence.

theorem CategoryTheory.Adjunction.has_colimits_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D] : CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C

Transport a HasColimitsOfSize instance across an equivalence.

def CategoryTheory.Adjunction.functorialityLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) : CategoryTheory.Functor (CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K G)) (CategoryTheory.Limits.Cone K)

The left adjoint of Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G).

Auxiliary definition for functorialityIsRightAdjoint.

@[simp]

theorem CategoryTheory.Adjunction.functorialityUnit'_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K G)) : ((CategoryTheory.Adjunction.functorialityUnit' adj K).app c).hom = adj.unit.app c.pt

def CategoryTheory.Adjunction.functorialityUnit' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) : CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K G)) ⟶ CategoryTheory.Functor.comp (CategoryTheory.Adjunction.functorialityLeftAdjoint adj K) (CategoryTheory.Limits.Cones.functoriality K G)

The unit for the adjunction for Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G).

Auxiliary definition for functorialityIsRightAdjoint.

@[simp]

theorem CategoryTheory.Adjunction.functorialityCounit'_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (c : CategoryTheory.Limits.Cone K) : ((CategoryTheory.Adjunction.functorialityCounit' adj K).app c).hom = adj.counit.app c.pt

def CategoryTheory.Adjunction.functorialityCounit' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cones.functoriality K G) (CategoryTheory.Adjunction.functorialityLeftAdjoint adj K) ⟶ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone K)

The counit for the adjunction for Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G).

Auxiliary definition for functorialityIsRightAdjoint.

def CategoryTheory.Adjunction.functorialityIsRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) : CategoryTheory.IsRightAdjoint (CategoryTheory.Limits.Cones.functoriality K G)

The functor Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G) is a right adjoint.

def CategoryTheory.Adjunction.rightAdjointPreservesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} G

A right adjoint preserves limits.

See https://stacks.math.columbia.edu/tag/0038.

instance CategoryTheory.Adjunction.isEquivalencePreservesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence E] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E

instance CategoryTheory.Adjunction.isEquivalenceReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence E] : CategoryTheory.Limits.ReflectsLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E

instance CategoryTheory.Adjunction.isEquivalenceCreatesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (H : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence H] : CategoryTheory.CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H

theorem CategoryTheory.Adjunction.hasLimit_comp_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (E : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasLimit K] : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp K E)

theorem CategoryTheory.Adjunction.hasLimit_of_comp_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (E : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp K E)] : CategoryTheory.Limits.HasLimit K

theorem CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (E : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J D

Transport a HasLimitsOfShape instance across an equivalence.

theorem CategoryTheory.Adjunction.has_limits_of_equivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [CategoryTheory.IsEquivalence E] [CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C] : CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D

Transport a HasLimitsOfSize instance across an equivalence.

def CategoryTheory.Adjunction.coconesIsoComponentHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J C} (Y : D) (t : ((CategoryTheory.cocones J D).obj (Opposite.op (CategoryTheory.Functor.comp K F))).obj Y) : (CategoryTheory.Functor.comp G ((CategoryTheory.cocones J C).obj (Opposite.op K))).obj Y

auxiliary construction for coconesIso

def CategoryTheory.Adjunction.coconesIsoComponentInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J C} (Y : D) (t : (CategoryTheory.Functor.comp G ((CategoryTheory.cocones J C).obj (Opposite.op K))).obj Y) : ((CategoryTheory.cocones J D).obj (Opposite.op (CategoryTheory.Functor.comp K F))).obj Y

auxiliary construction for coconesIso

def CategoryTheory.Adjunction.conesIsoComponentHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J D} (X : Cᵒᵖ) (t : (CategoryTheory.Functor.comp F.op ((CategoryTheory.cones J D).obj K)).obj X) : ((CategoryTheory.cones J C).obj (CategoryTheory.Functor.comp K G)).obj X

auxiliary construction for conesIso

def CategoryTheory.Adjunction.conesIsoComponentInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J D} (X : Cᵒᵖ) (t : ((CategoryTheory.cones J C).obj (CategoryTheory.Functor.comp K G)).obj X) : (CategoryTheory.Functor.comp F.op ((CategoryTheory.cones J D).obj K)).obj X

auxiliary construction for conesIso

def CategoryTheory.Adjunction.coconesIso {C : Type u₁} [CategoryTheory.Category.{v₀, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₀, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J C} : (CategoryTheory.cocones J D).obj (Opposite.op (CategoryTheory.Functor.comp K F)) ≅ CategoryTheory.Functor.comp G ((CategoryTheory.cocones J C).obj (Opposite.op K))

When F ⊣ G, the functor associating to each Y the cocones over K ⋙ F with cone point Y is naturally isomorphic to the functor associating to each Y the cocones over K with cone point G.obj Y.

def CategoryTheory.Adjunction.conesIso {C : Type u₁} [CategoryTheory.Category.{v₀, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₀, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u} [CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J D} : CategoryTheory.Functor.comp F.op ((CategoryTheory.cones J D).obj K) ≅ (CategoryTheory.cones J C).obj (CategoryTheory.Functor.comp K G)

When F ⊣ G, the functor associating to each X the cones over K with cone point F.op.obj X is naturally isomorphic to the functor associating to each X the cones over K ⋙ G with cone point X.