The associated sheaf of a presheaf of modules #
In this file, given a presheaf of modules M₀ over a presheaf of rings R₀,
we construct the associated sheaf of M₀. More precisely, if R is a sheaf of
rings and α : R₀ ⟶ R.val is locally bijective, and A is the sheafification
of the underlying presheaf of abelian groups of M₀, i.e. we have a locally bijective
map φ : M₀.presheaf ⟶ A.val, then we endow A with the structure of a
sheaf of modules over R: this is PresheafOfModules.sheafify α φ.
In many applications, the morphism α shall be the identity, but this more
general construction allows the sheafification of both the presheaf of rings
and the presheaf of modules.
def
CategoryTheory.Presieve.FamilyOfElements.smul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M : PresheafOfModules R}
{X : C}
{P : CategoryTheory.Presieve X}
(r : CategoryTheory.Presieve.FamilyOfElements (R.comp (CategoryTheory.forget RingCat)) P)
(m : CategoryTheory.Presieve.FamilyOfElements (M.presheaf.comp (CategoryTheory.forget Ab)) P)
:
CategoryTheory.Presieve.FamilyOfElements (M.presheaf.comp (CategoryTheory.forget Ab)) P
The scalar multiplication of family of elements of a presheaf of modules M over R
by a family of elements of R.
Instances For
theorem
PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R₀ ⟶ R)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Functor Cᵒᵖ AddCommGrp}
(φ : M₀.presheaf ⟶ A)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
(hA : CategoryTheory.Presheaf.IsSeparated J A)
{Y : C}
(r₀ : ↑(R₀.obj (Opposite.op Y)))
(r₀' : ↑(R₀.obj (Opposite.op Y)))
(m₀ : ↑(M₀.obj (Opposite.op Y)))
(m₀' : ↑(M₀.obj (Opposite.op Y)))
(hr₀ : (α.app (Opposite.op Y)) r₀ = (α.app (Opposite.op Y)) r₀')
(hm₀ : (φ.app (Opposite.op Y)) m₀ = (φ.app (Opposite.op Y)) m₀')
:
(φ.app (Opposite.op Y)) (r₀ • m₀) = (φ.app (Opposite.op Y)) (r₀' • m₀')
theorem
CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R₀ ⟶ R)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Functor Cᵒᵖ AddCommGrp}
(φ : M₀.presheaf ⟶ A)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
(hA : CategoryTheory.Presheaf.IsSeparated J A)
{X : C}
(r : ↑(R.obj (Opposite.op X)))
(m : ↑(A.obj (Opposite.op X)))
{Y : C}
{Z : C}
(f : Y ⟶ X)
(g : Z ⟶ Y)
(r₀ : ↑(R₀.obj (Opposite.op Y)))
(r₀' : ↑(R₀.obj (Opposite.op Z)))
(m₀ : ↑(M₀.obj (Opposite.op Y)))
(m₀' : ↑(M₀.obj (Opposite.op Z)))
(hr₀ : (α.app (Opposite.op Y)) r₀ = (R.map f.op) r)
(hr₀' : (α.app (Opposite.op Z)) r₀' = (R.map (CategoryTheory.CategoryStruct.comp f.op g.op)) r)
(hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.map f.op) m)
(hm₀' : (φ.app (Opposite.op Z)) m₀' = (A.map (CategoryTheory.CategoryStruct.comp f.op g.op)) m)
:
(φ.app (Opposite.op Z)) ((M₀.map g.op) (r₀ • m₀)) = (φ.app (Opposite.op Z)) (r₀' • m₀')
theorem
CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
{R₀ : CategoryTheory.Functor Cᵒᵖ RingCat}
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R₀ ⟶ R)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Functor Cᵒᵖ AddCommGrp}
(φ : M₀.presheaf ⟶ A)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
(hA : CategoryTheory.Presheaf.IsSeparated J A)
{X : C}
(r : ↑(R.obj (Opposite.op X)))
(m : ↑(A.obj (Opposite.op X)))
{P : CategoryTheory.Presieve X}
(r₀ : CategoryTheory.Presieve.FamilyOfElements (R₀.comp (CategoryTheory.forget RingCat)) P)
(m₀ : CategoryTheory.Presieve.FamilyOfElements (M₀.presheaf.comp (CategoryTheory.forget Ab)) P)
(hr₀ : (r₀.map (CategoryTheory.whiskerRight α (CategoryTheory.forget RingCat))).IsAmalgamation r)
(hm₀ : (m₀.map (CategoryTheory.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation m)
:
((r₀.smul m₀).map (CategoryTheory.whiskerRight φ (CategoryTheory.forget Ab))).Compatible
structure
PresheafOfModules.Sheafify.SMulCandidate
{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)
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
Type v
Assuming α : R₀ ⟶ R.val is the sheafification map of a presheaf of rings R₀
and φ : M₀.presheaf ⟶ A.val is the sheafification map of the underlying
sheaf of abelian groups of a presheaf of modules M₀ over R₀, then given
r : R.val.obj X and m : A.val.obj X, this structure contains the data
of x : A.val.obj X along with the property which makes x a good candidate
for the definition of the scalar multiplication r • m.
- x : ↑(A.val.obj X)
The candidate for the scalar product
r • m.
Instances For
theorem
PresheafOfModules.Sheafify.SMulCandidate.h
{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}
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
{φ : M₀.presheaf ⟶ A.val}
{X : Cᵒᵖ}
{r : ↑(R.val.obj X)}
{m : ↑(A.val.obj X)}
(self : PresheafOfModules.Sheafify.SMulCandidate α φ r m)
⦃Y : Cᵒᵖ⦄
(f : X ⟶ Y)
(r₀ : ↑(R₀.obj Y))
(hr₀ : (α.app Y) r₀ = (R.val.map f) r)
(m₀ : ↑(M₀.obj Y))
(hm₀ : (φ.app Y) m₀ = (A.val.map f) m)
:
def
PresheafOfModules.Sheafify.SMulCandidate.mk'
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
(S : CategoryTheory.Sieve (Opposite.unop X))
(hS : S ∈ J (Opposite.unop X))
(r₀ : CategoryTheory.Presieve.FamilyOfElements (R₀.comp (CategoryTheory.forget RingCat)) S.arrows)
(m₀ : CategoryTheory.Presieve.FamilyOfElements (M₀.presheaf.comp (CategoryTheory.forget Ab)) S.arrows)
(hr₀ : (r₀.map (CategoryTheory.whiskerRight α (CategoryTheory.forget RingCat))).IsAmalgamation r)
(hm₀ : (m₀.map (CategoryTheory.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation m)
(a : ↑(A.val.obj X))
(ha : ((r₀.smul m₀).map (CategoryTheory.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation a)
:
Constructor for SMulCandidate.
Equations
- PresheafOfModules.Sheafify.SMulCandidate.mk' α φ r m S hS r₀ m₀ hr₀ hm₀ a ha = { x := a, h := ⋯ }
Instances For
instance
PresheafOfModules.Sheafify.instNonemptySMulCandidate
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
Equations
- ⋯ = ⋯
instance
PresheafOfModules.Sheafify.instSubsingletonSMulCandidate
{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.IsLocallySurjective J α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
Equations
- ⋯ = ⋯
noncomputable instance
PresheafOfModules.Sheafify.instUniqueSMulCandidate
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
Equations
noncomputable def
PresheafOfModules.Sheafify.smulCandidate
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
The (unique) element in SMulCandidate α φ r m.
Equations
- PresheafOfModules.Sheafify.smulCandidate α φ r m = default
Instances For
noncomputable def
PresheafOfModules.Sheafify.smul
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
↑(A.val.obj X)
The scalar multiplication on the sheafification of a presheaf of modules.
Equations
- PresheafOfModules.Sheafify.smul α φ r m = (PresheafOfModules.Sheafify.smulCandidate α φ r m).x
Instances For
theorem
PresheafOfModules.Sheafify.map_smul_eq
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
{Y : Cᵒᵖ}
(f : X ⟶ Y)
(r₀ : ↑(R₀.obj Y))
(hr₀ : (α.app Y) r₀ = (R.val.map f) r)
(m₀ : ↑(M₀.obj Y))
(hm₀ : (φ.app Y) m₀ = (A.val.map f) m)
:
(A.val.map f) (PresheafOfModules.Sheafify.smul α φ r m) = (φ.app Y) (r₀ • m₀)
theorem
PresheafOfModules.Sheafify.one_smul
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(m : ↑(A.val.obj X))
:
PresheafOfModules.Sheafify.smul α φ 1 m = m
theorem
PresheafOfModules.Sheafify.zero_smul
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(m : ↑(A.val.obj X))
:
PresheafOfModules.Sheafify.smul α φ 0 m = 0
theorem
PresheafOfModules.Sheafify.smul_zero
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
:
PresheafOfModules.Sheafify.smul α φ r 0 = 0
theorem
PresheafOfModules.Sheafify.smul_add
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
(m' : ↑(A.val.obj X))
:
PresheafOfModules.Sheafify.smul α φ r (m + m') = PresheafOfModules.Sheafify.smul α φ r m + PresheafOfModules.Sheafify.smul α φ r m'
theorem
PresheafOfModules.Sheafify.add_smul
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(r' : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
PresheafOfModules.Sheafify.smul α φ (r + r') m = PresheafOfModules.Sheafify.smul α φ r m + PresheafOfModules.Sheafify.smul α φ r' m
theorem
PresheafOfModules.Sheafify.mul_smul
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
{X : Cᵒᵖ}
(r : ↑(R.val.obj X))
(r' : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
PresheafOfModules.Sheafify.smul α φ (r * r') m = PresheafOfModules.Sheafify.smul α φ r (PresheafOfModules.Sheafify.smul α φ r' m)
noncomputable def
PresheafOfModules.Sheafify.module
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
(X : Cᵒᵖ)
:
Module ↑(R.val.obj X) ↑(A.val.obj X)
The module structure on the sections of the sheafification of the underlying presheaf of abelian groups of a presheaf of modules.
Equations
- PresheafOfModules.Sheafify.module α φ X = Module.mk ⋯ ⋯
Instances For
theorem
PresheafOfModules.Sheafify.map_smul
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
(X : Cᵒᵖ)
{Y : Cᵒᵖ}
(π : X ⟶ Y)
(r : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
(A.val.map π) (PresheafOfModules.Sheafify.smul α φ r m) = PresheafOfModules.Sheafify.smul α φ ((R.val.map π) r) ((A.val.map π) m)
noncomputable def
PresheafOfModules.sheafify
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
:
Assuming α : R₀ ⟶ R.val is the sheafification map of a presheaf of rings R₀
and φ : M₀.presheaf ⟶ A.val is the sheafification map of the underlying
sheaf of abelian groups of a presheaf of modules M₀ over R₀, this is
the sheaf of modules over R which is obtained by endowing the sections of
A.val with a scalar multiplication.
Equations
- PresheafOfModules.sheafify α φ = { val := PresheafOfModules.ofPresheaf A.val ⋯, isSheaf := ⋯ }
Instances For
def
PresheafOfModules.toSheafify
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
:
M₀ ⟶ (PresheafOfModules.restrictScalars α).obj (PresheafOfModules.sheafify α φ).val
The canonical morphism from a presheaf of modules to its associated sheaf.
Equations
Instances For
@[simp]
theorem
PresheafOfModules.toSheafify_app_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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
(X : Cᵒᵖ)
(x : ↑(M₀.obj X))
:
((PresheafOfModules.toSheafify α φ).app X) x = (φ.app X) x
@[simp]
theorem
PresheafOfModules.toPresheaf_map_toSheafify
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
:
(PresheafOfModules.toPresheaf R₀).map (PresheafOfModules.toSheafify α φ) = φ
instance
PresheafOfModules.instIsLocallyInjectiveToSheafify
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
:
Equations
- ⋯ = ⋯
instance
PresheafOfModules.instIsLocallySurjectiveToSheafify
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
:
Equations
- ⋯ = ⋯
noncomputable def
PresheafOfModules.sheafifyHomEquiv'
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
[J.WEqualsLocallyBijective AddCommGrp]
{F : PresheafOfModules R.val}
(hF : CategoryTheory.Presheaf.IsSheaf J F.presheaf)
:
((PresheafOfModules.sheafify α φ).val ⟶ F) ≃ (M₀ ⟶ (PresheafOfModules.restrictScalars α).obj F)
The bijection ((sheafify α φ).val ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj F) which
is part of the universal property of the sheafification of the presheaf of modules M₀,
when F is a presheaf of modules which is a sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
[J.WEqualsLocallyBijective AddCommGrp]
{F : PresheafOfModules R.val}
(hF : CategoryTheory.Presheaf.IsSheaf J F.presheaf)
(f : M₀ ⟶ (PresheafOfModules.restrictScalars α).obj F)
:
CategoryTheory.CategoryStruct.comp φ
((PresheafOfModules.toPresheaf R.val).map ((PresheafOfModules.sheafifyHomEquiv' α φ hF).symm f)) = (PresheafOfModules.toPresheaf R₀).map f
noncomputable def
PresheafOfModules.sheafifyHomEquiv
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
[J.WEqualsLocallyBijective AddCommGrp]
{F : SheafOfModules R}
:
(PresheafOfModules.sheafify α φ ⟶ F) ≃ (M₀ ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F))
The bijection
(sheafify α φ ⟶ F) ≃ (M₀ ⟶ (restrictScalars α).obj ((SheafOfModules.forget _).obj F))
which is part of the universal property of the sheafification of the presheaf of modules M₀,
for any sheaf of modules F, see PresheafOfModules.sheafificationAdjunction
Equations
- PresheafOfModules.sheafifyHomEquiv α φ = (SheafOfModules.fullyFaithfulForget R).homEquiv.trans (PresheafOfModules.sheafifyHomEquiv' α φ ⋯)
Instances For
def
PresheafOfModules.sheafifyMap
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
[J.WEqualsLocallyBijective AddCommGrp]
{M₀' : PresheafOfModules R₀}
{A' : CategoryTheory.Sheaf J AddCommGrp}
(φ' : M₀'.presheaf ⟶ A'.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ']
[CategoryTheory.Presheaf.IsLocallySurjective J φ']
(τ₀ : M₀ ⟶ M₀')
(τ : A ⟶ A')
(fac : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.toPresheaf R₀).map τ₀) φ' = CategoryTheory.CategoryStruct.comp φ τ.val)
:
The morphism of sheaves of modules sheafify α φ ⟶ sheafify α φ'
induced by morphisms τ₀ : M₀ ⟶ M₀' and τ : A ⟶ A'
which satisfy τ₀.hom ≫ φ' = φ ≫ τ.val.
Equations
- PresheafOfModules.sheafifyMap α φ φ' τ₀ τ fac = { val := PresheafOfModules.homMk τ.val ⋯ }
Instances For
@[simp]
theorem
PresheafOfModules.sheafifyMap_val
{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 α]
{M₀ : PresheafOfModules R₀}
{A : CategoryTheory.Sheaf J AddCommGrp}
(φ : M₀.presheaf ⟶ A.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ]
[CategoryTheory.Presheaf.IsLocallySurjective J φ]
[J.WEqualsLocallyBijective AddCommGrp]
{M₀' : PresheafOfModules R₀}
{A' : CategoryTheory.Sheaf J AddCommGrp}
(φ' : M₀'.presheaf ⟶ A'.val)
[CategoryTheory.Presheaf.IsLocallyInjective J φ']
[CategoryTheory.Presheaf.IsLocallySurjective J φ']
(τ₀ : M₀ ⟶ M₀')
(τ : A ⟶ A')
(fac : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.toPresheaf R₀).map τ₀) φ' = CategoryTheory.CategoryStruct.comp φ τ.val)
:
(PresheafOfModules.sheafifyMap α φ φ' τ₀ τ fac).val = PresheafOfModules.homMk τ.val ⋯