Module

QuasicoherentAffineLocalization.lean

Nyll.SchemeTheory.Modules.QuasicoherentAffineLocalization

10 declarations indexed from sourceView source ↗

Module documentation

Affine localization of quasicoherent sections

Relates the actual basic-open restriction maps to their elementwise localization clauses.

Imports5

Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.Algebra.Module.LocalizedModule.Away

Imported by3

def

BasicOpenLocalization

L30 ↗

AlgebraicGeometry.Scheme.Modules.BasicOpenLocalization

Documentation

The two elementwise localization conditions for the actual restriction to a basic open. The scalar actions are the existing section actions.

Source context 4 commands

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

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

Lean source · statement

def BasicOpenLocalization {X : Scheme.{u}} (M : X.Modules)
    (U : X.Opens) (f : Γ(X, U)) : Prop

theorem

basicOpenLocalization_restrict_iff

L40 ↗

AlgebraicGeometry.Scheme.Modules.basicOpenLocalization_restrict_iff

Documentation

Restriction along an open immersion preserves the localization clauses on its actual image, including the section and scalar restriction maps.

Source context 4 commands

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

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

Lean source · statement

theorem basicOpenLocalization_restrict_iff {X Y : Scheme.{u}}
    (M : X.Modules) (j : Y ⟶ X) [IsOpenImmersion j]
    (V : Y.Opens) (f : Γ(Y, V)) :
    BasicOpenLocalization (M.restrict j) V f ↔
      BasicOpenLocalization M (j ''ᵁ V) ((j.appIso V).inv f)

theorem

spec_native_localization

L120 ↗

AlgebraicGeometry.Scheme.Modules.spec_native_localization

Source context 4 commands

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

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

Lean source · statement

theorem spec_native_localization (R : CommRingCat.{u}) (M : (Spec R).Modules)
    [M.IsQuasicoherent] (r : R) :
    IsLocalizedModule (Submonoid.powers r)
      (((modulesSpecToSheaf.obj M).obj.map (PrimeSpectrum.basicOpen r).leTop.op).hom)

theorem

spec_native_surjectivity

L126 ↗

AlgebraicGeometry.Scheme.Modules.spec_native_surjectivity

Source context 4 commands

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

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

Lean source · statement

theorem spec_native_surjectivity (R : CommRingCat.{u}) (M : (Spec R).Modules)
    [M.IsQuasicoherent] (r : R)
    (x : (modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen r))) :
    ∃ (n : ℕ) (y : (modulesSpecToSheaf.obj M).obj.obj (op ⊤)),
      ((modulesSpecToSheaf.obj M).obj.map (PrimeSpectrum.basicOpen r).leTop.op).hom y =
        r ^ n • x

theorem

spec_native_kernel

L137 ↗

AlgebraicGeometry.Scheme.Modules.spec_native_kernel

Source context 4 commands

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

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

Lean source · statement

theorem spec_native_kernel (R : CommRingCat.{u}) (M : (Spec R).Modules)
    [M.IsQuasicoherent] (r : R) (y : Γ(M, ⊤))
    (hy : M.presheaf.map (PrimeSpectrum.basicOpen r).leTop.op y = 0) :
    ∃ n : ℕ, r ^ n • y = 0

theorem

spec_basic_scalar

L149 ↗

AlgebraicGeometry.Scheme.Modules.spec_basic_scalar

Source context 4 commands

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

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

Lean source · statement

theorem spec_basic_scalar (R : CommRingCat.{u}) (M : (Spec R).Modules)
    (U : (Spec R).Opens) (r : R) (n : ℕ) (x : Γ(M, U)) :
    r ^ n • x = (Spec R).presheaf.map U.leTop.op
      (((Scheme.ΓSpecIso R).inv r) ^ n) • x

theorem

spec_top_scalar

L155 ↗

AlgebraicGeometry.Scheme.Modules.spec_top_scalar

Source context 4 commands

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

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

Lean source · statement

theorem spec_top_scalar (R : CommRingCat.{u}) (M : (Spec R).Modules)
    (r : R) (n : ℕ) (y : Γ(M, ⊤)) :
    r ^ n • y = ((Scheme.ΓSpecIso R).inv r) ^ n • y

theorem

spec_transported_clauses

L164 ↗

AlgebraicGeometry.Scheme.Modules.spec_transported_clauses

Source context 4 commands

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

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

Lean source · statement

theorem spec_transported_clauses (R : CommRingCat.{u}) (M : (Spec R).Modules)
    [M.IsQuasicoherent] (r : R) :
    (∀ x : Γ(M, (Spec R).basicOpen ((Scheme.ΓSpecIso R).inv r)),
      ∃ (n : ℕ) (y : Γ(M, ⊤)),
        M.presheaf.map ((Spec R).basicOpen ((Scheme.ΓSpecIso R).inv r)).leTop.op y =
          (Spec R).presheaf.map
            ((Spec R).basicOpen ((Scheme.ΓSpecIso R).inv r)).leTop.op
            (((Scheme.ΓSpecIso R).inv r) ^ n) • x) ∧
    (∀ y : Γ(M, ⊤),
      M.presheaf.map ((Spec R).basicOpen ((Scheme.ΓSpecIso R).inv r)).leTop.op y = 0 →
        ∃ n : ℕ, ((Scheme.ΓSpecIso R).inv r) ^ n • y = 0)

theorem

basicOpenLocalization_spec

L184 ↗

AlgebraicGeometry.Scheme.Modules.basicOpenLocalization_spec

Source context 4 commands

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

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

Lean source · statement

theorem basicOpenLocalization_spec {R : CommRingCat.{u}}
    (M : (Spec R).Modules) [M.IsQuasicoherent] (f : Γ(Spec R, ⊤)) :
    BasicOpenLocalization M ⊤ f

theorem

basicOpenLocalization_of_isQuasicoherent

L194 ↗

AlgebraicGeometry.Scheme.Modules.basicOpenLocalization_of_isQuasicoherent

Documentation

Quasicoherence supplies the actual affine localization input to the compact-open section-gluing argument.

Source context 4 commands

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

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

Lean source · statement

theorem basicOpenLocalization_of_isQuasicoherent {X : Scheme.{u}}
    (M : X.Modules) [M.IsQuasicoherent] (U : X.affineOpens) (f : Γ(X, U.1)) :
    BasicOpenLocalization M U.1 f

Module documentation

Affine localization of quasicoherent sections

Declarations