# 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 structured_arrow category on G is equivalent to a left adjoint to G, as well as the dual.

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

The duals are also shown.

@[simp]
theorem category_theory.left_adjoint_of_structured_arrow_initials_aux_apply {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] (A : C) (B : D) (g : B) :
@[simp]
theorem category_theory.left_adjoint_of_structured_arrow_initials_aux_symm_apply {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] (A : C) (B : D) (f : A G.obj B) :
noncomputable def category_theory.left_adjoint_of_structured_arrow_initials_aux {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] (A : C) (B : D) :
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
noncomputable def category_theory.left_adjoint_of_structured_arrow_initials {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] :
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 adjunction_of_structured_arrow_initials.

Equations
noncomputable def category_theory.adjunction_of_structured_arrow_initials {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] :

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

Equations
noncomputable def category_theory.is_right_adjoint_of_structured_arrow_initials {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] :

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

Equations
noncomputable def category_theory.right_adjoint_of_costructured_arrow_terminals_aux {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] (B : D) (A : C) :
(G.obj B A) (B

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
@[simp]
theorem category_theory.right_adjoint_of_costructured_arrow_terminals_aux_apply {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] (B : D) (A : C) (g : G.obj B A) :
@[simp]
theorem category_theory.right_adjoint_of_costructured_arrow_terminals_aux_symm_apply {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] (B : D) (A : C) (g : B ) :
noncomputable def category_theory.right_adjoint_of_costructured_arrow_terminals {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] :
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 adjunction_of_structured_arrow_initials.

Equations
noncomputable def category_theory.adjunction_of_costructured_arrow_terminals {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] :

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

Equations
noncomputable def category_theory.is_right_adjoint_of_costructured_arrow_terminals {C : Type u₁} {D : Type u₂} (G : D C) [∀ (A : C), ] :

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

Equations
def category_theory.mk_initial_of_left_adjoint {C : Type u₁} {D : Type u₂} (G : D C) {F : C D} (h : F G) (A : C) :

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

Equations
def category_theory.mk_terminal_of_right_adjoint {C : Type u₁} {D : Type u₂} (G : D C) {F : C D} (h : F G) (A : D) :

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

Equations