NYLL
Module

Scheme_Modules_IsInvertible_exists_functionField_presentation.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_functionField_presentation
28 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible exists function Field presentation

Imports2
Imported by4

Declarations

def

trivApp

L39 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.trivApp
Documentation

The section map of the chosen local trivialization.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
def trivApp (V : W.toScheme.Opens) : Γ(M, W.ι ''ᵁ V) →+ Γ(W.toScheme, V)
theorem

trivApp_apply

L42 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.trivApp_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
theorem trivApp_apply (V : W.toScheme.Opens) (m : Γ(M, W.ι ''ᵁ V)) :
    trivApp M W E V m = ((Scheme.Modules.Hom.app E.hom V).hom : Γ(M.restrict W.ι, V) →+
      Γ(W.toScheme, V)) m
def

coord

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.coord
Documentation

Local coordinates in the original scheme obtained from the trivialization and the canonical section ring isomorphism.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
def coord (V : W.toScheme.Opens) : Γ(M, W.ι ''ᵁ V) →+ Γ(X, W.ι ''ᵁ V)
theorem

coord_apply

L52 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.coord_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
theorem coord_apply (V : W.toScheme.Opens) (m : Γ(M, W.ι ''ᵁ V)) :
    coord M W E V m = (W.ι.appIso V).inv.hom (trivApp M W E V m)
theorem

trivApp_injective

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.trivApp_injective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
theorem trivApp_injective (V : W.toScheme.Opens) : Function.Injective (trivApp M W E V)
theorem

coord_injective

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.coord_injective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
theorem coord_injective (V : W.toScheme.Opens) : Function.Injective (coord M W E V)
theorem

map_trivApp

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.map_trivApp
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
theorem map_trivApp {V V' : W.toScheme.Opens} (i : V' ≤ V) (m : Γ(M, W.ι ''ᵁ V)) :
    (W.toScheme.presheaf.map (homOfLE i).op).hom (trivApp M W E V m)
      = trivApp M W E V' ((M.presheaf.map (homOfLE (W.ι.image_mono i)).op).hom m)
theorem

map_coord

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.map_coord
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
theorem map_coord {V V' : W.toScheme.Opens} (i : V' ≤ V) (m : Γ(M, W.ι ''ᵁ V)) :
    (X.presheaf.map (homOfLE (W.ι.image_mono i)).op).hom (coord M W E V m)
      = coord M W E V' ((M.presheaf.map (homOfLE (W.ι.image_mono i)).op).hom m)
theorem

coord_smul

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.coord_smul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Coord
variable (W : X.Opens)
  (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
Lean source · statement
theorem coord_smul (V : W.toScheme.Opens) (a : Γ(X, W.ι ''ᵁ V)) (m : Γ(M, W.ι ''ᵁ V)) :
    coord M W E V (a • m) = a * coord M W E V m
abbrev

inW

L113 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.inW
Documentation

The intersection with the chosen open expressed as the image of its inverse image.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section InW
variable (W : X.Opens)
Lean source · statement
abbrev inW (U : X.Opens) : X.Opens
theorem

inW_le

L115 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.inW_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section InW
variable (W : X.Opens)
Lean source · statement
theorem inW_le (U : X.Opens) : inW W U ≤ U
theorem

inW_eq

L117 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.inW_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section InW
variable (W : X.Opens)
Lean source · statement
theorem inW_eq (U : X.Opens) : inW W U = W ⊓ U
theorem

mem_inW

L120 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.mem_inW
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section InW
variable (W : X.Opens)
Lean source · statement
theorem mem_inW {U : X.Opens} {x : X} (hxW : x ∈ W) (hxU : x ∈ U) : x ∈ inW W U
theorem

preimage_mono_of_le

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.preimage_mono_of_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section InW
variable (W : X.Opens)
Lean source · statement
theorem preimage_mono_of_le {U U' : X.Opens} (h : U' ≤ U) : W.ι ⁻¹ᵁ U' ≤ W.ι ⁻¹ᵁ U
theorem

inW_mono

L126 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.inW_mono
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section InW
variable (W : X.Opens)
Lean source · statement
theorem inW_mono {U U' : X.Opens} (h : U' ≤ U) : inW W U' ≤ inW W U
theorem

genericPoint_mem

L135 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.genericPoint_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Generic
variable [IsIntegral X]
Lean source · statement
theorem genericPoint_mem (U : X.Opens) [h : Nonempty U] : genericPoint X ∈ U
theorem

genericPoint_mem_of_mem

L138 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.genericPoint_mem_of_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Generic
variable [IsIntegral X]
Lean source · statement
theorem genericPoint_mem_of_mem {U : X.Opens} {x : X} (hx : x ∈ U) : genericPoint X ∈ U
theorem

eq_zero_of_res_eq_zero

L142 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.eq_zero_of_res_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Generic
variable [IsIntegral X]
Lean source · statement
theorem eq_zero_of_res_eq_zero {U V : X.Opens} (i : V ≤ U) (hV : genericPoint X ∈ V) (f : Γ(X, U))
    (h : (X.presheaf.map (homOfLE i).op).hom f = 0) : f = 0
abbrev

resIn

L157 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.resIn
Documentation

Restriction of module sections to the intersection with the chosen trivializing open.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Pres
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
  (E₀ : (M.restrict W₀.ι) ≅ (SheafOfModules.unit W₀.toScheme.ringCatSheaf : W₀.toScheme.Modules))
Lean source · statement
abbrev resIn (U : X.Opens) : Γ(M, U) →+ Γ(M, inW W₀ U)
def

pres

L162 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.pres
Documentation

The function field presentation obtained by taking the germ of the local coordinate at the generic point.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Pres
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
  (E₀ : (M.restrict W₀.ι) ≅ (SheafOfModules.unit W₀.toScheme.ringCatSheaf : W₀.toScheme.Modules))
Lean source · statement
def pres (U : X.Opens) : Γ(M, U) →+ (X.functionField : Type u)
theorem

pres_apply

L169 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.pres_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Pres
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
  (E₀ : (M.restrict W₀.ι) ≅ (SheafOfModules.unit W₀.toScheme.ringCatSheaf : W₀.toScheme.Modules))
Lean source · statement
theorem pres_apply {U : X.Opens} (hU : genericPoint X ∈ U) (m : Γ(M, U)) :
    pres M W₀ hξ E₀ U m = (X.presheaf.germ (inW W₀ U) (genericPoint X) (mem_inW W₀ hξ hU)).hom
      (coord M W₀ E₀ (W₀.ι ⁻¹ᵁ U) (resIn M W₀ U m))
theorem

pres_natural

L176 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.pres_natural
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Pres
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
  (E₀ : (M.restrict W₀.ι) ≅ (SheafOfModules.unit W₀.toScheme.ringCatSheaf : W₀.toScheme.Modules))
Lean source · statement
theorem pres_natural (U V : X.Opens) (h : V ≤ U) (hV : Nonempty V) (m : Γ(M, U)) :
    pres M W₀ hξ E₀ V (M.presheaf.map (homOfLE h).op m) = pres M W₀ hξ E₀ U m
theorem

pres_smul

L193 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.pres_smul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Pres
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
  (E₀ : (M.restrict W₀.ι) ≅ (SheafOfModules.unit W₀.toScheme.ringCatSheaf : W₀.toScheme.Modules))
Lean source · statement
theorem pres_smul (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)) :
    pres M W₀ hξ E₀ U (a • m) = algebraMap Γ(X, U) X.functionField a * pres M W₀ hξ E₀ U m
def

restrictIsoOfPullbackIso

L213 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.restrictIsoOfPullbackIso
Documentation

The restriction trivialization obtained from a pullback trivialization through the canonical comparison isomorphism.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Inj
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
Lean source · statement
def restrictIsoOfPullbackIso (W : X.Opens)
    (e : (Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf) :
    (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules)
theorem

resIn_eq_zero_of_resIn_eq_zero

L219 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.resIn_eq_zero_of_resIn_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Inj
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
include hξ in
Lean source · statement
theorem resIn_eq_zero_of_resIn_eq_zero (W : X.Opens)
    (E : (M.restrict W.ι) ≅ (SheafOfModules.unit W.toScheme.ringCatSheaf : W.toScheme.Modules))
    (U : X.Opens) (m : Γ(M, U)) {x : X} (hxW : x ∈ W) (hxU : x ∈ U)
    (h0 : resIn M W₀ U m = 0) : resIn M W U m = 0
theorem

eq_zero_of_resIn_eq_zero

L243 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.eq_zero_of_resIn_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
section Inj
variable [IsIntegral X] (W₀ : X.Opens) (hξ : genericPoint X ∈ W₀)
include hξ in
Lean source · statement
theorem eq_zero_of_resIn_eq_zero (hM : Scheme.Modules.IsInvertible M) (U : X.Opens) (m : Γ(M, U))
    (h0 : resIn M W₀ U m = 0) : m = 0
theorem

main

L258 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_functionField_presentation.P2mKPresSol.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mKPresSol
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
theorem main [IsIntegral X] (hM : Scheme.Modules.IsInvertible M) :
    ∃ φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u),
      (∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
          ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m) ∧
      (∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
          φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ U : X.Opens, Nonempty U → Function.Injective (φ U))
theorem

exists_functionField_presentation

L285 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_functionField_presentation
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_functionField_presentation
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_functionField_presentation
    {X : Scheme.{u}} [IsIntegral X] (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
    ∃ φ : ∀ U : X.Opens, Γ(M, U) →+ (X.functionField : Type u),
      (∀ (U V : X.Opens) (h : V ≤ U), Nonempty V →
          ∀ m : Γ(M, U), φ V (M.presheaf.map (homOfLE h).op m) = φ U m) ∧
      (∀ (U : X.Opens) [Nonempty U] (a : Γ(X, U)) (m : Γ(M, U)),
          φ U (a • m) = algebraMap Γ(X, U) X.functionField a * φ U m) ∧
      (∀ U : X.Opens, Nonempty U → Function.Injective (φ U))

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