# Documentation

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₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (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.
Instances For
@[simp]
theorem CategoryTheory.Adjunction.functorialityUnit_app_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) (c : ) :
def CategoryTheory.Adjunction.functorialityUnit {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (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 : ) => { hom := adj.unit.app c.pt, w := }, naturality := }
Instances For
@[simp]
theorem CategoryTheory.Adjunction.functorialityCounit_app_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) (c : CategoryTheory.Limits.Cocone (K.comp F)) :
def CategoryTheory.Adjunction.functorialityCounit {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) :

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 := }
Instances For
def CategoryTheory.Adjunction.functorialityAdjunction {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) :

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

Equations
Instances For
def CategoryTheory.Adjunction.leftAdjointPreservesColimits {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) :

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[instance 100]
noncomputable instance CategoryTheory.Adjunction.isEquivalencePreservesColimits {C : Type u₁} [] {D : Type u₂} [] (E : ) [E.IsEquivalence] :
Equations
@[instance 100]
noncomputable instance CategoryTheory.Adjunction.isEquivalenceReflectsColimits {C : Type u₁} [] {D : Type u₂} [] (E : ) [E.IsEquivalence] :
Equations
• One or more equations did not get rendered due to their size.
@[instance 100]
noncomputable instance CategoryTheory.Adjunction.isEquivalenceCreatesColimits {C : Type u₁} [] {D : Type u₂} [] (H : ) [H.IsEquivalence] :
Equations
• One or more equations did not get rendered due to their size.
theorem CategoryTheory.Adjunction.hasColimit_comp_equivalence {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (K : ) (E : ) [E.IsEquivalence] :
theorem CategoryTheory.Adjunction.hasColimit_of_comp_equivalence {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (K : ) (E : ) [E.IsEquivalence] [CategoryTheory.Limits.HasColimit (K.comp E)] :
theorem CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (E : ) [E.IsEquivalence] :

Transport a HasColimitsOfShape instance across an equivalence.

theorem CategoryTheory.Adjunction.has_colimits_of_equivalence {C : Type u₁} [] {D : Type u₂} [] (E : ) [E.IsEquivalence] [] :

Transport a HasColimitsOfSize instance across an equivalence.

def CategoryTheory.Adjunction.functorialityLeftAdjoint {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (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.
Instances For
@[simp]
theorem CategoryTheory.Adjunction.functorialityUnit'_app_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) (c : CategoryTheory.Limits.Cone (K.comp G)) :
def CategoryTheory.Adjunction.functorialityUnit' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) :

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 := }
Instances For
@[simp]
theorem CategoryTheory.Adjunction.functorialityCounit'_app_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) (c : ) :
def CategoryTheory.Adjunction.functorialityCounit' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (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 : ) => { hom := adj.counit.app c.pt, w := }, naturality := }
Instances For
def CategoryTheory.Adjunction.functorialityAdjunction' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} (K : ) :

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

Equations
Instances For
def CategoryTheory.Adjunction.rightAdjointPreservesLimits {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) :

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[instance 100]
noncomputable instance CategoryTheory.Adjunction.isEquivalencePreservesLimits {C : Type u₁} [] {D : Type u₂} [] (E : ) [E.IsEquivalence] :
Equations
@[instance 100]
noncomputable instance CategoryTheory.Adjunction.isEquivalenceReflectsLimits {C : Type u₁} [] {D : Type u₂} [] (E : ) [E.IsEquivalence] :
Equations
• One or more equations did not get rendered due to their size.
@[instance 100]
noncomputable instance CategoryTheory.Adjunction.isEquivalenceCreatesLimits {C : Type u₁} [] {D : Type u₂} [] (H : ) [H.IsEquivalence] :
Equations
• One or more equations did not get rendered due to their size.
theorem CategoryTheory.Adjunction.hasLimit_comp_equivalence {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (K : ) (E : ) [E.IsEquivalence] :
theorem CategoryTheory.Adjunction.hasLimit_of_comp_equivalence {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (K : ) (E : ) [E.IsEquivalence] [CategoryTheory.Limits.HasLimit (K.comp E)] :
theorem CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (E : ) [E.IsEquivalence] :

Transport a HasLimitsOfShape instance across an equivalence.

theorem CategoryTheory.Adjunction.has_limits_of_equivalence {C : Type u₁} [] {D : Type u₂} [] (E : ) [E.IsEquivalence] [] :

Transport a HasLimitsOfSize instance across an equivalence.

def CategoryTheory.Adjunction.coconesIsoComponentHom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} {K : } (Y : D) (t : (().obj { unop := K.comp F }).obj Y) :
(G.comp (().obj { unop := 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 := }
Instances For
def CategoryTheory.Adjunction.coconesIsoComponentInv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} {K : } (Y : D) (t : (G.comp (().obj { unop := K })).obj Y) :
(().obj { unop := 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 := }
Instances For
def CategoryTheory.Adjunction.conesIsoComponentHom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} {K : } (X : Cᵒᵖ) (t : (F.op.comp (().obj K)).obj X) :
(().obj (K.comp G)).obj X

auxiliary construction for conesIso

Equations
• adj.conesIsoComponentHom X t = { app := fun (j : J) => (adj.homEquiv X.unop (K.obj j)) (t.app j), naturality := }
Instances For
def CategoryTheory.Adjunction.conesIsoComponentInv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} {K : } (X : Cᵒᵖ) (t : (().obj (K.comp G)).obj X) :
(F.op.comp (().obj K)).obj X

auxiliary construction for conesIso

Equations
• adj.conesIsoComponentInv X t = { app := fun (j : J) => (adj.homEquiv X.unop (K.obj j)).symm (t.app j), naturality := }
Instances For
def CategoryTheory.Adjunction.coconesIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} {K : } :
().obj { unop := K.comp F } G.comp (().obj { unop := 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 := })
Instances For
def CategoryTheory.Adjunction.conesIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (adj : F G) {J : Type u} {K : } :
F.op.comp (().obj K) ().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
Instances For
noncomputable instance CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint {J : Type u_1} {C : Type u_2} {D : Type u_3} [] [] [] (F : ) [F.IsLeftAdjoint] :
Equations