NYLL
Module

Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
39 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Proj Presentation exists linear Map sections tensor Pow twist Obj

Imports6
Imported by3

Declarations

abbrev

rM

L42 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rM
Documentation

Restricts a module section along an inclusion of open subsets.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
abbrev rM (M : X.Modules) {W W' : X.Opens} (h : W ≤ W') : Γ(M, W') → Γ(M, W)
abbrev

rO

L46 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rO
Documentation

Restricts a structure-sheaf section along an inclusion of open subsets.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
abbrev rO {W W' : X.Opens} (h : W ≤ W') : Γ(X, W') → Γ(X, W)
theorem

rM_rM

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rM_rM
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rM_rM (M : X.Modules) {W₁ W₂ W₃ : X.Opens} (h₁ : W₁ ≤ W₂) (h₂ : W₂ ≤ W₃) (x : Γ(M, W₃)) :
    rM M h₁ (rM M h₂ x) = rM M (h₁.trans h₂) x
theorem

rM_irrel

L55 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rM_irrel
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rM_irrel (M : X.Modules) {W₁ W₂ : X.Opens} (h h' : W₁ ≤ W₂) (x : Γ(M, W₂)) : rM M h x = rM
  M h' x
theorem

rM_refl

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rM_refl
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rM_refl (M : X.Modules) {W : X.Opens} (h : W ≤ W) (x : Γ(M, W)) : rM M h x = x
theorem

rM_smul

L63 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rM_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_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rM_smul (M : X.Modules) {W W' : X.Opens} (h : W ≤ W') (a : Γ(X, W')) (x : Γ(M, W')) :
    rM M h (a • x) = rO h a • rM M h x
theorem

rM_add

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rM_add
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rM_add (M : X.Modules) {W W' : X.Opens} (h : W ≤ W') (x y : Γ(M, W')) :
    rM M h (x + y) = rM M h x + rM M h y
theorem

rM_bijective_of_ge

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rM_bijective_of_ge
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rM_bijective_of_ge (M : X.Modules) {W W' : X.Opens} (h : W ≤ W') (h' : W' ≤ W) :
    Function.Bijective (rM M h)
theorem

rO_rO

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rO_rO
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rO_rO {W₁ W₂ W₃ : X.Opens} (h₁ : W₁ ≤ W₂) (h₂ : W₂ ≤ W₃) (a : Γ(X, W₃)) :
    rO h₁ (rO h₂ a) = rO (h₁.trans h₂) a
theorem

rO_irrel

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rO_irrel
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rO_irrel {W₁ W₂ : X.Opens} (h h' : W₁ ≤ W₂) (a : Γ(X, W₂)) : rO h a = rO h' a
theorem

rO_pow

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rO_pow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rO_pow {W₁ W₂ : X.Opens} (h : W₁ ≤ W₂) (a : Γ(X, W₂)) (n : ℕ) : rO h (a ^ n) = rO h a ^ n
theorem

rO_mul

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rO_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rO_mul {W₁ W₂ : X.Opens} (h : W₁ ≤ W₂) (a b : Γ(X, W₂)) : rO h (a * b) = rO h a * rO h b
def

coef

L98 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.coef
Documentation

The unique scalar coefficient of a section with respect to a frame on the given open subset.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
def coef {U V : X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {W : X.Opens} (hWU : W ≤
  U) (hWV : W ≤ V)
    (x : Γ(M, W)) : Γ(X, W)
theorem

coef_smul

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.coef_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_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem coef_smul {U V : X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U)
  (hWV : W ≤ V)
    (x : Γ(M, W)) : coef hs hWU hWV x • rM M hWU s = x
theorem

coef_unique

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.coef_unique
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem coef_unique {U V : X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U)
  (hWV : W ≤ V)
    (x : Γ(M, W)) (g : Γ(X, W)) (hg : g • rM M hWU s = x) : g = coef hs hWU hWV x
theorem

coef_eq_iff

L113 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.coef_eq_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem coef_eq_iff {U V : X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U)
  (hWV : W ≤ V)
    (x : Γ(M, W)) (g : Γ(X, W)) : coef hs hWU hWV x = g ↔ g • rM M hWU s = x
theorem

coef_add

L118 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.coef_add
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem coef_add {U V : X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U)
  (hWV : W ≤ V)
    (x y : Γ(M, W)) : coef hs hWU hWV (x + y) = coef hs hWU hWV x + coef hs hWU hWV y
theorem

coef_mul_smul

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.coef_mul_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_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem coef_mul_smul {U V : X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {W : X.Opens} (hWU : W ≤
  U) (hWV : W ≤ V)
    (a : Γ(X, W)) (x : Γ(M, W)) : coef hs hWU hWV (a • x) = a * coef hs hWU hWV x
theorem

rO_coef

L128 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rO_coef
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem rO_coef {U V : X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {W W' : X.Opens} (hWU : W' ≤ U)
  (hWV : W' ≤ V)
    (h : W ≤ W') (x : Γ(M, W')) :
    rO h (coef hs hWU hWV x) = coef hs (h.trans hWU) (h.trans hWV) (rM M h x)
theorem

coef_eq_mul_coef

L135 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.coef_eq_mul_coef
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem coef_eq_mul_coef {U U' V V' : X.Opens} {s : Γ(M, U)} {s' : Γ(M, U')} (hs : IsFrameOn s V)
  (hs' : IsFrameOn s' V')
    {W : X.Opens} (hWU : W ≤ U) (hWV : W ≤ V) (hWU' : W ≤ U') (hWV' : W ≤ V') (u : Γ(X, W))
    (hu : rM M hWU' s' = u • rM M hWU s) (x : Γ(M, W)) :
    coef hs hWU hWV x = coef hs' hWU' hWV' x * u
abbrev

Uc

L155 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.Uc
Documentation

The inverse image of a standard projective chart under the projective presentation.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
abbrev Uc (i : Fin (N + 1)) : X.Opens
theorem

isFrameOn_σ

L157 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.isFrameOn_σ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem isFrameOn_σ (i : Fin (N + 1)) : IsFrameOn (𝔓.σ i) (Uc 𝔓 i)
abbrev

τ

L161 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.τ
Documentation

The tensor power of the global section providing the frame on the chosen projective chart.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
abbrev τ (i : Fin (N + 1)) : Γ(L.tensorPow m, ⊤)
theorem

isFrameOn_τ

L163 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.isFrameOn_τ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem isFrameOn_τ (i : Fin (N + 1)) : IsFrameOn (τ 𝔓 m i) (Uc 𝔓 i)
theorem

σ_rel

L166 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.σ_rel
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem σ_rel (i j : Fin (N + 1)) :
    rM L (le_top : Uc 𝔓 i ≤ ⊤) (𝔓.σ j) = frameUnit 𝔓.toProj i j • rM L (le_top : Uc 𝔓 i ≤ ⊤) (𝔓.σ
      i)
theorem

τ_rel

L171 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.τ_rel
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem τ_rel (i j : Fin (N + 1)) :
    rM (L.tensorPow m) (le_top : Uc 𝔓 i ≤ ⊤) (τ 𝔓 m j) =
      frameUnit 𝔓.toProj i j ^ m • rM (L.tensorPow m) (le_top : Uc 𝔓 i ≤ ⊤) (τ 𝔓 m i)
theorem

τ_rel_on

L180 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.τ_rel_on
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem τ_rel_on (i j : Fin (N + 1)) {W : X.Opens} (hW : W ≤ Uc 𝔓 i) :
    rM (L.tensorPow m) (le_top : W ≤ ⊤) (τ 𝔓 m j) =
      rO hW (frameUnit 𝔓.toProj i j) ^ m • rM (L.tensorPow m) (le_top : W ≤ ⊤) (τ 𝔓 m i)
def

gcoef

L186 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.gcoef
Documentation

The local coefficient of a tensor-power section on the intersection with a projective chart.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
def gcoef (U : X.Opens) (x : Γ(L.tensorPow m, U)) (i : Fin (N + 1)) : Γ(X, U ⊓ Uc 𝔓
  i)
theorem

gcoef_spec

L190 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.gcoef_spec
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem gcoef_spec (U : X.Opens) (x : Γ(L.tensorPow m, U)) (i : Fin (N + 1)) :
    gcoef 𝔓 m U x i • rM (L.tensorPow m) (le_top : U ⊓ Uc 𝔓 i ≤ ⊤) (τ 𝔓 m i) = rM (L.tensorPow m)
      inf_le_left x
theorem

rO_gcoef_eq

L195 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.rO_gcoef_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem rO_gcoef_eq (U : X.Opens) (x : Γ(L.tensorPow m, U)) (i j : Fin (N + 1)) {W : X.Opens}
    (hi : W ≤ U ⊓ Uc 𝔓 i) (hj : W ≤ U ⊓ Uc 𝔓 j) :
    rO hi (gcoef 𝔓 m U x i) = rO (hi.trans inf_le_right) (frameUnit 𝔓.toProj i j) ^ m * rO hj
      (gcoef 𝔓 m U x j)
theorem

gcoef_compat

L203 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.gcoef_compat
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem gcoef_compat (U : X.Opens) (x : Γ(L.tensorPow m, U)) : TwistCompat 𝔓.toProj m U (gcoef 𝔓 m
  U x)
theorem

gcoef_add

L207 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.gcoef_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem gcoef_add (U : X.Opens) (x y : Γ(L.tensorPow m, U)) (i : Fin (N + 1)) :
    gcoef 𝔓 m U (x + y) i = gcoef 𝔓 m U x i + gcoef 𝔓 m U y i
theorem

gcoef_smul

L211 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.gcoef_smul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem gcoef_smul (U : X.Opens) (a : Γ(X, U)) (x : Γ(L.tensorPow m, U)) (i : Fin (N + 1)) :
    gcoef 𝔓 m U (a • x) i = rO inf_le_left a * gcoef 𝔓 m U x i
def

eMap

L217 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.eMap
Documentation

The linear map from tensor-power sections to compatible twist sections given by their chart coefficients.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · full declaration
def eMap (U : X.Opens) : Γ(L.tensorPow m, U) →ₗ[Γ(X, U)] twistObj f 𝔓.toProj m U where
  toFun x := ⟨gcoef 𝔓 m U x, gcoef_compat 𝔓 m U x⟩
  map_add' x y := twistObj.ext (funext fun i => by
    change gcoef 𝔓 m U (x + y) i = gcoef 𝔓 m U x i + gcoef 𝔓 m U y i
    exact gcoef_add 𝔓 m U x y i)
  map_smul' a x := twistObj.ext (funext fun i => by
    change gcoef 𝔓 m U (a • x) i = restrictFun inf_le_left a * gcoef 𝔓 m U x i
    exact gcoef_smul 𝔓 m U a x i)
theorem

eMap_val

L226 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.eMap_val
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem eMap_val (U : X.Opens) (x : Γ(L.tensorPow m, U)) : (eMap 𝔓 m U x).val =
  gcoef 𝔓 m U x
theorem

eMap_res

L229 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.eMap_res
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem eMap_res (U U' : X.Opens) (h : U ≤ U') (x : Γ(L.tensorPow m, U')) :
    eMap 𝔓 m U (rM (L.tensorPow m) h x) = twistRes f 𝔓.toProj m h (eMap 𝔓 m U' x)
theorem

eMap_bijective

L236 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.eMap_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem eMap_bijective (U : X.Opens) (i₀ : Fin (N + 1)) (hU : U ≤ Uc 𝔓 i₀) : Function.Bijective
  (eMap 𝔓 m U)
theorem

main

L278 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj.S1Sketch.main
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj
universe u
open CategoryTheory Opposite AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
namespace S1Sketch
open AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.ProjSpace
attribute [local instance] MvPolynomial.gradedAlgebra
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
  X.Modules}
  (𝔓 : L.ProjPresentation f N) (m : ℕ)
Lean source · statement
theorem main :
    ∃ e : ∀ U : X.Opens, Γ(L.tensorPow m, U) →ₗ[Γ(X, U)] twistObj f 𝔓.toProj m U,
      (∀ (U : X.Opens) (x : Γ(L.tensorPow m, U)) (i : Fin (N + 1)),
          ((e U x).val i) •
              (L.tensorPow m).presheaf.map (homOfLE (le_top : U ⊓ pullbackChart 𝔓.toProj i ≤ ⊤)).op
                (tensorPowSection (𝔓.σ i) m) =
            (L.tensorPow m).presheaf.map (homOfLE (inf_le_left : U ⊓ pullbackChart 𝔓.toProj i ≤
              U)).op x) ∧
      (∀ (U U' : X.Opens) (h : U ≤ U') (x : Γ(L.tensorPow m, U')),
          e U ((L.tensorPow m).presheaf.map (homOfLE h).op x) = twistRes f 𝔓.toProj m h (e U' x)) ∧
      (∀ (U : X.Opens) (i : Fin (N + 1)), U ≤ pullbackChart 𝔓.toProj i → Function.Bijective (e U))
theorem

exists_linearMap_sections_tensorPow_twistObj

L309 ↗
AlgebraicGeometry.Scheme.Modules.ProjPresentation.exists_linearMap_sections_tensorPow_twistObj
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open CategoryTheory Opposite
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj in
open S1Sketch in
Lean source · statement
theorem Scheme.Modules.ProjPresentation.exists_linearMap_sections_tensorPow_twistObj
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of A)} {L :
      X.Modules}
    (𝔓 : L.ProjPresentation f N) (m : ℕ) :
    ∃ e : ∀ U : X.Opens, Γ(L.tensorPow m, U) →ₗ[Γ(X, U)] ProjSpace.twistObj f 𝔓.toProj m U,
      (∀ (U : X.Opens) (x : Γ(L.tensorPow m, U)) (i : Fin (N + 1)),
          ((e U x).val i) •
              (L.tensorPow m).presheaf.map (homOfLE (le_top : U ⊓ ProjSpace.pullbackChart 𝔓.toProj
                i ≤ ⊤)).op
                (Scheme.Modules.tensorPowSection (𝔓.σ i) m) =
            (L.tensorPow m).presheaf.map (homOfLE (inf_le_left : U ⊓ ProjSpace.pullbackChart
              𝔓.toProj i ≤ U)).op x) ∧
      (∀ (U U' : X.Opens) (h : U ≤ U') (x : Γ(L.tensorPow m, U')),
          e U ((L.tensorPow m).presheaf.map (homOfLE h).op x) = ProjSpace.twistRes f 𝔓.toProj m h
            (e U' x)) ∧
      (∀ (U : X.Opens) (i : Fin (N + 1)), U ≤ ProjSpace.pullbackChart 𝔓.toProj i →
        Function.Bijective (e U))

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