Module

PolarisedAbelianScheme.lean

Nyll.AlgebraicCurves.Geometry.Picard.PolarisedAbelianScheme

6 declarations indexed from sourceView source ↗

Module documentation

Polarised Abelian Scheme

Imports5

Imported by12

def

finComb

L32 ↗

GoodReductionJacobian.RelativeGroupLaw.finComb

Documentation

The finite product of relative points with the specified natural-number exponents.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace GoodReductionJacobian.RelativeGroupLaw

Lean source · statement

def finComb {S : Type u} [CommRing S] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of S)}
    (L : RelativeGroupLaw S f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of S)) {m : ℕ}
    (x : Fin m → SchemeHomOver t f) (c : Fin m → ℕ) : SchemeHomOver t f

def

geomFibreH0Finrank

L43 ↗

AlgebraicGeometry.Scheme.Modules.geomFibreH0Finrank

Documentation

The rank of global sections of the sheaf on the specified geometric fibre.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry

Lean source · statement

def Scheme.Modules.geomFibreH0Finrank {S : Type u} [CommRing S] {A : Scheme.{u}}
    (f : A ⟶ Spec (CommRingCat.of S)) (M : A.Modules) (k : Type u) [Field k] (sk : S →+* k) : ℕ

structure

PolarisedAbelianScheme

L55 ↗

AlgebraicGeometry.PolarisedAbelianScheme

Documentation

An abelian scheme with level structure and a chosen very ample polarisation.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry

Lean source · full declaration

structure PolarisedAbelianScheme (g d n : ℕ) (S : Type u) [CommRing S] : Type (u + 1) where
  /-- The total space of the abelian scheme. -/
  A : Scheme.{u}
  /-- The structure morphism to the base spectrum. -/
  f : A ⟶ Spec (CommRingCat.of S)
  /-- The relative group law on the total space. -/
  L : RelativeGroupLaw S f
  /-- Commutativity of the relative group law. -/
  comm : L.IsCommutative
  /-- The geometric properties required of an abelian scheme. -/
  bundle : AbelianSchemePropertyBundle S f
  /-- Each fibre has the specified dimension. -/
  dim_fibre : ∀ s : ↥(Spec (CommRingCat.of S)), topologicalKrullDim ↥(f.base ⁻¹' {s}) = g
  /-- The chosen sections defining the level structure. -/
  P : Fin (2 * g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of S))) f
  /-- The chosen sections are killed by the level integer. -/
  P_torsion : ∀ i, L.nsmul (𝟙 (Spec (CommRingCat.of S))) n (P i) = L.one (𝟙 (Spec (CommRingCat.of
    S)))
  /-- The chosen torsion sections are independent on every geometric fibre. -/
  P_indep : ∀ (k : Type u) [Field k] [IsAlgClosed k] (sk : S →+* k) (c c' : Fin (2 * g) → Fin n),
    L.finComb (Spec.map (CommRingCat.ofHom sk))
        (fun i => schemeHomOverComp (Spec.map (CommRingCat.ofHom sk)) (Category.comp_id _) (P i))
          (fun i => (c i : ℕ)) =
      L.finComb (Spec.map (CommRingCat.ofHom sk))
        (fun i => schemeHomOverComp (Spec.map (CommRingCat.ofHom sk)) (Category.comp_id _) (P i))
          (fun i => (c' i : ℕ)) →
      c = c'
  /-- The chosen torsion sections span the geometric torsion points. -/
  P_span : ∀ (k : Type u) [Field k] [IsAlgClosed k] (sk : S →+* k) (Q : SchemeHomOver (Spec.map
    (CommRingCat.ofHom sk)) f),
    L.nsmul (Spec.map (CommRingCat.ofHom sk)) n Q = L.one (Spec.map (CommRingCat.ofHom sk)) →
      ∃ c : Fin (2 * g) → Fin n,
        L.finComb (Spec.map (CommRingCat.ofHom sk))
          (fun i => schemeHomOverComp (Spec.map (CommRingCat.ofHom sk)) (Category.comp_id _) (P
            i)) (fun i => (c i : ℕ)) = Q
  /-- The sheaf of modules defining the polarisation. -/
  pol : A.Modules
  /-- The polarisation sheaf is invertible. -/
  pol_isInvertible : Scheme.Modules.IsInvertible pol
  /-- Sections of the polarisation define a relative closed immersion. -/
  pol_veryAmple : Scheme.Modules.ClosedImmersionBySections pol f
  /-- The polarisation has the specified rank of sections on geometric fibres. -/
  pol_finrank : ∀ (k : Type u) [Field k] [IsAlgClosed k] (sk : S →+* k),
    Scheme.Modules.geomFibreH0Finrank f pol k sk = d

def

Iso

L105 ↗

AlgebraicGeometry.PolarisedAbelianScheme.Iso

Documentation

Isomorphism of the group schemes preserving the level sections and local polarisations.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry
namespace PolarisedAbelianScheme
variable {g d n : ℕ}

Lean source · statement

def Iso {S : Type u} [CommRing S] (u u' : PolarisedAbelianScheme g d n S) : Prop

def

IsPullback

L118 ↗

AlgebraicGeometry.PolarisedAbelianScheme.IsPullback

Documentation

Compatibility of the group law, level sections, and polarisation with base change.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry
namespace PolarisedAbelianScheme
variable {g d n : ℕ}

Lean source · statement

def IsPullback {S S' : Type u} [CommRing S] [CommRing S'] (φ : S →+* S')
    (u : PolarisedAbelianScheme g d n S) (u' : PolarisedAbelianScheme g d n S') : Prop

structure

IsFineModuli

L130 ↗

AlgebraicGeometry.PolarisedAbelianScheme.IsFineModuli

Documentation

The classification properties of the given map to the proposed moduli scheme.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry
namespace PolarisedAbelianScheme
variable {g d n : ℕ}

Lean source · full declaration

structure IsFineModuli (g d n : ℕ) {B : Type} [CommRing B]
    (M : Scheme.{0}) (πM : M ⟶ Spec (CommRingCat.of B))
    (pt : ∀ (S : Type) [CommRing S] (s : Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of B)),
      PolarisedAbelianScheme g d n S → SchemeHomOver s πM) : Prop where
  /-- Isomorphic polarised abelian schemes determine the same moduli point. -/
  pt_iso : ∀ (S : Type) [CommRing S] (s : Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of B))
    (u u' : PolarisedAbelianScheme g d n S), Iso u u' → pt S s u = pt S s u'
  /-- The classification map is compatible with base change. -/
  pt_pullback : ∀ (S S' : Type) [CommRing S] [CommRing S'] (φ : S →+* S')
    (s : Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of B)) (s' : Spec (CommRingCat.of S') ⟶ Spec
      (CommRingCat.of B)),
    Spec.map (CommRingCat.ofHom φ) ≫ s = s' →
    ∀ (u : PolarisedAbelianScheme g d n S) (u' : PolarisedAbelianScheme g d n S'),
    IsPullback φ u u' → (pt S' s' u').1 = Spec.map (CommRingCat.ofHom φ) ≫ (pt S s u).1
  /-- Every relative point of the moduli scheme represents an object. -/
  pt_surjective : ∀ (S : Type) [CommRing S] (s : Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of
    B)) (x : SchemeHomOver s πM),
    ∃ u : PolarisedAbelianScheme g d n S, pt S s u = x
  /-- Objects defining the same moduli point are isomorphic. -/
  pt_injective : ∀ (S : Type) [CommRing S] (s : Spec (CommRingCat.of S) ⟶ Spec (CommRingCat.of B))
    (u u' : PolarisedAbelianScheme g d n S), pt S s u = pt S s u' → Iso u u'

Module documentation

Polarised Abelian Scheme

Declarations

finComb

geomFibreH0Finrank

PolarisedAbelianScheme

Iso

IsPullback

IsFineModuli