Module

ModulesSectionZeroScheme.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesSectionZeroScheme

22 declarations indexed from sourceView source ↗

Module documentation

Zero schemes of module sections

Local coefficients of a module section generate its zero-scheme ideal. This file supplies restriction and pullback operations, coefficient maps, and the associated closed subscheme.

Imports2

Imported by93

def

toUnitSection

L36 ↗

AlgebraicGeometry.Scheme.Modules.toUnitSection

Documentation

View a structure-sheaf section as a section of the unit module.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def toUnitSection (U : X.Opens) (r : Γ(X, U)) : Γ(𝟙_ X.Modules, U)

def

ofUnitSection

L39 ↗

AlgebraicGeometry.Scheme.Modules.ofUnitSection

Documentation

View a section of the unit module as a structure-sheaf section.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def ofUnitSection (U : X.Opens) (m : Γ(𝟙_ X.Modules, U)) : Γ(X, U)

lemma

ofUnitSection_toUnitSection

L41 ↗

AlgebraicGeometry.Scheme.Modules.ofUnitSection_toUnitSection

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma ofUnitSection_toUnitSection (U : X.Opens) (r : Γ(X, U)) :
    ofUnitSection U (toUnitSection U r) = r

lemma

toUnitSection_ofUnitSection

L44 ↗

AlgebraicGeometry.Scheme.Modules.toUnitSection_ofUnitSection

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma toUnitSection_ofUnitSection (U : X.Opens) (m : Γ(𝟙_ X.Modules, U)) :
    toUnitSection U (ofUnitSection U m) = m

lemma

ofUnitSection_injective

L47 ↗

AlgebraicGeometry.Scheme.Modules.ofUnitSection_injective

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma ofUnitSection_injective (U : X.Opens) : Function.Injective (ofUnitSection (X := X) U)

lemma

ofUnitSection_map

L50 ↗

AlgebraicGeometry.Scheme.Modules.ofUnitSection_map

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma ofUnitSection_map {U V : X.Opens} (i : V ⟶ U) (m : Γ(𝟙_ X.Modules, U)) :
    ofUnitSection V ((𝟙_ X.Modules).presheaf.map i.op m) =
      X.presheaf.map i.op (ofUnitSection U m)

lemma

ofUnitSection_smul

L54 ↗

AlgebraicGeometry.Scheme.Modules.ofUnitSection_smul

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma ofUnitSection_smul (U : X.Opens) (r : Γ(X, U)) (m : Γ(𝟙_ X.Modules, U)) :
    ofUnitSection U (r • m) = r * ofUnitSection U m

def

restrictSection

L58 ↗

AlgebraicGeometry.Scheme.Modules.restrictSection

Documentation

Restrict a global module section to the indicated open subscheme.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def restrictSection (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens) : Γ(M.restrict U.ι, ⊤)

def

coeff

L62 ↗

AlgebraicGeometry.Scheme.Modules.coeff

Documentation

The coefficient of the restricted section under a map to the unit module.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def coeff (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
    (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) : Γ(X, U)

def

coeffIdeal

L67 ↗

AlgebraicGeometry.Scheme.Modules.coeffIdeal

Documentation

The ideal generated by all local coefficients of the section.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def coeffIdeal (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens) : Ideal Γ(X, U)

lemma

coeff_mem_coeffIdeal

L70 ↗

AlgebraicGeometry.Scheme.Modules.coeff_mem_coeffIdeal

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma coeff_mem_coeffIdeal (s : 𝟙_ X.Modules ⟶ M) (U : X.Opens)
    (φ : M.restrict U.ι ⟶ 𝟙_ (U : Scheme.{u}).Modules) : coeff s U φ ∈ coeffIdeal s U

def

zeroSchemeIdeal

L75 ↗

AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal

Documentation

The infimum of ideal sheaves containing the coefficient ideals on affine opens.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def zeroSchemeIdeal (s : 𝟙_ X.Modules ⟶ M) : X.IdealSheafData

abbrev

zeroScheme

L79 ↗

AlgebraicGeometry.Scheme.Modules.zeroScheme

Documentation

The closed subscheme associated with the zero-scheme ideal of the section.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

abbrev zeroScheme (s : 𝟙_ X.Modules ⟶ M) : Scheme.{u}

lemma

zeroSchemeIdeal_le

L82 ↗

AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal_le

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma zeroSchemeIdeal_le {s : 𝟙_ X.Modules ⟶ M} {J : X.IdealSheafData}
    (h : ∀ U : X.affineOpens, coeffIdeal s U.1 ≤ J.ideal U) : zeroSchemeIdeal s ≤ J

lemma

le_zeroSchemeIdeal

L86 ↗

AlgebraicGeometry.Scheme.Modules.le_zeroSchemeIdeal

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma le_zeroSchemeIdeal {s : 𝟙_ X.Modules ⟶ M} {K : X.IdealSheafData}
    (h : ∀ J : X.IdealSheafData, (∀ U : X.affineOpens, coeffIdeal s U.1 ≤ J.ideal U) → K ≤ J) :
    K ≤ zeroSchemeIdeal s

lemma

zeroSchemeIdeal_eq_of_isLeast

L91 ↗

AlgebraicGeometry.Scheme.Modules.zeroSchemeIdeal_eq_of_isLeast

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma zeroSchemeIdeal_eq_of_isLeast {s : 𝟙_ X.Modules ⟶ M} {P : X.IdealSheafData}
    (hP : IsLeast {J : X.IdealSheafData | ∀ U : X.affineOpens, coeffIdeal s U.1 ≤ J.ideal U} P) :
    zeroSchemeIdeal s = P

def

pullbackSection

L97 ↗

AlgebraicGeometry.Scheme.Modules.pullbackSection

Documentation

Pull back a module section using the canonical pullback isomorphism for the unit.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def pullbackSection {X' : Scheme.{u}} (F : X' ⟶ X) (s : 𝟙_ X.Modules ⟶ M) :
    𝟙_ X'.Modules ⟶ (Scheme.Modules.pullback F).obj M

lemma

pullbackSection_def

L101 ↗

AlgebraicGeometry.Scheme.Modules.pullbackSection_def

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

lemma pullbackSection_def {X' : Scheme.{u}} (F : X' ⟶ X) (s : 𝟙_ X.Modules ⟶ M) :
    pullbackSection F s =
      (Scheme.Modules.pullbackUnitIso F).inv ≫ (Scheme.Modules.pullback F).map s

def

restrictIsoOfLE

L107 ↗

AlgebraicGeometry.Scheme.Modules.restrictIsoOfLE

Documentation

Restrict a pullback trivialization to a smaller open subscheme.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def restrictIsoOfLE {U W : X.Opens} (h : W ≤ U)
    (e : (Scheme.Modules.pullback U.ι).obj M ≅ SheafOfModules.unit (U : Scheme.{u}).ringCatSheaf) :
    M.restrict W.ι ≅ 𝟙_ (W : Scheme.{u}).Modules

theorem

exists_restrict_iso

L116 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_restrict_iso

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem IsInvertible.exists_restrict_iso (hM : Scheme.Modules.IsInvertible M) {V : X.Opens} {x : X}
    (hx : x ∈ V) :
    ∃ U : X.affineOpens, x ∈ U.1 ∧ U.1 ≤ V ∧
      Nonempty (M.restrict U.1.ι ≅ 𝟙_ (U.1 : Scheme.{u}).Modules)

def

sectionDual

L127 ↗

AlgebraicGeometry.Scheme.Modules.sectionDual

Documentation

The dual map of a section, valued in the unit module.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

def sectionDual (s : 𝟙_ X.Modules ⟶ M) : Scheme.Modules.dual M ⟶ 𝟙_ X.Modules

def

invModuleSection

L134 ↗

AlgebraicGeometry.Scheme.IdealSheafData.invModuleSection

Documentation

The canonical section of the dual ideal module induced by the ideal inclusion.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory
noncomputable section
namespace AlgebraicGeometry

Lean source · statement

def Scheme.IdealSheafData.invModuleSection {X : Scheme.{u}} (I : X.IdealSheafData) :
    𝟙_ X.Modules ⟶ I.invModule

Module documentation

Zero schemes of module sections

Declarations