NYLL
Module

SectionsLocalizationFiniteCover.lean

Nyll.SchemeTheory.Modules.SectionsLocalizationFiniteCover
17 declarations indexed from sourceView source ↗

Module documentation

Basic-open localization from a finite cover

Glue compatible local numerators and bound the powers that annihilate restriction kernels to obtain localization on an affine open from a finite basic-open cover.

Imports2
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.AlgebraicGeometry.AffineScheme
Imported by2

Declarations

abbrev

rM

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rM
Documentation

Restrict a section of M along the open inclusion h.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev rM {V W : X.Opens} (h : V ≤ W) : Γ(M, W) → Γ(M, V)
abbrev

rO

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rO
Documentation

Restrict a regular function along the open inclusion h.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev rO {V W : X.Opens} (h : V ≤ W) : Γ(X, W) → Γ(X, V)
theorem

rM_rM

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rM_rM
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_rM {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (y : Γ(M, V₁)) :
    rM M h₃₂ (rM M h₂₁ y) = rM M (h₃₂.trans h₂₁) y
theorem

rO_rO

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rO_rO
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
omit M in
Lean source · statement
theorem rO_rO {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (g : Γ(X, V₁)) :
    rO h₃₂ (rO h₂₁ g) = rO (h₃₂.trans h₂₁) g
theorem

rM_smul

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rM_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_smul {V W : X.Opens} (h : V ≤ W) (g : Γ(X, W)) (y : Γ(M, W)) :
    rM M h (g • y) = rO h g • rM M h y
theorem

rM_add

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rM_add
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_add {V W : X.Opens} (h : V ≤ W) (y z : Γ(M, W)) : rM M h (y + z) = rM M h y + rM M h z
theorem

rM_sub

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rM_sub
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_sub {V W : X.Opens} (h : V ≤ W) (y z : Γ(M, W)) : rM M h (y - z) = rM M h y - rM M h z
theorem

rM_zero

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rM_zero
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_zero {V W : X.Opens} (h : V ≤ W) : rM M h (0 : Γ(M, W)) = 0
theorem

rO_pow

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.rO_pow
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
omit M in
Lean source · statement
theorem rO_pow {V W : X.Opens} (h : V ≤ W) (g : Γ(X, W)) (n : ℕ) : rO h (g ^ n) = rO h g ^ n
def

F

L81 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.F
Documentation

The sheaf of abelian groups underlying the module sheaf M.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
def F : TopCat.Sheaf Ab X.carrier
theorem

eq_of_forall_rM_eq

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.eq_of_forall_rM_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem eq_of_forall_rM_eq {ι : Type u} (W : ι → X.Opens) (V : X.Opens) (hWV : ∀ i, W i ≤ V)
    (hcov : V ≤ iSup W) (y z : Γ(M, V)) (h : ∀ i, rM M (hWV i) y = rM M (hWV i) z) : y = z
theorem

exists_of_compatible

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.exists_of_compatible
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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 LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem exists_of_compatible {ι : Type u} (W : ι → X.Opens) (V : X.Opens) (hWV : ∀ i, W i ≤ V)
    (hcov : V ≤ iSup W) (z : ∀ i, Γ(M, W i))
    (hz : ∀ i j, rM M (inf_le_left : W i ⊓ W j ≤ W i) (z i) = rM M (inf_le_right : W i ⊓ W j ≤ W j)
        (z j)) :
    ∃ y : Γ(M, V), ∀ i, rM M (hWV i) y = z i
def

LocProp

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocProp
Documentation

The numerator and kernel conditions for restriction to the basic open of g: sections acquire numerators after multiplication by a power of g, and a section vanishing there is killed by a power of g.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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
open LocGlue
Lean source · statement
def LocProp {X : Scheme.{u}} (M : X.Modules) (V : X.Opens) (g : Γ(X, V)) : Prop
theorem

pow_smul_eq_zero_of_le

L114 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.pow_smul_eq_zero_of_le
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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
open LocGlue
namespace LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem pow_smul_eq_zero_of_le {V : X.Opens} (g : Γ(X, V)) (y : Γ(M, V)) {n k : ℕ} (hnk : n ≤ k)
    (h : (g ^ n : Γ(X, V)) • y = 0) : (g ^ k : Γ(X, V)) • y = 0
theorem

exists_of_le

L119 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.LocGlue.exists_of_le
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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
open LocGlue
namespace LocGlue
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem exists_of_le {V : X.Opens} (g : Γ(X, V)) (x : Γ(M, X.basicOpen g)) {n k : ℕ} (hnk : n ≤ k)
    (y : Γ(M, V)) (h : rM M (X.basicOpen_le g) y = rO (X.basicOpen_le g) (g ^ n) • x) :
    rM M (X.basicOpen_le g) ((g ^ (k - n) : Γ(X, V)) • y) = rO (X.basicOpen_le g) (g ^ k) • x
theorem

isLocalization_basicOpen_of_finite_basicOpen_cover'

L127 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover.AlgebraicGeometry.Scheme.Modules.isLocalization_basicOpen_of_finite_basicOpen_cover'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
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
open LocGlue
open LocGlue in
Lean source · statement
theorem isLocalization_basicOpen_of_finite_basicOpen_cover'
    {X : Scheme.{u}} (M : X.Modules) (U : X.affineOpens) (s : Finset Γ(X, U.1))
    (hs : U.1 ≤ ⨆ h ∈ s, X.basicOpen h)
    (hloc : ∀ h ∈ s, ∀ g : Γ(X, X.basicOpen h),
      ((∀ x : Γ(M, X.basicOpen g), ∃ (n : ℕ) (y : Γ(M, X.basicOpen h)),
          M.presheaf.map (homOfLE (X.basicOpen_le g)).op y
            = X.presheaf.map (homOfLE (X.basicOpen_le g)).op (g ^ n) • x)
        ∧ (∀ y : Γ(M, X.basicOpen h), M.presheaf.map (homOfLE (X.basicOpen_le g)).op y = 0 →
            ∃ n : ℕ, (g ^ n : Γ(X, X.basicOpen h)) • y = 0)))
    (hloc₂ : ∀ h ∈ s, ∀ h' ∈ s, ∀ g : Γ(X, X.basicOpen h ⊓ X.basicOpen h'),
      ((∀ x : Γ(M, X.basicOpen g), ∃ (n : ℕ) (y : Γ(M, (X.basicOpen h ⊓ X.basicOpen h'))),
          M.presheaf.map (homOfLE (X.basicOpen_le g)).op y
            = X.presheaf.map (homOfLE (X.basicOpen_le g)).op (g ^ n) • x)
        ∧ (∀ y : Γ(M, (X.basicOpen h ⊓ X.basicOpen h')), M.presheaf.map (homOfLE (X.basicOpen_le
            g)).op y = 0 →
            ∃ n : ℕ, (g ^ n : Γ(X, (X.basicOpen h ⊓ X.basicOpen h'))) • y = 0)))
    (f : Γ(X, U.1)) :
    ((∀ x : Γ(M, X.basicOpen f), ∃ (n : ℕ) (y : Γ(M, U.1)),
          M.presheaf.map (homOfLE (X.basicOpen_le f)).op y
            = X.presheaf.map (homOfLE (X.basicOpen_le f)).op (f ^ n) • x)
        ∧ (∀ y : Γ(M, U.1), M.presheaf.map (homOfLE (X.basicOpen_le f)).op y = 0 →
            ∃ n : ℕ, (f ^ n : Γ(X, U.1)) • y = 0))
theorem

isLocalization_basicOpen_of_finite_basicOpen_cover

L250 ↗
AlgebraicGeometry.Scheme.Modules.isLocalization_basicOpen_of_finite_basicOpen_cover
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_finite_basicOpen_cover
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isLocalization_basicOpen_of_finite_basicOpen_cover
    {X : Scheme.{u}} (M : X.Modules) (U : X.affineOpens) (s : Finset Γ(X, U.1))
    (hs : U.1 ≤ ⨆ h ∈ s, X.basicOpen h)
    (hloc : ∀ h ∈ s, ∀ g : Γ(X, X.basicOpen h),
      ((∀ x : Γ(M, X.basicOpen g), ∃ (n : ℕ) (y : Γ(M, X.basicOpen h)),
          M.presheaf.map (homOfLE (X.basicOpen_le g)).op y
            = X.presheaf.map (homOfLE (X.basicOpen_le g)).op (g ^ n) • x)
        ∧ (∀ y : Γ(M, X.basicOpen h), M.presheaf.map (homOfLE (X.basicOpen_le g)).op y = 0 →
            ∃ n : ℕ, (g ^ n : Γ(X, X.basicOpen h)) • y = 0)))
    (hloc₂ : ∀ h ∈ s, ∀ h' ∈ s, ∀ g : Γ(X, X.basicOpen h ⊓ X.basicOpen h'),
      ((∀ x : Γ(M, X.basicOpen g), ∃ (n : ℕ) (y : Γ(M, (X.basicOpen h ⊓ X.basicOpen h'))),
          M.presheaf.map (homOfLE (X.basicOpen_le g)).op y
            = X.presheaf.map (homOfLE (X.basicOpen_le g)).op (g ^ n) • x)
        ∧ (∀ y : Γ(M, (X.basicOpen h ⊓ X.basicOpen h')), M.presheaf.map (homOfLE (X.basicOpen_le
            g)).op y = 0 →
            ∃ n : ℕ, (g ^ n : Γ(X, (X.basicOpen h ⊓ X.basicOpen h'))) • y = 0)))
    (f : Γ(X, U.1)) :
    ((∀ x : Γ(M, X.basicOpen f), ∃ (n : ℕ) (y : Γ(M, U.1)),
          M.presheaf.map (homOfLE (X.basicOpen_le f)).op y
            = X.presheaf.map (homOfLE (X.basicOpen_le f)).op (f ^ n) • x)
        ∧ (∀ y : Γ(M, U.1), M.presheaf.map (homOfLE (X.basicOpen_le f)).op y = 0 →
            ∃ n : ℕ, (f ^ n : Γ(X, U.1)) • y = 0))

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