Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/AlgebraicGeometry/Sites/BigZariski.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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_yoneda_isSheaf
intro X
rw [Presieve.isSheaf_pretopology]
rintro Y S ⟨𝓤,rfl⟩ x hx
Expand Down
61 changes: 42 additions & 19 deletions Mathlib/CategoryTheory/Sites/Canonical.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This lemma could be renamed yoneda_obj_isSheaf.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I renamed it to of_isSheaf_yoneda_obj, which seems to be the most correct

(h : ∀ X, Presieve.IsSheaf J (yoneda.obj X)) : Subcanonical J :=
le_finestTopology _ _
(by
rintro P ⟨X, rfl⟩
apply h)
(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_yoneda_isSheaf :=
GrothendieckTopology.Subcanonical.of_yoneda_isSheaf
@[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
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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_yoneda_isSheaf _ isSheaf_yoneda_obj

end coherentTopology

Expand Down
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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_yoneda_isSheaf _ isSheaf_yoneda_obj

variable [FinitaryExtensive C]

Expand Down
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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_yoneda_isSheaf _ isSheaf_yoneda_obj

end regularTopology

Expand Down
6 changes: 3 additions & 3 deletions Mathlib/CategoryTheory/Sites/Types.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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_yoneda_isSheaf _ 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
Expand Down
10 changes: 5 additions & 5 deletions Mathlib/Condensed/Functors.lean
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,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} :=
Expand All @@ -75,13 +75,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
8 changes: 4 additions & 4 deletions Mathlib/Condensed/Light/Functors.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,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} :=
Expand All @@ -40,10 +40,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