Module

Scheme_Modules_isIso_fromTildeGamma_iff_isLocalizedModule.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_fromTildeGamma_iff_isLocalizedModule

1 declaration indexed from sourceView source ↗

Module documentation

Affine modules detected by localization of sections

Characterizes the global-sections comparison by localization on basic open sets.

Imports2

Nyll.AlgebraicCurves.Foundations.CategoryTheory.TopCat_Sheaf_isIso_of_isIso_app_of_isBasis
Mathlib.AlgebraicGeometry.Modules.Tilde

Imported by3

theorem

isIso_fromTildeGamma_iff_isLocalizedModule

L31 ↗

AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_iff_isLocalizedModule

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_fromTildeGamma_iff_isLocalizedModule
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_fromTildeGamma_iff_isLocalizedModule {R :
  CommRingCat.{u}}
    (M : (Spec (.of R)).Modules) :
    IsIso M.fromTildeΓ ↔ ∀ f : R, IsLocalizedModule (Submonoid.powers (M := R) f)
      ((modulesSpecToSheaf.obj M).1.map
        (homOfLE (le_top : PrimeSpectrum.basicOpen f ≤ ⊤)).op).hom

Module documentation

Affine modules detected by localization of sections

Declarations

isIso_fromTildeGamma_iff_isLocalizedModule