Sheaves of modules over a sheaf of rings #
In this file, we define the category SheafOfModules R when R : Sheaf J RingCat
is a sheaf of rings on a category C equipped with a Grothendieck topology J.
structure
SheafOfModules
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
Type (max (max (max u u₁) (v + 1)) v₁)
A sheaf of modules is a presheaf of modules such that the underlying presheaf of abelian groups is a sheaf.
- val : PresheafOfModules R.val
the underlying presheaf of modules of a sheaf of modules
- isSheaf : CategoryTheory.Presheaf.IsSheaf J self.val.presheaf
structure
SheafOfModules.Hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
(X Y : SheafOfModules R)
:
Type (max u₁ v)
A morphism between sheaves of modules is a morphism between the underlying presheaves of modules.
- val : X.val ⟶ Y.val
a morphism between the underlying presheaves of modules
theorem
SheafOfModules.Hom.ext
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{X Y : SheafOfModules R}
{x y : X.Hom Y}
(val : x.val = y.val)
:
x = y
instance
SheafOfModules.instCategory
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
:
Equations
- SheafOfModules.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
theorem
SheafOfModules.hom_ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{X Y : SheafOfModules R}
{f g : X ⟶ Y}
(h : f.val = g.val)
:
f = g
@[simp]
theorem
SheafOfModules.id_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
(X : SheafOfModules R)
:
@[simp]
theorem
SheafOfModules.comp_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{X Y Z : SheafOfModules R}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
(CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
theorem
SheafOfModules.comp_val_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{X Y Z : SheafOfModules R}
(f : X ⟶ Y)
(g : Y ⟶ Z)
{Z✝ : PresheafOfModules R.val}
(h : Z.val ⟶ Z✝)
:
def
SheafOfModules.forget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
CategoryTheory.Functor (SheafOfModules R) (PresheafOfModules R.val)
The forgetful functor SheafOfModules.{v} R ⥤ PresheafOfModules R.val.
Equations
- SheafOfModules.forget R = { obj := fun (F : SheafOfModules R) => F.val, map := fun {X Y : SheafOfModules R} (φ : X ⟶ Y) => φ.val, map_id := ⋯, map_comp := ⋯ }
@[simp]
theorem
SheafOfModules.forget_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(F : SheafOfModules R)
:
(SheafOfModules.forget R).obj F = F.val
@[simp]
theorem
SheafOfModules.forget_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
{X✝ Y✝ : SheafOfModules R}
(φ : X✝ ⟶ Y✝)
:
(SheafOfModules.forget R).map φ = φ.val
def
SheafOfModules.fullyFaithfulForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
(SheafOfModules.forget R).FullyFaithful
The forget functor SheafOfModules R ⥤ PresheafOfModules R.val is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
SheafOfModules.fullyFaithfulForget_preimage_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
{X✝ Y✝ : SheafOfModules R}
(φ : (SheafOfModules.forget R).obj X✝ ⟶ (SheafOfModules.forget R).obj Y✝)
:
((SheafOfModules.fullyFaithfulForget R).preimage φ).val = φ
instance
SheafOfModules.instFaithfulPresheafOfModulesValRingCatForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
(SheafOfModules.forget R).Faithful
Equations
- ⋯ = ⋯
instance
SheafOfModules.instFullPresheafOfModulesValRingCatForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
(SheafOfModules.forget R).Full
Equations
- ⋯ = ⋯
instance
SheafOfModules.instReflectsIsomorphismsPresheafOfModulesValRingCatForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
(SheafOfModules.forget R).ReflectsIsomorphisms
Equations
- ⋯ = ⋯
def
SheafOfModules.evaluation
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(X : Cᵒᵖ)
:
CategoryTheory.Functor (SheafOfModules R) (ModuleCat ↑(R.val.obj X))
Evaluation on an object X gives a functor
SheafOfModules R ⥤ ModuleCat (R.val.obj X).
Equations
- SheafOfModules.evaluation R X = (SheafOfModules.forget R).comp (PresheafOfModules.evaluation R.val X)
def
SheafOfModules.toSheaf
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
The forget functor SheafOfModules R ⥤ Sheaf J AddCommGrp.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
SheafOfModules.toSheaf_obj_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(M : SheafOfModules R)
:
((SheafOfModules.toSheaf R).obj M).val = M.val.presheaf
@[simp]
theorem
SheafOfModules.toSheaf_map_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
{X✝ Y✝ : SheafOfModules R}
(f : X✝ ⟶ Y✝)
:
((SheafOfModules.toSheaf R).map f).val = ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.val)).map f
noncomputable def
SheafOfModules.forgetToSheafModuleCat
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(X : Cᵒᵖ)
(hX : CategoryTheory.Limits.IsInitial X)
:
CategoryTheory.Functor (SheafOfModules R) (CategoryTheory.Sheaf J (ModuleCat ↑(R.val.obj X)))
The forgetful functor from sheaves of modules over sheaf of ring R to sheaves of R(X)-module
when X is initial.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
SheafOfModules.forgetToSheafModuleCat_map_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(X : Cᵒᵖ)
(hX : CategoryTheory.Limits.IsInitial X)
{X✝ Y✝ : SheafOfModules R}
(f : X✝ ⟶ Y✝)
:
((SheafOfModules.forgetToSheafModuleCat R X hX).map f).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.val
@[simp]
theorem
SheafOfModules.forgetToSheafModuleCat_obj_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(X : Cᵒᵖ)
(hX : CategoryTheory.Limits.IsInitial X)
(M : SheafOfModules R)
:
((SheafOfModules.forgetToSheafModuleCat R X hX).obj M).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.val
def
SheafOfModules.toSheafCompSheafToPresheafIso
{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) ≅ (SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.val)
The canonical isomorphism between
SheafOfModules.toSheaf R ⋙ sheafToPresheaf J AddCommGrp.{v}
and SheafOfModules.forget R ⋙ PresheafOfModules.toPresheaf R.val.
instance
SheafOfModules.instFaithfulSheafAddCommGrpToSheaf
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
(SheafOfModules.toSheaf R).Faithful
Equations
- ⋯ = ⋯
instance
SheafOfModules.instAddCommGroupHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(M N : SheafOfModules R)
:
AddCommGroup (M ⟶ N)
Equations
- SheafOfModules.instAddCommGroupHom R M N = (SheafOfModules.fullyFaithfulForget R).homEquiv.addCommGroup
@[simp]
theorem
SheafOfModules.add_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
{M N : SheafOfModules R}
(f g : M ⟶ N)
:
instance
SheafOfModules.instPreadditive
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
Equations
- SheafOfModules.instPreadditive R = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }
instance
SheafOfModules.instAdditivePresheafOfModulesValRingCatForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
(SheafOfModules.forget R).Additive
Equations
- ⋯ = ⋯
instance
SheafOfModules.instAdditiveSheafAddCommGrpToSheaf
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
(SheafOfModules.toSheaf R).Additive
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
SheafOfModules.sections
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
(M : SheafOfModules R)
:
Type (max u₁ v)
The type of sections of a sheaf of modules.
Equations
- M.sections = M.val.sections
@[reducible, inline]
abbrev
SheafOfModules.sectionsMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M N : SheafOfModules R}
(f : M ⟶ N)
(s : M.sections)
:
N.sections
The map M.sections → N.sections induced by a morphisms M ⟶ N of sheaves of modules.
Equations
- SheafOfModules.sectionsMap f s = PresheafOfModules.sectionsMap f.val s
@[simp]
theorem
SheafOfModules.sectionsMap_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M N P : SheafOfModules R}
(f : M ⟶ N)
(g : N ⟶ P)
(s : M.sections)
:
@[simp]
theorem
SheafOfModules.sectionsMap_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M : SheafOfModules R}
(s : M.sections)
:
def
SheafOfModules.sectionsFunctor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
:
CategoryTheory.Functor (SheafOfModules R) (Type (max u₁ v))
The functor which sends a sheaf of modules to its type of sections.
Equations
- SheafOfModules.sectionsFunctor R = { obj := SheafOfModules.sections, map := fun {X Y : SheafOfModules R} (f : X ⟶ Y) => SheafOfModules.sectionsMap f, map_id := ⋯, map_comp := ⋯ }
@[simp]
theorem
SheafOfModules.sectionsFunctor_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
{X✝ Y✝ : SheafOfModules R}
(f : X✝ ⟶ Y✝)
(s : X✝.sections)
:
(SheafOfModules.sectionsFunctor R).map f s = SheafOfModules.sectionsMap f s
@[simp]
theorem
SheafOfModules.sectionsFunctor_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
(M : SheafOfModules R)
:
(SheafOfModules.sectionsFunctor R).obj M = M.sections
def
SheafOfModules.unit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)]
:
The obvious free sheaf of modules of rank 1.
Equations
- SheafOfModules.unit R = { val := PresheafOfModules.unit R.val, isSheaf := ⋯ }
@[simp]
theorem
SheafOfModules.unit_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(R : CategoryTheory.Sheaf J RingCat)
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)]
:
(SheafOfModules.unit R).val = PresheafOfModules.unit R.val
def
SheafOfModules.unitHomEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)]
(M : SheafOfModules R)
:
(SheafOfModules.unit R ⟶ M) ≃ M.sections
The bijection (unit R ⟶ M) ≃ M.sections for M : SheafOfModules R.
Equations
- M.unitHomEquiv = (SheafOfModules.fullyFaithfulForget R).homEquiv.trans M.val.unitHomEquiv
@[simp]
theorem
SheafOfModules.unitHomEquiv_apply_coe
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)]
(M : SheafOfModules R)
(f : SheafOfModules.unit R ⟶ M)
(X : Cᵒᵖ)
:
↑(M.unitHomEquiv f) X = (f.val.app X) 1
theorem
SheafOfModules.unitHomEquiv_comp_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)]
{M N : SheafOfModules R}
(f : SheafOfModules.unit R ⟶ M)
(p : M ⟶ N)
:
N.unitHomEquiv (CategoryTheory.CategoryStruct.comp f p) = SheafOfModules.sectionsMap p (M.unitHomEquiv f)
theorem
SheafOfModules.unitHomEquiv_symm_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
[J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)]
{M N : SheafOfModules R}
(s : M.sections)
(p : M ⟶ N)
:
CategoryTheory.CategoryStruct.comp (M.unitHomEquiv.symm s) p = N.unitHomEquiv.symm (SheafOfModules.sectionsMap p s)
@[reducible, inline]
abbrev
PresheafOfModules.IsLocallySurjective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
:
A morphism of presheaves of modules is locally surjective if the underlying morphism of presheaves of abelian groups is.
Equations
@[reducible, inline]
abbrev
PresheafOfModules.IsLocallyInjective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : CategoryTheory.GrothendieckTopology C)
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
:
A morphism of presheaves of modules is locally injective if the underlying morphism of presheaves of abelian groups is.
Equations
noncomputable def
PresheafOfModules.homEquivOfIsLocallyBijective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
{N : PresheafOfModules R}
(hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf)
[J.WEqualsLocallyBijective AddCommGrp]
[PresheafOfModules.IsLocallySurjective J f]
[PresheafOfModules.IsLocallyInjective J f]
:
The bijection (M₂ ⟶ N) ≃ (M₁ ⟶ N) induced by a locally bijective morphism
f : M₁ ⟶ M₂ of presheaves of modules, when N is a sheaf.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
PresheafOfModules.homEquivOfIsLocallyBijective_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
{N : PresheafOfModules R}
(hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf)
[J.WEqualsLocallyBijective AddCommGrp]
[PresheafOfModules.IsLocallySurjective J f]
[PresheafOfModules.IsLocallyInjective J f]
(ψ : M₁ ⟶ N)
:
(PresheafOfModules.homEquivOfIsLocallyBijective f hN).symm ψ = PresheafOfModules.homMk
((CategoryTheory.Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN).symm
((PresheafOfModules.toPresheaf R).map ψ))
⋯
@[simp]
theorem
PresheafOfModules.homEquivOfIsLocallyBijective_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
{N : PresheafOfModules R}
(hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf)
[J.WEqualsLocallyBijective AddCommGrp]
[PresheafOfModules.IsLocallySurjective J f]
[PresheafOfModules.IsLocallyInjective J f]
(φ : M₂ ⟶ N)
: