From fef8efdf78f223294c34a41875923ab1272322d4 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@himmel-villmar.de>
Date: Sat, 27 Aug 2022 16:01:27 +0000
Subject: [PATCH] feat(category_theory): coseparators in structured_arrow
 (#15981)

Hopefully the last preliminary PR for the Special Adjoint Functor Theorem.
---
 src/category_theory/generator.lean        | 40 ++++++++++++++++++-----
 src/category_theory/structured_arrow.lean | 17 ++++++++++
 2 files changed, 49 insertions(+), 8 deletions(-)

diff --git a/src/category_theory/generator.lean b/src/category_theory/generator.lean
index e398a80921da1..aed1af711e8f1 100644
--- a/src/category_theory/generator.lean
+++ b/src/category_theory/generator.lean
@@ -51,12 +51,12 @@ We
 
 -/
 
-universes w v u
+universes w v₁ v₂ u₁ u₂
 
 open category_theory.limits opposite
 
 namespace category_theory
-variables {C : Type u} [category.{v} C]
+variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
 
 /-- We say that `𝒢` is a separating set if the functors `C(G, -)` for `G ∈ 𝒢` are collectively
     faithful, i.e., if `h ≫ f = h ≫ g` for all `h` with domain in `𝒢` implies `f = g`. -/
@@ -264,11 +264,11 @@ end
     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} 𝒢]
+lemma has_initial_of_is_coseparating [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)),
+  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) },
@@ -288,12 +288,12 @@ end
     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} 𝒢]
+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𝒢),
+  haveI : small.{v₁} 𝒢.op := small_of_injective (set.op_equiv_self 𝒢).injective,
+  haveI : has_initial Cᵒᵖ := has_initial_of_is_coseparating ((is_coseparating_op_iff _).2 h𝒢),
   exact has_terminal_of_has_initial_op
 end
 
@@ -327,13 +327,37 @@ calc P = P ⊓ Q : eq.symm $ inf_eq_of_is_detecting h𝒢 _ _ $ λ G hG f hf, (h
 end subobject
 
 /-- A category with pullbacks and a small detecting set is well-powered. -/
-lemma well_powered_of_is_detecting [has_pullbacks C] {𝒢 : set C} [small.{v} 𝒢]
+lemma well_powered_of_is_detecting [has_pullbacks C] {𝒢 : set C} [small.{v₁} 𝒢]
   (h𝒢 : is_detecting 𝒢) : well_powered C :=
 ⟨λ X, @small_of_injective _ _ _ (λ P : subobject X, { f : Σ G : 𝒢, G.1 ⟶ X | P.factors f.2 }) $
   λ P Q h, subobject.eq_of_is_detecting h𝒢 _ _ (by simpa [set.ext_iff] using h)⟩
 
 end well_powered
 
+namespace structured_arrow
+variables (S : D) (T : C ⥤ D)
+
+lemma is_coseparating_proj_preimage {𝒢 : set C} (h𝒢 : is_coseparating 𝒢) :
+  is_coseparating ((proj S T).obj ⁻¹' 𝒢) :=
+begin
+  refine λ X Y f g hfg, ext _ _ (h𝒢 _ _ (λ G hG h, _)),
+  exact congr_arg comma_morphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (hom_mk h rfl))
+end
+
+end structured_arrow
+
+namespace costructured_arrow
+variables (S : C ⥤ D) (T : D)
+
+lemma is_separating_proj_preimage {𝒢 : set C} (h𝒢 : is_separating 𝒢) :
+  is_separating ((proj S T).obj ⁻¹' 𝒢) :=
+begin
+  refine λ X Y f g hfg, ext _ _ (h𝒢 _ _ (λ G hG h, _)),
+  convert congr_arg comma_morphism.left (hfg (mk (S.map h ≫ X.hom)) hG (hom_mk h rfl))
+end
+
+end costructured_arrow
+
 /-- We say that `G` is a separator if the functor `C(G, -)` is faithful. -/
 def is_separator (G : C) : Prop :=
 is_separating ({G} : set C)
diff --git a/src/category_theory/structured_arrow.lean b/src/category_theory/structured_arrow.lean
index b478571ddaa5c..2b289b795b53b 100644
--- a/src/category_theory/structured_arrow.lean
+++ b/src/category_theory/structured_arrow.lean
@@ -6,6 +6,7 @@ Authors: Adam Topaz, Scott Morrison
 import category_theory.punit
 import category_theory.comma
 import category_theory.limits.shapes.terminal
+import category_theory.essentially_small
 
 /-!
 # The category of "structured arrows"
@@ -168,6 +169,14 @@ comma.pre_right _ F G
   map := λ X Y f, { right := f.right, w' :=
     by { simp [functor.comp_map, ←G.map_comp, ← f.w] } } }
 
+instance small_proj_preimage_of_locally_small {𝒢 : set C} [small.{v₁} 𝒢] [locally_small.{v₁} D] :
+  small.{v₁} ((proj S T).obj ⁻¹' 𝒢) :=
+begin
+  suffices : (proj S T).obj ⁻¹' 𝒢 = set.range (λ f : Σ G : 𝒢, S ⟶ T.obj G, mk f.2),
+  { rw this, apply_instance },
+  exact set.ext (λ X, ⟨λ h, ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by tidy⟩)
+end
+
 end structured_arrow
 
 
@@ -310,6 +319,14 @@ comma.pre_left F G _
   map := λ X Y f, { left := f.left, w' :=
     by { simp [functor.comp_map, ←G.map_comp, ← f.w] } } }
 
+instance small_proj_preimage_of_locally_small {𝒢 : set C} [small.{v₁} 𝒢] [locally_small.{v₁} D] :
+  small.{v₁} ((proj S T).obj ⁻¹' 𝒢) :=
+begin
+  suffices : (proj S T).obj ⁻¹' 𝒢 = set.range (λ f : Σ G : 𝒢, S.obj G ⟶ T, mk f.2),
+  { rw this, apply_instance },
+  exact set.ext (λ X, ⟨λ h, ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by tidy⟩)
+end
+
 end costructured_arrow
 
 open opposite