The sheafification functor for presheaves of modules #
In this file, we construct a functor
PresheafOfModules.sheafification α : PresheafOfModules R₀ ⥤ SheafOfModules R
for a locally bijective morphism α : R₀ ⟶ R.val where R₀ is a presheaf of rings
and R a sheaf of rings.
In particular, if α is the identity of R.val, we obtain the
sheafification functor PresheafOfModules R.val ⥤ SheafOfModules R.
noncomputable def
PresheafOfModules.sheafification
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
:
Given a locally bijective morphism α : R₀ ⟶ R.val where R₀ is a presheaf of rings
and R a sheaf of rings (i.e. R identifies to the sheafification of R₀), this is
the associated sheaf of modules functor PresheafOfModules.{v} R₀ ⥤ SheafOfModules.{v} R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
PresheafOfModules.sheafification_map
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
{X✝ Y✝ : PresheafOfModules R₀}
(f : X✝ ⟶ Y✝)
:
(PresheafOfModules.sheafification α).map f = PresheafOfModules.sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Y✝.presheaf) f
((CategoryTheory.presheafToSheaf J AddCommGrp).map ((PresheafOfModules.toPresheaf R₀).map f)) ⋯
noncomputable def
PresheafOfModules.sheafificationCompToSheaf
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
:
(PresheafOfModules.sheafification α).comp (SheafOfModules.toSheaf R) ≅ (PresheafOfModules.toPresheaf R₀).comp (CategoryTheory.presheafToSheaf J AddCommGrp)
The sheafification of presheaves of modules commutes with the functor which forgets the module structures.
Instances For
noncomputable def
PresheafOfModules.sheafificationCompForgetCompToPresheaf
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
:
(PresheafOfModules.sheafification α).comp ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.val)) ≅ (PresheafOfModules.toPresheaf R₀).comp
((CategoryTheory.presheafToSheaf J AddCommGrp).comp (CategoryTheory.sheafToPresheaf J AddCommGrp))
The sheafification of presheaves of modules commutes with the functor which forgets the module structures.
Instances For
noncomputable def
PresheafOfModules.sheafificationHomEquiv
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
{P : PresheafOfModules R₀}
{F : SheafOfModules R}
:
((PresheafOfModules.sheafification α).obj P ⟶ F) ≃ (P ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F))
The bijection between types of morphisms which is part of the adjunction
sheafificationAdjunction.
Equations
Instances For
theorem
PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
{P : PresheafOfModules R₀}
{F : SheafOfModules R}
(f : (PresheafOfModules.sheafification α).obj P ⟶ F)
:
(PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationHomEquiv α) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P.presheaf)
((PresheafOfModules.toPresheaf R.val).map f.val)
theorem
PresheafOfModules.toPresheaf_map_sheafificationHomEquiv
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
{P : PresheafOfModules R₀}
{F : SheafOfModules R}
(f : (PresheafOfModules.sheafification α).obj P ⟶ F)
:
(PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationHomEquiv α) f) = ((CategoryTheory.sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
((SheafOfModules.toSheaf R).map f)
theorem
PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
{P : PresheafOfModules R₀}
{F : SheafOfModules R}
(g : P ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F))
:
(SheafOfModules.toSheaf R).map ((PresheafOfModules.sheafificationHomEquiv α).symm g) = ((CategoryTheory.sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
((PresheafOfModules.toPresheaf R₀).map g)
noncomputable def
PresheafOfModules.sheafificationAdjunction
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
:
Given a locally bijective morphism α : R₀ ⟶ R.val where R₀ is a presheaf of rings
and R a sheaf of rings, this is the adjunction
sheafification.{v} α ⊣ SheafOfModules.forget R ⋙ restrictScalars α.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
PresheafOfModules.sheafificationAdjunction_homEquiv_apply
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
{P : PresheafOfModules R₀}
{F : SheafOfModules R}
(f : (PresheafOfModules.sheafification α).obj P ⟶ F)
:
((PresheafOfModules.sheafificationAdjunction α).homEquiv P F) f = (PresheafOfModules.sheafificationHomEquiv α) f
@[simp]
theorem
PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
(M₀ : PresheafOfModules R₀)
:
(PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationAdjunction α).unit.app M₀) = CategoryTheory.toSheafify J M₀.presheaf
instance
PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasWeakSheafify J AddCommGrp]
:
(PresheafOfModules.sheafification α).IsLeftAdjoint
Equations
- ⋯ = ⋯
noncomputable instance
PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCompSheafOfModulesSheafificationToSheaf
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasSheafify J AddCommGrp]
:
Equations
- ⋯ = ⋯
instance
PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCompSheafToSheafSheafToPresheaf
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
:
((SheafOfModules.toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrp)).ReflectsIsomorphisms
Equations
- ⋯ = ⋯
instance
PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpToSheaf
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
:
(SheafOfModules.toSheaf R).ReflectsIsomorphisms
Equations
- ⋯ = ⋯
noncomputable instance
PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpToSheaf
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
:
Equations
- ⋯ = ⋯
noncomputable instance
PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Sheaf J RingCat}
(α : R₀ ⟶ R.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrp]
[CategoryTheory.HasSheafify J AddCommGrp]
:
Equations
- ⋯ = ⋯