feat(CategoryTheory/Sites): being subcanonical is reflected by fully faithful continuous functors (leanprover-community#36082)

Author: chrisflav

Mathlib/CategoryTheory/Sites/Subcanonical.lean

@@ -9,6 +9,7 @@ public import Mathlib.CategoryTheory.Limits.Preserves.Ulift
 public import Mathlib.CategoryTheory.Sites.Canonical
 public import Mathlib.CategoryTheory.Sites.Whiskering
 public import Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
+public import Mathlib.CategoryTheory.Sites.Continuous
 /-!
 
 # Subcanonical Grothendieck topologies
@@ -326,4 +327,23 @@ lemma preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem {ι : Type*}
   refine isColimitCofanMkYoneda _ _ (hcov hc) htriv fun hij Y a b hab ↦ ⟨?_⟩
   exact .ofCoproductDisjointOfCommSq hij hc _ _ hab
 
+variable {D : Type*} [Category.{v'} D] (F : C ⥤ D) (J : GrothendieckTopology C)
+  (K : GrothendieckTopology D)
+
+lemma subcanonical_of_full_of_faithful [F.Full] [F.Faithful]
+    [Functor.IsContinuous.{max v v'} F J K] [K.Subcanonical] :
+    J.Subcanonical := by
+  refine .of_isSheaf_yoneda_obj _ fun Y ↦ ?_
+  suffices h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v'}.obj Y) by
+    rwa [Presieve.isSheaf_iff_of_nat_equiv]
+    · intro
+      exact Equiv.ulift.symm
+    · intros
+      rfl
+  rw [← isSheaf_iff_isSheaf_of_type, Presheaf.isSheaf_of_iso_iff
+    ((Functor.FullyFaithful.ofFullyFaithful F).compUliftYonedaCompWhiskeringLeft.app Y).symm]
+  refine F.op_comp_isSheaf_of_isSheaf J K _ ?_
+  rw [isSheaf_iff_isSheaf_of_type]
+  apply GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
+
 end CategoryTheory.GrothendieckTopology

Mathlib/CategoryTheory/Yoneda.lean

@@ -489,6 +489,9 @@ lemma IsRepresentable.mk' {F : Cᵒᵖ ⥤ Type v₁} {X : C} (e : yoneda.obj X
 instance {X : C} : IsRepresentable (yoneda.obj X) :=
   IsRepresentable.mk' (Iso.refl _)
 
+instance {X : C} : IsRepresentable (uliftYoneda.{w}.obj X) :=
+  RepresentableBy.isRepresentable (representableByUliftFunctorEquiv.symm (RepresentableBy.yoneda X))
+
 /-- A functor `F : C ⥤ Type v₁` is corepresentable if there is object `X` so `F ≅ coyoneda.obj X`.
 -/
 @[stacks 001Q]
@@ -508,6 +511,10 @@ lemma IsCorepresentable.mk' {F : C ⥤ Type v₁} {X : C} (e : coyoneda.obj (op
 instance {X : Cᵒᵖ} : IsCorepresentable (coyoneda.obj X) :=
   IsCorepresentable.mk' (Iso.refl _)
 
+instance {X : Cᵒᵖ} : IsCorepresentable (uliftCoyoneda.{w}.obj X) :=
+  CorepresentableBy.isCorepresentable
+    (corepresentableByUliftFunctorEquiv.symm (CorepresentableBy.coyoneda X))
+
 -- instance : corepresentable (𝟭 (Type v₁)) :=
 -- corepresentable_of_nat_iso (op punit) coyoneda.punit_iso
 section Representable