NYLL
Module

Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
9 declarations indexed from sourceView source ↗

Module documentation

Sheafification from localized global sections

Localization conditions on restrictions to basic opens identify the module sheaf with the sheaf associated to its global sections on an affine scheme.

Imports2
Imported by2

Declarations

abbrev

Γ'

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.Γ'
Documentation

The R-module of sections of M over W, using the module-valued presheaf on Spec R.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
Lean source · statement
abbrev Γ' (W : (Spec (.of R)).Opens) : ModuleCat R
abbrev

res'

L54 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.res'
Documentation

The R-linear restriction map from global sections to sections over W.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
Lean source · statement
abbrev res' (W : (Spec (.of R)).Opens) : Γ' M ⊤ →ₗ[R] Γ' M W
theorem

res'_apply

L57 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.res'_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
Lean source · statement
theorem res'_apply (W : (Spec (.of R)).Opens) (y : Γ(M, ⊤)) :
    res' M W y = (M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op) y
theorem

smul_def

L60 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.smul_def
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
Lean source · full declaration
theorem smul_def (W : (Spec (.of R)).Opens) (r : R) (m : Γ' M W) :
    r • m = (((Spec (.of R)).presheaf.map (homOfLE (le_top : W ≤ ⊤)).op).hom
      ((StructureSheaf.globalSectionsIso R).hom.hom r)) • (show Γ(M, W) from m) := rfl
theorem

globalSectionsIso_hom_apply

L65 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.globalSectionsIso_hom_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
omit M in
Lean source · statement
theorem globalSectionsIso_hom_apply (r : R) :
    (StructureSheaf.globalSectionsIso R).hom.hom r = (Scheme.ΓSpecIso (.of R)).inv.hom r
theorem

res_top_top

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.res_top_top
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
omit M in
Lean source · statement
theorem res_top_top (s : Γ(Spec (.of R), ⊤)) :
    ((Spec (.of R)).presheaf.map (homOfLE (le_top : (⊤ : (Spec (.of R)).Opens) ≤ ⊤)).op).hom s = s
def

LocClauses

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.LocClauses
Documentation

Numerator and kernel conditions for restricting global sections to W and clearing denominators with powers of g.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
Lean source · statement
def LocClauses (W : (Spec (.of R)).Opens) (g : Γ(Spec (.of R), ⊤)) : Prop
theorem

isLocalizedModule_of_locClauses

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen.AlgebraicGeometry.Scheme.Modules.TildeOfLoc.isLocalizedModule_of_locClauses
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace TildeOfLoc
variable {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
Lean source · statement
theorem isLocalizedModule_of_locClauses (f : R) (W : (Spec (.of R)).Opens)
    (hunit : IsUnit (algebraMap R (Module.End R (Γ' M W)) f))
    (h : LocClauses M W ((Scheme.ΓSpecIso (.of R)).inv.hom f)) :
    IsLocalizedModule (Submonoid.powers f) (res' M W)
theorem

isIso_fromTildeGamma_of_isLocalization_basicOpen

L112 ↗
AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_of_isLocalization_basicOpen
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_of_isLocalization_basicOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_of_isLocalization_basicOpen
    {R : CommRingCat.{u}} (M : (Spec (.of R)).Modules)
    (hloc : ∀ g : Γ(Spec (.of R), ⊤),
      (∀ x : Γ(M, (Spec (.of R)).basicOpen g), ∃ (n : ℕ) (y : Γ(M, ⊤)),
          M.presheaf.map (homOfLE ((Spec (.of R)).basicOpen_le g)).op y
            = ((Spec (.of R)).presheaf.map (homOfLE ((Spec (.of R)).basicOpen_le g)).op).hom (g ^ n)
                • x)
        ∧ (∀ y : Γ(M, ⊤), M.presheaf.map (homOfLE ((Spec (.of R)).basicOpen_le g)).op y = 0 →
            ∃ n : ℕ, (g ^ n) • y = 0)) :
    IsIso M.fromTildeΓ

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