Module

OModulePresheafSectionsLinearRes.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafSectionsLinearRes

4 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf Sections Linear Res

Imports1

Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech

Imported by3

def

moduleRestrict

L31 ↗

AlgebraicGeometry.OModulePresheaf.moduleRestrict

Documentation

The section module with scalars restricted along the ring restriction homomorphism.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)

Lean source · statement

def moduleRestrict {U U' : V.Opens} (h : U ≤ U') : Module Γ(V, U') (F.obj U)

def

resₗ

L35 ↗

AlgebraicGeometry.OModulePresheaf.resₗ

Documentation

The restriction map viewed as linear over sections on the larger open.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)

Lean source · full declaration

def resₗ {U U' : V.Opens} (h : U ≤ U') :
    letI := F.moduleRestrict h
    F.obj U' →ₗ[Γ(V, U')] F.obj U :=
  letI := F.moduleRestrict h
  { toFun := F.res h
    map_add' := map_add _
    map_smul' := fun a x => F.res_smul h a x }

theorem

resₗ_apply

L43 ↗

AlgebraicGeometry.OModulePresheaf.resₗ_apply

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)

Lean source · full declaration

theorem resₗ_apply {U U' : V.Opens} (h : U ≤ U') (x : F.obj U') :
    letI := F.moduleRestrict h
    F.resₗ h x = F.res h x := rfl

theorem

moduleRestrict_smul_def

L47 ↗

AlgebraicGeometry.OModulePresheaf.moduleRestrict_smul_def

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)

Lean source · full declaration

theorem moduleRestrict_smul_def {U U' : V.Opens} (h : U ≤ U') (a : Γ(V, U')) (x : F.obj U) :
    letI := F.moduleRestrict h
    a • x = (V.presheaf.map (homOfLE h).op).hom a • x := rfl

Module documentation

OModule Presheaf Sections Linear Res

Declarations

moduleRestrict

resₗ

resₗ_apply

moduleRestrict_smul_def