Module

CurveModelDivisibility.lean

Nyll.JacobianVarieties.Picard.CurveModelDivisibility

1 declaration indexed from sourceView source ↗

Module documentation

Divisibility of the actual degree-zero divisor class group

The curve supplies its Picard scheme and its actual group law. The proved geometric surjectivity of multiplication then supplies divisibility of Pic⁰; neither a Jacobian presentation nor divisibility is an input.

Imports5

Imported by2

theorem

pic0_exists_nsmul_eq

L32 ↗

AlgebraicCurve.CurveModel.pic0_exists_nsmul_eq

Documentation

Multiplication by an integer invertible in the algebraically closed constant field is surjective on the actual degree-zero divisor class group.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian GoodReductionJacobian.RelativeGroupLaw
open AlgebraicCurves.Models.Proofs
open IsCurveOver_of_isIntegral_of_smoothOfRelativeDimension_one
namespace AlgebraicCurve.CurveModel

Lean source · statement

theorem pic0_exists_nsmul_eq
    {K F : Type} [Field K] [IsAlgClosed K]
    [Field F] [Algebra K F] [IsCurveOver K F]
    (M : CurveModel K F)
    (ε : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
    (n : ℕ) (hn : n ≠ 0) (hchar : (n : K) ≠ 0) (x : Pic0 K F) :
    ∃ y : Pic0 K F, n • y = x

Module documentation

Divisibility of the actual degree-zero divisor class group

Declarations

pic0_exists_nsmul_eq