NYLL
Module

CurveCoverGenericCharacter.lean

Nyll.JacobianVarieties.Kummer.CurveCoverGenericCharacter
6 declarations indexed from sourceView source ↗

Module documentation

The actual Kummer character at the geometric generic point

A chosen root defines a point of the original generic root algebra and hence of its relative normalization. Root scaling and actual Galois monodromy send that point to the same point precisely at the usual root quotient. The proved free action then computes the character as the factor carrying β to σ β.

Imports9
Imported by5

Declarations

def

genericKummerRootLift

L45 ↗
AlgebraicCurve.CurveModel.genericKummerRootLift
Source context 8 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
attribute [local instance] IsSepClosure.sep_closed
variable {K : Type u} [Field K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  {Ω : Type u} [Field Ω] [Algebra M.C.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap M.C.functionField Ω (M.ffEquiv (u.val : F)))
Lean source · statement
def genericKummerRootLift :
    AdjoinRoot (Polynomial.X ^ (n : ℕ) -
      Polynomial.C (M.ffEquiv (u.val : F)) : Polynomial M.C.functionField) →ₐ[M.C.functionField]
        Ω
theorem

genericKummerRootLift_root

L54 ↗
AlgebraicCurve.CurveModel.genericKummerRootLift_root
Source context 8 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
attribute [local instance] IsSepClosure.sep_closed
variable {K : Type u} [Field K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  {Ω : Type u} [Field Ω] [Algebra M.C.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap M.C.functionField Ω (M.ffEquiv (u.val : F)))
Lean source · statement
theorem genericKummerRootLift_root :
    genericKummerRootLift M n u β hβ (AdjoinRoot.root _) = β
def

genericKummerRootPoint

L58 ↗
AlgebraicCurve.CurveModel.genericKummerRootPoint
Source context 8 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
attribute [local instance] IsSepClosure.sep_closed
variable {K : Type u} [Field K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  {Ω : Type u} [Field Ω] [Algebra M.C.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap M.C.functionField Ω (M.ffEquiv (u.val : F)))
Lean source · statement
def genericKummerRootPoint :
    Spec (.of Ω) ⟶ (M.kummerGenericMap n u).normalization
theorem

genericKummerRootPoint_over

L63 ↗
AlgebraicCurve.CurveModel.genericKummerRootPoint_over
Source context 8 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
attribute [local instance] IsSepClosure.sep_closed
variable {K : Type u} [Field K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  {Ω : Type u} [Field Ω] [Algebra M.C.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap M.C.functionField Ω (M.ffEquiv (u.val : F)))
Lean source · statement
theorem genericKummerRootPoint_over :
    genericKummerRootPoint M n u β hβ ≫ (M.kummerGenericMap n u).fromNormalization =
      Spec.map (CommRingCat.ofHom (algebraMap M.C.functionField Ω)) ≫
        M.C.fromSpecStalk (genericPoint M.C)
theorem

genericKummerRootPoint_scale

L80 ↗
AlgebraicCurve.CurveModel.genericKummerRootPoint_scale
Source context 8 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
attribute [local instance] IsSepClosure.sep_closed
variable {K : Type u} [Field K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  {Ω : Type u} [Field Ω] [Algebra M.C.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap M.C.functionField Ω (M.ffEquiv (u.val : F)))
Lean source · statement
theorem genericKummerRootPoint_scale
    (ζ : rootsOfUnity (n : ℕ) K) (σ : Ω ≃ₐ[M.C.functionField] Ω)
    (hscale : algebraMap M.C.functionField Ω
      (baseToFunctionField M.toBase ((ζ : Kˣ) : K)) * β = σ β) :
    genericKummerRootPoint M n u β hβ ≫ (M.kummerNormalizationRootScale n u ζ).hom =
      Spec.map (CommRingCat.ofHom (σ : Ω →+* Ω)) ≫ genericKummerRootPoint M n u β hβ
theorem

kummerMonodromyCharacter_generic_mul_root

L112 ↗
AlgebraicCurve.CurveModel.kummerMonodromyCharacter_generic_mul_root
Documentation

At the actual geometric generic point, the Kummer monodromy character multiplies a chosen root β by exactly the factor that sends β to σ β.

Source context 10 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel
attribute [local instance] IsSepClosure.sep_closed
variable {K : Type u} [Field K]
  {F : Type v} [Field F] [Algebra K F]
  (M : CurveModel K F) (n : ℕ+) (u : Pic0.kummerUnits K F n)
  {Ω : Type u} [Field Ω] [Algebra M.C.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap M.C.functionField Ω (M.ffEquiv (u.val : F)))
variable [IsSepClosed K]
include hβ
Lean source · full declaration
theorem kummerMonodromyCharacter_generic_mul_root
    [IsSepClosure M.C.functionField Ω] (hn : IsUnit ((n : ℕ) : K))
    (σ : Ω ≃ₐ[M.C.functionField] Ω) :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let xi := Spec.map (CommRingCat.ofHom (algebraMap M.C.functionField Ω))
    let j := M.C.fromSpecStalk (genericPoint M.C)
    let g := FiniteEtale.fundamentalGroupHom j xi
      (toAut (FiniteEtale.fiber xi) (Ω ≃ₐ[M.C.functionField] Ω) σ)
    algebraMap M.C.functionField Ω (baseToFunctionField M.toBase
      ((M.kummerMonodromyCharacter n u hn (xi ≫ j) g : Kˣ) : K)) * β = σ β := by
  intro tμ xi j g
  let T := M.kummerGeometricRootTorsor n u hn (xi ≫ j)
  have := M.kummerGeometricRootAction_commutes n u hn (xi ≫ j)
  let ι : K →+* Ω := (algebraMap M.C.functionField Ω).comp (baseToFunctionField M.toBase)
  have hβ0 : β ≠ 0 := by
    intro hz
    have hzero : algebraMap M.C.functionField Ω (M.ffEquiv (u.val : F)) = 0 := by
      rw [← hβ, hz, zero_pow n.ne_zero]
    have hzero' : M.ffEquiv (u.val : F) = 0 :=
      (algebraMap M.C.functionField Ω).injective
        (hzero.trans (map_zero (algebraMap M.C.functionField Ω)).symm)
    exact (Units.ne_zero u.val) (M.ffEquiv.injective
      (hzero'.trans (map_zero M.ffEquiv).symm))
  have hpow : β ^ (n : ℕ) = (σ β) ^ (n : ℕ) := by
    rw [← map_pow, hβ, AlgEquiv.commutes]
  obtain ⟨ζ, hζ, _⟩ := EtaleFundamentalGroups.Kummer.existsUnique_rootScale
    ι n hn β (σ β) hβ0 hpow
  let W := M.kummerCover n hn u
  let s := genericKummerRootPoint M n u β hβ
  let e := FiniteEtale.fiberObjEquivHom (xi ≫ j) W
  let x : (FiniteEtale.fiber (xi ≫ j)).obj W :=
    e.symm (Over.homMk s (genericKummerRootPoint_over M n u β hβ))
  have hx : (e x).left = s := congrArg (fun q => q.left) (e.apply_symm_apply _)
  have hζx : ζ • x = g • x := by
    apply e.injective
    apply Over.OverMorphism.ext
    have hleft := congrArg (fun q => q.left)
      (FiniteEtale.fiberObjEquivHom_naturality (xi ≫ j)
        (M.kummerCoverRootScale n u hn ζ).hom x)
    have hright := FiniteEtale.fundamentalGroupHom_field_fiberLift j W σ x
    change (e x).left ≫ (M.kummerNormalizationRootScale n u ζ).hom =
      (e (ζ • x)).left at hleft
    change (e (g • x)).left = Spec.map (CommRingCat.ofHom (σ : Ω →+* Ω)) ≫
      (e x).left at hright
    exact hleft.symm.trans ((congrArg (· ≫ (M.kummerNormalizationRootScale n u ζ).hom) hx).trans
      ((genericKummerRootPoint_scale M n u β hβ ζ σ hζ).trans
        ((congrArg (Spec.map (CommRingCat.ofHom (σ : Ω →+* Ω)) ≫ ·) hx.symm).trans
          hright.symm)))
  have hχx : M.kummerMonodromyCharacter n u hn (xi ≫ j) g • x = g • x := by
    rw [M.kummerMonodromyCharacter_eq_torsorCharacter n u hn (xi ≫ j) x]
    exact sdiv_smul (g • x) x
  have hζχ : ζ = M.kummerMonodromyCharacter n u hn (xi ≫ j) g :=
    (M.kummerGeometricRootAction_existsUnique n u hn (xi ≫ j) x (g • x)).unique hζx hχx
  rw [← hζχ]
  exact hζ

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