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 Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F).

Auxiliary definition for functorialityIsLeftAdjoint.

Equations

• One or more equations did not get rendered due to their size.

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.Cocones.functoriality K F).comp (adj.functorialityRightAdjoint K)

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

Auxiliary definition for functorialityIsLeftAdjoint.

Equations

• adj.functorialityUnit K = { app := fun (c : CategoryTheory.Limits.Cocone K) => { hom := adj.unit.app c.pt, w := ⋯ }, naturality := ⋯ }

@[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.Cocones.functoriality K F) ⟶ Functor.id (Limits.Cocone (K.comp F))

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

Auxiliary definition for functorialityIsLeftAdjoint.

Equations

• adj.functorialityCounit K = { app := fun (c : CategoryTheory.Limits.Cocone (K.comp F)) => { hom := adj.counit.app c.pt, w := ⋯ }, naturality := ⋯ }

@[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.Cocones.functoriality K F ⊣ adj.functorialityRightAdjoint K

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

Equations

• adj.functorialityAdjunction K = { unit := adj.functorialityUnit K, counit := adj.functorialityCounit K, left_triangle_components := ⋯, right_triangle_components := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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 Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G).

Auxiliary definition for functorialityIsRightAdjoint.

Equations

• One or more equations did not get rendered due to their size.

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.Cones.functoriality K G)

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

Auxiliary definition for functorialityIsRightAdjoint.

Equations

• adj.functorialityUnit' K = { app := fun (c : CategoryTheory.Limits.Cone (K.comp G)) => { hom := adj.unit.app c.pt, w := ⋯ }, naturality := ⋯ }

@[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.Cones.functoriality K G).comp (adj.functorialityLeftAdjoint K) ⟶ Functor.id (Limits.Cone K)

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

Auxiliary definition for functorialityIsRightAdjoint.

Equations

• adj.functorialityCounit' K = { app := fun (c : CategoryTheory.Limits.Cone K) => { hom := adj.counit.app c.pt, w := ⋯ }, naturality := ⋯ }

@[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.Cones.functoriality K G

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

Equations

• adj.functorialityAdjunction' K = { unit := adj.functorialityUnit' K, counit := adj.functorialityCounit' K, left_triangle_components := ⋯, right_triangle_components := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• adj.coconesIsoComponentHom Y t = { app := fun (j : J) => (adj.homEquiv (K.obj j) Y) (t.app j), naturality := ⋯ }

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

Equations

• adj.coconesIsoComponentInv Y t = { app := fun (j : J) => (adj.homEquiv (K.obj j) Y).symm (t.app j), naturality := ⋯ }

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

Equations

• adj.conesIsoComponentHom X t = { app := fun (j : J) => (adj.homEquiv (Opposite.unop X) (K.obj j)) (t.app j), naturality := ⋯ }

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

Equations

• adj.conesIsoComponentInv X t = { app := fun (j : J) => (adj.homEquiv (Opposite.unop X) (K.obj j)).symm (t.app j), naturality := ⋯ }

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.

Equations

• adj.coconesIso = CategoryTheory.NatIso.ofComponents (fun (Y : D) => { hom := adj.coconesIsoComponentHom Y, inv := adj.coconesIsoComponentInv Y, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯

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.

Equations

• adj.conesIso = CategoryTheory.NatIso.ofComponents (fun (X : Cᵒᵖ) => { hom := adj.conesIsoComponentHom X, inv := adj.conesIsoComponentInv X, hom_inv_id := ⋯, inv_hom_id := ⋯ }) ⋯

instance CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_6, u_1} J] [Category.{u_4, u_2} C] [Category.{u_5, 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.{u_4, u_2} C] [Category.{u_5, u_3} D] (F : Functor C D) [F.IsLeftAdjoint] : Limits.PreservesColimitsOfSize.{v, u, u_4, u_5, u_2, u_3} F

instance CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_6, u_1} J] [Category.{u_5, u_2} C] [Category.{u_4, 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.{u_5, u_2} C] [Category.{u_4, u_3} D] (F : Functor C D) [F.IsRightAdjoint] : Limits.PreservesLimitsOfSize.{v, u, u_5, u_4, u_2, u_3} F