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.

noncomputable def CategoryTheory.leftAdjointOfStructuredArrowInitialsAux {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (G : Functor D C) [∀ (A : C), Limits.HasInitial (StructuredArrow A G)] (A : C) (B : D) : ((⊥_ 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.

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.leftAdjointOfStructuredArrowInitials {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (G : Functor D C) [∀ (A : C), Limits.HasInitial (StructuredArrow A G)] : 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.

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

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

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

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

noncomputable def CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (G : Functor D C) [∀ (A : C), Limits.HasTerminal (CostructuredArrow G A)] (B : D) (A : C) : (G.obj B ⟶ A) ≃ (B ⟶ (⊤_ 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.

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.rightAdjointOfCostructuredArrowTerminals {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (G : Functor D C) [∀ (A : C), Limits.HasTerminal (CostructuredArrow G A)] : 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 adjunctionOfCostructuredArrowTerminals.

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

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

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

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

def CategoryTheory.mkInitialOfLeftAdjoint {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (G : Functor D C) {F : Functor C D} (h : F ⊣ G) (A : C) : Limits.IsInitial (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.

def CategoryTheory.mkTerminalOfRightAdjoint {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (G : Functor D C) {F : Functor C D} (h : F ⊣ G) (A : D) : Limits.IsTerminal (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.

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

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