Module

RelativeSectionTwist.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.RelativeSectionTwist

3 declarations indexed from sourceView source ↗

Module documentation

Twists by a rigidifying section

Defines the ideal and module twists of the rigidifying section after base change.

Imports2

Imported by16

def

sectionIdeal

L35 ↗

AlgebraicGeometry.RelPicard.sectionIdeal

Documentation

The ideal sheaf of the rigidifying section after base change.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra MonoidalCategory
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}} (t : T ⟶ Spec
    (CommRingCat.of R))

Lean source · statement

def sectionIdeal : (pullback c t).IdealSheafData

def

sectionTwist

L38 ↗

AlgebraicGeometry.RelPicard.sectionTwist

Documentation

The inverse ideal module of the rigidifying section raised to the given power.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra MonoidalCategory
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}} (t : T ⟶ Spec
    (CommRingCat.of R))

Lean source · statement

def sectionTwist (r : ℕ) : (pullback c t).Modules

abbrev

fibreModule

L41 ↗

AlgebraicGeometry.RelPicard.fibreModule

Documentation

The pullback of a module to the fibre over the given field-valued point.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra MonoidalCategory
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}} (t : T ⟶ Spec
    (CommRingCat.of R))

Lean source · statement

abbrev fibreModule {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
    (F : (pullback c t).Modules) : (pullback (pullback.snd c t) s).Modules

Module documentation

Twists by a rigidifying section

Declarations

sectionIdeal

sectionTwist

fibreModule