feat(category_theory/adjunction): general adjoint functor theorem (#4885

)

A proof of the general adjoint functor theorem. This PR also adds an API for wide equalizers (essentially copied from the equalizer API), as well as results relating adjunctions to (co)structured arrow categories and weakly initial objects. I can split this into smaller PRs if necessary?

src/category_theory/adjunction/adjoint_functor_theorems.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2021 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import category_theory.adjunction.basic
+import category_theory.adjunction.comma
+import category_theory.limits.constructions.weakly_initial
+import category_theory.limits.preserves.basic
+import category_theory.limits.creates
+import category_theory.limits.comma
+import category_theory.punit
+
+/-!
+# Adjoint functor theorem
+
+This file proves the (general) adjoint functor theorem, in the form:
+* If `G : D ⥤ C` preserves limits and `D` has limits, and satisfies the solution set condition,
+  then it has a left adjoint: `is_right_adjoint_of_preserves_limits_of_solution_set_condition`.
+
+We show that the converse holds, i.e. that if `G` has a left adjoint then it satisfies the solution
+set condition, see `solution_set_condition_of_is_right_adjoint`
+(the file `category_theory/adjunction/limits` already shows it preserves limits).
+
+We define the *solution set condition* for the functor `G : D ⥤ C` to mean, for every object
+`A : C`, there is a set-indexed family ${f_i : A ⟶ G (B_i)}$ such that any morphism `A ⟶ G X`
+factors through one of the `f_i`.
+
+-/
+universes v u
+
+namespace category_theory
+open limits
+
+variables {J : Type v}
+variables {C : Type u} [category.{v} C]
+
+/--
+The functor `G : D ⥤ C` satisfies the *solution set condition* if for every `A : C`, there is a
+family of morphisms `{f_i : A ⟶ G (B_i) // i ∈ ι}` such that given any morphism `h : A ⟶ G X`,
+there is some `i ∈ ι` such that `h` factors through `f_i`.
+
+The key part of this definition is that the indexing set `ι` lives in `Type v`, where `v` is the
+universe of morphisms of the category: this is the "smallness" condition which allows the general
+adjoint functor theorem to go through.
+-/
+def solution_set_condition {D : Type u} [category.{v} D] (G : D ⥤ C) : Prop :=
+∀ (A : C), ∃ (ι : Type v) (B : ι → D) (f : Π (i : ι), A ⟶ G.obj (B i)),
+  ∀ X (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
+
+variables {D : Type u} [category.{v} D]
+
+section general_adjoint_functor_theorem
+
+variables (G : D ⥤ C)
+
+/-- If `G : D ⥤ C` is a right adjoint it satisfies the solution set condition.  -/
+lemma solution_set_condition_of_is_right_adjoint [is_right_adjoint G] :
+  solution_set_condition G :=
+begin
+  intros A,
+  refine ⟨punit, λ _, (left_adjoint G).obj A, λ _, (adjunction.of_right_adjoint G).unit.app A, _⟩,
+  intros B h,
+  refine ⟨punit.star, ((adjunction.of_right_adjoint G).hom_equiv _ _).symm h, _⟩,
+  rw [←adjunction.hom_equiv_unit, equiv.apply_symm_apply],
+end
+
+/--
+The general adjoint functor theorem says that if `G : D ⥤ C` preserves limits and `D` has them,
+if `G` satisfies the solution set condition then `G` is a right adjoint.
+-/
+noncomputable def is_right_adjoint_of_preserves_limits_of_solution_set_condition
+  [has_limits D] [preserves_limits G] (hG : solution_set_condition G) :
+  is_right_adjoint G :=
+begin
+  apply is_right_adjoint_of_structured_arrow_initials _,
+  intro A,
+  specialize hG A,
+  choose ι B f g using hG,
+  let B' : ι → structured_arrow A G := λ i, structured_arrow.mk (f i),
+  have hB' : ∀ (A' : structured_arrow A G), ∃ i, nonempty (B' i ⟶ A'),
+  { intros A',
+    obtain ⟨i, _, t⟩ := g _ A'.hom,
+    exact ⟨i, ⟨structured_arrow.hom_mk _ t⟩⟩ },
+  obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_has_products hB',
+  apply has_initial_of_weakly_initial_and_has_wide_equalizers hT,
+end
+
+end general_adjoint_functor_theorem
+
+end category_theory

src/category_theory/adjunction/comma.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2021 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import category_theory.adjunction.basic
+import category_theory.limits.constructions.weakly_initial
+import category_theory.limits.preserves.basic
+import category_theory.limits.creates
+import category_theory.limits.comma
+import category_theory.punit
+
+/-!
+# 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.
+-/
+universes v u₁ u₂
+
+noncomputable theory
+
+namespace category_theory
+open limits
+
+variables {C : Type u₁} {D : Type u₂} [category.{v} C] [category.{v} D] (G : D ⥤ C)
+
+section of_initials
+variables [∀ A, has_initial (structured_arrow A G)]
+
+/--
+Implementation: If each structured arrow category on `G` has an initial object, an equivalence
+which is helpful for constructing a left adjoint to `G`.
+-/
+@[simps]
+def left_adjoint_of_structured_arrow_initials_aux (A : C) (B : D) :
+  ((⊥_ (structured_arrow A G)).right ⟶ B) ≃ (A ⟶ G.obj B) :=
+{ to_fun := λ g, (⊥_ (structured_arrow A G)).hom ≫ G.map g,
+  inv_fun := λ f, comma_morphism.right (initial.to (structured_arrow.mk f)),
+  left_inv := λ g,
+  begin
+    let B' : structured_arrow A G :=
+      structured_arrow.mk ((⊥_ (structured_arrow A G)).hom ≫ G.map g),
+    let g' : ⊥_ (structured_arrow A G) ⟶ B' := structured_arrow.hom_mk g rfl,
+    have : initial.to _ = g',
+    { apply colimit.hom_ext, rintro ⟨⟩ },
+    change comma_morphism.right (initial.to B') = _,
+    rw this,
+    refl
+  end,
+  right_inv := λ f,
+  begin
+    let B' : structured_arrow A G := { right := B, hom := f },
+    apply (comma_morphism.w (initial.to B')).symm.trans (category.id_comp _),
+  end }
+
+/--
+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`.
+-/
+def left_adjoint_of_structured_arrow_initials : C ⥤ D :=
+adjunction.left_adjoint_of_equiv (left_adjoint_of_structured_arrow_initials_aux G) (λ _ _, by simp)
+
+/--
+If each structured arrow category on `G` has an initial object, we have a constructed left adjoint
+to `G`.
+-/
+def adjunction_of_structured_arrow_initials :
+  left_adjoint_of_structured_arrow_initials G ⊣ G :=
+adjunction.adjunction_of_equiv_left _ _
+
+/-- If each structured arrow category on `G` has an initial object, `G` is a right adjoint. -/
+def is_right_adjoint_of_structured_arrow_initials : is_right_adjoint G :=
+{ left := _, adj := adjunction_of_structured_arrow_initials G }
+
+end of_initials
+
+section of_terminals
+variables [∀ A, has_terminal (costructured_arrow G A)]
+
+/--
+Implementation: If each costructured arrow category on `G` has a terminal object, an equivalence
+which is helpful for constructing a right adjoint to `G`.
+-/
+@[simps]
+def right_adjoint_of_costructured_arrow_terminals_aux (B : D) (A : C) :
+  (G.obj B ⟶ A) ≃ (B ⟶ (⊤_ (costructured_arrow G A)).left) :=
+{ to_fun := λ g, comma_morphism.left (terminal.from (costructured_arrow.mk g)),
+  inv_fun := λ g, G.map g ≫ (⊤_ (costructured_arrow G A)).hom,
+  left_inv := by tidy,
+  right_inv := λ g,
+  begin
+    let B' : costructured_arrow G A :=
+      costructured_arrow.mk (G.map g ≫ (⊤_ (costructured_arrow G A)).hom),
+    let g' : B' ⟶ ⊤_ (costructured_arrow G A) := costructured_arrow.hom_mk g rfl,
+    have : terminal.from _ = g',
+    { apply limit.hom_ext, rintro ⟨⟩ },
+    change comma_morphism.left (terminal.from B') = _,
+    rw this,
+    refl
+  end }
+
+/--
+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`.
+-/
+def right_adjoint_of_costructured_arrow_terminals : C ⥤ D :=
+adjunction.right_adjoint_of_equiv (right_adjoint_of_costructured_arrow_terminals_aux G)
+  (λ B₁ B₂ A f g, by { rw ←equiv.eq_symm_apply, simp })
+
+/--
+If each costructured arrow category on `G` has a terminal object, we have a constructed right
+adjoint to `G`.
+-/
+def adjunction_of_costructured_arrow_terminals :
+  G ⊣ right_adjoint_of_costructured_arrow_terminals G :=
+adjunction.adjunction_of_equiv_right _ _
+
+/-- If each costructured arrow category on `G` has an terminal object, `G` is a left adjoint. -/
+def is_right_adjoint_of_costructured_arrow_terminals : is_left_adjoint G :=
+{ right := right_adjoint_of_costructured_arrow_terminals G,
+  adj := adjunction.adjunction_of_equiv_right _ _ }
+
+end of_terminals
+
+section
+variables {F : C ⥤ D}
+
+/-- Given a left adjoint to `G`, we can construct an initial object in each structured arrow
+category on `G`. -/
+def mk_initial_of_left_adjoint (h : F ⊣ G) (A : C) :
+  is_initial (structured_arrow.mk (h.unit.app A) : structured_arrow A G) :=
+{ desc := λ B, structured_arrow.hom_mk ((h.hom_equiv _ _).symm B.X.hom) (by tidy),
+  uniq' := λ s m w,
+  begin
+    ext,
+    dsimp,
+    rw [equiv.eq_symm_apply, adjunction.hom_equiv_unit],
+    apply structured_arrow.w m,
+  end }
+
+/-- Given a right adjoint to `F`, we can construct a terminal object in each costructured arrow
+category on `F`. -/
+def mk_terminal_of_right_adjoint (h : F ⊣ G) (A : D) :
+  is_terminal (costructured_arrow.mk (h.counit.app A) : costructured_arrow F A) :=
+{ lift := λ B, costructured_arrow.hom_mk (h.hom_equiv _ _ B.X.hom) (by tidy),
+  uniq' := λ s m w,
+  begin
+    ext,
+    dsimp,
+    rw [h.eq_hom_equiv_apply, adjunction.hom_equiv_counit],
+    exact costructured_arrow.w m,
+  end }
+
+end
+
+end category_theory

src/category_theory/limits/constructions/weakly_initial.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2021 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import category_theory.limits.shapes.wide_equalizers
+import category_theory.limits.shapes.products
+import category_theory.limits.shapes.terminal
+
+/-!
+# Constructions related to weakly initial objects
+
+This file gives constructions related to weakly initial objects, namely:
+* If a category has small products and a small weakly initial set of objects, then it has a weakly
+  initial object.
+* If a category has wide equalizers and a weakly initial object, then it has an initial object.
+
+These are primarily useful to show the General Adjoint Functor Theorem.
+-/
+universes v u
+
+namespace category_theory
+open limits
+
+variables {C : Type u} [category.{v} C]
+
+/--
+If `C` has (small) products and a small weakly initial set of objects, then it has a weakly initial
+object.
+-/
+lemma has_weakly_initial_of_weakly_initial_set_and_has_products [has_products C]
+  {ι : Type v} {B : ι → C} (hB : ∀ (A : C), ∃ i, nonempty (B i ⟶ A)) :
+  ∃ (T : C), ∀ X, nonempty (T ⟶ X) :=
+⟨∏ B, λ X, ⟨pi.π _ _ ≫ (hB X).some_spec.some⟩⟩
+
+/--
+If `C` has (small) wide equalizers and a weakly initial object, then it has an initial object.
+
+The initial object is constructed as the wide equalizer of all endomorphisms on the given weakly
+initial object.
+-/
+lemma has_initial_of_weakly_initial_and_has_wide_equalizers [has_wide_equalizers C]
+  {T : C} (hT : ∀ X, nonempty (T ⟶ X)) :
+  has_initial C :=
+begin
+  let endos := T ⟶ T,
+  let i := wide_equalizer.ι (id : endos → endos),
+  haveI : nonempty endos := ⟨𝟙 _⟩,
+  have : ∀ (X : C), unique (wide_equalizer (id : endos → endos) ⟶ X),
+  { intro X,
+    refine ⟨⟨i ≫ classical.choice (hT X)⟩, λ a, _⟩,
+    let E := equalizer a (i ≫ classical.choice (hT _)),
+    let e : E ⟶ wide_equalizer id := equalizer.ι _ _,
+    let h : T ⟶ E := classical.choice (hT E),
+    have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _,
+    { rw [category.assoc, category.assoc],
+      apply wide_equalizer.condition (id : endos → endos) (h ≫ e ≫ i) },
+    rw [category.comp_id, cancel_mono_id i] at this,
+    haveI : split_epi e := ⟨i ≫ h, this⟩,
+    rw ←cancel_epi e,
+    apply equalizer.condition },
+  exactI has_initial_of_unique (wide_equalizer (id : endos → endos)),
+end
+
+end category_theory