Module

SectionRingConstruction.lean

Nyll.SchemeTheory.Modules.SectionRingConstruction

64 declarations indexed from sourceView source ↗

Module documentation

Constructing the graded section ring

The direct sum of tensor-power global sections is embedded into products of polynomial rings using local frames. The injective coefficient map supplies the ring laws, and the natural summand ranges supply the grading. No section-ring witness is assumed.

Imports7

Nyll.SchemeTheory.Modules.SectionRing
Nyll.SchemeTheory.Modules.FrameFromTrivialization
Nyll.SchemeTheory.Modules.TensorPowerFrames
Nyll.SchemeTheory.Modules.TensorPowerSectionProduct
Nyll.SchemeTheory.Modules.SectionsGluing
Mathlib.Algebra.DirectSum.Ring
Mathlib.Algebra.Polynomial.Coeff

Imported by1

Nyll.SchemeTheory.Modules.All

theorem

app_map

L47 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.app_map

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · statement

theorem app_map {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (i : V ⟶ U) (s : Γ(M, U)) :
    N.presheaf.map i.op (φ.app U s) = φ.app V (M.presheaf.map i.op s)

def

baseHom

L52 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.baseHom

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · statement

def baseHom : S →+* Γ(X, ⊤)

def

Sec

L56 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.Sec

Documentation

Global tensor-power sections with the base action pulled back through f.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · statement

def Sec (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules) (n : ℕ) : ModuleCat S

instance

(anonymous instance)

L60 ↗

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · statement

instance (n : ℕ) : Module Γ(X, ⊤) (Sec f L n)

theorem

baseHom_apply

L63 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.baseHom_apply

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · statement

theorem baseHom_apply (s : S) : baseHom f s = GradedOAlgebra.baseScalar f s

theorem

smul_def

L65 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.smul_def

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · statement

theorem smul_def (n : ℕ) (s : S) (a : Sec f L n) :
    s • a = (GradedOAlgebra.baseScalar f s • (a : Γ(L.tensorPow n, ⊤)) : Γ(L.tensorPow n, ⊤))

def

mulSec

L68 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.mulSec

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · statement

def mulSec {m n : ℕ} (a : Sec f L m) (b : Sec f L n) : Sec f L (m + n)

instance

(anonymous instance)

L72 ↗

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · full declaration

instance : GradedMonoid.GMul (fun n => (Sec f L n : Type u)) where
  mul a b := mulSec f L a b

instance

(anonymous instance)

L75 ↗

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · full declaration

instance : GradedMonoid.GOne (fun n => (Sec f L n : Type u)) where
  one := (unitSection ⊤ : Γ(𝟙_ X.Modules, ⊤))

theorem

gmul_def

L78 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.gmul_def

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · full declaration

theorem gmul_def {m n : ℕ} (a : Sec f L m) (b : Sec f L n) :
    GradedMonoid.GMul.mul (A := fun n => (Sec f L n : Type u)) a b =
      ((tensorPowAdd L m n).hom.app ⊤
        (tensorSections (L := L.tensorPow m) (M := L.tensorPow n) a b) :
        Γ(L.tensorPow (m + n), ⊤)) := rfl

theorem

gone_def

L84 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.gone_def

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · full declaration

theorem gone_def :
    GradedMonoid.GOne.one (A := fun n => (Sec f L n : Type u)) =
    (unitSection ⊤ : Γ(𝟙_ X.Modules, ⊤)) := rfl

instance

(anonymous instance)

L88 ↗

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)

Lean source · full declaration

instance : DirectSum.GNonUnitalNonAssocSemiring (fun n => (Sec f L n : Type u)) where
  mul_zero a := by
    rw [gmul_def]
    erw [tensorSections_zero_right]
    exact ((tensorPowAdd L _ _).hom.app ⊤).hom.map_zero
  zero_mul b := by
    rw [gmul_def]
    erw [tensorSections_zero_left]
    exact ((tensorPowAdd L _ _).hom.app ⊤).hom.map_zero
  mul_add a b c := by
    rw [gmul_def, gmul_def, gmul_def]
    erw [tensorSections_add_right]
    exact ((tensorPowAdd L _ _).hom.app ⊤).hom.map_add _ _
  add_mul a b c := by
    rw [gmul_def, gmul_def, gmul_def]
    erw [tensorSections_add_left]
    exact ((tensorPowAdd L _ _).hom.app ⊤).hom.map_add _ _

theorem

exists_frame

L110 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.exists_frame

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem exists_frame (x : X) :
    ∃ (U : X.Opens) (g : Γ(L, U)), x ∈ U ∧ IsFrameOn g U

def

frU

L116 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.frU

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def frU (x : X) : X.Opens

def

frG

L119 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.frG

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def frG (x : X) : Γ(L, frU L x)

theorem

mem_frU

L122 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.mem_frU

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem mem_frU (x : X) : x ∈ frU L x

theorem

isFrameOn_frG

L125 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.isFrameOn_frG

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem isFrameOn_frG (x : X) : IsFrameOn (frG L x) (frU L x)

theorem

iSup_frU

L128 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.iSup_frU

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem iSup_frU : (⊤ : X.Opens) ≤ ⨆ x, frU L x

def

frG'

L131 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.frG'

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def frG' (x : X) : Γ(L, frU L x)

def

frE

L134 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.frE

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def frE (x : X) (n : ℕ) : Γ(L.tensorPow n, frU L x)

theorem

bijective_smul_frE

L136 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.bijective_smul_frE

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

theorem bijective_smul_frE (x : X) (n : ℕ) :
    Function.Bijective fun g : Γ(X, frU L x) => g • frE L x n := by
  have h := ((isFrameOn_frG L x).tensorPowSection_monoidalV2 n) (le_refl _) (le_refl _)
  have e : (L.tensorPow n).presheaf.map (homOfLE (le_refl (frU L x))).op
      (tensorPowSection (frG L x) n) =
      frE L x n := map_tensorPowSection _ _ _
  simpa only [e] using h

def

resU

L144 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.resU

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def resU (x : X) (n : ℕ) (c : Γ(L.tensorPow n, ⊤)) : Γ(L.tensorPow n, frU L x)

def

coef

L147 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def coef (x : X) (n : ℕ) (c : Γ(L.tensorPow n, ⊤)) : Γ(X, frU L x)

theorem

coef_smul_frE

L150 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef_smul_frE

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem coef_smul_frE (x : X) (n : ℕ) (c : Γ(L.tensorPow n, ⊤)) :
    coef L x n c • frE L x n = resU L x n c

theorem

coef_eq_of_smul_eq

L154 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef_eq_of_smul_eq

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem coef_eq_of_smul_eq (x : X) (n : ℕ) (c : Γ(L.tensorPow n, ⊤)) (a : Γ(X, frU L x))
    (h : a • frE L x n = resU L x n c) : coef L x n c = a

theorem

coef_zero

L158 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef_zero

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem coef_zero (x : X) (n : ℕ) : coef L x n 0 = 0

theorem

coef_add

L161 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef_add

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem coef_add (x : X) (n : ℕ) (c d : Γ(L.tensorPow n, ⊤)) :
    coef L x n (c + d) = coef L x n c + coef L x n d

theorem

coef_smul

L166 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef_smul

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem coef_smul (x : X) (n : ℕ) (r : Γ(X, ⊤)) (c : Γ(L.tensorPow n, ⊤)) :
    coef L x n (r • c) = X.presheaf.map (homOfLE (le_top : frU L x ≤ ⊤)).op r * coef L x n c

theorem

coef_gmul

L171 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef_gmul

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

theorem coef_gmul (x : X) {m n : ℕ} (a : Sec f L m) (b : Sec f L n) :
    coef L x (m + n) (GradedMonoid.GMul.mul (A := fun n => (Sec f L n : Type u)) a b) =
      coef L x m a * coef L x n b := by
  apply coef_eq_of_smul_eq
  erw [resU, gmul_def, app_map, map_homOfLE_tensorSections]
  change (coef L x m a * coef L x n b) • frE L x (m + n) =
    (tensorPowAdd L m n).hom.app (frU L x) (tensorSections (resU L x m a) (resU L x n b))
  erw [← coef_smul_frE L x m a, ← coef_smul_frE L x n b, tensorSections_smul_left,
    tensorSections_smul_right, Hom.app_smul,
    Hom.app_smul, smul_smul]
  simp only [frE]
  erw [tensorPowAdd_hom_app_tensorSections_tensorPowSection]

theorem

coef_gone

L184 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coef_gone

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

theorem coef_gone (x : X) :
    coef L x 0 (GradedMonoid.GOne.one (A := fun n => (Sec f L n : Type u))) = 1 :=
  coef_eq_of_smul_eq L x 0 _ _ (by
    rw [one_smul, gone_def]
    erw [resU]
    exact (map_unitSection (homOfLE (le_top : frU L x ≤ ⊤))).symm)

theorem

eq_zero_of_forall_coef_eq_zero

L191 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.eq_zero_of_forall_coef_eq_zero

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem eq_zero_of_forall_coef_eq_zero {n : ℕ} (c : Γ(L.tensorPow n, ⊤))
    (h : ∀ x, coef L x n c = 0) : c = 0

abbrev

Tgt

L199 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.Tgt

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

abbrev Tgt : Type u

def

coefHom

L201 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coefHom

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

def coefHom (n : ℕ) : Sec f L n →+ Tgt L where
  toFun c := fun x => Polynomial.monomial n (coef L x n c)
  map_zero' := by funext x; simp only [Pi.zero_apply]; erw [coef_zero]; exact map_zero _
  map_add' c d := by funext x; simp only [Pi.add_apply]; erw [coef_add]; exact map_add _ _ _

theorem

coefHom_apply

L206 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coefHom_apply

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem coefHom_apply (n : ℕ) (c : Sec f L n) (x : X) :
    coefHom f L n c x = Polynomial.monomial n (coef L x n c)

def

F

L209 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.F

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def F : (⨁ n, Sec f L n) →+ Tgt L

theorem

F_of

L211 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.F_of

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

theorem F_of (n : ℕ) (c : Sec f L n) :
    F f L (DirectSum.of (fun n => (Sec f L n : Type u)) n c) = coefHom f L n c :=
  DirectSum.toAddMonoid_of _ _ _

theorem

F_mul

L215 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.F_mul

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem F_mul (r s : ⨁ n, Sec f L n) : F f L (r * s) = F f L r * F f L s

theorem

F_one

L230 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.F_one

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem F_one : F f L 1 = 1

theorem

F_apply_coeff

L235 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.F_apply_coeff

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem F_apply_coeff (r : ⨁ n, Sec f L n) (x : X) (n : ℕ) :
    (F f L r x).coeff n = coef L x n (r n)

theorem

F_injective

L247 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.F_injective

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
section Frames
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem F_injective : Function.Injective (F f L)

theorem

one_mul'

L261 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.one_mul'

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem one_mul' (a : ⨁ n, Sec f L n) : 1 * a = a

theorem

mul_one'

L264 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.mul_one'

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem mul_one' (a : ⨁ n, Sec f L n) : a * 1 = a

theorem

mul_assoc'

L267 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.mul_assoc'

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem mul_assoc' (a b c : ⨁ n, Sec f L n) : a * b * c = a * (b * c)

theorem

mul_comm'

L270 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.mul_comm'

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem mul_comm' (a b : ⨁ n, Sec f L n) : a * b = b * a

instance

instCommRing

L273 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.instCommRing

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

instance instCommRing : CommRing (⨁ n, Sec f L n)

def

cS

L282 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.cS

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def cS (s : S) : Tgt L

theorem

F_smul

L285 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.F_smul

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem F_smul (s : S) (r : ⨁ n, Sec f L n) : F f L (s • r) = cS f L s * F f L r

theorem

smul_mul'

L295 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.smul_mul'

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem smul_mul' (s : S) (a b : ⨁ n, Sec f L n) : s • a * b = s • (a * b)

theorem

mul_smul'

L298 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.mul_smul'

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem mul_smul' (s : S) (a b : ⨁ n, Sec f L n) : a * s • b = s • (a * b)

instance

instAlgebra

L301 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.instAlgebra

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

instance instAlgebra : Algebra S (⨁ n, Sec f L n)

def

𝓡

L304 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.𝓡

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

def 𝓡 (n : ℕ) : Submodule S (⨁ n, Sec f L n) where
  carrier := Set.range (DirectSum.of (fun n => (Sec f L n : Type u)) n)
  zero_mem' := ⟨0, map_zero _⟩
  add_mem' := by
    rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩
    exact ⟨a + b, map_add _ a b⟩
  smul_mem' := by
    rintro s _ ⟨a, rfl⟩
    exact ⟨s • a, DirectSum.of_smul _ _ _ _⟩

theorem

mem_𝓡_iff

L315 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.mem_𝓡_iff

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]
omit [Fact (Scheme.Modules.IsInvertible L)] in

Lean source · full declaration

theorem mem_𝓡_iff {n : ℕ} (r : ⨁ n, Sec f L n) :
    r ∈ 𝓡 f L n ↔ ∃ a, DirectSum.of (fun n => (Sec f L n : Type u)) n a = r := Iff.rfl

instance

(anonymous instance)

L318 ↗

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

instance : SetLike.GradedMonoid (𝓡 f L) where
  one_mem := ⟨GradedMonoid.GOne.one (A := fun n => (Sec f L n : Type u)), rfl⟩
  mul_mem := by
    rintro i j _ _ ⟨a, rfl⟩ ⟨b, rfl⟩
    exact ⟨GradedMonoid.GMul.mul (A := fun n => (Sec f L n : Type u)) a b,
      (DirectSum.of_mul_of (A := fun n => (Sec f L n : Type u)) a b).symm⟩

def

toPiece

L325 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.toPiece

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

def toPiece (n : ℕ) : Sec f L n →+ 𝓡 f L n where
  toFun a := ⟨DirectSum.of (fun n => (Sec f L n : Type u)) n a, a, rfl⟩
  map_zero' := Subtype.ext (map_zero _)
  map_add' a b := Subtype.ext (map_add _ a b)

def

decomposeHom

L330 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.decomposeHom

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def decomposeHom : (⨁ n, Sec f L n) →+ ⨁ n, 𝓡 f L n

theorem

decomposeHom_of

L333 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.decomposeHom_of

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

theorem decomposeHom_of (n : ℕ) (a : Sec f L n) :
    decomposeHom f L (DirectSum.of (fun n => (Sec f L n : Type u)) n a) =
      DirectSum.of (fun n => 𝓡 f L n) n (toPiece f L n a) :=
  DirectSum.toAddMonoid_of _ _ _

theorem

coe_comp_decomposeHom

L338 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.coe_comp_decomposeHom

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem coe_comp_decomposeHom :
    (DirectSum.coeAddMonoidHom (𝓡 f L)).comp (decomposeHom f L) = AddMonoidHom.id _

theorem

decomposeHom_comp_coe

L346 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.decomposeHom_comp_coe

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

theorem decomposeHom_comp_coe :
    (decomposeHom f L).comp (DirectSum.coeAddMonoidHom (𝓡 f L)) = AddMonoidHom.id _

instance

(anonymous instance)

L354 ↗

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

instance : DirectSum.Decomposition (𝓡 f L) where
  decompose' := decomposeHom f L
  left_inv r := by
    have := congrArg (fun k => k r) (coe_comp_decomposeHom f L)
    exact this
  right_inv y := by
    have := congrArg (fun k => k y) (decomposeHom_comp_coe f L)
    exact this

instance

instGradedAlgebra

L363 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.instGradedAlgebra

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

instance instGradedAlgebra : GradedAlgebra (𝓡 f L)

def

ι

L367 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.ι

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · statement

def ι (n : ℕ) (x : 𝓡 f L n) : Γ(L.tensorPow n, ⊤)

theorem

ι_of

L370 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.ι_of

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]
omit [Fact (Scheme.Modules.IsInvertible L)] in

Lean source · full declaration

theorem ι_of (n : ℕ) (a : Sec f L n)
    (h : DirectSum.of (fun n => (Sec f L n : Type u)) n a ∈ 𝓡 f L n) :
    ι f L n ⟨DirectSum.of (fun n => (Sec f L n : Type u)) n a, h⟩ = a :=
  DirectSum.of_eq_same (β := fun n => (Sec f L n : Type u)) n a

theorem

isSectionRing

L375 ↗

AlgebraicGeometry.GradedOAlgebra.SectionRingConstruction.isSectionRing

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
namespace SectionRingConstruction
open Opposite DirectSum
variable {S : Type u} [CommRing S] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
variable [Fact (Scheme.Modules.IsInvertible L)]

Lean source · full declaration

theorem isSectionRing :
    GradedOAlgebra.IsSectionRing f L (⨁ n, Sec f L n) (𝓡 f L) (ι f L) where
  bijective n := by
    constructor
    · rintro ⟨_, a, rfl⟩ ⟨_, b, rfl⟩ h
      erw [ι_of f L n a _, ι_of f L n b _] at h
      subst h
      rfl
    · intro c
      exact ⟨⟨DirectSum.of (fun n => (Sec f L n : Type u)) n c, c, rfl⟩, ι_of f L n c _⟩
  map_add n x y := DirectSum.add_apply _ _ _
  map_smul n s x := by
    change ((s • (x : ⨁ n, Sec f L n)) n : Sec f L n) = GradedOAlgebra.baseScalar f s • ι f L n x
    rw [DirectSum.smul_apply]
    rfl
  map_one := by
    change ((1 : ⨁ n, Sec f L n) 0 : Sec f L 0) = unitSection ⊤
    rw [DirectSum.one_def, DirectSum.of_eq_same]
    rfl
  map_mul m n x y := by
    obtain ⟨_, a, rfl⟩ := x
    obtain ⟨_, b, rfl⟩ := y
    change ((DirectSum.of (fun n => (Sec f L n : Type u)) m a *
        DirectSum.of (fun n => (Sec f L n : Type u)) n b) (m + n) : Sec f L (m + n)) =
      (tensorPowAdd L m n).hom.app ⊤
        (tensorSections (ι f L m ⟨_, a, rfl⟩) (ι f L n ⟨_, b, rfl⟩))
    rw [DirectSum.of_mul_of, DirectSum.of_eq_same]
    erw [ι_of f L m a _, ι_of f L n b _]
    rfl

theorem

exists_isSectionRing

L409 ↗

AlgebraicGeometry.GradedOAlgebra.exists_isSectionRing

Documentation

An invertible module sheaf has its concrete graded ring of global tensor-power sections.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry.GradedOAlgebra
open scoped DirectSum SectionRingConstruction in

Lean source · statement

theorem exists_isSectionRing
    {S : Type u} [CommRing S] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
    (hL : Scheme.Modules.IsInvertible L) :
    ∃ (R : Type u) (_ : CommRing R) (_ : Algebra S R) (𝓡 : ℕ → Submodule S R) (_ : GradedAlgebra 𝓡)
        (ι : ∀ n : ℕ, 𝓡 n → Γ(L.tensorPow n, ⊤)),
      AlgebraicGeometry.GradedOAlgebra.IsSectionRing f L R 𝓡 ι

Module documentation

Constructing the graded section ring

Declarations