Sheafification #
We construct the sheafification of a presheaf over a site C with values in D whenever
D is a concrete category for which the forgetful functor preserves the appropriate (co)limits
and reflects isomorphisms.
We generally follow the approach of https://stacks.math.columbia.edu/tag/00W1
def
CategoryTheory.Meq
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
(P : Functor Cᵒᵖ D)
(S : J.Cover X)
:
Type (max 0 u v)
A concrete version of the multiequalizer, to be used below.
Equations
- CategoryTheory.Meq P S = { x : (I : S.Arrow) → (CategoryTheory.forget D).obj (P.obj (Opposite.op I.Y)) // ∀ (I : S.Relation), (P.map I.r.g₁.op) (x I.fst) = (P.map I.r.g₂.op) (x I.snd) }
Instances For
instance
CategoryTheory.Meq.instCoeFunForallObjForgetOppositeOpY
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
(P : Functor Cᵒᵖ D)
(S : J.Cover X)
:
CoeFun (Meq P S) fun (x : Meq P S) => (I : S.Arrow) → (forget D).obj (P.obj (Opposite.op I.Y))
Equations
- CategoryTheory.Meq.instCoeFunForallObjForgetOppositeOpY P S = { coe := fun (x : CategoryTheory.Meq P S) => ↑x }
theorem
CategoryTheory.Meq.congr_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
(x : Meq P S)
{Y : C}
{f g : Y ⟶ X}
(h : f = g)
(hf : (↑S).arrows f)
:
↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }
theorem
CategoryTheory.Meq.ext
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
(x y : Meq P S)
(h : ∀ (I : S.Arrow), ↑x I = ↑y I)
:
x = y
theorem
CategoryTheory.Meq.condition
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
(x : Meq P S)
(I : S.Relation)
:
(P.map I.r.g₁.op) (↑x ((S.index P).fstTo I)) = (P.map I.r.g₂.op) (↑x ((S.index P).sndTo I))
def
CategoryTheory.Meq.refine
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
{P : Functor Cᵒᵖ D}
{S T : J.Cover X}
(x : Meq P T)
(e : S ⟶ T)
:
Meq P S
Refine a term of Meq P T with respect to a refinement S ⟶ T of covers.
Equations
- x.refine e = ⟨fun (I : S.Arrow) => ↑x { Y := I.Y, f := I.f, hf := ⋯ }, ⋯⟩
Instances For
@[simp]
theorem
CategoryTheory.Meq.refine_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
{P : Functor Cᵒᵖ D}
{S T : J.Cover X}
(x : Meq P T)
(e : S ⟶ T)
(I : S.Arrow)
:
↑(x.refine e) I = ↑x { Y := I.Y, f := I.f, hf := ⋯ }
def
CategoryTheory.Meq.pullback
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{Y X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
(x : Meq P S)
(f : Y ⟶ X)
:
Meq P ((J.pullback f).obj S)
Pull back a term of Meq P S with respect to a morphism f : Y ⟶ X in C.
Equations
- x.pullback f = ⟨fun (I : ((J.pullback f).obj S).Arrow) => ↑x { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := ⋯ }, ⋯⟩
Instances For
@[simp]
theorem
CategoryTheory.Meq.pullback_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{Y X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
(x : Meq P S)
(f : Y ⟶ X)
(I : ((J.pullback f).obj S).Arrow)
:
↑(x.pullback f) I = ↑x { Y := I.Y, f := CategoryStruct.comp I.f f, hf := ⋯ }
@[simp]
theorem
CategoryTheory.Meq.pullback_refine
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{Y X : C}
{P : Functor Cᵒᵖ D}
{S T : J.Cover X}
(h : S ⟶ T)
(f : Y ⟶ X)
(x : Meq P T)
:
(x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f
def
CategoryTheory.Meq.mk
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
{P : Functor Cᵒᵖ D}
(S : J.Cover X)
(x : (forget D).obj (P.obj (Opposite.op X)))
:
Meq P S
Make a term of Meq P S.
Equations
- CategoryTheory.Meq.mk S x = ⟨fun (I : S.Arrow) => (P.map I.f.op) x, ⋯⟩
Instances For
theorem
CategoryTheory.Meq.mk_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
{X : C}
{P : Functor Cᵒᵖ D}
(S : J.Cover X)
(x : (forget D).obj (P.obj (Opposite.op X)))
(I : S.Arrow)
:
noncomputable def
CategoryTheory.Meq.equiv
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
{X : C}
(P : Functor Cᵒᵖ D)
(S : J.Cover X)
[Limits.HasMultiequalizer (S.index P)]
:
(forget D).obj (Limits.multiequalizer (S.index P)) ≃ Meq P S
The equivalence between the type associated to multiequalizer (S.index P) and Meq P S.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Meq.equiv_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
{X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
[Limits.HasMultiequalizer (S.index P)]
(x : (forget D).obj (Limits.multiequalizer (S.index P)))
(I : S.Arrow)
:
↑((equiv P S) x) I = (Limits.Multiequalizer.ι (S.index P) I) x
theorem
CategoryTheory.Meq.equiv_symm_eq_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
{X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
[Limits.HasMultiequalizer (S.index P)]
(x : Meq P S)
(I : S.Arrow)
:
(Limits.Multiequalizer.ι (S.index P) I) ((equiv P S).symm x) = ↑x I
def
CategoryTheory.GrothendieckTopology.Plus.mk
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
{X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
(x : Meq P S)
:
(forget D).obj ((J.plusObj P).obj (Opposite.op X))
Make a term of (J.plusObj P).obj (op X) from x : Meq P S.
Equations
- CategoryTheory.GrothendieckTopology.Plus.mk x = (CategoryTheory.Limits.colimit.ι (J.diagram P X) (Opposite.op S)) ((CategoryTheory.Meq.equiv P S).symm x)
Instances For
theorem
CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
{Y X : C}
{P : Functor Cᵒᵖ D}
{S : J.Cover X}
(x : Meq P S)
(f : Y ⟶ X)
:
theorem
CategoryTheory.GrothendieckTopology.Plus.toPlus_mk
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
{X : C}
{P : Functor Cᵒᵖ D}
(S : J.Cover X)
(x : (forget D).obj (P.obj (Opposite.op X)))
:
((J.toPlus P).app (Opposite.op X)) x = mk (Meq.mk S x)
theorem
CategoryTheory.GrothendieckTopology.Plus.toPlus_apply
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
{X : C}
{P : Functor Cᵒᵖ D}
(S : J.Cover X)
(x : Meq P S)
(I : S.Arrow)
:
((J.toPlus P).app (Opposite.op I.Y)) (↑x I) = ((J.plusObj P).map I.f.op) (mk x)
theorem
CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
{X : C}
{P : Functor Cᵒᵖ D}
(x : (forget D).obj (P.obj (Opposite.op X)))
:
((J.toPlus P).app (Opposite.op X)) x = mk (Meq.mk ⊤ x)
theorem
CategoryTheory.GrothendieckTopology.Plus.exists_rep
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
{X : C}
{P : Functor Cᵒᵖ D}
(x : (forget D).obj ((J.plusObj P).obj (Opposite.op X)))
:
theorem
CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
{X : C}
{P : Functor Cᵒᵖ D}
{S T : J.Cover X}
(x : Meq P S)
(y : Meq P T)
:
theorem
CategoryTheory.GrothendieckTopology.Plus.sep
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
{X : C}
(P : Functor Cᵒᵖ D)
(S : J.Cover X)
(x y : (forget D).obj ((J.plusObj P).obj (Opposite.op X)))
(h : ∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) x = ((J.plusObj P).map I.f.op) y)
:
x = y
P⁺ is always separated.
theorem
CategoryTheory.GrothendieckTopology.Plus.inj_of_sep
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
(P : Functor Cᵒᵖ D)
(hsep :
∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (Opposite.op X))),
(∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y)
(X : C)
:
Function.Injective ⇑((J.toPlus P).app (Opposite.op X))
def
CategoryTheory.GrothendieckTopology.Plus.meqOfSep
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
(P : Functor Cᵒᵖ D)
(hsep :
∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (Opposite.op X))),
(∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y)
(X : C)
(S : J.Cover X)
(s : Meq (J.plusObj P) S)
(T : (I : S.Arrow) → J.Cover I.Y)
(t : (I : S.Arrow) → Meq P (T I))
(ht : ∀ (I : S.Arrow), ↑s I = mk (t I))
:
Meq P (S.bind T)
An auxiliary definition to be used in the proof of exists_of_sep below.
Given a compatible family of local sections for P⁺, and representatives of said sections,
construct a compatible family of local sections of P over the combination of the covers
associated to the representatives.
The separatedness condition is used to prove compatibility among these local sections of P.
Equations
- CategoryTheory.GrothendieckTopology.Plus.meqOfSep P hsep X S s T t ht = ⟨fun (I : (S.bind T).Arrow) => ↑(t I.fromMiddle) I.toMiddle, ⋯⟩
Instances For
theorem
CategoryTheory.GrothendieckTopology.Plus.exists_of_sep
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
(P : Functor Cᵒᵖ D)
(hsep :
∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (Opposite.op X))),
(∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y)
(X : C)
(S : J.Cover X)
(s : Meq (J.plusObj P) S)
:
∃ (t : (forget D).obj ((J.plusObj P).obj (Opposite.op X))), Meq.mk S t = s
theorem
CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
(P : Functor Cᵒᵖ D)
(hsep :
∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (Opposite.op X))),
(∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y)
:
Presheaf.IsSheaf J (J.plusObj P)
If P is separated, then P⁺ is a sheaf.
theorem
CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
(P : Functor Cᵒᵖ D)
:
Presheaf.IsSheaf J (J.plusObj (J.plusObj P))
P⁺⁺ is always a sheaf.
noncomputable def
CategoryTheory.GrothendieckTopology.sheafify
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
(P : Functor Cᵒᵖ D)
:
The sheafification of a presheaf P.
NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!
Equations
- J.sheafify P = J.plusObj (J.plusObj P)
Instances For
noncomputable def
CategoryTheory.GrothendieckTopology.toSheafify
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
(P : Functor Cᵒᵖ D)
:
P ⟶ J.sheafify P
The canonical map from P to its sheafification.
Equations
- J.toSheafify P = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap (J.toPlus P))
Instances For
noncomputable def
CategoryTheory.GrothendieckTopology.sheafifyMap
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
:
J.sheafify P ⟶ J.sheafify Q
The canonical map on sheafifications induced by a morphism.
Equations
- J.sheafifyMap η = J.plusMap (J.plusMap η)
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.sheafifyMap_id
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
(P : Functor Cᵒᵖ D)
:
J.sheafifyMap (CategoryStruct.id P) = CategoryStruct.id (J.sheafify P)
@[simp]
theorem
CategoryTheory.GrothendieckTopology.sheafifyMap_comp
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q R : Functor Cᵒᵖ D}
(η : P ⟶ Q)
(γ : Q ⟶ R)
:
J.sheafifyMap (CategoryStruct.comp η γ) = CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyMap γ)
@[simp]
theorem
CategoryTheory.GrothendieckTopology.toSheafify_naturality
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
:
CategoryStruct.comp η (J.toSheafify Q) = CategoryStruct.comp (J.toSheafify P) (J.sheafifyMap η)
@[simp]
theorem
CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
{Z : Functor Cᵒᵖ D}
(h : J.sheafify Q ⟶ Z)
:
CategoryStruct.comp η (CategoryStruct.comp (J.toSheafify Q) h) = CategoryStruct.comp (J.toSheafify P) (CategoryStruct.comp (J.sheafifyMap η) h)
noncomputable def
CategoryTheory.GrothendieckTopology.sheafification
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
:
The sheafification of a presheaf P, as a functor.
NOTE: Additional hypotheses are needed to obtain a proof that this is a sheaf!
Equations
- J.sheafification D = (J.plusFunctor D).comp (J.plusFunctor D)
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.sheafification_obj
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
(P : Functor Cᵒᵖ D)
:
(J.sheafification D).obj P = J.sheafify P
@[simp]
theorem
CategoryTheory.GrothendieckTopology.sheafification_map
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
:
(J.sheafification D).map η = J.sheafifyMap η
noncomputable def
CategoryTheory.GrothendieckTopology.toSheafification
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
:
Functor.id (Functor Cᵒᵖ D) ⟶ J.sheafification D
The canonical map from P to its sheafification, as a natural transformation.
Note: We only show this is a sheaf under additional hypotheses on D.
Equations
- J.toSheafification D = CategoryTheory.CategoryStruct.comp (J.toPlusNatTrans D) (CategoryTheory.whiskerRight (J.toPlusNatTrans D) (J.plusFunctor D))
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.toSheafification_app
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
(P : Functor Cᵒᵖ D)
:
(J.toSheafification D).app P = J.toSheafify P
theorem
CategoryTheory.GrothendieckTopology.isIso_toSheafify
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P : Functor Cᵒᵖ D}
(hP : Presheaf.IsSheaf J P)
:
IsIso (J.toSheafify P)
noncomputable def
CategoryTheory.GrothendieckTopology.isoSheafify
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P : Functor Cᵒᵖ D}
(hP : Presheaf.IsSheaf J P)
:
P ≅ J.sheafify P
If P is a sheaf, then P is isomorphic to J.sheafify P.
Equations
- J.isoSheafify hP = CategoryTheory.asIso (J.toSheafify P)
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.isoSheafify_hom
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P : Functor Cᵒᵖ D}
(hP : Presheaf.IsSheaf J P)
:
(J.isoSheafify hP).hom = J.toSheafify P
noncomputable def
CategoryTheory.GrothendieckTopology.sheafifyLift
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
(hQ : Presheaf.IsSheaf J Q)
:
J.sheafify P ⟶ Q
Given a sheaf Q and a morphism P ⟶ Q, construct a morphism from J.sheafify P to Q.
Equations
- J.sheafifyLift η hQ = J.plusLift (J.plusLift η hQ) hQ
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
(hQ : Presheaf.IsSheaf J Q)
:
CategoryStruct.comp (J.toSheafify P) (J.sheafifyLift η hQ) = η
@[simp]
theorem
CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
(hQ : Presheaf.IsSheaf J Q)
{Z : Functor Cᵒᵖ D}
(h : Q ⟶ Z)
:
CategoryStruct.comp (J.toSheafify P) (CategoryStruct.comp (J.sheafifyLift η hQ) h) = CategoryStruct.comp η h
theorem
CategoryTheory.GrothendieckTopology.sheafifyLift_unique
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η : P ⟶ Q)
(hQ : Presheaf.IsSheaf J Q)
(γ : J.sheafify P ⟶ Q)
:
CategoryStruct.comp (J.toSheafify P) γ = η → γ = J.sheafifyLift η hQ
@[simp]
theorem
CategoryTheory.GrothendieckTopology.isoSheafify_inv
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P : Functor Cᵒᵖ D}
(hP : Presheaf.IsSheaf J P)
:
(J.isoSheafify hP).inv = J.sheafifyLift (CategoryStruct.id P) hP
theorem
CategoryTheory.GrothendieckTopology.sheafify_hom_ext
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : Functor Cᵒᵖ D}
(η γ : J.sheafify P ⟶ Q)
(hQ : Presheaf.IsSheaf J Q)
(h : CategoryStruct.comp (J.toSheafify P) η = CategoryStruct.comp (J.toSheafify P) γ)
:
η = γ
@[simp]
theorem
CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q R : Functor Cᵒᵖ D}
(η : P ⟶ Q)
(γ : Q ⟶ R)
(hR : Presheaf.IsSheaf J R)
:
CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyLift γ hR) = J.sheafifyLift (CategoryStruct.comp η γ) hR
@[simp]
theorem
CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q R : Functor Cᵒᵖ D}
(η : P ⟶ Q)
(γ : Q ⟶ R)
(hR : Presheaf.IsSheaf J R)
{Z : Functor Cᵒᵖ D}
(h : R ⟶ Z)
:
CategoryStruct.comp (J.sheafifyMap η) (CategoryStruct.comp (J.sheafifyLift γ hR) h) = CategoryStruct.comp (J.sheafifyLift (CategoryStruct.comp η γ) hR) h
theorem
CategoryTheory.GrothendieckTopology.sheafify_isSheaf
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
(P : Functor Cᵒᵖ D)
:
Presheaf.IsSheaf J (J.sheafify P)
noncomputable def
CategoryTheory.plusPlusSheaf
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
:
The sheafification functor, as a functor taking values in Sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.plusPlusSheaf_map_val
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
{X✝ Y✝ : Functor Cᵒᵖ D}
(η : X✝ ⟶ Y✝)
:
((plusPlusSheaf J D).map η).val = J.sheafifyMap η
@[simp]
theorem
CategoryTheory.plusPlusSheaf_obj_val
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
(P : Functor Cᵒᵖ D)
:
((plusPlusSheaf J D).obj P).val = J.sheafify P
instance
CategoryTheory.plusPlusSheaf_preservesZeroMorphisms
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
[Preadditive D]
:
(plusPlusSheaf J D).PreservesZeroMorphisms
noncomputable def
CategoryTheory.plusPlusAdjunction
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
:
plusPlusSheaf J D ⊣ sheafToPresheaf J D
The sheafification functor is left adjoint to the forgetful functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.plusPlusAdjunction_unit_app
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
(X : Functor Cᵒᵖ D)
:
(plusPlusAdjunction J D).unit.app X = J.toSheafify X
@[simp]
theorem
CategoryTheory.plusPlusAdjunction_counit_app_val
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
(Y : Sheaf J D)
:
((plusPlusAdjunction J D).counit.app Y).val = J.sheafifyLift (CategoryStruct.id Y.val) ⋯
instance
CategoryTheory.sheafToPresheaf_isRightAdjoint
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
:
(sheafToPresheaf J D).IsRightAdjoint
instance
CategoryTheory.presheaf_mono_of_mono
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
{F G : Sheaf J D}
(f : F ⟶ G)
[Mono f]
:
Mono f.val
theorem
CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(D : Type w)
[Category.{max v u, w} D]
[HasForget D]
[Limits.PreservesLimits (forget D)]
[∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)]
[∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
[∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
[(forget D).ReflectsIsomorphisms]
{F G : Sheaf J D}
(f : F ⟶ G)
: