NYLL
Module

Scheme_Modules_FiniteBySections_tensorPow.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_FiniteBySections_tensorPow
29 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Finite By Sections tensor Pow

Imports6
Imported by3

Declarations

abbrev

resTop

L55 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.resTop
Documentation

Restricts a global module section to the specified open subset.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
Lean source · statement
abbrev resTop (M : X.Modules) (s : Γ(M, ⊤)) (V : X.Opens) : Γ(M, V)
theorem

resTop_map

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.resTop_map
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
Lean source · statement
theorem resTop_map {M : X.Modules} (s : Γ(M, ⊤)) {V W : X.Opens} (h : W ≤ V) :
    M.presheaf.map (homOfLE h).op (resTop M s V) = resTop M s W
theorem

isFrameOn_top_iff

L63 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.isFrameOn_top_iff
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
Lean source · full declaration
theorem isFrameOn_top_iff {M : X.Modules} (s : Γ(M, ⊤)) (V : X.Opens) :
    IsFrameOn s V ↔ ∀ W : X.Opens, W ≤ V →
      Function.Bijective fun g : Γ(X, W) => g • (M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op s :
        Γ(M, W)) :=
  ⟨fun h _W hWV => h le_top hWV, fun h W _ hWV => h W hWV⟩
def

wordSection

L75 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.wordSection
Documentation

The tensor product of a finite ordered list of sections, with the unit section for the empty list.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Word
variable {M : X.Modules} {U : X.Opens}
Lean source · full declaration
def wordSection : (n : ℕ) → (Fin n → Γ(M, U)) → Γ(M.tensorPow n, U)
  | 0, _ => unitSection U
  | n + 1, s => tensorSections (L := M.tensorPow n) (M := M)
      (wordSection n (fun k => s k.castSucc)) (s (Fin.last n))
theorem

wordSection_zero

L80 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.wordSection_zero
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Word
variable {M : X.Modules} {U : X.Opens}
Lean source · statement
theorem wordSection_zero (s : Fin 0 → Γ(M, U)) : wordSection 0 s = unitSection U
theorem

wordSection_succ

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.wordSection_succ
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Word
variable {M : X.Modules} {U : X.Opens}
Lean source · full declaration
theorem wordSection_succ (n : ℕ) (s : Fin (n + 1) → Γ(M, U)) :
    wordSection (n + 1) s = tensorSections (L := M.tensorPow n) (M := M)
      (wordSection n (fun k => s k.castSucc)) (s (Fin.last n)) := rfl
theorem

map_wordSection

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.map_wordSection
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Word
variable {M : X.Modules} {U : X.Opens}
Lean source · full declaration
theorem map_wordSection {V : X.Opens} (h : V ≤ U) :
    ∀ (n : ℕ) (s : Fin n → Γ(M, U)),
      (M.tensorPow n).presheaf.map (homOfLE h).op (wordSection n s)
        = wordSection n (fun k => M.presheaf.map (homOfLE h).op (s k))
  | 0, s => by
      rw [wordSection_zero, wordSection_zero]
      exact map_unitSection (homOfLE h)
  | n + 1, s => by
      rw [wordSection_succ, wordSection_succ]
      rw [show (M.tensorPow (n + 1)).presheaf.map (homOfLE h).op
          (tensorSections (L := M.tensorPow n) (M := M) (wordSection n fun k => s k.castSucc) (s
            (Fin.last n)))
          = tensorSections (L := M.tensorPow n) (M := M)
              ((M.tensorPow n).presheaf.map (homOfLE h).op (wordSection n fun k => s k.castSucc))
              (M.presheaf.map (homOfLE h).op (s (Fin.last n))) from
        map_homOfLE_tensorSections (L := M.tensorPow n) (M := M) h _ _]
      rw [map_wordSection h n]
theorem

wordSection_smul

L104 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.wordSection_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Word
variable {M : X.Modules} {U : X.Opens}
Lean source · full declaration
theorem wordSection_smul :
    ∀ (n : ℕ) (g : Fin n → Γ(X, U)) (s : Fin n → Γ(M, U)),
      wordSection n (fun k => g k • s k) = (∏ k, g k) • wordSection n s
  | 0, g, s => by
      change unitSection U = (∏ k : Fin 0, g k) • unitSection U
      rw [Fin.prod_univ_zero]
      exact (one_smul Γ(X, U) (unitSection U)).symm
  | n + 1, g, s => by
      rw [wordSection_succ, wordSection_succ, Fin.prod_univ_castSucc]
      rw [show (fun k : Fin n => (fun k => g k • s k) k.castSucc) = fun k => g k.castSucc • s
        k.castSucc from rfl,
        wordSection_smul n, tensorSections_smul_left, tensorSections_smul_right, smul_smul,
          mul_comm]
      rfl
theorem

isFrameOn_wordSection

L119 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.isFrameOn_wordSection
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Word
variable {M : X.Modules} {U : X.Opens}
Lean source · full declaration
theorem isFrameOn_wordSection {V : X.Opens} :
    ∀ (n : ℕ) (s : Fin n → Γ(M, U)), (∀ k, IsFrameOn (s k) V) → IsFrameOn (wordSection n s) V
  | 0, s, _ => by rw [wordSection_zero]; exact isFrameOn_unitSection V
  | n + 1, s, hs => by
      rw [wordSection_succ]
      exact (isFrameOn_wordSection n _ (fun k => hs k.castSucc)).tensorSections (hs (Fin.last n))
theorem

exists_coef

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.exists_coef
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Frames
variable {M : X.Modules} {U : X.Opens} {s t : Γ(M, U)} {V : X.Opens}
Lean source · statement
theorem exists_coef (h : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U) (hWV : W ≤ V) (m : Γ(M, W)) :
    ∃ g : Γ(X, W), g • M.presheaf.map (homOfLE hWU).op s = m
theorem

isUnit_of_frame_eq_smul

L136 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.isUnit_of_frame_eq_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Frames
variable {M : X.Modules} {U : X.Opens} {s t : Γ(M, U)} {V : X.Opens}
Lean source · statement
theorem isUnit_of_frame_eq_smul (hs : IsFrameOn s V) (ht : IsFrameOn t V) {W : X.Opens} (hWU : W ≤
  U) (hWV : W ≤ V)
    (g : Γ(X, W)) (hg : M.presheaf.map (homOfLE hWU).op t = g • M.presheaf.map (homOfLE hWU).op s)
      : IsUnit g
theorem

isFrameOn_of_eq_unit_smul

L146 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.isFrameOn_of_eq_unit_smul
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Frames
variable {M : X.Modules} {U : X.Opens} {s t : Γ(M, U)} {V : X.Opens}
Lean source · statement
theorem isFrameOn_of_eq_unit_smul (hs : IsFrameOn s V) {W : X.Opens} (hWU : W ≤ U) (hWV : W ≤ V)
    (u : Γ(X, W)) (hu : IsUnit u)
    (ht : M.presheaf.map (homOfLE hWU).op t = u • M.presheaf.map (homOfLE hWU).op s) : IsFrameOn t
      W
abbrev

chart

L183 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.chart
Documentation

The preimage of a coordinate basic open under the given projective presentation.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
abbrev chart (i : Fin (N + 1)) : X.Opens
abbrev

wordMonomial

L187 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.wordMonomial
Documentation

The product of coordinate variables indexed by a word of the given length.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
abbrev wordMonomial (w : Fin b → Fin (N + 1)) : MvPolynomial (Fin (N + 1)) R
theorem

wordMonomial_mem

L190 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.wordMonomial_mem
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
theorem wordMonomial_mem (w : Fin b → Fin (N + 1)) : wordMonomial b w ∈ (𝒜 N) b
abbrev

Uw

L197 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.Uw
Documentation

The preimage of the basic open of a word monomial under the projective presentation.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
abbrev Uw (w : Fin b → Fin (N + 1)) : X.Opens
theorem

prod_not_mem_of_forall

L200 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.prod_not_mem_of_forall
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
omit 𝔓 in
Lean source · statement
theorem prod_not_mem_of_forall {A : Type*} [CommRing A] {I : Ideal A} (hI : I.IsPrime) {ι : Type*}
  (F : Finset ι)
    (g : ι → A) (h : ∀ k ∈ F, g k ∉ I) : ∏ k ∈ F, g k ∉ I
theorem

basicOpen_wordMonomial_le

L215 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.basicOpen_wordMonomial_le
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
theorem basicOpen_wordMonomial_le (w : Fin b → Fin (N + 1)) (k : Fin b) :
    Proj.basicOpen (𝒜 N) (wordMonomial b w) ≤ Proj.basicOpen (𝒜 N) (MvPolynomial.X (w k))
theorem

Uw_le_chart

L224 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.Uw_le_chart
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
theorem Uw_le_chart (w : Fin b → Fin (N + 1)) (k : Fin b) : Uw 𝔓 b w ≤ chart 𝔓 (w k)
abbrev

τ

L228 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.τ
Documentation

The global tensor-power section indexed by the coordinate sections of a word.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
abbrev τ (w : Fin b → Fin (N + 1)) : Γ(M.tensorPow b, ⊤)
theorem

isFrameOn_σ

L230 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.isFrameOn_σ
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
theorem isFrameOn_σ (i : Fin (N + 1)) : IsFrameOn (𝔓.σ i) (chart 𝔓 i)
theorem

isFrameOn_τ

L233 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.isFrameOn_τ
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
theorem isFrameOn_τ (w : Fin b → Fin (N + 1)) : IsFrameOn (τ 𝔓 b w) (Uw 𝔓 b w)
theorem

iSup_chart

L236 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.iSup_chart
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
Lean source · statement
theorem iSup_chart : ⨆ i, chart 𝔓 i = ⊤
theorem

Uw_const

L250 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.Uw_const
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable (hb : 0 < b)
include hb
Lean source · full declaration
theorem Uw_const (i : Fin (N + 1)) : Uw 𝔓 b (fun _ => i) = chart 𝔓 i := by
  change 𝔓.toProj ⁻¹ᵁ _ = 𝔓.toProj ⁻¹ᵁ _
  congr 1
  rw [show wordMonomial b (fun _ : Fin b => i) = MvPolynomial.X i ^ b
    by simp [wordMonomial, Finset.prod_const]]
  exact Proj.basicOpen_pow (𝒜 N) _ b hb
theorem

iSup_Uw

L257 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.iSup_Uw
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable (hb : 0 < b)
include hb
Lean source · statement
theorem iSup_Uw : ⨆ w : Fin b → Fin (N + 1), Uw 𝔓 b w = ⊤
theorem

isAffineOpen_Uw

L264 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.isAffineOpen_Uw
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable (hb : 0 < b)
include hb
Lean source · statement
theorem isAffineOpen_Uw [IsAffineHom 𝔓.toProj] (w : Fin b → Fin (N + 1)) : IsAffineOpen (Uw 𝔓 b w)
theorem

mem_chart_of_isFrameOn_τ

L271 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.mem_chart_of_isFrameOn_τ
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable (hb : 0 < b)
include hb
omit hb in
Lean source · statement
theorem mem_chart_of_isFrameOn_τ (w : Fin b → Fin (N + 1)) (x : X) (U : X.Opens) (hxU : x ∈ U)
    (hτ : IsFrameOn (τ 𝔓 b w) U) (k : Fin b) : x ∈ chart 𝔓 (w k)
theorem

finiteBySections_tensorPow

L297 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow.AlgebraicGeometry.Scheme.Modules.Veronese.finiteBySections_tensorPow
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
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 Veronese
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
section Main
variable {f : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f N) (b : ℕ)
local notation "𝒜" n' => MvPolynomial.homogeneousSubmodule (Fin (n' + 1)) R
variable (hb : 0 < b)
include hb
Lean source · statement
theorem finiteBySections_tensorPow [IsProper f] (hfin : IsFinite 𝔓.toProj) :
    (M.tensorPow b).FiniteBySections f
theorem

tensorPow

L361 ↗
AlgebraicGeometry.Scheme.Modules.FiniteBySections.tensorPow
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_FiniteBySections_tensorPow
universe u
open _root_.AlgebraicGeometry AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.FiniteBySections.tensorPow
    {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} [IsProper f]
    {M : X.Modules} (hM : M.FiniteBySections f) {b : ℕ} (hb : 0 < b) :
    (M.tensorPow b).FiniteBySections f

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