Properties of comma categories relating to adjunctions

This file shows that for a functor G : D ⥤ C the data of an initial object in each StructuredArrow category on G is equivalent to a left adjoint to G, as well as the dual.

Specifically, adjunctionOfStructuredArrowInitials gives the left adjoint assuming the appropriate initial objects exist, and mkInitialOfLeftAdjoint constructs the initial objects provided a left adjoint.

The duals are also shown.

@[simp]

theorem CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_symm_apply {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D) (f : A ⟶ G.obj B) : (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B).symm f = (CategoryTheory.Limits.initial.to (CategoryTheory.StructuredArrow.mk f)).right

@[simp]

theorem CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_apply {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D) (g : (⊥_ CategoryTheory.StructuredArrow A G).right ⟶ B) : (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B) g = CategoryTheory.CategoryStruct.comp (⊥_ CategoryTheory.StructuredArrow A G).hom (G.map g)

def CategoryTheory.leftAdjointOfStructuredArrowInitialsAux {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] (A : C) (B : D) : ((⊥_ CategoryTheory.StructuredArrow A G).right ⟶ B) ≃ (A ⟶ G.obj B)

Implementation: If each structured arrow category on G has an initial object, an equivalence which is helpful for constructing a left adjoint to G.

Equations

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

def CategoryTheory.leftAdjointOfStructuredArrowInitials {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] : CategoryTheory.Functor C D

If each structured arrow category on G has an initial object, construct a left adjoint to G. It is shown that it is a left adjoint in adjunctionOfStructuredArrowInitials.

Equations

• CategoryTheory.leftAdjointOfStructuredArrowInitials G = CategoryTheory.Adjunction.leftAdjointOfEquiv (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G) ⋯

def CategoryTheory.adjunctionOfStructuredArrowInitials {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] : CategoryTheory.leftAdjointOfStructuredArrowInitials G ⊣ G

If each structured arrow category on G has an initial object, we have a constructed left adjoint to G.

Equations

• CategoryTheory.adjunctionOfStructuredArrowInitials G = CategoryTheory.Adjunction.adjunctionOfEquivLeft (CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G) ⋯

def CategoryTheory.isRightAdjointOfStructuredArrowInitials {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] : CategoryTheory.IsRightAdjoint G

If each structured arrow category on G has an initial object, G is a right adjoint.

Equations

• CategoryTheory.isRightAdjointOfStructuredArrowInitials G = { left := CategoryTheory.leftAdjointOfStructuredArrowInitials G, adj := CategoryTheory.adjunctionOfStructuredArrowInitials G }

@[simp]

theorem CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_apply {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C) (g : G.obj B ⟶ A) : (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A) g = (CategoryTheory.Limits.terminal.from (CategoryTheory.CostructuredArrow.mk g)).left

@[simp]

theorem CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_symm_apply {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C) (g : B ⟶ (⊤_ CategoryTheory.CostructuredArrow G A).left) : (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A).symm g = CategoryTheory.CategoryStruct.comp (G.map g) (⊤_ CategoryTheory.CostructuredArrow G A).hom

def CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] (B : D) (A : C) : (G.obj B ⟶ A) ≃ (B ⟶ (⊤_ CategoryTheory.CostructuredArrow G A).left)

Implementation: If each costructured arrow category on G has a terminal object, an equivalence which is helpful for constructing a right adjoint to G.

Equations

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

def CategoryTheory.rightAdjointOfCostructuredArrowTerminals {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] : CategoryTheory.Functor C D

If each costructured arrow category on G has a terminal object, construct a right adjoint to G. It is shown that it is a right adjoint in adjunctionOfStructuredArrowInitials.

Equations

• CategoryTheory.rightAdjointOfCostructuredArrowTerminals G = CategoryTheory.Adjunction.rightAdjointOfEquiv (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G) ⋯

def CategoryTheory.adjunctionOfCostructuredArrowTerminals {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] : G ⊣ CategoryTheory.rightAdjointOfCostructuredArrowTerminals G

If each costructured arrow category on G has a terminal object, we have a constructed right adjoint to G.

Equations

• CategoryTheory.adjunctionOfCostructuredArrowTerminals G = CategoryTheory.Adjunction.adjunctionOfEquivRight (CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G) ⋯

def CategoryTheory.isLeftAdjointOfCostructuredArrowTerminals {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) [∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)] : CategoryTheory.IsLeftAdjoint G

If each costructured arrow category on G has a terminal object, G is a left adjoint.

Equations

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

def CategoryTheory.mkInitialOfLeftAdjoint {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) {F : CategoryTheory.Functor C D} (h : F ⊣ G) (A : C) : CategoryTheory.Limits.IsInitial (CategoryTheory.StructuredArrow.mk (h.unit.app A))

Given a left adjoint to G, we can construct an initial object in each structured arrow category on G.

Equations

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

def CategoryTheory.mkTerminalOfRightAdjoint {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) {F : CategoryTheory.Functor C D} (h : F ⊣ G) (A : D) : CategoryTheory.Limits.IsTerminal (CategoryTheory.CostructuredArrow.mk (h.counit.app A))

Given a right adjoint to F, we can construct a terminal object in each costructured arrow category on F.

Equations

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

theorem CategoryTheory.nonempty_isRightAdjoint_iff_hasInitial_structuredArrow {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} : Nonempty (CategoryTheory.IsRightAdjoint G) ↔ ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)

theorem CategoryTheory.nonempty_isLeftAdjoint_iff_hasTerminal_costructuredArrow {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : Nonempty (CategoryTheory.IsLeftAdjoint F) ↔ ∀ (A : D), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow F A)