Module

OpenCurveCoverSplitting.lean

Nyll.JacobianVarieties.Kummer.OpenCurveCoverSplitting

4 declarations indexed from sourceView source ↗

Module documentation

Splitting and the kernel of the actual open Kummer class

A section of the actual normalized cover is equivalent to an actual nth power in the original function field. Consequently the kernel of the derived H¹ class is exactly the previously defined subgroup of powers.

Imports5

Imported by2

theorem

exists_section_of_pow

L40 ↗

AlgebraicCurve.CurveModel.OpenKummer.exists_section_of_pow

Documentation

An actual function-field root gives a section on the open curve.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  (w : Pic0.openKummerUnits K F S n)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))

Lean source · statement

theorem exists_section_of_pow (b : F) (hb : b ^ (n : ℕ) = (w.val : F)) :
    ∃ s : X ⟶ (M.openKummerCover S n hn w j hj hinterior).left,
      s ≫ (M.openKummerCover S n hn w j hj hinterior).hom = 𝟙 X

theorem

exists_pow_of_section

L85 ↗

AlgebraicCurve.CurveModel.OpenKummer.exists_pow_of_section

Documentation

A section forces a root in the original function field, using the canonical function-field equivalence of the open immersion.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  (w : Pic0.openKummerUnits K F S n)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))

Lean source · statement

theorem exists_pow_of_section
    (s : X ⟶ (M.openKummerCover S n hn w j hj hinterior).left)
    (hs : s ≫ (M.openKummerCover S n hn w j hj hinterior).hom = 𝟙 X) :
    ∃ b : F, b ^ (n : ℕ) = (w.val : F)

theorem

mem_openKummerPowers_iff_exists_section

L102 ↗

AlgebraicCurve.CurveModel.OpenKummer.mem_openKummerPowers_iff_exists_section

Documentation

The actual covering section criterion is precisely the actual power subgroup, with no Picard or cohomology comparison assumed.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  (w : Pic0.openKummerUnits K F S n)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))

Lean source · statement

theorem mem_openKummerPowers_iff_exists_section :
    w ∈ Pic0.openKummerPowers K F S n ↔
      ∃ s : X ⟶ (M.openKummerCover S n hn w j hj hinterior).left,
        s ≫ (M.openKummerCover S n hn w j hj hinterior).hom = 𝟙 X

theorem

kummerEtaleClass_eq_zero_iff_mem_powers

L121 ↗

AlgebraicCurve.CurveModel.OpenKummer.kummerEtaleClass_eq_zero_iff_mem_powers

Documentation

The genuine derived H¹ class vanishes exactly on actual powers.

Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory AlgebraicGeometry TopologicalSpace
namespace AlgebraicCurve.CurveModel.OpenKummer
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (S : Set (Place K F)) (n : ℕ+)
  (w : Pic0.openKummerUnits K F S n)
  {X : Scheme.{u}} [IsIntegral X] [CompactSpace X]
  (j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
  (hinterior : ∀ (y : X) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
  (hn : IsUnit ((n : ℕ) : K))

Lean source · statement

theorem kummerEtaleClass_eq_zero_iff_mem_powers
    [IsSepClosed K] {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ X) :
    kummerEtaleClass M S n w j hj hinterior hn ξ = 0 ↔
      w ∈ Pic0.openKummerPowers K F S n

Module documentation

Splitting and the kernel of the actual open Kummer class

Declarations

exists_section_of_pow

exists_pow_of_section

mem_openKummerPowers_iff_exists_section

kummerEtaleClass_eq_zero_iff_mem_powers