NYLL
Module

OpenDivisorResidueLifting.lean

Nyll.JacobianVarieties.Kummer.OpenDivisorResidueLifting
2 declarations indexed from sourceView source ↗

Module documentation

Lifting boundary divisor residues to actual functions

Divide the actual Pic⁰ class of a degree-zero divisor by the exponent. Subtracting the resulting multiple gives a principal divisor and hence an actual nonzero function with the prescribed orders modulo the exponent. The divisor's class is divided using the actual Picard scheme of the curve.

Imports2
Imported by2

Declarations

theorem

exists_function_ord_mod_eq

L27 ↗
AlgebraicCurve.CurveModel.exists_function_ord_mod_eq
Documentation

Every degree-zero divisor is congruent modulo an invertible exponent to the principal divisor of an actual nonzero function.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace AlgebraicCurve.CurveModel
Lean source · statement
theorem exists_function_ord_mod_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 : ℕ+) (hchar : ((n : ℕ) : K) ≠ 0)
    (D : Divisor.degZero (K := K) (F := F)) :
    ∃ u : Fˣ, ∀ v : Place K F,
      (v.ord (u : F) : ZMod (n : ℕ)) = ((D : Divisor K F) v : ZMod (n : ℕ))
theorem

exists_openKummerUnits_residue_eq

L56 ↗
AlgebraicCurve.CurveModel.exists_openKummerUnits_residue_eq
Documentation

If the given divisor has divisible coefficients away from the boundary, the function constructed from it is unramified there and has its prescribed boundary residues.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace AlgebraicCurve.CurveModel
Lean source · full declaration
theorem exists_openKummerUnits_residue_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)
    (S : Set (Place K F)) (n : ℕ+) (hchar : ((n : ℕ) : K) ≠ 0)
    (D : Divisor.degZero (K := K) (F := F))
    (hD : ∀ v : Place K F, v ∉ S → (n : ℤ) ∣ (D : Divisor K F) v) :
    ∃ u : Pic0.openKummerUnits K F S n,
      Pic0.openKummerResidue S n u =
        Multiplicative.ofAdd (fun v : S => ((D : Divisor K F) v.val : ZMod (n : ℕ))) := by
  obtain ⟨u, hu⟩ := M.exists_function_ord_mod_eq ε n hchar D
  have hunit : u ∈ Pic0.openKummerUnits K F S n := by
    intro v hv
    apply (ZMod.intCast_zmod_eq_zero_iff_dvd (v.ord (u : F)) (n : ℕ)).mp
    rw [hu v]
    exact (ZMod.intCast_zmod_eq_zero_iff_dvd
      ((D : Divisor K F) v) (n : ℕ)).mpr (hD v hv)
  refine ⟨⟨u, hunit⟩, ?_⟩
  apply Multiplicative.toAdd.injective
  funext v
  exact hu v.val

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.