NYLL
Module

ProjSpace_isQuasicoherent_twist.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_isQuasicoherent_twist
26 declarations indexed from sourceView source ↗

Module documentation

Proj Space is Quasicoherent twist

Imports4
Imported by4

Declarations

theorem

restrictFun_injective_of_ge

L41 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.restrictFun_injective_of_ge
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
Lean source · statement
theorem restrictFun_injective_of_ge {W W' : X.Opens} (h : W ≤ W') (h' : W' ≤ W) :
    Function.Injective (restrictFun h)
theorem

basicOpen_restrictFun

L47 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.basicOpen_restrictFun
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
Lean source · statement
theorem basicOpen_restrictFun {V W : X.Opens} (h : V ≤ W) (f : Γ(X, W)) :
    X.basicOpen (restrictFun h f) = V ⊓ X.basicOpen f
theorem

exists_pow_mul_eq_zero

L51 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.exists_pow_mul_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
Lean source · statement
theorem exists_pow_mul_eq_zero {V : X.Opens} (hV : IsAffineOpen V) (s x : Γ(X, V))
    (hx : restrictFun (X.basicOpen_le s) x = 0) : ∃ n : ℕ, s ^ n * x = 0
theorem

exists_restrictFun_eq_mul_pow

L58 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.exists_restrictFun_eq_mul_pow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
Lean source · statement
theorem exists_restrictFun_eq_mul_pow {V : X.Opens} (hV : IsAffineOpen V) (s : Γ(X, V)) (z : Γ(X,
  X.basicOpen s)) :
    ∃ (n : ℕ) (a : Γ(X, V)),
      restrictFun (X.basicOpen_le s) a = z * restrictFun (X.basicOpen_le s) (s ^ n)
theorem

restrictFun_mul_pow_eq

L66 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.restrictFun_mul_pow_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
Lean source · statement
theorem restrictFun_mul_pow_eq {V : X.Opens} (s : Γ(X, V)) (z : Γ(X, X.basicOpen s)) {n : ℕ} {a :
  Γ(X, V)}
    (h : restrictFun (X.basicOpen_le s) a = z * restrictFun (X.basicOpen_le s) (s ^ n)) {n' : ℕ}
      (hn : n ≤ n') :
    restrictFun (X.basicOpen_le s) (s ^ (n' - n) * a) = z * restrictFun (X.basicOpen_le s) (s ^ n')
abbrev

V

L81 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.V
Documentation

The intersection of the affine open with the chosen pullback chart.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
abbrev V (j : Fin (N + 1)) : X.Opens
abbrev

V₂

L84 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.V₂
Documentation

The intersection of the affine open with two pullback charts.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
abbrev V₂ (j l : Fin (N + 1)) : X.Opens
theorem

isAffineOpen_V

L86 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.isAffineOpen_V
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem isAffineOpen_V [IsSeparated π] [IsAffineHom φ] (j : Fin (N + 1)) : IsAffineOpen (V φ U j)
theorem

isAffineOpen_V₂

L89 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.isAffineOpen_V₂
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem isAffineOpen_V₂ [IsSeparated π] [IsAffineHom φ] (j l : Fin (N + 1)) : IsAffineOpen (V₂ φ U
  j l)
abbrev

fV

L95 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.fV
Documentation

The restriction of the function to the intersection with one pullback chart.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
abbrev fV (j : Fin (N + 1)) : Γ(X, V φ U j)
abbrev

fV₂

L98 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.fV₂
Documentation

The restriction of the function to the intersection with two pullback charts.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
abbrev fV₂ (j l : Fin (N + 1)) : Γ(X, V₂ φ U j l)
theorem

basicOpen_fV

L100 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.basicOpen_fV
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem basicOpen_fV (j : Fin (N + 1)) : X.basicOpen (fV φ U f j) = V φ U j ⊓ X.basicOpen f
theorem

basicOpen_fV₂

L103 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.basicOpen_fV₂
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem basicOpen_fV₂ (j l : Fin (N + 1)) : X.basicOpen (fV₂ φ U f j l) = V₂ φ U j l ⊓ X.basicOpen
  f
theorem

inf_le_basicOpen_fV

L107 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.inf_le_basicOpen_fV
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem inf_le_basicOpen_fV (j : Fin (N + 1)) : X.basicOpen f ⊓ pullbackChart φ j ≤ X.basicOpen (fV
  φ U f j)
theorem

basicOpen_fV_le_inf

L112 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.basicOpen_fV_le_inf
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem basicOpen_fV_le_inf (j : Fin (N + 1)) : X.basicOpen (fV φ U f j) ≤ X.basicOpen f ⊓
  pullbackChart φ j
theorem

basicOpen_fV₂_le_left

L116 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.basicOpen_fV₂_le_left
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem basicOpen_fV₂_le_left (j l : Fin (N + 1)) : X.basicOpen (fV₂ φ U f j l) ≤ X.basicOpen (fV φ
  U f j)
theorem

basicOpen_fV₂_le_right

L121 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.basicOpen_fV₂_le_right
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem basicOpen_fV₂_le_right (j l : Fin (N + 1)) : X.basicOpen (fV₂ φ U f j l) ≤ X.basicOpen (fV
  φ U f l)
theorem

basicOpen_fV₂_le_inf

L127 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.basicOpen_fV₂_le_inf
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Pieces
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem basicOpen_fV₂_le_inf (j l : Fin (N + 1)) :
    X.basicOpen (fV₂ φ U f j l) ≤ (X.basicOpen f ⊓ pullbackChart φ j) ⊓ pullbackChart φ l
theorem

torsion

L138 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.torsion
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Torsion
variable (U : X.affineOpens) (f : Γ(X, U.1))
Lean source · statement
theorem torsion [IsSeparated π] [IsAffineHom φ] (y : (twist π φ m).obj U.1) (hy : (twist π φ m).res
  (X.basicOpen_le f) y = 0) :
    ∃ n : ℕ, (f ^ n : Γ(X, U.1)) • y = 0
def

z

L169 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.z
Documentation

The chosen chart component of a twisted section, restricted to the corresponding basic open.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Extension
variable (U : X.affineOpens) (f : Γ(X, U.1)) (x : (twist π φ m).obj (X.basicOpen f))
Lean source · statement
def z (j : Fin (N + 1)) : Γ(X, X.basicOpen (fV φ U f j))
theorem

exists_numerators

L172 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.exists_numerators
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Extension
variable (U : X.affineOpens) (f : Γ(X, U.1)) (x : (twist π φ m).obj (X.basicOpen f))
Lean source · statement
theorem exists_numerators [IsSeparated π] [IsAffineHom φ] :
    ∃ (n : ℕ) (a : ∀ j : Fin (N + 1), Γ(X, V φ U j)),
      ∀ j, restrictFun (X.basicOpen_le (fV φ U f j)) (a j)
        = z π φ m U f x j * restrictFun (X.basicOpen_le (fV φ U f j)) (fV φ U f j ^ n)
def

defect

L184 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.defect
Documentation

The difference between two candidate sections after applying the twist transition function.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Extension
variable (U : X.affineOpens) (f : Γ(X, U.1)) (x : (twist π φ m).obj (X.basicOpen f))
Lean source · statement
def defect (a : ∀ j : Fin (N + 1), Γ(X, V φ U j)) (j l : Fin (N + 1)) : Γ(X, V₂ φ U j l)
theorem

restrictFun_defect_eq_zero

L191 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.restrictFun_defect_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Extension
variable (U : X.affineOpens) (f : Γ(X, U.1)) (x : (twist π φ m).obj (X.basicOpen f))
Lean source · statement
theorem restrictFun_defect_eq_zero {n : ℕ} {a : ∀ j : Fin (N + 1), Γ(X, V φ U j)}
    (ha : ∀ j, restrictFun (X.basicOpen_le (fV φ U f j)) (a j)
      = z π φ m U f x j * restrictFun (X.basicOpen_le (fV φ U f j)) (fV φ U f j ^ n)) (j l : Fin (N
        + 1)) :
    restrictFun (X.basicOpen_le (fV₂ φ U f j l)) (defect φ m U a j l) = 0
theorem

extension

L209 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.extension
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
section Extension
variable (U : X.affineOpens) (f : Γ(X, U.1)) (x : (twist π φ m).obj (X.basicOpen f))
Lean source · statement
theorem extension [IsSeparated π] [IsAffineHom φ] :
    ∃ (k : ℕ) (y : (twist π φ m).obj U.1),
      (twist π φ m).res (X.basicOpen_le f) y = restrictFun (X.basicOpen_le f) (f ^ k) • x
theorem

main

L242 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist.P2mTwistQC.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace P2mTwistQC
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) (m : ℕ)
Lean source · statement
theorem main [IsSeparated π] [IsAffineHom φ] : (twist π φ m).IsQuasicoherent
theorem

isQuasicoherent_twist

L252 ↗
AlgebraicGeometry.ProjSpace.isQuasicoherent_twist
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isQuasicoherent_twist
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.isQuasicoherent_twist
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
    (π : X ⟶ Spec (.of A)) [IsSeparated π]
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A)) [IsAffineHom φ] (m : ℕ) :
    (ProjSpace.twist π φ m).IsQuasicoherent

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