Nyll.SchemeTheory.Modules.SectionRing

def

baseScalar

AlgebraicGeometry.GradedOAlgebra.baseScalar

Documentation

Pull a base scalar back to a global section of the structure sheaf.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.GradedOAlgebra
open AlgebraicGeometry.Scheme.Modules
variable {S : Type u} [CommRing S] {X : Scheme.{u}}

Lean source · statement

def baseScalar (f : X ⟶ Spec (CommRingCat.of S)) (s : S) : Γ(X, ⊤)

structure

IsSectionRing

L45 ↗

AlgebraicGeometry.GradedOAlgebra.IsSectionRing

Documentation

Degreewise sections of tensor powers, compatible with addition, scalars, unit and product.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.GradedOAlgebra
open AlgebraicGeometry.Scheme.Modules
variable {S : Type u} [CommRing S] {X : Scheme.{u}}

Lean source · full declaration

structure IsSectionRing (f : X ⟶ Spec (CommRingCat.of S)) (L : X.Modules)
    (R : Type u) [CommRing R] [Algebra S R] (𝓡 : ℕ → Submodule S R) [GradedAlgebra 𝓡]
    (ι : ∀ n : ℕ, 𝓡 n → Γ(L.tensorPow n, ⊤)) : Prop where
  /-- Every homogeneous component is identified bijectively with its tensor-power sections. -/
  bijective : ∀ n, Function.Bijective (ι n)
  /-- The degreewise identification is additive. -/
  map_add : ∀ n (x y : 𝓡 n), ι n (x + y) = ι n x + ι n y
  /-- Base scalar multiplication agrees with multiplication by the pulled-back scalar. -/
  map_smul : ∀ n (s : S) (x : 𝓡 n), ι n (s • x) = baseScalar f s • ι n x
  /-- The graded unit is the tensor-unit section. -/
  map_one : ι 0 ⟨1, SetLike.GradedOne.one_mem⟩ = unitSection ⊤
  /-- Graded multiplication is induced by tensoring sections. -/
  map_mul : ∀ m n (x : 𝓡 m) (y : 𝓡 n),
    ι (m + n) ⟨(x : R) * (y : R), SetLike.GradedMul.mul_mem x.2 y.2⟩ =
      ((tensorPowAdd L m n).hom.app ⊤) (tensorSections (ι m x) (ι n y))

SectionRing.lean

Module documentation

Section rings of invertible module sheaves

baseScalar

IsSectionRing

Module documentation

Section rings of invertible module sheaves

Declarations

baseScalar

IsSectionRing