Adjunctions and limits

A left adjoint preserves colimits (CategoryTheory.Adjunction.leftAdjoint_preservesColimits), and a right adjoint preserves limits (CategoryTheory.Adjunction.rightAdjoint_preservesLimits).

Equivalences create and reflect (co)limits. (CategoryTheory.Functor.createsLimitsOfIsEquivalence, CategoryTheory.Functor.createsColimitsOfIsEquivalence, CategoryTheory.Functor.reflectsLimits_of_isEquivalence, CategoryTheory.Functor.reflectsColimits_of_isEquivalence.)

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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J C) : Functor (Limits.Cocone (K.comp F)) (Limits.Cocone K)

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

Auxiliary definition for functorialityAdjunction.

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

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

Auxiliary definition for functorialityAdjunction.

@[simp]

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

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

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

Auxiliary definition for functorialityAdjunction.

@[simp]

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

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

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

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

A left adjoint preserves colimits.

instance CategoryTheory.Adjunction.colim_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] [Limits.HasColimitsOfShape J C] : Limits.PreservesColimits Limits.colim

@[instance 100]

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

@[instance 100]

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

@[implicit_reducible, instance 100]

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

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

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

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

Transport a HasColimitsOfShape instance across an equivalence.

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

Transport a HasColimitsOfSize instance across an equivalence.

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

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

Auxiliary definition for functorialityAdjunction'.

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

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

Auxiliary definition for functorialityAdjunction'.

@[simp]

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

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

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

Auxiliary definition for functorialityAdjunction'.

@[simp]

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

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

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

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

A right adjoint preserves limits.

instance CategoryTheory.Adjunction.lim_preservesLimits {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] [Limits.HasLimitsOfShape J C] : Limits.PreservesLimits Limits.lim

@[instance 100]

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

@[instance 100]

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

@[implicit_reducible, instance 100]

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

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

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

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

Transport a HasLimitsOfShape instance across an equivalence.

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

Transport a HasLimitsOfSize instance across an equivalence.

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

auxiliary construction for coconesIso

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

auxiliary construction for coconesIso

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

auxiliary construction for conesIso

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

auxiliary construction for conesIso

def CategoryTheory.Adjunction.coconesIso {C : Type u₁} [Category.{v₀, u₁} C] {D : Type u₂} [Category.{v₀, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J C} : (cocones J D).obj (Opposite.op (K.comp F)) ≅ G.comp ((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₁} [Category.{v₀, u₁} C] {D : Type u₂} [Category.{v₀, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J D} : F.op.comp ((cones J D).obj K) ≅ (cones J C).obj (K.comp 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.

instance CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] (F : Functor C D) [F.IsLeftAdjoint] : Limits.PreservesColimitsOfShape J F

instance CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint {C : Type u_2} {D : Type u_3} [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] (F : Functor C D) [F.IsLeftAdjoint] : Limits.PreservesColimitsOfSize.{v, u, v_2, v_3, u_2, u_3} F

instance CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] (F : Functor C D) [F.IsRightAdjoint] : Limits.PreservesLimitsOfShape J F

instance CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint {C : Type u_2} {D : Type u_3} [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] (F : Functor C D) [F.IsRightAdjoint] : Limits.PreservesLimitsOfSize.{v, u, v_2, v_3, u_2, u_3} F