mathlib3 documentation

category_theory.adjunction.comma

Properties of comma categories relating to adjunctions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G)] (A : C) (B : D) (g : (⊥_ category_theory.structured_arrow A G).right ⟶ B) :

⇑(category_theory.left_adjoint_of_structured_arrow_initials_aux G A B) g = (⊥_ category_theory.structured_arrow A G).hom ≫ G.map g

@[simp]

theorem category_theory.left_adjoint_of_structured_arrow_initials_aux_symm_apply {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G)] (A : C) (B : D) (f : A ⟶ G.obj B) :

⇑((category_theory.left_adjoint_of_structured_arrow_initials_aux G A B).symm) f = (category_theory.limits.initial.to (category_theory.structured_arrow.mk f)).right

noncomputable def category_theory.left_adjoint_of_structured_arrow_initials_aux {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G)] (A : C) (B : D) :

((⊥_ category_theory.structured_arrow 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

category_theory.left_adjoint_of_structured_arrow_initials_aux G A B = {to_fun := λ (g : (⊥_ category_theory.structured_arrow A G).right ⟶ B), (⊥_ category_theory.structured_arrow A G).hom ≫ G.map g, inv_fun := λ (f : A ⟶ G.obj B), (category_theory.limits.initial.to (category_theory.structured_arrow.mk f)).right, left_inv := _, right_inv := _}

noncomputable def category_theory.left_adjoint_of_structured_arrow_initials {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G)] :

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

category_theory.left_adjoint_of_structured_arrow_initials G = category_theory.adjunction.left_adjoint_of_equiv (category_theory.left_adjoint_of_structured_arrow_initials_aux G) _

noncomputable def category_theory.adjunction_of_structured_arrow_initials {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G)] :

category_theory.left_adjoint_of_structured_arrow_initials G ⊣ G

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

Equations

category_theory.adjunction_of_structured_arrow_initials G = category_theory.adjunction.adjunction_of_equiv_left (category_theory.left_adjoint_of_structured_arrow_initials_aux G) _

noncomputable def category_theory.is_right_adjoint_of_structured_arrow_initials {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G)] :

category_theory.is_right_adjoint G

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

Equations

category_theory.is_right_adjoint_of_structured_arrow_initials G = {left := category_theory.left_adjoint_of_structured_arrow_initials G _, adj := category_theory.adjunction_of_structured_arrow_initials G _}

noncomputable def category_theory.right_adjoint_of_costructured_arrow_terminals_aux {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_terminal (category_theory.costructured_arrow G A)] (B : D) (A : C) :

(G.obj B ⟶ A) ≃ (B ⟶ (⊤_ category_theory.costructured_arrow 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

category_theory.right_adjoint_of_costructured_arrow_terminals_aux G B A = {to_fun := λ (g : G.obj B ⟶ A), (category_theory.limits.terminal.from (category_theory.costructured_arrow.mk g)).left, inv_fun := λ (g : B ⟶ (⊤_ category_theory.costructured_arrow G A).left), G.map g ≫ (⊤_ category_theory.costructured_arrow G A).hom, left_inv := _, right_inv := _}

@[simp]

theorem category_theory.right_adjoint_of_costructured_arrow_terminals_aux_apply {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_terminal (category_theory.costructured_arrow G A)] (B : D) (A : C) (g : G.obj B ⟶ A) :

⇑(category_theory.right_adjoint_of_costructured_arrow_terminals_aux G B A) g = (category_theory.limits.terminal.from (category_theory.costructured_arrow.mk g)).left

@[simp]

theorem category_theory.right_adjoint_of_costructured_arrow_terminals_aux_symm_apply {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_terminal (category_theory.costructured_arrow G A)] (B : D) (A : C) (g : B ⟶ (⊤_ category_theory.costructured_arrow G A).left) :

⇑((category_theory.right_adjoint_of_costructured_arrow_terminals_aux G B A).symm) g = G.map g ≫ (⊤_ category_theory.costructured_arrow G A).hom

noncomputable def category_theory.right_adjoint_of_costructured_arrow_terminals {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_terminal (category_theory.costructured_arrow G A)] :

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

category_theory.right_adjoint_of_costructured_arrow_terminals G = category_theory.adjunction.right_adjoint_of_equiv (category_theory.right_adjoint_of_costructured_arrow_terminals_aux G) _

noncomputable def category_theory.adjunction_of_costructured_arrow_terminals {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_terminal (category_theory.costructured_arrow G A)] :

G ⊣ category_theory.right_adjoint_of_costructured_arrow_terminals G

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

Equations

category_theory.adjunction_of_costructured_arrow_terminals G = category_theory.adjunction.adjunction_of_equiv_right (category_theory.right_adjoint_of_costructured_arrow_terminals_aux G) _

noncomputable def category_theory.is_left_adjoint_of_costructured_arrow_terminals {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) [∀ (A : C), category_theory.limits.has_terminal (category_theory.costructured_arrow G A)] :

category_theory.is_left_adjoint G

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

Equations

category_theory.is_left_adjoint_of_costructured_arrow_terminals G = {right := category_theory.right_adjoint_of_costructured_arrow_terminals G _, adj := category_theory.adjunction.adjunction_of_equiv_right (category_theory.right_adjoint_of_costructured_arrow_terminals_aux G) _}

def category_theory.mk_initial_of_left_adjoint {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) {F : C ⥤ D} (h : F ⊣ G) (A : C) :

category_theory.limits.is_initial (category_theory.structured_arrow.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

category_theory.mk_initial_of_left_adjoint G h A = {desc := λ (B : category_theory.limits.cocone (category_theory.functor.empty (category_theory.structured_arrow A G))), category_theory.structured_arrow.hom_mk (⇑((h.hom_equiv ((category_theory.functor.from_punit A).obj B.X.left) B.X.right).symm) B.X.hom) _, fac' := _, uniq' := _}

def category_theory.mk_terminal_of_right_adjoint {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] (G : D ⥤ C) {F : C ⥤ D} (h : F ⊣ G) (A : D) :

category_theory.limits.is_terminal (category_theory.costructured_arrow.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

category_theory.mk_terminal_of_right_adjoint G h A = {lift := λ (B : category_theory.limits.cone (category_theory.functor.empty (category_theory.costructured_arrow F A))), category_theory.costructured_arrow.hom_mk (⇑(h.hom_equiv B.X.left ((category_theory.functor.from_punit A).obj B.X.right)) B.X.hom) _, fac' := _, uniq' := _}

theorem category_theory.nonempty_is_right_adjoint_iff_has_initial_structured_arrow {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {G : D ⥤ C} :

nonempty (category_theory.is_right_adjoint G) ↔ ∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G)

theorem category_theory.nonempty_is_left_adjoint_iff_has_terminal_costructured_arrow {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {F : C ⥤ D} :

nonempty (category_theory.is_left_adjoint F) ↔ ∀ (A : D), category_theory.limits.has_terminal (category_theory.costructured_arrow F A)