@@ -37,6 +37,16 @@ and `A` live in the same universe.
3737 Cf https://stacks.math.columbia.edu/tag/0073, which is a weaker version of this statement (it's
3838 only over spaces, not sites) and https://stacks.math.columbia.edu/tag/00YR (a), which
3939 additionally assumes filtered colimits.
40+
41+
42+
43+ Occasionally we need to take a limit in `A` of a collection of morphisms of `C` indexed
44+ by a collection of objects in `C`. This turns out to force the morphisms of `A` to be
45+ in a sufficiently large universe. Rather than use `UnivLE` we prove some results for
46+ a category `A'` instead, whose morphism universe of `A'` is defined to be `max u₁ v₁`, where
47+ `u₁, v₁` are the universes for `C`. Perhaps after we get better at handling universe
48+ inequalities this can be changed.
49+
4050-/
4151
4252
@@ -215,15 +225,15 @@ variable {J}
215225 If `P`s a sheaf, `S` is a cover of `X`, and `x` is a collection of morphisms from `E`
216226 to `P` evaluated at terms in the cover which are compatible, then we can amalgamate
217227 the `x`s to obtain a single morphism `E ⟶ P.obj (op X)`. -/
218- def IsSheaf.amalgamate {A : Type u₂} [Category.{max v₁ u₁ } A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A}
228+ def IsSheaf.amalgamate {A : Type u₂} [Category.{v₂ } A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A}
219229 (hP : Presheaf.IsSheaf J P) (S : J.Cover X) (x : ∀ I : S.Arrow, E ⟶ P.obj (op I.Y))
220230 (hx : ∀ I : S.Relation, x I.fst ≫ P.map I.g₁.op = x I.snd ≫ P.map I.g₂.op) : E ⟶ P.obj (op X) :=
221231 (hP _ _ S.condition).amalgamate (fun Y f hf => x ⟨Y, f, hf⟩) fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ w =>
222232 hx ⟨Y₁, Y₂, Z, g₁, g₂, f₁, f₂, h₁, h₂, w⟩
223233#align category_theory.presheaf.is_sheaf.amalgamate CategoryTheory.Presheaf.IsSheaf.amalgamate
224234
225235@ [reassoc (attr := simp)]
226- theorem IsSheaf.amalgamate_map {A : Type u₂} [Category.{max v₁ u₁ } A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A}
236+ theorem IsSheaf.amalgamate_map {A : Type u₂} [Category.{v₂ } A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A}
227237 (hP : Presheaf.IsSheaf J P) (S : J.Cover X) (x : ∀ I : S.Arrow, E ⟶ P.obj (op I.Y))
228238 (hx : ∀ I : S.Relation, x I.fst ≫ P.map I.g₁.op = x I.snd ≫ P.map I.g₂.op) (I : S.Arrow) :
229239 hP.amalgamate S x hx ≫ P.map I.f.op = x _ := by
@@ -233,7 +243,7 @@ theorem IsSheaf.amalgamate_map {A : Type u₂} [Category.{max v₁ u₁} A] {E :
233243 (fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ w => hx ⟨Y₁, Y₂, Z, g₁, g₂, f₁, f₂, h₁, h₂, w⟩) f hf
234244#align category_theory.presheaf.is_sheaf.amalgamate_map CategoryTheory.Presheaf.IsSheaf.amalgamate_map
235245
236- theorem IsSheaf.hom_ext {A : Type u₂} [Category.{max v₁ u₁ } A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A}
246+ theorem IsSheaf.hom_ext {A : Type u₂} [Category.{v₂ } A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A}
237247 (hP : Presheaf.IsSheaf J P) (S : J.Cover X) (e₁ e₂ : E ⟶ P.obj (op X))
238248 (h : ∀ I : S.Arrow, e₁ ≫ P.map I.f.op = e₂ ≫ P.map I.f.op) : e₁ = e₂ :=
239249 (hP _ _ S.condition).isSeparatedFor.ext fun Y f hf => h ⟨Y, f, hf⟩
@@ -454,13 +464,20 @@ namespace Presheaf
454464-- between 00VQ and 00VR.
455465variable {C : Type u₁} [Category.{v₁} C]
456466
457- variable {A : Type u₂} [Category.{max v₁ u₁} A]
467+ -- `A` is a general category; `A'` is a variant where the morphisms live in a large enough
468+ -- universe to guarantee that we can take limits in A of things coming from C.
469+ -- I would have liked to use something like `UnivLE.{max v₁ u₁, v₂}` as a hypothesis on
470+ -- `A`'s morphism universe rather than introducing `A'` but I can't get it to work.
471+ -- So, for now, results which need max v₁ u₁ ≤ v₂ are just stated for `A'` and `P' : Cᵒᵖ ⥤ A'`
472+ -- instead.
473+ variable {A : Type u₂} [Category.{v₂} A]
474+ variable {A' : Type u₂} [Category.{max v₁ u₁} A']
458475
459476variable (J : GrothendieckTopology C)
460477
461478variable {U : C} (R : Presieve U)
462479
463- variable (P : Cᵒᵖ ⥤ A)
480+ variable (P : Cᵒᵖ ⥤ A) (P' : Cᵒᵖ ⥤ A')
464481
465482section MultiequalizerConditions
466483
@@ -527,6 +544,7 @@ end MultiequalizerConditions
527544section
528545
529546variable [HasProducts.{max u₁ v₁} A]
547+ variable [HasProducts.{max u₁ v₁} A']
530548
531549/--
532550The middle object of the fork diagram given in Equation (3) of [ MM92 ] , as well as the fork diagram
@@ -580,6 +598,8 @@ def IsSheaf' (P : Cᵒᵖ ⥤ A) : Prop :=
580598 ∀ (U : C) (R : Presieve U) (_ : generate R ∈ J U), Nonempty (IsLimit (Fork.ofι _ (w R P)))
581599#align category_theory.presheaf.is_sheaf' CategoryTheory.Presheaf.IsSheaf'
582600
601+ -- Again I wonder whether `UnivLE` can somehow be used to allow `s` to take
602+ -- values in a more general universe.
583603/-- (Implementation). An auxiliary lemma to convert between sheaf conditions. -/
584604def isSheafForIsSheafFor' (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type max v₁ u₁)
585605 [∀ J, PreservesLimitsOfShape (Discrete.{max v₁ u₁} J) s] (U : C) (R : Presieve U) :
@@ -608,14 +628,16 @@ def isSheafForIsSheafFor' (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type max v₁ u₁)
608628 simp [Fork.ι]
609629#align category_theory.presheaf.is_sheaf_for_is_sheaf_for' CategoryTheory.Presheaf.isSheafForIsSheafFor'
610630
631+ -- Remark : this lemma and the next use `A'` not `A`; `A'` is `A` but with a universe
632+ -- restriction. Can they be generalised?
611633/-- The equalizer definition of a sheaf given by `isSheaf'` is equivalent to `isSheaf`. -/
612- theorem isSheaf_iff_isSheaf' : IsSheaf J P ↔ IsSheaf' J P := by
634+ theorem isSheaf_iff_isSheaf' : IsSheaf J P' ↔ IsSheaf' J P' := by
613635 constructor
614636 · intro h U R hR
615637 refine' ⟨_⟩
616638 apply coyonedaJointlyReflectsLimits
617639 intro X
618- have q : Presieve.IsSheafFor (P ⋙ coyoneda.obj X) _ := h X.unop _ hR
640+ have q : Presieve.IsSheafFor (P' ⋙ coyoneda.obj X) _ := h X.unop _ hR
619641 rw [← Presieve.isSheafFor_iff_generate] at q
620642 rw [Equalizer.Presieve.sheaf_condition] at q
621643 replace q := Classical.choice q
@@ -645,13 +667,13 @@ Note this lemma applies for "algebraic" categories, eg groups, abelian groups an
645667for the category of topological spaces, topological rings, etc since reflecting isomorphisms doesn't
646668hold.
647669-/
648- theorem isSheaf_iff_isSheaf_forget (s : A ⥤ Type max v₁ u₁) [HasLimits A] [PreservesLimits s]
649- [ReflectsIsomorphisms s] : IsSheaf J P ↔ IsSheaf J (P ⋙ s) := by
670+ theorem isSheaf_iff_isSheaf_forget (s : A' ⥤ Type max v₁ u₁) [HasLimits A' ] [PreservesLimits s]
671+ [ReflectsIsomorphisms s] : IsSheaf J P' ↔ IsSheaf J (P' ⋙ s) := by
650672 rw [isSheaf_iff_isSheaf', isSheaf_iff_isSheaf']
651673 refine' forall_congr' (fun U => ball_congr (fun R _ => _))
652674 letI : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
653- have : IsLimit (s.mapCone (Fork.ofι _ (w R P))) ≃ IsLimit (Fork.ofι _ (w R (P ⋙ s))) :=
654- isSheafForIsSheafFor' P s U R
675+ have : IsLimit (s.mapCone (Fork.ofι _ (w R P' ))) ≃ IsLimit (Fork.ofι _ (w R (P' ⋙ s))) :=
676+ isSheafForIsSheafFor' P' s U R
655677 rw [← Equiv.nonempty_congr this]
656678 constructor
657679 · haveI := preservesSmallestLimitsOfPreservesLimits s
0 commit comments