NYLL
Module

TwoChartCechSectionsOf.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechSectionsOf
10 declarations indexed from sourceView source ↗

Module documentation

Sections of a module sheaf on two affine charts

A morphism to an affine base supplies the base-ring action on module sections. Restriction is linear for this action, and evaluation on two affine opens and their overlap gives the corresponding two-chart Cech section datum.

Imports2
Imported by190

Declarations

def

moduleSectionsOfHom

L35 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.moduleSectionsOfHom
Documentation

The base-ring action on module sections induced by the morphism c.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
Lean source · statement
def moduleSectionsOfHom (c : X ⟶ Spec (.of R)) (M : X.Modules) (U : X.Opens) :
    Module R Γ(M, U)
theorem

isScalarTower_sections

L40 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.isScalarTower_sections
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
Lean source · full declaration
theorem isScalarTower_sections (c : X ⟶ Spec (.of R)) (M : X.Modules) (U : X.Opens) :
    letI := algebraOfHom c U; letI := moduleSectionsOfHom c M U
    IsScalarTower R Γ(X, U) Γ(M, U) :=
  letI := algebraOfHom c U; letI := moduleSectionsOfHom c M U
  IsScalarTower.of_algebraMap_smul fun _ _ => rfl
def

restrictSections

L47 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.restrictSections
Documentation

Restriction of module sections, linear over the base ring through c.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
Lean source · full declaration
def restrictSections (c : X ⟶ Spec (.of R)) (M : X.Modules) {U V : X.Opens} (h : V ≤ U) :
    letI := moduleSectionsOfHom c M U; letI := moduleSectionsOfHom c M V
    Γ(M, U) →ₗ[R] Γ(M, V) :=
  letI := algebraOfHom c U; letI := algebraOfHom c V
  letI := moduleSectionsOfHom c M U; letI := moduleSectionsOfHom c M V
  { toFun := fun x => M.presheaf.map (homOfLE h).op x
    map_add' := fun x y => map_add _ x y
    map_smul' := fun r x => by
      change M.presheaf.map (homOfLE h).op ((algebraMap R Γ(X, U) r) • x)
        = (algebraMap R Γ(X, V) r) • M.presheaf.map (homOfLE h).op x
      rw [Scheme.Modules.map_smul]
      congr 1
      exact (restrictAlgHom c h).commutes r }
theorem

restrictSections_apply

L61 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.restrictSections_apply
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
Lean source · full declaration
theorem restrictSections_apply (c : X ⟶ Spec (.of R)) (M : X.Modules) {U V : X.Opens}
    (h : V ≤ U) (x : Γ(M, U)) :
    letI := moduleSectionsOfHom c M U; letI := moduleSectionsOfHom c M V
    restrictSections c M h x = M.presheaf.map (homOfLE h).op x := rfl
def

sectionsOf

L69 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf
Documentation

The two-chart section datum of M, using its restrictions to the overlap.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) (M : X.Modules)
Lean source · statement
def sectionsOf : TwoChartCech.Sections (𝒱.cover c)
theorem

sectionsOf_M0

L91 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf_M0
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) (M : X.Modules)
Lean source · statement
theorem sectionsOf_M0 : (𝒱.sectionsOf c M).M0 = Γ(M, 𝒱.U0)
theorem

sectionsOf_M1

L92 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf_M1
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) (M : X.Modules)
Lean source · statement
theorem sectionsOf_M1 : (𝒱.sectionsOf c M).M1 = Γ(M, 𝒱.U1)
theorem

sectionsOf_M01

L93 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf_M01
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) (M : X.Modules)
Lean source · statement
theorem sectionsOf_M01 : (𝒱.sectionsOf c M).M01 = Γ(M, 𝒱.U0 ⊓ 𝒱.U1)
theorem

sectionsOf_r0_apply

L94 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf_r0_apply
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) (M : X.Modules)
Lean source · full declaration
theorem sectionsOf_r0_apply (x : Γ(M, 𝒱.U0)) :
    (𝒱.sectionsOf c M).r0 (show (𝒱.sectionsOf c M).M0 from x)
      = M.presheaf.map (homOfLE (inf_le_left : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U0)).op x := rfl
theorem

sectionsOf_r1_apply

L97 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.sectionsOf_r1_apply
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R)) (M : X.Modules)
Lean source · full declaration
theorem sectionsOf_r1_apply (x : Γ(M, 𝒱.U1)) :
    (𝒱.sectionsOf c M).r1 (show (𝒱.sectionsOf c M).M1 from x)
      = M.presheaf.map (homOfLE (inf_le_right : 𝒱.U0 ⊓ 𝒱.U1 ≤ 𝒱.U1)).op x := rfl

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