Module

ChartSections.lean

Nyll.AlgebraicCurves.Geometry.Picard.ChartSections

4 declarations indexed from sourceView source ↗

Module documentation

Fibrewise section conditions for charts of the relative Picard functor. The conditions combine Riemann--Roch with point removals prescribed by sections.

Imports3

Imported by25

def

sectionFibrePoint

L29 ↗

AlgebraicGeometry.RelPicard.sectionFibrePoint

Documentation

The point of a geometric fibre induced by a section, with its projection identity.

Source context 3 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra AlgebraicCurve
universe u

Lean source · statement

def sectionFibrePoint {R : Type u} [CommRing R] {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)}
    (γ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {k : Type u} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R)) :
    {p : Spec (CommRingCat.of k) ⟶ pullback c s // p ≫ pullback.snd c s = 𝟙 _}

def

ChartSectionsAt

L38 ↗

AlgebraicGeometry.RelPicard.ChartSectionsAt

Documentation

The fibre satisfies Riemann--Roch and the dimension-one point-removal chart condition.

Source context 3 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra AlgebraicCurve
universe u

Lean source · statement

def ChartSectionsAt {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {n g r : ℕ} (γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {k : Type u} [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    {L : Type u} [Field L] [Algebra k L] (M : CurveModel k L)
    (e : M.C ≅ pullback c s) (he : e.hom ≫ pullback.snd c s = M.toBase) : Prop

def

HasChartSections

L52 ↗

AlgebraicGeometry.RelPicard.HasChartSections

Documentation

The section chart condition holds on every algebraically closed geometric fibre.

Source context 3 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra AlgebraicCurve
universe u

Lean source · statement

def HasChartSections {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {n g r : ℕ} (γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) : Prop

def

HasChartSectionsOverClosedPoints

L60 ↗

AlgebraicGeometry.RelPicard.HasChartSectionsOverClosedPoints

Documentation

The section chart condition holds on every closed algebraically closed geometric fibre.

Source context 3 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra AlgebraicCurve
universe u

Lean source · statement

def HasChartSectionsOverClosedPoints {R : Type u} [CommRing R] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    {n g r : ℕ} (γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) : Prop

Module documentation

Declarations

sectionFibrePoint

ChartSectionsAt

HasChartSections

HasChartSectionsOverClosedPoints