Module

GlobalSectionLocalization.lean

Nyll.SchemeTheory.Modules.GlobalSectionLocalization

8 declarations indexed from sourceView source ↗

Module documentation

Localization from global sections

Transports the section-localization results through the existing global coefficient modules.

Imports12

Nyll.SchemeTheory.Modules.SectionLocalization
Nyll.SchemeTheory.Modules.LocalizationRestrictionOfScalars
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.Scheme
Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.Algebra.Category.ModuleCat.Presheaf
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.CategoryTheory.Limits.Shapes.Terminal
Mathlib.Topology.Compactness.Compact
Mathlib.Topology.QuasiSeparated

Imported by2

def

globalModulePresheaf

L35 ↗

AlgebraicGeometry.Scheme.Modules.globalModulePresheaf

Documentation

The existing native global-section module presheaf, evaluated once at its ringed-site owner.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

def globalModulePresheaf {X : Scheme.{u}} (M : X.Modules) :
    X.Opensᵒᵖ ⥤ ModuleCat.{u} Γ(X, ⊤)

lemma

topMap_id

L40 ↗

AlgebraicGeometry.Scheme.Modules.topMap_id

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

lemma topMap_id {X : Scheme.{u}} :
    (X.presheaf.map (⊤ : X.Opens).leTop.op).hom = RingHom.id Γ(X, ⊤)

def

nativeTopIso

L46 ↗

AlgebraicGeometry.Scheme.Modules.nativeTopIso

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

def nativeTopIso {X : Scheme.{u}} (M : X.Modules) :
    (globalModulePresheaf M).obj (op ⊤) ≅ ModuleCat.of Γ(X, ⊤) Γ(M, ⊤)

abbrev

nativeRestriction

L51 ↗

AlgebraicGeometry.Scheme.Modules.nativeRestriction

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

abbrev nativeRestriction {X : Scheme.{u}} (M : X.Modules) (W : X.Opens) :
    ModuleCat.of Γ(X, ⊤) Γ(M, ⊤) ⟶ (globalModulePresheaf M).obj (op W)

theorem

restriction_comparison

L58 ↗

AlgebraicGeometry.Scheme.Modules.restriction_comparison

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem restriction_comparison {X : Scheme.{u}} (M : X.Modules) (W : X.Opens) :
    (globalModulePresheaf M).map W.leTop.op = (nativeTopIso M).hom ≫ nativeRestriction M W

lemma

nativeRestriction_isLocalized

L64 ↗

AlgebraicGeometry.Scheme.Modules.nativeRestriction_isLocalized

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

lemma nativeRestriction_isLocalized {X : Scheme.{u}} (M : X.Modules)
    [M.IsQuasicoherent] [CompactSpace X] [QuasiSeparatedSpace X] (g : Γ(X, ⊤)) :
    IsLocalizedModule (Submonoid.powers g) (nativeRestriction M (X.basicOpen g)).hom

theorem

isLocalizedModule_forgetToModuleCat_of_qcqs

L72 ↗

AlgebraicGeometry.Scheme.Modules.isLocalizedModule_forgetToModuleCat_of_qcqs

Documentation

The native global-section module presheaf sends a basic-open restriction of a quasicoherent module on a qcqs scheme to actual localization.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isLocalizedModule_forgetToModuleCat_of_qcqs {X : Scheme.{u}} (M : X.Modules)
    [M.IsQuasicoherent] [CompactSpace X] [QuasiSeparatedSpace X] (g : Γ(X, ⊤)) :
    IsLocalizedModule (Submonoid.powers g)
      ((globalModulePresheaf M).map (X.basicOpen g).leTop.op).hom

theorem

isLocalizedModule_restrictGlobalScalars_of_qcqs

L84 ↗

AlgebraicGeometry.Scheme.Modules.isLocalizedModule_restrictGlobalScalars_of_qcqs

Documentation

The same genuine localization persists under the native restriction of coefficients along a prescribed ring homomorphism.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isLocalizedModule_restrictGlobalScalars_of_qcqs {R : CommRingCat.{u}}
    {X : Scheme.{u}} (M : X.Modules) [M.IsQuasicoherent]
    [CompactSpace X] [QuasiSeparatedSpace X] (σ : R →+* Γ(X, ⊤)) (r : R) :
    IsLocalizedModule (Submonoid.powers r)
      ((globalModulePresheaf M ⋙
            ModuleCat.restrictScalars σ).map (X.basicOpen (σ r)).leTop.op).hom

Module documentation

Localization from global sections

Declarations