Documentation

Mathlib.CategoryTheory.Adjunction.Limits

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.

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.

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

Auxiliary definition for functorialityIsLeftAdjoint.

Equations
@[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 (K.comp F)) :
((adj.functorialityCounit K).app c).hom = adj.counit.app c.pt

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 := }

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 := }
Equations
  • CategoryTheory.Adjunction.colimPreservesColimits = CategoryTheory.Limits.colimConstAdj.leftAdjointPreservesColimits
@[instance 100]
Equations
  • One or more equations did not get rendered due to their size.
@[instance 100]
Equations
  • One or more equations did not get rendered due to their size.

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.
@[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 (K.comp G)) :
((adj.functorialityUnit' K).app c).hom = adj.unit.app c.pt

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]

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 := }

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 := }
Equations
  • CategoryTheory.Adjunction.limPreservesLimits = CategoryTheory.Limits.constLimAdj.rightAdjointPreservesLimits
@[instance 100]
Equations
  • One or more equations did not get rendered due to their size.
@[instance 100]
Equations
  • One or more equations did not get rendered due to their size.

auxiliary construction for coconesIso

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

auxiliary construction for coconesIso

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

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 := }

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 := }

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 := })

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
Equations
  • F.instPreservesColimitsOfShapeOfIsLeftAdjoint = CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
Equations
Equations
  • F.instPreservesLimitsOfShapeOfIsRightAdjoint = CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
Equations