NYLL
Module

Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
37 declarations indexed from sourceView source ↗

Module documentation

Descent of finiteness by sections from principal open base changes

Imports10
Imported by2

Declarations

theorem

app_naturality

L60 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.app_naturality
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Generalities
variable {X : Scheme.{u}}
Lean source · statement
theorem app_naturality {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (i : U ⟶ V) (m : Γ(M, V)) :
    N.presheaf.map i.op (φ.app V m) = φ.app U (M.presheaf.map i.op m)
theorem

subsingleton_sections_bot

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.subsingleton_sections_bot
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Generalities
variable {X : Scheme.{u}}
Lean source · statement
theorem subsingleton_sections_bot (M : X.Modules) : Subsingleton (Γ(M, (⊥ : X.Opens)) : Type u)
theorem

subsingleton_functions_bot

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.subsingleton_functions_bot
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Generalities
variable {X : Scheme.{u}}
Lean source · statement
theorem subsingleton_functions_bot : Subsingleton (Γ(X, (⊥ : X.Opens)) : Type u)
theorem

bijective_smul_of_le_bot

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.bijective_smul_of_le_bot
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Generalities
variable {X : Scheme.{u}}
Lean source · full declaration
theorem bijective_smul_of_le_bot (M : X.Modules) {W : X.Opens} (hW : W ≤ ⊥) (s : Γ(M, W)) :
    Function.Bijective fun g : Γ(X, W) => g • s := by
  obtain rfl : W = ⊥ := le_bot_iff.mp hW
  have := subsingleton_sections_bot M
  have : Subsingleton (Γ(X, (⊥ : X.Opens)) : Type u) := subsingleton_functions_bot
  exact ⟨fun a b _ => Subsingleton.elim a b, fun y => ⟨0, Subsingleton.elim _ _⟩⟩
abbrev

η

L93 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.η
Documentation

The unit map to the pushforward of the pulled-back module.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section OpenImm
variable {X X' : Scheme.{u}} (p : X' ⟶ X) [IsOpenImmersion p] (M : X.Modules)
Lean source · statement
abbrev η : M ⟶ (Scheme.Modules.pushforward p).obj ((Scheme.Modules.pullback p).obj M)
abbrev

pull

L97 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.pull
Documentation

Pull a section back along the given open immersion.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section OpenImm
variable {X X' : Scheme.{u}} (p : X' ⟶ X) [IsOpenImmersion p] (M : X.Modules)
Lean source · statement
abbrev pull (V : X.Opens) (m : Γ(M, V)) : Γ((Scheme.Modules.pullback p).obj M, p ⁻¹ᵁ V)
theorem

pull_smul

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.pull_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section OpenImm
variable {X X' : Scheme.{u}} (p : X' ⟶ X) [IsOpenImmersion p] (M : X.Modules)
omit [IsOpenImmersion p] in
Lean source · statement
theorem pull_smul (V : X.Opens) (c : Γ(X, V)) (m : Γ(M, V)) :
    pull p M V (c • m) = p.app V c • pull p M V m
theorem

map_pull

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.map_pull
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section OpenImm
variable {X X' : Scheme.{u}} (p : X' ⟶ X) [IsOpenImmersion p] (M : X.Modules)
omit [IsOpenImmersion p] in
Lean source · statement
theorem map_pull {U V : X.Opens} (h : U ≤ V) (m : Γ(M, V)) :
    ((Scheme.Modules.pullback p).obj M).presheaf.map (homOfLE ((Opens.map p.base).monotone
        h)).op (pull p M V m)
      = pull p M U (M.presheaf.map (homOfLE h).op m)
theorem

pull_bijective

L112 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.pull_bijective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section OpenImm
variable {X X' : Scheme.{u}} (p : X' ⟶ X) [IsOpenImmersion p] (M : X.Modules)
Lean source · statement
theorem pull_bijective (V : X.Opens) (hV : V ≤ p.opensRange) : Function.Bijective (pull p M V)
theorem

app_bijective

L115 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.app_bijective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section OpenImm
variable {X X' : Scheme.{u}} (p : X' ⟶ X) [IsOpenImmersion p] (M : X.Modules)
Lean source · statement
theorem app_bijective (V : X.Opens) (hV : V ≤ p.opensRange) : Function.Bijective (p.app V)
theorem

bijective_smul_of_bijective_smul_pull

L119 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.bijective_smul_of_bijective_smul_pull
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section OpenImm
variable {X X' : Scheme.{u}} (p : X' ⟶ X) [IsOpenImmersion p] (M : X.Modules)
Lean source · full declaration
theorem bijective_smul_of_bijective_smul_pull (σ : Γ(M, ⊤)) {V : X.Opens} (hV : V ≤ p.opensRange)
    (h : ∀ W' : X'.Opens, W' ≤ p ⁻¹ᵁ V →
      Function.Bijective fun g' : Γ(X', W') =>
        g' • ((Scheme.Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : W' ≤ p ⁻¹ᵁ
            ⊤)).op (pull p M ⊤ σ))
    (W : X.Opens) (hW : W ≤ V) :
    Function.Bijective fun g : Γ(X, W) => g • M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op σ := by
  have hWr : W ≤ p.opensRange := hW.trans hV
  have hsq : (pull p M W) ∘ (fun g : Γ(X, W) => g • M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op σ)
      = (fun g' : Γ(X', p ⁻¹ᵁ W) =>
          g' • ((Scheme.Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : p ⁻¹ᵁ W ≤ p
              ⁻¹ᵁ ⊤)).op
            (pull p M ⊤ σ)) ∘ (p.app W) := by
    funext g
    simp only [Function.comp_apply]
    rw [pull_smul]
    congr 1
    exact (map_pull p M (le_top : W ≤ ⊤) σ).symm
  have h1 := (h (p ⁻¹ᵁ W) ((Opens.map p.base).monotone hW)).comp (app_bijective p W hWr)
  rw [← hsq] at h1
  exact (Function.Bijective.of_comp_iff' (pull_bijective p M W hWr) _).mp h1
abbrev

Sg

L148 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.Sg
Documentation

The spectrum map of localization away from the chosen ring element.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
abbrev Sg : Spec (.of (Localization.Away g)) ⟶ Spec (.of R)
abbrev

pg

L152 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.pg
Documentation

The projection from the principal-open base change to the original scheme.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
abbrev pg
abbrev

fg

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.fg
Documentation

The structure map of the principal-open base change.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
abbrev fg
abbrev

gX

L157 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.gX
Documentation

The chosen base-ring element viewed as a global regular function.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
abbrev gX : Γ(X, ⊤)
abbrev

Ug

L160 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.Ug
Documentation

The basic open where the induced global function is invertible.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
abbrev Ug : X.Opens
theorem

coe_opensRange_Sg

L162 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.coe_opensRange_Sg
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
omit M in
Lean source · statement
theorem coe_opensRange_Sg : ((Sg g).opensRange : Set (Spec (.of R))) = (PrimeSpectrum.basicOpen
    g : Set (PrimeSpectrum R))
theorem

preimage_basicOpen_eq_Ug

L171 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.preimage_basicOpen_eq_Ug
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem preimage_basicOpen_eq_Ug : f ⁻¹ᵁ PrimeSpectrum.basicOpen g = Ug f g
theorem

opensRange_pg

L177 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.opensRange_pg
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem opensRange_pg : (pg f g).opensRange = Ug f g
theorem

preimage_Ug

L184 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.preimage_Ug
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem preimage_Ug : (pg f g) ⁻¹ᵁ Ug f g = ⊤
theorem

mem_range_pg_of

L187 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.mem_range_pg_of
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem mem_range_pg_of {x : X} (hx : x ∈ Ug f g) : ∃ y, (pg f g).base y = x
theorem

appTop_pg_gX

L191 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.appTop_pg_gX
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem appTop_pg_gX :
    (pg f g).appTop (gX f g)
      = (fg f g).appTop ((Scheme.ΓSpecIso (.of (Localization.Away g))).inv (algebraMap R
          (Localization.Away g) g))
theorem

isUnit_appTop_pg_gX

L205 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.isUnit_appTop_pg_gX
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem isUnit_appTop_pg_gX : IsUnit ((pg f g).appTop (gX f g))
theorem

isUnit_res_appTop_pg_gX

L209 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.isUnit_res_appTop_pg_gX
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem isUnit_res_appTop_pg_gX {W' : (Limits.pullback f (Sg g)).Opens} (hW : W' ≤ ⊤) :
    IsUnit ((Limits.pullback f (Sg g)).presheaf.map (homOfLE hW).op ((pg f g).appTop (gX f g)))
theorem

res_app_res

L213 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.res_app_res
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem res_app_res (n : ℕ) {W' : (Limits.pullback f (Sg g)).Opens} (hle : W' ≤ (pg f g) ⁻¹ᵁ Ug
    f g) :
    (Limits.pullback f (Sg g)).presheaf.map (homOfLE hle).op
        ((pg f g).app (Ug f g) (X.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op (gX f g ^ n)))
      = (Limits.pullback f (Sg g)).presheaf.map (homOfLE (le_top : W' ≤ ⊤)).op ((pg f g).appTop
          (gX f g)) ^ n
theorem

exists_clear

L229 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.exists_clear
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Away
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem exists_clear (hinv : Scheme.Modules.IsInvertible M) [CompactSpace X] [QuasiSeparatedSpace X]
    (t : Γ(M, Ug f g)) :
    ∃ (n : ℕ) (m : Γ(M, ⊤)), M.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op m
      = X.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op (gX f g ^ n) • t
theorem

bijective_smul_smul_of_isUnit

L247 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.bijective_smul_smul_of_isUnit
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Transfer
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · full declaration
theorem bijective_smul_smul_of_isUnit {Y : Scheme.{u}} {N : Y.Modules} {W : Y.Opens} (s : Γ(N,
    W)) (u : Γ(Y, W))
    (hu : IsUnit u) (hs : Function.Bijective fun c : Γ(Y, W) => c • s) :
    Function.Bijective fun c : Γ(Y, W) => c • (u • s) := by
  obtain ⟨uinv, hu1, hu2⟩ : ∃ uinv, u * uinv = 1 ∧ uinv * u = 1 :=
    ⟨((hu.unit⁻¹ : Γ(Y, W)ˣ) : Γ(Y, W)), hu.mul_val_inv, hu.val_inv_mul⟩
  have hb : Function.Bijective (fun c : Γ(Y, W) => c * u) := by
    refine ⟨fun a b h => ?_, fun y => ⟨y * uinv, ?_⟩⟩
    · have := congr_arg (· * uinv) h
      simpa only [mul_assoc, hu1, mul_one] using this
    · simp only [mul_assoc, hu2, mul_one]
  have key : (fun c : Γ(Y, W) => c • (u • s)) = (fun c : Γ(Y, W) => c • s) ∘ fun c => c * u := by
    funext c; simp only [Function.comp_apply, mul_smul]
  rw [key]
  exact hs.comp hb
abbrev

chart'

L267 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.chart'
Documentation

The inverse image of a standard projective coordinate chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Transfer
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable {N' : ℕ}
  (𝔓 : ((Scheme.Modules.pullback (pg f g)).obj M).ProjPresentation (fg f g) N')
Lean source · statement
abbrev chart' (i : Fin (N' + 1)) : (Limits.pullback f (Sg g)).Opens
abbrev

chartX

L272 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.chartX
Documentation

The image of the pulled-back projective coordinate chart in the original scheme.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Transfer
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable {N' : ℕ}
  (𝔓 : ((Scheme.Modules.pullback (pg f g)).obj M).ProjPresentation (fg f g) N')
Lean source · statement
abbrev chartX (i : Fin (N' + 1)) : X.Opens
theorem

exists_t

L274 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.exists_t
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Transfer
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable {N' : ℕ}
  (𝔓 : ((Scheme.Modules.pullback (pg f g)).obj M).ProjPresentation (fg f g) N')
Lean source · statement
theorem exists_t (i : Fin (N' + 1)) :
    ∃ t : Γ(M, Ug f g), pull (pg f g) M (Ug f g) t
      = ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map (homOfLE (le_top : (pg f g) ⁻¹ᵁ
          Ug f g ≤ ⊤)).op (𝔓.σ i)
theorem

exists_descend

L283 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.exists_descend
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Transfer
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable {N' : ℕ}
  (𝔓 : ((Scheme.Modules.pullback (pg f g)).obj M).ProjPresentation (fg f g) N')
variable (hinv : Scheme.Modules.IsInvertible M) [CompactSpace X] [QuasiSeparatedSpace X]
include hinv
Lean source · full declaration
theorem exists_descend (i : Fin (N' + 1)) :
    ∃ (n : ℕ) (m : Γ(M, ⊤)),
      ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map (homOfLE (le_top : (pg f g) ⁻¹ᵁ Ug
          f g ≤ ⊤)).op
          (pull (pg f g) M ⊤ m)
        = ((pg f g).app (Ug f g) (X.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op (gX f g
            ^ n))) •
          ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map (homOfLE (le_top : (pg f g)
              ⁻¹ᵁ Ug f g ≤ ⊤)).op (𝔓.σ i)
      ∧ ∀ W : X.Opens, W ≤ chartX f M g 𝔓 i →
          Function.Bijective fun c : Γ(X, W) => c • M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op
              m := by
  obtain ⟨t, ht⟩ := exists_t f M g 𝔓 i
  obtain ⟨n, m, hm⟩ := exists_clear f M g hinv t
  have key : ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map
        (homOfLE (le_top : (pg f g) ⁻¹ᵁ Ug f g ≤ ⊤)).op (pull (pg f g) M ⊤ m)
      = ((pg f g).app (Ug f g) (X.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op (gX f g ^
          n))) •
          ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map
            (homOfLE (le_top : (pg f g) ⁻¹ᵁ Ug f g ≤ ⊤)).op (𝔓.σ i) := by
    have h1 := map_pull (pg f g) M (X.basicOpen_le (gX f g)) m
    rw [hm, pull_smul, ht] at h1
    exact h1
  refine ⟨n, m, key, ?_⟩
  refine bijective_smul_of_bijective_smul_pull (pg f g) M m (Scheme.Hom.image_le_opensRange _ _) ?_
  intro W' hW'
  rw [Scheme.Hom.preimage_image_eq] at hW'
  have hle : W' ≤ (pg f g) ⁻¹ᵁ Ug f g := by rw [preimage_Ug]; exact le_top
  have hres : ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map (homOfLE (le_top : W' ≤
      (pg f g) ⁻¹ᵁ ⊤)).op
        (pull (pg f g) M ⊤ m)
      = ((Limits.pullback f (Sg g)).presheaf.map (homOfLE hle).op
          ((pg f g).app (Ug f g) (X.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op (gX f g
              ^ n)))) •
        ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map (homOfLE (le_top : W' ≤ ⊤)).op
            (𝔓.σ i) := by
    let N : (Limits.pullback f (Sg g)).Modules := (Scheme.Modules.pullback (pg f g)).obj M
    have hcomp {U V W : (Limits.pullback f (Sg g)).Opens}
        (hUV : U ≤ V) (hVW : V ≤ W) (x : Γ(N, W)) :
        N.presheaf.map (homOfLE hUV).op (N.presheaf.map (homOfLE hVW).op x) =
          N.presheaf.map (homOfLE (hUV.trans hVW)).op x :=
      (ConcreteCategory.congr_hom
        (N.presheaf.map_comp (homOfLE hVW).op (homOfLE hUV).op) x).symm
    have hrestrict := congrArg (N.presheaf.map (homOfLE hle).op) key
    rw [Scheme.Modules.map_smul] at hrestrict
    have hleft := hcomp (W := (pg f g) ⁻¹ᵁ ⊤) hle
      (le_top : (pg f g) ⁻¹ᵁ Ug f g ≤ (pg f g) ⁻¹ᵁ ⊤) (pull (pg f g) M ⊤ m)
    have hright := hcomp (W := ⊤) hle
      (le_top : (pg f g) ⁻¹ᵁ Ug f g ≤ ⊤) (𝔓.σ i)
    exact hleft.symm.trans (hrestrict.trans (congrArg
      (fun x : Γ(N, W') =>
        ((Limits.pullback f (Sg g)).presheaf.map (homOfLE hle).op
          ((pg f g).app (Ug f g)
            (X.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op (gX f g ^ n)))) • x)
      hright))
  have hunit : IsUnit ((Limits.pullback f (Sg g)).presheaf.map (homOfLE hle).op
      ((pg f g).app (Ug f g) (X.presheaf.map (homOfLE (X.basicOpen_le (gX f g))).op (gX f g ^
          n)))) := by
    rw [res_app_res]
    exact (isUnit_res_appTop_pg_gX f g _).pow n
  change Function.Bijective fun g' : Γ(Limits.pullback f (Sg g), W') =>
    g' • ((Scheme.Modules.pullback (pg f g)).obj M).presheaf.map (homOfLE (le_top : W' ≤ (pg f
        g) ⁻¹ᵁ ⊤)).op
      (pull (pg f g) M ⊤ m)
  rw [hres]
  exact bijective_smul_smul_of_isUnit _ _ hunit (𝔓.frame i W' hW')
theorem

exists_mem_chart'

L356 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.exists_mem_chart'
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem exists_mem_chart' {N' : ℕ} (𝔓 : ((Scheme.Modules.pullback (pg f g)).obj
    M).ProjPresentation (fg f g) N')
    (y : ↑(Limits.pullback f (Sg g))) : ∃ i, y ∈ chart' f M g 𝔓 i
theorem

map_injective_of_eq

L371 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.map_injective_of_eq
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem map_injective_of_eq {Y : Scheme.{u}} (N : Y.Modules) {W W' : Y.Opens} (h : W = W') (hle
    : W ≤ W') :
    Function.Injective (N.presheaf.map (homOfLE hle).op)
theorem

exists_coeff

L380 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.exists_coeff
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
Lean source · statement
theorem exists_coeff (n : ℕ) :
    ∃ c₀ : Localization.Away g,
      (fg f g).appTop ((Scheme.ΓSpecIso (.of (Localization.Away g))).inv c₀) * (pg f g).appTop
          (gX f g) ^ n = 1
theorem

exists_mem_Ug

L398 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.exists_mem_Ug
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
variable [IsProper f] (hinv : Scheme.Modules.IsInvertible M) (s : Finset R) (hs : Ideal.span (s
    : Set R) = ⊤)
  (h : ∀ g ∈ s, Scheme.Modules.FiniteBySections
      ((Scheme.Modules.pullback (Limits.pullback.fst f
          (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away g)))))).obj M)
      (Limits.pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away g))))))
include hinv hs h
omit hinv h [IsProper f] in
Lean source · statement
theorem exists_mem_Ug (x : X) : ∃ g ∈ s, x ∈ Ug f g
theorem

finiteBySections

L412 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry.Scheme.Modules.FbsLocal.finiteBySections
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace FbsLocal
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) (M : X.Modules) (g : R)
variable [IsProper f] (hinv : Scheme.Modules.IsInvertible M) (s : Finset R) (hs : Ideal.span (s
    : Set R) = ⊤)
  (h : ∀ g ∈ s, Scheme.Modules.FiniteBySections
      ((Scheme.Modules.pullback (Limits.pullback.fst f
          (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away g)))))).obj M)
      (Limits.pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away g))))))
include hinv hs h
Lean source · statement
theorem finiteBySections : Scheme.Modules.FiniteBySections M f
theorem

of_forall_mem_finset_away

L527 ↗
AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_forall_mem_finset_away
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_FiniteBySections_of_forall_mem_finset_away
universe u
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open CategoryTheory CategoryTheory.Limits _root_.AlgebraicGeometry
  Scheme_Modules_FiniteBySections_of_forall_mem_finset_away.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.FiniteBySections.of_forall_mem_finset_away
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsProper f]
    (M : X.Modules) (hinv : Scheme.Modules.IsInvertible M)
    (s : Finset R) (hs : Ideal.span (s : Set R) = ⊤)
    (h : ∀ g ∈ s, Scheme.Modules.FiniteBySections
        ((Scheme.Modules.pullback (Limits.pullback.fst f
            (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away g)))))).obj M)
        (Limits.pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away
            g)))))) :
    Scheme.Modules.FiniteBySections M f

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