NYLL
Module

AbelianSectionLocalization.lean

Nyll.SchemeTheory.Modules.AbelianSectionLocalization
15 declarations indexed from sourceView source ↗

Module documentation

Section localization under an endomorphism

This extracts the finite-cover kernel bound and compact-open gluing argument from the attributed source above. The same induction now uses powers of a natural endomorphism of an abelian sheaf. Scalar multiplication is supplied outside this core, so distinct rings of sections and their module actions are not simultaneously materialized in the gluing proof.

Imports6
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
  • Mathlib.Algebra.Category.Grp.Basic
  • Mathlib.Algebra.Category.Grp.Limits
  • Mathlib.CategoryTheory.Endomorphism
  • Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
  • Mathlib.Tactic.Choose
Imported by2

Declarations

def

sheaf

L43 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.sheaf
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
def sheaf : TopCat.Sheaf Ab.{u} (TopCat.of (X : Type u))
abbrev

res

L46 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.res
Documentation

The actual restriction map of the abelian presheaf.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
abbrev res {V W : X.Opens} (h : V ≤ W) : F.obj (op W) → F.obj (op V)
abbrev

act

L50 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.act
Documentation

Iteration of the fixed natural endomorphism on one open.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
abbrev act (n : ℕ) (V : X.Opens) : F.obj (op V) → F.obj (op V)
lemma

res_res

L53 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.res_res
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
lemma res_res {V W Z : X.Opens} (hVW : V ≤ W) (hZV : Z ≤ V)
    (x : F.obj (op W)) : res F hZV (res F hVW x) = res F (hZV.trans hVW) x
lemma

res_act

L59 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.res_act
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
lemma res_act {V W : X.Opens} (h : V ≤ W) (n : ℕ) (x : F.obj (op W)) :
    res F h (act F α n W x) = act F α n V (res F h x)
lemma

act_add

L65 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.act_add
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
lemma act_add (m n : ℕ) (V : X.Opens) (x : F.obj (op V)) :
    act F α (m + n) V x = act F α m V (act F α n V x)
lemma

act_zero

L70 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.act_zero
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
lemma act_zero (n : ℕ) (V : X.Opens) : act F α n V 0 = 0
lemma

act_sub

L72 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.act_sub
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
lemma act_sub (n : ℕ) (V : X.Opens) (x y : F.obj (op V)) :
    act F α n V (x - y) = act F α n V x - act F α n V y
lemma

res_zero

L75 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.res_zero
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
lemma res_zero {V W : X.Opens} (h : V ≤ W) : res F h 0 = 0
lemma

res_sub

L77 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.res_sub
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
lemma res_sub {V W : X.Opens} (h : V ≤ W) (x y : F.obj (op W)) :
    res F h (x - y) = res F h x - res F h y
def

Clauses

L82 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.Clauses
Documentation

The two elementwise localization conditions for the actual restriction map to the intersection with D.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
Lean source · statement
def Clauses (D U : X.Opens) : Prop
lemma

glue_two

L89 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.glue_two
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
include hF in
Lean source · statement
lemma glue_two {S V : X.Opens} (a : F.obj (op S)) (b : F.obj (op V))
    (h : res F (inf_le_left : S ⊓ V ≤ S) a = res F inf_le_right b) :
    ∃ y : F.obj (op (S ⊔ V)), res F le_sup_left y = a ∧ res F le_sup_right y = b
lemma

ker_of_isCompact

L121 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.ker_of_isCompact
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
variable (D : X.Opens) (hlocal : ∀ V : X.affineOpens, Clauses F α D V.1)
include hF hlocal in
Lean source · statement
lemma ker_of_isCompact {U : X.Opens} (hU : IsCompact (U : Set X))
    (y : F.obj (op U)) (hy : res F (inf_le_left : U ⊓ D ≤ U) y = 0) :
    ∃ n : ℕ, act F α n U y = 0
lemma

surj_of_qcqs

L148 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.surj_of_qcqs
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
variable (D : X.Opens) (hlocal : ∀ V : X.affineOpens, Clauses F α D V.1)
include hF hlocal in
Lean source · statement
lemma surj_of_qcqs {U : X.Opens} (hU : IsCompact (U : Set X))
    (hqs : IsQuasiSeparated (U : Set X)) (x : F.obj (op (U ⊓ D))) :
    ∃ n : ℕ, ∃ y : F.obj (op U), res F inf_le_left y = act F α n (U ⊓ D) x
theorem

clauses_of_qcqs

L207 ↗
AlgebraicGeometry.Scheme.AbelianSectionLocalization.clauses_of_qcqs
Documentation

The existing compact-open gluing argument, with all local hypotheses supplied on the actual affine charts.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.AbelianSectionLocalization
variable {X : Scheme.{u}} (F : X.Opensᵒᵖ ⥤ Ab.{u})
  (hF : CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (X : Type u)) F)
  (α : End F)
variable (D : X.Opens) (hlocal : ∀ V : X.affineOpens, Clauses F α D V.1)
include hF hlocal in
Lean source · statement
theorem clauses_of_qcqs {U : X.Opens} (hU : IsCompact (U : Set X))
    (hqs : IsQuasiSeparated (U : Set X)) : Clauses F α D U

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