NYLL
Module

OpenCurveCoverGenericCharacter.lean

Nyll.JacobianVarieties.Kummer.OpenCurveCoverGenericCharacter
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 by3

Declarations

def

genericKummerRootLift

L51 ↗
AlgebraicCurve.CurveModel.OpenKummer.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 TopologicalSpace
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel.OpenKummer
attribute [local instance] IsSepClosure.sep_closed
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)
  {Ω : Type u} [Field Ω] [Algebra X.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap X.functionField Ω (j.functionFieldMap hj (M.ffEquiv
    (w.val : F))))
Lean source · statement
def genericKummerRootLift :
    AdjoinRoot (Polynomial.X ^ (n : ℕ) -
      Polynomial.C (j.functionFieldMap hj (M.ffEquiv (w.val : F))) : Polynomial
        X.functionField) →ₐ[X.functionField]
        Ω
theorem

genericKummerRootLift_root

L62 ↗
AlgebraicCurve.CurveModel.OpenKummer.genericKummerRootLift_root
Source context 9 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory TopologicalSpace
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel.OpenKummer
attribute [local instance] IsSepClosure.sep_closed
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)
  {Ω : Type u} [Field Ω] [Algebra X.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap X.functionField Ω (j.functionFieldMap hj (M.ffEquiv
    (w.val : F))))
omit [CompactSpace X] [IsOpenImmersion j] in
Lean source · statement
theorem genericKummerRootLift_root :
    genericKummerRootLift M S n w j hj β hβ (AdjoinRoot.root _) = β
def

genericKummerRootPoint

L66 ↗
AlgebraicCurve.CurveModel.OpenKummer.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 TopologicalSpace
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel.OpenKummer
attribute [local instance] IsSepClosure.sep_closed
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)
  {Ω : Type u} [Field Ω] [Algebra X.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap X.functionField Ω (j.functionFieldMap hj (M.ffEquiv
    (w.val : F))))
Lean source · statement
def genericKummerRootPoint :
    Spec (.of Ω) ⟶ (M.openKummerGenericMap S n w j hj).normalization
theorem

genericKummerRootPoint_over

L72 ↗
AlgebraicCurve.CurveModel.OpenKummer.genericKummerRootPoint_over
Source context 9 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory TopologicalSpace
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel.OpenKummer
attribute [local instance] IsSepClosure.sep_closed
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)
  {Ω : Type u} [Field Ω] [Algebra X.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap X.functionField Ω (j.functionFieldMap hj (M.ffEquiv
    (w.val : F))))
omit [CompactSpace X] [IsOpenImmersion j] in
Lean source · statement
theorem genericKummerRootPoint_over :
    genericKummerRootPoint M S n w j hj β hβ ≫ (M.openKummerGenericMap S n w j
      hj).fromNormalization =
      Spec.map (CommRingCat.ofHom (algebraMap X.functionField Ω)) ≫
        X.fromSpecStalk (genericPoint X)
theorem

genericKummerRootPoint_scale

L91 ↗
AlgebraicCurve.CurveModel.OpenKummer.genericKummerRootPoint_scale
Source context 9 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory TopologicalSpace
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel.OpenKummer
attribute [local instance] IsSepClosure.sep_closed
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)
  {Ω : Type u} [Field Ω] [Algebra X.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap X.functionField Ω (j.functionFieldMap hj (M.ffEquiv
    (w.val : F))))
omit [CompactSpace X] [IsOpenImmersion j] in
Lean source · statement
theorem genericKummerRootPoint_scale
    (ζ : rootsOfUnity (n : ℕ) K) (σ : Ω ≃ₐ[X.functionField] Ω)
    (hscale : algebraMap X.functionField Ω
      (baseToFunctionField (j ≫ M.toBase) ((ζ : Kˣ) : K)) * β = σ β) :
    genericKummerRootPoint M S n w j hj β hβ ≫ (kummerNormalizationRootScale M S n w j hj ζ).hom =
      Spec.map (CommRingCat.ofHom (σ : Ω →+* Ω)) ≫ genericKummerRootPoint M S n w j hj β hβ
theorem

kummerMonodromyCharacter_generic_mul_root

L124 ↗
AlgebraicCurve.CurveModel.OpenKummer.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 TopologicalSpace
open JacobianVarieties.Kummer EtaleFundamentalGroups.Cohomology
open scoped FintypeCatDiscrete
namespace AlgebraicCurve.CurveModel.OpenKummer
attribute [local instance] IsSepClosure.sep_closed
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)
  {Ω : Type u} [Field Ω] [Algebra X.functionField Ω]
  (β : Ω) (hβ : β ^ (n : ℕ) = algebraMap X.functionField Ω (j.functionFieldMap hj (M.ffEquiv
    (w.val : F))))
variable [IsSepClosed K]
include hβ
Lean source · full declaration
theorem kummerMonodromyCharacter_generic_mul_root
    [IsSepClosure X.functionField Ω] (hn : IsUnit ((n : ℕ) : K))
    (σ : Ω ≃ₐ[X.functionField] Ω) :
    let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
    let xi := Spec.map (CommRingCat.ofHom (algebraMap X.functionField Ω))
    let genericMap := X.fromSpecStalk (genericPoint X)
    let g := FiniteEtale.fundamentalGroupHom genericMap xi
      (toAut (FiniteEtale.fiber xi) (Ω ≃ₐ[X.functionField] Ω) σ)
    algebraMap X.functionField Ω (baseToFunctionField (j ≫ M.toBase)
      ((kummerMonodromyCharacter M S n w j hj hinterior hn (xi ≫ genericMap) g : Kˣ) : K)) * β
        = σ β := by
  intro tμ xi genericMap g
  let T := kummerGeometricRootTorsor M S n w j hj hinterior hn (xi ≫ genericMap)
  have := kummerGeometricRootAction_commutes M S n w j hj hinterior hn (xi ≫ genericMap)
  let ι : K →+* Ω := (algebraMap X.functionField Ω).comp (baseToFunctionField (j ≫ M.toBase))
  have hβ0 : β ≠ 0 := by
    intro hz
    have hzero : algebraMap X.functionField Ω (j.functionFieldMap hj (M.ffEquiv (w.val : F)))
      = 0 := by
      rw [← hβ, hz, zero_pow n.ne_zero]
    have hzero' : j.functionFieldMap hj (M.ffEquiv (w.val : F)) = 0 :=
      (algebraMap X.functionField Ω).injective
        (hzero.trans (map_zero (algebraMap X.functionField Ω)).symm)
    have hzero'' : M.ffEquiv (w.val : F) = 0 :=
      (j.functionFieldMap hj).injective
        (hzero'.trans (map_zero (j.functionFieldMap hj)).symm)
    exact (Units.ne_zero w.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.openKummerCover S n hn w j hj hinterior
  let s := genericKummerRootPoint M S n w j hj β hβ
  let e := FiniteEtale.fiberObjEquivHom (xi ≫ genericMap) W
  let x : (FiniteEtale.fiber (xi ≫ genericMap)).obj W :=
    e.symm (Over.homMk s (genericKummerRootPoint_over M S n w j hj β 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 ≫ genericMap)
        (kummerCoverRootScale M S n w j hj hinterior hn ζ).hom x)
    have hright := FiniteEtale.fundamentalGroupHom_field_fiberLift genericMap W σ x
    change (e x).left ≫ (kummerNormalizationRootScale M S n w j hj ζ).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 (· ≫ (kummerNormalizationRootScale M S n w j hj ζ).hom)
      hx).trans
      ((genericKummerRootPoint_scale M S n w j hj β hβ ζ σ hζ).trans
        ((congrArg (Spec.map (CommRingCat.ofHom (σ : Ω →+* Ω)) ≫ ·) hx.symm).trans
          hright.symm)))
  have hχx : kummerMonodromyCharacter M S n w j hj hinterior hn (xi ≫ genericMap) g • x = g •
    x := by
    rw [kummerMonodromyCharacter_eq_torsorCharacter M S n w j hj hinterior hn (xi ≫ genericMap) x]
    exact sdiv_smul (g • x) x
  have hζχ : ζ = kummerMonodromyCharacter M S n w j hj hinterior hn (xi ≫ genericMap) g :=
    (kummerGeometricRootAction_existsUnique M S n w j hj hinterior hn (xi ≫ genericMap) 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.