Skip to content

Commit

Permalink
chore(CategoryTheory/Sites): generalise universes for extensive sheav…
Browse files Browse the repository at this point in the history
…es (#12801)
  • Loading branch information
dagurtomas committed May 12, 2024
1 parent 3fc1e3d commit 61fdb6c
Show file tree
Hide file tree
Showing 4 changed files with 33 additions and 23 deletions.
6 changes: 3 additions & 3 deletions Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ This file characterises sheaves for the extensive topology.
extensive topology are precisely those preserving finite products.
-/

universe v u
universe v u w

namespace CategoryTheory

Expand Down Expand Up @@ -49,7 +49,7 @@ A finite product preserving presheaf is a sheaf for the extensive topology on a
`FinitaryPreExtensive`.
-/
theorem isSheafFor_extensive_of_preservesFiniteProducts {X : C} (S : Presieve X) [S.Extensive]
(F : Cᵒᵖ ⥤ Type max u v) [PreservesFiniteProducts F] : S.IsSheafFor F := by
(F : Cᵒᵖ ⥤ Type w) [PreservesFiniteProducts F] : S.IsSheafFor F := by
obtain ⟨α, _, Z, π, rfl, ⟨hc⟩⟩ := Extensive.arrows_nonempty_isColimit (R := S)
have : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks :=
(inferInstance : (ofArrows Z π).hasPullbacks)
Expand All @@ -62,7 +62,7 @@ instance {α : Type} [Finite α] (Z : α → C) : (ofArrows Z (fun i ↦ Sigma.
/--
A presheaf on a category which is `FinitaryExtensive` is a sheaf iff it preserves finite products.
-/
theorem isSheaf_iff_preservesFiniteProducts [FinitaryExtensive C] (F : Cᵒᵖ ⥤ Type max u v) :
theorem isSheaf_iff_preservesFiniteProducts [FinitaryExtensive C] (F : Cᵒᵖ ⥤ Type w) :
Presieve.IsSheaf (extensiveCoverage C).toGrothendieck F ↔
Nonempty (PreservesFiniteProducts F) := by
refine ⟨fun hF ↦ ⟨⟨fun α _ ↦ ⟨fun {K} ↦ ?_⟩⟩⟩, fun hF ↦ ?_⟩
Expand Down
8 changes: 5 additions & 3 deletions Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
Original file line number Diff line number Diff line change
Expand Up @@ -263,9 +263,11 @@ theorem sheaf_condition : R.IsSheafFor P ↔ Nonempty (IsLimit (Fork.ofι _ (w P

namespace Arrows

variable (P : Cᵒᵖ ⥤ Type w) {X : C} (R : Presieve X) (S : Sieve X)

open Presieve

variable {B : C} {I : Type} (X : I → C) (π : (i : I) → X i ⟶ B) [UnivLE.{w, max v u}]
variable {B : C} {I : Type} (X : I → C) (π : (i : I) → X i ⟶ B)
[(Presieve.ofArrows X π).hasPullbacks]
-- TODO: allow `I : Type w` 

Expand All @@ -274,7 +276,7 @@ The middle object of the fork diagram of <https://stacks.math.columbia.edu/tag/0
The difference between this and `Equalizer.FirstObj P (ofArrows X π)` arrises if the family of
arrows `π` contains duplicates. The `Presieve.ofArrows` doesn't see those.
-/
def FirstObj : Type max v u := ∏ (fun i ↦ P.obj (op (X i)))
def FirstObj : Type w := ∏ (fun i ↦ P.obj (op (X i)))

@[ext]
lemma FirstObj.ext (z₁ z₂ : FirstObj P X) (h : ∀ i, (Pi.π _ i : FirstObj P X ⟶ _) z₁ =
Expand All @@ -288,7 +290,7 @@ The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag
The difference between this and `Equalizer.Presieve.SecondObj P (ofArrows X π)` arrises if the
family of arrows `π` contains duplicates. The `Presieve.ofArrows` doesn't see those.
-/
def SecondObj : Type max v u :=
def SecondObj : Type w :=
∏ (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2))))

@[ext]
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/CategoryTheory/Sites/Preserves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -30,11 +30,11 @@ See `preservesProductOfIsSheafFor`.
See `isSheafFor_of_preservesProduct`.
-/

universe v u
universe v u w

namespace CategoryTheory.Presieve

variable {C : Type u} [Category.{v} C] {I : C} (F : Cᵒᵖ ⥤ Type (max u v))
variable {C : Type u} [Category.{v} C] {I : C} (F : Cᵒᵖ ⥤ Type w)

open Limits Opposite

Expand Down
38 changes: 23 additions & 15 deletions Mathlib/Condensed/Explicit.lean
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ continuous surjection), the presheaf `F` exhibits `F(B)` as the equalizer of th
`F(X) ⇉ F(X ×_B X)`
-/

universe v u
universe v u w

open CategoryTheory Limits Opposite Functor Presheaf regularTopology

Expand All @@ -46,7 +46,7 @@ end CategoryTheory
namespace CompHaus

theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
(F : CompHaus.{u}ᵒᵖ ⥤ Type (u+1)) :
(F : CompHaus.{u}ᵒᵖ ⥤ Type w) :
IsSheaf (coherentTopology CompHaus) F ↔
Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F := by
rw [isSheaf_coherent_iff_regular_and_extensive]
Expand All @@ -55,19 +55,20 @@ theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
· rw [equalizerCondition_iff_isSheaf, isSheaf_iff_isSheaf_of_type]

theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'
{A : Type (u+2)} [Category.{u+1} A] (G : A ⥤ Type (u+1))
[HasLimits A] [PreservesLimits G] [G.ReflectsIsomorphisms] (F : CompHaus.{u}ᵒᵖ ⥤ A) :
{A : Type*} [Category A] (G : A ⥤ Type w)
[HasLimitsOfSize.{u, u+1} A] [PreservesLimitsOfSize.{u, u+1} G]
[G.ReflectsIsomorphisms] (F : CompHaus.{u}ᵒᵖ ⥤ A) :
Presheaf.IsSheaf (coherentTopology CompHaus) F ↔
Nonempty (PreservesFiniteProducts (F ⋙ G)) ∧ EqualizerCondition (F ⋙ G) := by
rw [Presheaf.isSheaf_iff_isSheaf_forget (coherentTopology CompHaus) F G,
rw [Presheaf.isSheaf_iff_isSheaf_comp (coherentTopology CompHaus) F G,
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

end CompHaus

namespace Profinite

theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
(F : Profinite.{u}ᵒᵖ ⥤ Type (u+1)) :
(F : Profinite.{u}ᵒᵖ ⥤ Type w) :
IsSheaf (coherentTopology Profinite) F ↔
Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F := by
rw [isSheaf_coherent_iff_regular_and_extensive]
Expand All @@ -76,19 +77,20 @@ theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
· rw [equalizerCondition_iff_isSheaf, isSheaf_iff_isSheaf_of_type]

theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'
{A : Type (u+2)} [Category.{u+1} A] (G : A ⥤ Type (u+1))
[HasLimits A] [PreservesLimits G] [G.ReflectsIsomorphisms] (F : Profinite.{u}ᵒᵖ ⥤ A) :
{A : Type*} [Category A] (G : A ⥤ Type w)
[HasLimitsOfSize.{u, u+1} A] [PreservesLimitsOfSize.{u, u+1} G]
[G.ReflectsIsomorphisms] (F : Profinite.{u}ᵒᵖ ⥤ A) :
Presheaf.IsSheaf (coherentTopology Profinite) F ↔
Nonempty (PreservesFiniteProducts (F ⋙ G)) ∧ EqualizerCondition (F ⋙ G) := by
rw [Presheaf.isSheaf_iff_isSheaf_forget (coherentTopology Profinite) F G,
rw [Presheaf.isSheaf_iff_isSheaf_comp (coherentTopology Profinite) F G,
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

end Profinite

namespace Stonean

theorem isSheaf_iff_preservesFiniteProducts
(F : Stonean.{u}ᵒᵖ ⥤ Type (u+1)) :
(F : Stonean.{u}ᵒᵖ ⥤ Type w) :
IsSheaf (coherentTopology Stonean) F ↔ Nonempty (PreservesFiniteProducts F) := by
rw [isSheaf_coherent_iff_regular_and_extensive, and_iff_left ?_]
· rw [isSheaf_iff_isSheaf_of_type, extensiveTopology,
Expand All @@ -99,21 +101,24 @@ theorem isSheaf_iff_preservesFiniteProducts
exact isSheafFor_regular_of_projective R F

theorem isSheaf_iff_preservesFiniteProducts'
{A : Type (u+2)} [Category.{u+1} A] (G : A ⥤ Type (u+1))
[HasLimits A] [PreservesLimits G] [G.ReflectsIsomorphisms] (F : Stonean.{u}ᵒᵖ ⥤ A) :
{A : Type*} [Category A] (G : A ⥤ Type w)
[HasLimitsOfSize.{u, u+1} A] [PreservesLimitsOfSize.{u, u+1} G]
[G.ReflectsIsomorphisms] (F : Stonean.{u}ᵒᵖ ⥤ A) :
Presheaf.IsSheaf (coherentTopology Stonean) F ↔
Nonempty (PreservesFiniteProducts (F ⋙ G)) := by
rw [Presheaf.isSheaf_iff_isSheaf_forget (coherentTopology Stonean) F G,
rw [Presheaf.isSheaf_iff_isSheaf_comp (coherentTopology Stonean) F G,
isSheaf_iff_preservesFiniteProducts]

end Stonean

namespace Condensed

variable {A : Type (u+2)} [Category.{u+1} A] (G : A ⥤ Type (u+1)) [HasLimits A] [PreservesLimits G]
variable {A : Type*} [Category A] (G : A ⥤ Type w)
[HasLimitsOfSize.{u, u+1} A] [PreservesLimitsOfSize.{u, u+1} G]
[G.ReflectsIsomorphisms]

instance : HasLimitsOfSize.{u, u+1} A := hasLimitsOfSizeShrink.{u, u+1, u+1, u+1} _
noncomputable instance : PreservesLimitsOfSize.{0, 0} G :=
preservesLimitsOfSizeShrink.{0, u+1, 0, u} _

/-- The condensed set associated to a finite-product-preserving presheaf on `Stonean`. -/
noncomputable def ofSheafStonean (F : Stonean.{u}ᵒᵖ ⥤ A) [PreservesFiniteProducts F] :
Expand Down Expand Up @@ -195,16 +200,19 @@ variable (R : Type (u+1)) [Ring R]
/-- A `CondensedMod` version of `Condensed.ofSheafStonean`. -/
noncomputable abbrev ofSheafStonean (F : Stonean.{u}ᵒᵖ ⥤ ModuleCat.{u+1} R)
[PreservesFiniteProducts F] : CondensedMod R :=
haveI : HasLimitsOfSize.{u, u+1} (ModuleCat R) := hasLimitsOfSizeShrink.{u, u+1, u+1, u+1} _
Condensed.ofSheafStonean (forget _) F

/-- A `CondensedMod` version of `Condensed.ofSheafProfinite`. -/
noncomputable abbrev ofSheafProfinite (F : Profinite.{u}ᵒᵖ ⥤ ModuleCat.{u+1} R)
[PreservesFiniteProducts F] (hF : EqualizerCondition (F ⋙ forget _)) : CondensedMod R :=
haveI : HasLimitsOfSize.{u, u+1} (ModuleCat R) := hasLimitsOfSizeShrink.{u, u+1, u+1, u+1} _
Condensed.ofSheafProfinite (forget _) F hF

/-- A `CondensedMod` version of `Condensed.ofSheafCompHaus`. -/
noncomputable abbrev ofSheafCompHaus (F : CompHaus.{u}ᵒᵖ ⥤ ModuleCat.{u+1} R)
[PreservesFiniteProducts F] (hF : EqualizerCondition (F ⋙ forget _)) : CondensedMod R :=
haveI : HasLimitsOfSize.{u, u+1} (ModuleCat R) := hasLimitsOfSizeShrink.{u, u+1, u+1, u+1} _
Condensed.ofSheafCompHaus (forget _) F hF

end CondensedMod

0 comments on commit 61fdb6c

Please sign in to comment.