chore(CategoryTheory/Sites): make Subcanonical a class (#18186)

Author: dagurtomas

Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

@@ -70,8 +70,8 @@ lemma zariskiTopology_openCover {Y : Scheme.{u}} (U : OpenCover.{v} Y) :
   rintro _ _ ⟨y⟩
   exact ⟨_, 𝟙 _, U.map (U.f y), ⟨_⟩, by simp⟩
 
-lemma subcanonical_zariskiTopology : Sheaf.Subcanonical zariskiTopology := by
-  apply Sheaf.Subcanonical.of_yoneda_isSheaf
+instance subcanonical_zariskiTopology : zariskiTopology.Subcanonical := by
+  apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
   intro X
   rw [Presieve.isSheaf_pretopology]
   rintro Y S ⟨𝓤,rfl⟩ x hx

Mathlib/CategoryTheory/Sites/Canonical.lean

@@ -205,60 +205,83 @@ theorem isSheaf_of_isRepresentable (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable]
     Presieve.IsSheaf (canonicalTopology C) P :=
   Presieve.isSheaf_iso (canonicalTopology C) P.reprW (isSheaf_yoneda_obj _)
 
+end Sheaf
+
+namespace GrothendieckTopology
+
+open Sheaf
+
 /-- A subcanonical topology is a topology which is smaller than the canonical topology.
 Equivalently, a topology is subcanonical iff every representable is a sheaf.
 -/
-def Subcanonical (J : GrothendieckTopology C) : Prop :=
-  J ≤ canonicalTopology C
+class Subcanonical (J : GrothendieckTopology C) : Prop where
+  le_canonical : J ≤ canonicalTopology C
+
+lemma le_canonical (J : GrothendieckTopology C) [Subcanonical J] : J ≤ canonicalTopology C :=
+  Subcanonical.le_canonical
+
+instance : (canonicalTopology C).Subcanonical where
+  le_canonical := le_rfl
 
 namespace Subcanonical
 
 /-- If every functor `yoneda.obj X` is a `J`-sheaf, then `J` is subcanonical. -/
-theorem of_yoneda_isSheaf (J : GrothendieckTopology C)
-    (h : ∀ X, Presieve.IsSheaf J (yoneda.obj X)) : Subcanonical J :=
-  le_finestTopology _ _
-    (by
-      rintro P ⟨X, rfl⟩
-      apply h)
+theorem of_isSheaf_yoneda_obj (J : GrothendieckTopology C)
+    (h : ∀ X, Presieve.IsSheaf J (yoneda.obj X)) : Subcanonical J where
+  le_canonical := le_finestTopology _ _ (by rintro P ⟨X, rfl⟩; apply h)
 
 /-- If `J` is subcanonical, then any representable is a `J`-sheaf. -/
-theorem isSheaf_of_isRepresentable {J : GrothendieckTopology C} (hJ : Subcanonical J)
+theorem isSheaf_of_isRepresentable {J : GrothendieckTopology C} [Subcanonical J]
     (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable] : Presieve.IsSheaf J P :=
-  Presieve.isSheaf_of_le _ hJ (Sheaf.isSheaf_of_isRepresentable P)
+  Presieve.isSheaf_of_le _ J.le_canonical (Sheaf.isSheaf_of_isRepresentable P)
 
-variable {J}
+variable {J : GrothendieckTopology C}
+
+end Subcanonical
+
+variable {J : GrothendieckTopology C}
 
 /--
 If `J` is subcanonical, we obtain a "Yoneda" functor from the defining site
 into the sheaf category.
 -/
 @[simps]
-def yoneda (hJ : Subcanonical J) : C ⥤ Sheaf J (Type v) where
+def yoneda [J.Subcanonical] : C ⥤ Sheaf J (Type v) where
   obj X := ⟨CategoryTheory.yoneda.obj X, by
     rw [isSheaf_iff_isSheaf_of_type]
-    apply hJ.isSheaf_of_isRepresentable⟩
+    apply Subcanonical.isSheaf_of_isRepresentable⟩
   map f := ⟨CategoryTheory.yoneda.map f⟩
 
-variable (hJ : Subcanonical J)
+variable [Subcanonical J]
 
 /--
 The yoneda embedding into the presheaf category factors through the one
 to the sheaf category.
 -/
 def yonedaCompSheafToPresheaf :
-    hJ.yoneda ⋙ sheafToPresheaf J (Type v) ≅ CategoryTheory.yoneda :=
+    J.yoneda ⋙ sheafToPresheaf J (Type v) ≅ CategoryTheory.yoneda :=
   Iso.refl _
 
 /-- The yoneda functor into the sheaf category is fully faithful -/
-def yonedaFullyFaithful : hJ.yoneda.FullyFaithful :=
+def yonedaFullyFaithful : (J.yoneda).FullyFaithful :=
   Functor.FullyFaithful.ofCompFaithful (G := sheafToPresheaf J (Type v)) Yoneda.fullyFaithful
 
-instance : hJ.yoneda.Full := hJ.yonedaFullyFaithful.full
+instance : (J.yoneda).Full := (J.yonedaFullyFaithful).full
 
-instance : hJ.yoneda.Faithful := hJ.yonedaFullyFaithful.faithful
+instance : (J.yoneda).Faithful := (J.yonedaFullyFaithful).faithful
 
-end Subcanonical
+end GrothendieckTopology
 
-end Sheaf
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical := GrothendieckTopology.Subcanonical
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.of_isSheaf_yoneda_obj :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.isSheaf_of_isRepresentable :=
+  GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.yoneda :=
+  GrothendieckTopology.yoneda
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.yonedaCompSheafToPresheaf :=
+  GrothendieckTopology.yonedaCompSheafToPresheaf
+@[deprecated (since := "2024-10-29")] alias Sheaf.Subcanonical.yonedaFullyFaithful :=
+  GrothendieckTopology.yonedaFullyFaithful
 
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean

@@ -59,8 +59,8 @@ theorem isSheaf_yoneda_obj (W : C) : Presieve.IsSheaf (coherentTopology C) (yone
 
 variable (C) in
 /-- The coherent topology on a precoherent category is subcanonical. -/
-theorem subcanonical : Sheaf.Subcanonical (coherentTopology C) :=
-  Sheaf.Subcanonical.of_yoneda_isSheaf _ isSheaf_yoneda_obj
+instance subcanonical : (coherentTopology C).Subcanonical :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj
 
 end coherentTopology
 

Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

@@ -69,8 +69,8 @@ theorem extensiveTopology.isSheaf_yoneda_obj (W : C) : Presieve.IsSheaf (extensi
   exact isSheafFor_extensive_of_preservesFiniteProducts _ _
 
 /-- The extensive topology on a finitary pre-extensive category is subcanonical. -/
-theorem extensiveTopology.subcanonical : Sheaf.Subcanonical (extensiveTopology C) :=
-  Sheaf.Subcanonical.of_yoneda_isSheaf _ isSheaf_yoneda_obj
+instance extensiveTopology.subcanonical : (extensiveTopology C).Subcanonical :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj
 
 variable [FinitaryExtensive C]
 

Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean

@@ -257,8 +257,8 @@ lemma isSheaf_yoneda_obj [Preregular C] (W : C)  :
   · exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy
 
 /-- The regular topology on any preregular category is subcanonical. -/
-theorem subcanonical [Preregular C] : Sheaf.Subcanonical (regularTopology C) :=
-  Sheaf.Subcanonical.of_yoneda_isSheaf _ isSheaf_yoneda_obj
+instance subcanonical [Preregular C] : (regularTopology C).Subcanonical :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj
 
 end regularTopology
 

Mathlib/CategoryTheory/Sites/Types.lean

@@ -158,12 +158,12 @@ noncomputable def typeEquiv : Type u ≌ SheafOfTypes typesGrothendieckTopology
     dsimp [yoneda', yonedaEquiv, evalEquiv]
     erw [typesGlue_eval]
 
-theorem subcanonical_typesGrothendieckTopology : Sheaf.Subcanonical typesGrothendieckTopology.{u} :=
-  Sheaf.Subcanonical.of_yoneda_isSheaf _ fun _ => isSheaf_yoneda'
+instance subcanonical_typesGrothendieckTopology : typesGrothendieckTopology.{u}.Subcanonical :=
+  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ fun _ => isSheaf_yoneda'
 
 theorem typesGrothendieckTopology_eq_canonical :
     typesGrothendieckTopology.{u} = Sheaf.canonicalTopology (Type u) := by
-  refine le_antisymm subcanonical_typesGrothendieckTopology (sInf_le ?_)
+  refine le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)
   refine ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext ?_⟩
   funext α
   ext S

Mathlib/Condensed/Functors.lean

@@ -42,7 +42,7 @@ section Topology
 
 /-- The functor from `CompHaus` to `Condensed.{u} (Type u)` given by the Yoneda sheaf. -/
 def compHausToCondensed' : CompHaus.{u} ⥤ Condensed.{u} (Type u) :=
-  (coherentTopology.subcanonical CompHaus).yoneda
+  (coherentTopology CompHaus).yoneda
 
 /-- The yoneda presheaf as an actual condensed set. -/
 def compHausToCondensed : CompHaus.{u} ⥤ CondensedSet.{u} :=
@@ -66,13 +66,13 @@ def stoneanToCondensed : Stonean.{u} ⥤ CondensedSet.{u} :=
 abbrev Stonean.toCondensed (S : Stonean.{u}) : CondensedSet.{u} := stoneanToCondensed.obj S
 
 instance : compHausToCondensed'.Full :=
-  show (Sheaf.Subcanonical.yoneda _).Full from inferInstance
+  inferInstanceAs ((coherentTopology CompHaus).yoneda).Full
 
 instance : compHausToCondensed'.Faithful :=
-  show (Sheaf.Subcanonical.yoneda _).Faithful from inferInstance
+  inferInstanceAs ((coherentTopology CompHaus).yoneda).Faithful
 
-instance : compHausToCondensed.Full := show (_ ⋙ _).Full from inferInstance
+instance : compHausToCondensed.Full := inferInstanceAs (_ ⋙ _).Full
 
-instance : compHausToCondensed.Faithful := show (_ ⋙ _).Faithful from inferInstance
+instance : compHausToCondensed.Faithful := inferInstanceAs (_ ⋙ _).Faithful
 
 end Topology

Mathlib/Condensed/Light/Functors.lean

@@ -25,7 +25,7 @@ open CategoryTheory Limits
 
 /-- The functor from `LightProfinite.{u}` to `LightCondSet.{u}` given by the Yoneda sheaf. -/
 def lightProfiniteToLightCondSet : LightProfinite.{u} ⥤ LightCondSet.{u} :=
-  (coherentTopology.subcanonical LightProfinite).yoneda
+  (coherentTopology LightProfinite).yoneda
 
 /-- Dot notation for the value of `lightProfiniteToLightCondSet`. -/
 abbrev LightProfinite.toCondensed (S : LightProfinite.{u}) : LightCondSet.{u} :=
@@ -34,10 +34,10 @@ abbrev LightProfinite.toCondensed (S : LightProfinite.{u}) : LightCondSet.{u} :=
 /-- `lightProfiniteToLightCondSet` is fully faithful. -/
 abbrev lightProfiniteToLightCondSetFullyFaithful :
     lightProfiniteToLightCondSet.FullyFaithful :=
-  Sheaf.Subcanonical.yonedaFullyFaithful _
+  (coherentTopology LightProfinite).yonedaFullyFaithful
 
 instance : lightProfiniteToLightCondSet.Full :=
-  show (Sheaf.Subcanonical.yoneda _).Full from inferInstance
+  inferInstanceAs ((coherentTopology LightProfinite).yoneda).Full
 
 instance : lightProfiniteToLightCondSet.Faithful :=
-  show (Sheaf.Subcanonical.yoneda _).Faithful from inferInstance
+  inferInstanceAs ((coherentTopology LightProfinite).yoneda).Faithful