NYLL
Module

Monoidal.lean

Nyll.SchemeTheory.Modules.Monoidal
30 declarations indexed from sourceView source ↗

Module documentation

Tensor products and internal Hom of module sheaves

Module sheafification transfers the tensor product and its unit from module presheaves to module sheaves. The reflective adjunction supplies the monoidal closed structure. The file also defines the resulting tensor, dual, and sheafification operations for schemes.

Imports4
Imported by295

Declarations

abbrev

ringSheaf

L39 ↗
SheafOfModules.ringSheaf
Documentation

The sheaf of rings underlying the given sheaf of commutative rings.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev ringSheaf : Sheaf J RingCat.{u}
abbrev

PMod

L42 ↗
SheafOfModules.PMod
Documentation

The category of module presheaves over the given commutative-ring presheaf.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev PMod
abbrev

presheafW

L45 ↗
SheafOfModules.presheafW
Documentation

The morphisms whose underlying additive presheaf maps belong to the sheafification class.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev presheafW (J : GrothendieckTopology C) (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) :
    MorphismProperty (PMod 𝒪)
abbrev

sheafifyFunctor

L51 ↗
SheafOfModules.sheafifyFunctor
Documentation

The module-sheafification functor for the given sheaf of commutative rings.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev sheafifyFunctor : PMod 𝒪 ⥤ SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)
abbrev

toPMod

L55 ↗
SheafOfModules.toPMod
Documentation

The underlying module-presheaf functor for sheaves of modules.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev toPMod : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪) ⥤ PMod 𝒪
abbrev

sheafifyAdj

L60 ↗
SheafOfModules.sheafifyAdj
Documentation

The adjunction between module sheafification and the underlying presheaf functor.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
abbrev sheafifyAdj : sheafifyFunctor 𝒪 h𝒪 ⊣ toPMod 𝒪 h𝒪
instance

(anonymous instance)

L64 ↗
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
instance : (toPMod 𝒪 h𝒪).Faithful
instance

(anonymous instance)

L65 ↗
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
instance : (toPMod 𝒪 h𝒪).Full
instance

(anonymous instance)

L67 ↗
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
instance : (sheafifyFunctor 𝒪 h𝒪).IsLocalization (presheafW J 𝒪)
theorem

presheafW_isMonoidal

L70 ↗
SheafOfModules.presheafW_isMonoidal
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
include h𝒪 in
Lean source · statement
theorem presheafW_isMonoidal : (presheafW J 𝒪).IsMonoidal
def

sheafifyCounitIso

L80 ↗
SheafOfModules.sheafifyCounitIso
Documentation

The sheafification counit isomorphism for a sheaf of modules.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
Lean source · statement
def sheafifyCounitIso (M : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)) :
    (sheafifyFunctor 𝒪 h𝒪).obj ((toPMod 𝒪 h𝒪).obj M) ≅ M
def

sheafifyUnitIso

L88 ↗
SheafOfModules.sheafifyUnitIso
Documentation

The identification of the sheafified presheaf tensor unit with the sheaf tensor unit.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
Lean source · statement
def sheafifyUnitIso : (sheafifyFunctor 𝒪 h𝒪).obj (𝟙_ (PMod 𝒪)) ≅
    (unit (ringSheaf 𝒪 h𝒪) : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
instance

monoidalCategory

L92 ↗
SheafOfModules.monoidalCategory
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
Lean source · statement
instance monoidalCategory : MonoidalCategory (SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
instance

symmetricCategory

L97 ↗
SheafOfModules.symmetricCategory
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
Lean source · statement
instance symmetricCategory : SymmetricCategory (SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
instance

sheafifyFunctor_monoidal

L102 ↗
SheafOfModules.sheafifyFunctor_monoidal
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
Lean source · statement
instance sheafifyFunctor_monoidal : (sheafifyFunctor 𝒪 h𝒪).Monoidal
theorem

tensorUnit_eq

L108 ↗
SheafOfModules.tensorUnit_eq
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
omit [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] in
Lean source · statement
theorem tensorUnit_eq : 𝟙_ (SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)) = unit _
instance

monoidalClosed

L110 ↗
SheafOfModules.monoidalClosed
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
Lean source · statement
instance monoidalClosed : MonoidalClosed (SheafOfModules.{u} (ringSheaf 𝒪 h𝒪))
def

tensorIsoSheafify

L115 ↗
SheafOfModules.tensorIsoSheafify
Documentation

The comparison between the sheafified presheaf tensor product and the tensor product of module sheaves.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace SheafOfModules
variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
  (𝒪 : Cᵒᵖ ⥤ CommRingCat.{u}) (h𝒪 : Presheaf.IsSheaf J (𝒪 ⋙ forget₂ CommRingCat RingCat))
  [J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify J AddCommGrpCat.{u}]
variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
Lean source · statement
def tensorIsoSheafify (L M : SheafOfModules.{u} (ringSheaf 𝒪 h𝒪)) :
    (sheafifyFunctor 𝒪 h𝒪).obj (L.val ⊗ M.val) ≅ L ⊗ M
instance

monoidalCategory

L126 ↗
AlgebraicGeometry.Scheme.PresheafOfModules.monoidalCategory
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
Lean source · statement
instance Scheme.PresheafOfModules.monoidalCategory : MonoidalCategory X.PresheafOfModules
instance

symmetricCategory

L129 ↗
AlgebraicGeometry.Scheme.PresheafOfModules.symmetricCategory
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
Lean source · statement
instance Scheme.PresheafOfModules.symmetricCategory : SymmetricCategory X.PresheafOfModules
instance

monoidalClosed

L132 ↗
AlgebraicGeometry.Scheme.PresheafOfModules.monoidalClosed
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
Lean source · statement
instance Scheme.PresheafOfModules.monoidalClosed : MonoidalClosed X.PresheafOfModules
instance

monoidalCategory

L136 ↗
AlgebraicGeometry.Scheme.Modules.monoidalCategory
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
Lean source · statement
instance Scheme.Modules.monoidalCategory : MonoidalCategory X.Modules
instance

symmetricCategory

L139 ↗
AlgebraicGeometry.Scheme.Modules.symmetricCategory
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
Lean source · statement
instance Scheme.Modules.symmetricCategory : SymmetricCategory X.Modules
instance

monoidalClosed

L142 ↗
AlgebraicGeometry.Scheme.Modules.monoidalClosed
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
Lean source · statement
instance Scheme.Modules.monoidalClosed : MonoidalClosed X.Modules
abbrev

tensor

L149 ↗
AlgebraicGeometry.Scheme.Modules.tensor
Documentation

The tensor product of two sheaves of modules on a scheme.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
variable {X}
Lean source · statement
abbrev Scheme.Modules.tensor (L M : X.Modules) : X.Modules
abbrev

dual

L152 ↗
AlgebraicGeometry.Scheme.Modules.dual
Documentation

The internal Hom from a sheaf of modules to the tensor unit.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
variable {X}
Lean source · statement
abbrev Scheme.Modules.dual (L : X.Modules) : X.Modules
theorem

tensorUnit_eq

L154 ↗
AlgebraicGeometry.Scheme.Modules.tensorUnit_eq
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
variable {X}
Lean source · statement
theorem Scheme.Modules.tensorUnit_eq :
    𝟙_ X.Modules = SheafOfModules.unit X.ringCatSheaf
abbrev

sheafify

L159 ↗
AlgebraicGeometry.Scheme.Modules.sheafify
Documentation

The sheafification functor from module presheaves to sheaves of modules on a scheme.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
variable {X}
variable (X) in
Lean source · statement
abbrev Scheme.Modules.sheafify : X.PresheafOfModules ⥤ X.Modules
instance

(anonymous instance)

L162 ↗
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
variable {X}
variable (X) in
Lean source · statement
instance : (Scheme.Modules.sheafify X).Monoidal
def

tensorIsoSheafify

L168 ↗
AlgebraicGeometry.Scheme.Modules.tensorIsoSheafify
Documentation

The scheme-module comparison between the sheafified presheaf tensor product and the sheaf tensor product.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory MonoidalCategory Limits
noncomputable section
namespace AlgebraicGeometry
variable (X : Scheme.{u})
variable {X}
variable (X) in
Lean source · statement
def Scheme.Modules.tensorIsoSheafify (L M : X.Modules) :
    (Scheme.Modules.sheafify X).obj (L.val ⊗ M.val) ≅ L ⊗ M

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.