feat(category_theory/generator): complete well-powered category with small coseparating set has an initial object (#15865)

TwoFX · TwoFX · commit 952e7ee9eaf8 · 2022-08-10T10:23:33.000Z
A step towards the Special Adjoint Functor Theorem.
diff --git a/src/category_theory/generator.lean b/src/category_theory/generator.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import category_theory.balanced
+import category_theory.limits.essentially_small
 import category_theory.limits.opposites
 import category_theory.limits.shapes.zero_morphisms
 import category_theory.subobject.lattice
@@ -47,8 +48,6 @@ We
 
 * We currently don't have any examples yet.
 * We will want typeclasses `has_separator C` and similar.
-* To state the Special Adjoint Functor Theorem, we will need to be able to talk about *small*
-  separating sets.
 
 -/
 
@@ -261,6 +260,42 @@ begin
     simpa using hh j.as.1.1 j.as.1.2 j.as.2 }
 end
 
+/-- An ingredient of the proof of the Special Adjoint Functor Theorem: a complete well-powered
+    category with a small coseparating set has an initial object.
+
+    In fact, it follows from the Special Adjoint Functor Theorem that `C` is already cocomplete. -/
+lemma has_initial_of_is_cosepatating [well_powered C] [has_limits C] {𝒢 : set C} [small.{v} 𝒢]
+  (h𝒢 : is_coseparating 𝒢) : has_initial C :=
+begin
+  haveI := has_products_of_shape_of_small C 𝒢,
+  haveI := λ A, has_products_of_shape_of_small.{v} C (Σ G : 𝒢, A ⟶ (G : C)),
+  letI := complete_lattice_of_complete_semilattice_Inf (subobject (pi_obj (coe : 𝒢 → C))),
+  suffices : ∀ A : C, unique (((⊥ : subobject (pi_obj (coe : 𝒢 → C))) : C) ⟶ A),
+  { exactI has_initial_of_unique ((⊥ : subobject (pi_obj (coe : 𝒢 → C))) : C) },
+  refine λ A, ⟨⟨_⟩, λ f, _⟩,
+  { let s := pi.lift (λ f : Σ G : 𝒢, A ⟶ (G : C), id (pi.π (coe : 𝒢 → C)) f.1),
+    let t := pi.lift (@sigma.snd 𝒢 (λ G, A ⟶ (G : C))),
+    haveI : mono t := (is_coseparating_iff_mono 𝒢).1 h𝒢 A,
+    exact subobject.of_le_mk _ (pullback.fst : pullback s t ⟶ _) bot_le ≫ pullback.snd },
+  { generalize : default = g,
+    suffices : split_epi (equalizer.ι f g),
+    { exactI eq_of_epi_equalizer },
+    exact ⟨subobject.of_le_mk _ (equalizer.ι f g ≫ subobject.arrow _) bot_le, by { ext, simp }⟩ }
+end
+
+/-- An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered
+    category with a small separating set has a terminal object.
+
+    In fact, it follows from the Special Adjoint Functor Theorem that `C` is already complete. -/
+lemma has_terminal_of_is_separating [well_powered Cᵒᵖ] [has_colimits C] {𝒢 : set C} [small.{v} 𝒢]
+  (h𝒢 : is_separating 𝒢) : has_terminal C :=
+begin
+  haveI : has_limits Cᵒᵖ := has_limits_op_of_has_colimits,
+  haveI : small.{v} 𝒢.op := small_of_injective (set.op_equiv_self 𝒢).injective,
+  haveI : has_initial Cᵒᵖ := has_initial_of_is_cosepatating ((is_coseparating_op_iff _).2 h𝒢),
+  exact has_terminal_of_has_initial_op
+end
+
 section well_powered
 
 namespace subobject
diff --git a/src/category_theory/limits/essentially_small.lean b/src/category_theory/limits/essentially_small.lean
@@ -30,11 +30,11 @@ lemma has_colimits_of_shape_of_essentially_small [essentially_small.{w₁} J]
   [has_colimits_of_size.{w₁ w₁} C] : has_colimits_of_shape J C :=
 has_colimits_of_shape_of_equivalence $ equivalence.symm $ equiv_small_model.{w₁} J
 
-lemma has_products_of_shape_of_small (β : Type w₁) [small.{w₂} β] [has_products.{w₂} C] :
+lemma has_products_of_shape_of_small (β : Type w₂) [small.{w₁} β] [has_products.{w₁} C] :
   has_products_of_shape β C :=
 has_limits_of_shape_of_equivalence $ discrete.equivalence $ equiv.symm $ equiv_shrink β
 
-lemma has_coproducts_of_shape_of_small (β : Type w₁) [small.{w₂} β] [has_coproducts.{w₂} C] :
+lemma has_coproducts_of_shape_of_small (β : Type w₂) [small.{w₁} β] [has_coproducts.{w₁} C] :
   has_coproducts_of_shape β C :=
 has_colimits_of_shape_of_equivalence $ discrete.equivalence $ equiv.symm $ equiv_shrink β
 
diff --git a/src/category_theory/limits/shapes/terminal.lean b/src/category_theory/limits/shapes/terminal.lean
@@ -311,6 +311,18 @@ def initial_unop_of_terminal {X : Cᵒᵖ} (t : is_terminal X) : is_initial X.un
 { desc := λ s, (t.from (opposite.op s.X)).unop,
   uniq' := λ s m w, quiver.hom.op_inj (t.hom_ext _ _) }
 
+instance has_initial_op_of_has_terminal [has_terminal C] : has_initial Cᵒᵖ :=
+(initial_op_of_terminal terminal_is_terminal).has_initial
+
+instance has_terminal_op_of_has_initial [has_initial C] : has_terminal Cᵒᵖ :=
+(terminal_op_of_initial initial_is_initial).has_terminal
+
+lemma has_terminal_of_has_initial_op [has_initial Cᵒᵖ] : has_terminal C :=
+(terminal_unop_of_initial initial_is_initial).has_terminal
+
+lemma has_initial_of_has_terminal_op [has_terminal Cᵒᵖ] : has_initial C :=
+(initial_unop_of_terminal terminal_is_terminal).has_initial
+
 instance {J : Type*} [category J] {C : Type*} [category C] [has_terminal C] :
   has_limit ((category_theory.functor.const J).obj (⊤_ C)) :=
 has_limit.mk
diff --git a/src/data/set/opposite.lean b/src/data/set/opposite.lean
@@ -44,6 +44,10 @@ ext (by simp only [mem_unop, op_mem_op, iff_self, implies_true_iff])
 @[simp] lemma unop_op (s : set αᵒᵖ) : s.unop.op = s :=
 ext (by simp only [mem_op, unop_mem_unop, iff_self, implies_true_iff])
 
+/-- The members of the opposite of a set are in bijection with the members of the set itself. -/
+@[simps] def op_equiv_self (s : set α) : s.op ≃ s :=
+⟨λ x, ⟨unop x, x.2⟩, λ x, ⟨op x, x.2⟩, λ x, by simp, λ x, by simp⟩
+
 /-- Taking opposites as an equivalence of powersets. -/
 @[simps] def op_equiv : set α ≃ set αᵒᵖ :=
 ⟨set.op, set.unop, op_unop, unop_op⟩
