Module

AbelJacobiFiniteSums.lean

Nyll.JacobianVarieties.Albanese.AbelJacobiFiniteSums

4 declarations indexed from sourceView source ↗

Module documentation

Abel–Jacobi finite sums and principal differences

The group law and Abel–Jacobi map constructed from the represented Picard functor identify finite sums of geometric-fibre points with the classes of their normalized point divisors. Hence principal differences of those divisors give the same sum.

The proof uses the actual point-difference comparison supplied by the represented Picard construction, followed by list induction and the defining quotient for Pic⁰. It concerns that constructed Abel–Jacobi map over algebraically closed geometric fibres. It makes no universality claim for an arbitrary map to an abelian variety.

The imported Picard construction retains its Anthropic FLT provenance in its source. The point-divisor construction and finite-sum argument below are new contributions.

Imports13

Imported by2

def

pointDifference

L48 ↗

AlgebraicCurve.CurveModel.pointDifference

Documentation

The degree-zero divisor obtained by subtracting a base point from a geometric point.

Source context 4 commands

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

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

Lean source · statement

def pointDifference {K : Type u} [Field K] [IsAlgClosed K]
    {F : Type v} [Field F] [Algebra K F] [IsCurveOver K F] (M : CurveModel K F)
    (s x : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase) :
    Divisor.degZero (K := K) (F := F)

theorem

coe_sum_pointDifference

L58 ↗

AlgebraicCurve.CurveModel.coe_sum_pointDifference

Documentation

The sum of point differences is the point divisor minus its degree times the base point.

Source context 4 commands

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

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

Lean source · full declaration

theorem coe_sum_pointDifference {K : Type u} [Field K] [IsAlgClosed K]
    {F : Type v} [Field F] [Algebra K F] [IsCurveOver K F] (M : CurveModel K F)
    (s : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase)
    (xs : List (SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase)) :
    ((xs.map (M.pointDifference s)).sum : Divisor K F) =
      (xs.map (fun x => Finsupp.single (M.pointEquivPlace x) (1 : ℤ))).sum -
        xs.length • Finsupp.single (M.pointEquivPlace s) (1 : ℤ) := by
  induction xs with
  | nil =>
    simp only [List.map_nil, List.sum_nil, AddSubgroup.coe_zero, List.length_nil,
      zero_nsmul, sub_zero]
  | cons x xs ih =>
    simp only [List.map_cons, List.sum_cons, AddSubgroup.coe_add, List.length_cons]
    change (Finsupp.single (M.pointEquivPlace x) (1 : ℤ) -
      Finsupp.single (M.pointEquivPlace s) 1) +
        ((xs.map (M.pointDifference s)).sum : Divisor K F) = _
    rw [ih, add_nsmul, one_nsmul, sub_add_sub_comm]
    rw [add_comm (Finsupp.single (M.pointEquivPlace s) (1 : ℤ))]

def

fibrePointImage

L82 ↗

AlgebraicGeometry.RelPicard.fibrePointImage

Documentation

Evaluate a relative map at a point of a geometric-fibre curve model.

Source context 4 commands

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

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

Lean source · statement

def fibrePointImage {R : Type u} [CommRing R]
    {C A : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {a : A ⟶ Spec (CommRingCat.of R)} (q : SchemeHomOver c a)
    {K : Type u} [Field K] (i : R →+* K)
    {F : Type v} [Field F] [Algebra K F] (M : CurveModel K F)
    (e : M.C ⟶ pullback c (Spec.map (CommRingCat.ofHom i)))
    (he : e ≫ pullback.snd c (Spec.map (CommRingCat.ofHom i)) = M.toBase)
    (x : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase) :
    SchemeHomOver (Spec.map (CommRingCat.ofHom i)) a

theorem

exists_abelJacobi_finiteSums_of_representsRelSubPic

L98 ↗

AlgebraicGeometry.RelPicard.exists_abelJacobi_finiteSums_of_representsRelSubPic

Documentation

The constructed Abel–Jacobi map identifies finite sums with normalized divisor classes; principal differences therefore leave those sums unchanged on geometric fibres.

Source context 4 commands

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

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

Lean source · statement

theorem exists_abelJacobi_finiteSums_of_representsRelSubPic
    (R : Type u) [CommRing R]
    {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (hsm : Smooth D.toBase) (hpr : IsProper D.toBase)
    (hgc : GeometricallyConnected D.toBase) :
    ∃ (L : RelativeGroupLaw R D.toBase) (aj : SchemeHomOver c D.toBase),
      AbelianSchemePropertyBundle R D.toBase ∧
      (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
        (x y : SchemeHomOver t D.toBase), L.mul t x y = L.mul t y x) ∧
      (L.one (𝟙 (Spec (CommRingCat.of R)))).1 = D.zeroSection ∧
      ε.1 ≫ aj.1 = D.zeroSection ∧
      ∀ (K : Type u) [Field K] [IsAlgClosed K] (i : R →+* K)
        (F : Type v) [Field F] [Algebra K F] [IsCurveOver K F] (M : CurveModel K F)
        (e : M.C ⟶ pullback c (Spec.map (CommRingCat.ofHom i))) [IsIso e],
        ∀ he : e ≫ pullback.snd c (Spec.map (CommRingCat.ofHom i)) = M.toBase,
        ∃ pts : Pic0 K F ≃ SchemeHomOver (Spec.map (CommRingCat.ofHom i)) D.toBase,
          (∀ x y : Pic0 K F,
            pts (x + y) = L.mul (Spec.map (CommRingCat.ofHom i)) (pts x) (pts y)) ∧
          ∀ (s : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase),
            s.1 ≫ e ≫ pullback.fst c (Spec.map (CommRingCat.ofHom i)) =
              Spec.map (CommRingCat.ofHom i) ≫ ε.1 →
            (∀ xs : List (SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase),
              pts (Pic0.mk (xs.map (M.pointDifference s)).sum) =
                L.sumList (Spec.map (CommRingCat.ofHom i))
                  (xs.map (fibrePointImage c aj i M e he))) ∧
            (∀ xs ys : List (SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase),
              Divisor.IsPrincipal
                (((xs.map (M.pointDifference s)).sum : Divisor K F) -
                  ((ys.map (M.pointDifference s)).sum : Divisor K F)) →
              L.sumList (Spec.map (CommRingCat.ofHom i))
                  (xs.map (fibrePointImage c aj i M e he)) =
                L.sumList (Spec.map (CommRingCat.ofHom i))
                  (ys.map (fibrePointImage c aj i M e he)))

Module documentation

Abel–Jacobi finite sums and principal differences

Declarations

pointDifference

coe_sum_pointDifference

fibrePointImage

exists_abelJacobi_finiteSums_of_representsRelSubPic