NYLL
Module

Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs
14 declarations indexed from sourceView source ↗

Module documentation

Localization of module sections on quasi-compact quasi-separated opens

Imports2
Imported by2

Declarations

abbrev

rM

L46 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.rM
Documentation

Restriction of module sections along an inclusion of open subsets.

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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.rO
Documentation

Restriction of regular functions along an inclusion of open subsets.

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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L63 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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_zero

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_zero {V W : X.Opens} (h : V ≤ W) : rM M h 0 = 0
theorem

rM_sub

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem rM_sub {V W : X.Opens} (h : V ≤ W) (a b : Γ(M, W)) : rM M h (a - b) = rM M h a - rM M h b
theorem

rO_pow

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.F
Documentation

The underlying sheaf of abelian groups of the module sheaf.

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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
def F : TopCat.Sheaf Ab X.carrier
theorem

eq_of_le_bot

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.eq_of_le_bot
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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem eq_of_le_bot {W : X.Opens} (hW : W ≤ ⊥) (s t : Γ(M, W)) : s = t
theorem

glue₂

L80 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.glue₂
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_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem glue₂ {S V : X.Opens} (a : Γ(M, S)) (b : Γ(M, V))
    (h : rM M (inf_le_left : S ⊓ V ≤ S) a = rM M (inf_le_right : S ⊓ V ≤ V) b) :
    ∃ y : Γ(M, S ⊔ V), rM M le_sup_left y = a ∧ rM M le_sup_right y = b
theorem

ker_of_isCompact

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.ker_of_isCompact
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
  Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
include htriv in
Lean source · statement
theorem ker_of_isCompact {U : X.Opens} (hU : IsCompact (U : Set X)) (f : Γ(X, U)) (y : Γ(M, U))
    (hy : rM M (X.basicOpen_le f) y = 0) : ∃ n : ℕ, (f ^ n : Γ(X, U)) • y = 0
theorem

surj_of_qcqs

L136 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs.AlgebraicGeometry.Scheme.Modules.SectLoc.surj_of_qcqs
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocalization_basicOpen_of_locallyTrivial_of_qcqs
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
namespace SectLoc
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
  Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
include htriv in
Lean source · statement
theorem surj_of_qcqs {U : X.Opens} (hU : IsCompact (U : Set X)) (hU' : IsQuasiSeparated (U : Set X))
    (f : Γ(X, U)) (x : Γ(M, X.basicOpen f)) :
    ∃ (n : ℕ) (y : Γ(M, U)), rM M (X.basicOpen_le f) y = rO (X.basicOpen_le f) (f ^ n) • x
theorem

isLocalization_basicOpen_of_locallyTrivial_of_qcqs

L217 ↗
AlgebraicGeometry.Scheme.Modules.isLocalization_basicOpen_of_locallyTrivial_of_qcqs
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_locallyTrivial_of_qcqs
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_locallyTrivial_of_qcqs
    {X : Scheme.{u}} (M : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
    {U : X.Opens} (hU : IsCompact (U : Set X)) (hU' : IsQuasiSeparated (U : Set X)) (f : Γ(X, U)) :
    ((∀ x : Γ(M, X.basicOpen f), ∃ (n : ℕ) (y : Γ(M, U)),
          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), M.presheaf.map (homOfLE (X.basicOpen_le f)).op y = 0 →
            ∃ n : ℕ, (f ^ n : Γ(X, U)) • y = 0))

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