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₁}
[Category.{v₁, u₁} C]
{R : Functor Cᵒᵖ RingCat}
{M : PresheafOfModules R}
{X : C}
{P : Presieve X}
(r : FamilyOfElements (R.comp (forget RingCat)) P)
(m : FamilyOfElements (M.presheaf.comp (forget Ab)) P)
:
FamilyOfElements (M.presheaf.comp (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₀ 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₀' : ↑(R₀.obj (Opposite.op Y)))
(m₀ m₀' : ↑(M₀.obj (Opposite.op Y)))
(hr₀ : (α.app (Opposite.op Y)).hom r₀ = (α.app (Opposite.op Y)).hom 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₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{R₀ R : Functor Cᵒᵖ RingCat}
(α : R₀ ⟶ R)
[Presheaf.IsLocallyInjective J α]
{M₀ : PresheafOfModules R₀}
{A : Functor Cᵒᵖ AddCommGrp}
(φ : M₀.presheaf ⟶ A)
[Presheaf.IsLocallyInjective J φ]
(hA : Presheaf.IsSeparated J A)
{X : C}
(r : ↑(R.obj (Opposite.op X)))
(m : ↑(A.obj (Opposite.op X)))
{Y 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)).hom r₀ = (R.map f.op).hom r)
(hr₀' : (α.app (Opposite.op Z)).hom r₀' = (R.map (CategoryStruct.comp f.op g.op)).hom r)
(hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.map f.op) m)
(hm₀' : (φ.app (Opposite.op Z)) m₀' = (A.map (CategoryStruct.comp f.op g.op)) m)
:
(φ.app (Opposite.op Z)) ((M₀.map g.op).hom (r₀ • m₀)) = (φ.app (Opposite.op Z)) (r₀' • m₀')
theorem
CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : GrothendieckTopology C}
{R₀ R : Functor Cᵒᵖ RingCat}
(α : R₀ ⟶ R)
[Presheaf.IsLocallyInjective J α]
{M₀ : PresheafOfModules R₀}
{A : Functor Cᵒᵖ AddCommGrp}
(φ : M₀.presheaf ⟶ A)
[Presheaf.IsLocallyInjective J φ]
(hA : Presheaf.IsSeparated J A)
{X : C}
(r : ↑(R.obj (Opposite.op X)))
(m : ↑(A.obj (Opposite.op X)))
{P : Presieve X}
(r₀ : FamilyOfElements (R₀.comp (forget RingCat)) P)
(m₀ : FamilyOfElements (M₀.presheaf.comp (forget Ab)) P)
(hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r)
(hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m)
:
((r₀.smul m₀).map (whiskerRight φ (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
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)
:
SMulCandidate α φ r m
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))
:
Nonempty (SMulCandidate α φ r m)
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))
:
Subsingleton (SMulCandidate α φ r m)
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))
:
Unique (SMulCandidate α φ r m)
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))
:
SMulCandidate α φ r m
The (unique) element in SMulCandidate α φ r m.
Equations
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).hom r₀ = (R.val.map f).hom r)
(m₀ : ↑(M₀.obj Y))
(hm₀ : (φ.app Y) m₀ = (A.val.map f) 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))
:
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))
:
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))
:
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 m' : ↑(A.val.obj X))
:
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' : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
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' : ↑(R.val.obj X))
(m : ↑(A.val.obj X))
:
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))
:
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₀ ⟶ (restrictScalars α).obj (sheafify α φ).val
The canonical morphism from a presheaf of modules to its associated sheaf.
Equations
Instances For
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))
:
((toSheafify α φ).app X).hom x = (φ.app X) x
@[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))
:
((toSheafify α φ).app X).hom x = (φ.app X) x
@[simp]-normal form of toSheafify_app_apply.
@[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 φ]
:
(toPresheaf R₀).map (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 φ]
:
IsLocallyInjective J (toSheafify α φ)
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 φ]
:
IsLocallySurjective J (toSheafify α φ)
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)
:
((sheafify α φ).val ⟶ F) ≃ (M₀ ⟶ (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₀ ⟶ (restrictScalars α).obj F)
:
CategoryTheory.CategoryStruct.comp φ ((toPresheaf R.val).map ((sheafifyHomEquiv' α φ hF).symm f)) = (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}
:
(sheafify α φ ⟶ F) ≃ (M₀ ⟶ (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 ((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 ((toPresheaf R₀).map τ₀) φ' = CategoryTheory.CategoryStruct.comp φ τ.val)
:
(sheafifyMap α φ φ' τ₀ τ fac).val = homMk τ.val ⋯