NYLL
Module

OpenCurveCoverAction.lean

Nyll.JacobianVarieties.Kummer.OpenCurveCoverAction
14 declarations indexed from sourceView source ↗

Module documentation

Root-of-unity automorphisms of the actual normalized Kummer cover

The explicit scaling automorphism of the generic root algebra extends through the universal property of relative normalization. The construction uses the original normalized finite étale cover, without assuming its connectedness.

Imports5
Imported by6

Declarations

def

scalarRoot

L37 ↗
AlgebraicCurve.CurveModel.OpenKummer.scalarRoot
Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
Lean source · statement
def scalarRoot (ζ : rootsOfUnity (n : ℕ) K) :
    rootsOfUnity (n : ℕ) U.functionField
def

kummerGenericRootScale

L43 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerGenericRootScale
Documentation

Scaling of the root in the original generic Kummer algebra, as an actual isomorphism of its spectrum.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
Lean source · statement
def kummerGenericRootScale (ζ : rootsOfUnity (n : ℕ) K) :
    Spec (.of (AdjoinRoot (Polynomial.X ^ (n : ℕ) -
        Polynomial.C (j.functionFieldMap hj (M.ffEquiv (a.val : F))) : Polynomial
            U.functionField))) ≅
      Spec (.of (AdjoinRoot (Polynomial.X ^ (n : ℕ) -
        Polynomial.C (j.functionFieldMap hj (M.ffEquiv (a.val : F))) : Polynomial
            U.functionField)))
theorem

kummerGenericRootScale_hom_over

L56 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerGenericRootScale_hom_over
Documentation

Root scaling is over the original curve, since it fixes its function field.

Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
omit [IsOpenImmersion j] in
Lean source · statement
theorem kummerGenericRootScale_hom_over (ζ : rootsOfUnity (n : ℕ) K) :
    (kummerGenericRootScale M S n a j hj ζ).hom ≫ M.openKummerGenericMap S n a j hj =
      M.openKummerGenericMap S n a j hj
theorem

kummerGenericRootScale_one

L72 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerGenericRootScale_one
Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
omit [IsOpenImmersion j] in
Lean source · statement
theorem kummerGenericRootScale_one :
    (kummerGenericRootScale M S n a j hj 1).hom = 𝟙 _
theorem

kummerGenericRootScale_mul

L82 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerGenericRootScale_mul
Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
omit [IsOpenImmersion j] in
Lean source · statement
theorem kummerGenericRootScale_mul (ζ η : rootsOfUnity (n : ℕ) K) :
    (kummerGenericRootScale M S n a j hj (ζ * η)).hom =
      (kummerGenericRootScale M S n a j hj η).hom ≫ (kummerGenericRootScale M S n a j hj ζ).hom
def

kummerNormalizationRootScale

L108 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerNormalizationRootScale
Documentation

The generic root-scaling automorphism extends to the original relative normalization through its proved universal property.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
Lean source · statement
def kummerNormalizationRootScale (ζ : rootsOfUnity (n : ℕ) K) :
    (M.openKummerGenericMap S n a j hj).normalization ≅ (M.openKummerGenericMap S n a j
        hj).normalization
theorem

toNormalization_kummerNormalizationRootScale

L118 ↗
AlgebraicCurve.CurveModel.OpenKummer.toNormalization_kummerNormalizationRootScale
Documentation

The extension to normalization retains the original generic root scaling.

Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
omit [IsOpenImmersion j] in
Lean source · statement
theorem toNormalization_kummerNormalizationRootScale (ζ : rootsOfUnity (n : ℕ) K) :
    (M.openKummerGenericMap S n a j hj).toNormalization ≫ (kummerNormalizationRootScale M S n a
        j hj ζ).hom =
      (kummerGenericRootScale M S n a j hj ζ).hom ≫ (M.openKummerGenericMap S n a j
          hj).toNormalization
theorem

kummerNormalizationRootScale_over

L126 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerNormalizationRootScale_over
Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
omit [IsOpenImmersion j] in
Lean source · statement
theorem kummerNormalizationRootScale_over (ζ : rootsOfUnity (n : ℕ) K) :
    (kummerNormalizationRootScale M S n a j hj ζ).hom ≫ (M.openKummerGenericMap S n a j
        hj).fromNormalization =
      (M.openKummerGenericMap S n a j hj).fromNormalization
theorem

kummerNormalizationRootScale_one

L133 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerNormalizationRootScale_one
Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
omit [IsOpenImmersion j] in
Lean source · statement
theorem kummerNormalizationRootScale_one :
    (kummerNormalizationRootScale M S n a j hj 1).hom = 𝟙 _
theorem

kummerNormalizationRootScale_mul

L143 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerNormalizationRootScale_mul
Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
omit [IsOpenImmersion j] in
Lean source · statement
theorem kummerNormalizationRootScale_mul (ζ η : rootsOfUnity (n : ℕ) K) :
    (kummerNormalizationRootScale M S n a j hj (ζ * η)).hom =
      (kummerNormalizationRootScale M S n a j hj η).hom ≫
        (kummerNormalizationRootScale M S n a j hj ζ).hom
def

kummerCoverRootScale

L161 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerCoverRootScale
Documentation

The extended automorphism is an automorphism of the actual finite étale Kummer cover, including when the cover is disconnected.

Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
variable [CompactSpace U]
  (hinterior : ∀ (y : U) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
Lean source · statement
def kummerCoverRootScale (hn : IsUnit ((n : ℕ) : K)) (ζ : rootsOfUnity (n : ℕ) K) :
    Aut (M.openKummerCover S n hn a j hj hinterior)
def

kummerCoverRootScaleHom

L168 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerCoverRootScaleHom
Documentation

The actual roots of unity in the base field act by automorphisms of the original normalized Kummer cover.

Source context 7 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
variable [CompactSpace U]
  (hinterior : ∀ (y : U) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
Lean source · full declaration
def kummerCoverRootScaleHom (hn : IsUnit ((n : ℕ) : K)) :
    rootsOfUnity (n : ℕ) K →* Aut (M.openKummerCover S n hn a j hj hinterior) where
  toFun := kummerCoverRootScale M S n a j hj hinterior hn
  map_one' := by
    apply Iso.ext
    apply MorphismProperty.Comma.Hom.ext'
    apply Over.OverMorphism.ext
    exact kummerNormalizationRootScale_one M S n a j hj
  map_mul' ζ η := by
    apply Iso.ext
    apply MorphismProperty.Comma.Hom.ext'
    apply Over.OverMorphism.ext
    exact kummerNormalizationRootScale_mul M S n a j hj ζ η
def

kummerGeometricRootAction

L188 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerGeometricRootAction
Documentation

The root-of-unity action on the actual geometric fiber, obtained from the constructed automorphisms of the original Kummer cover.

Source context 8 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
variable [CompactSpace U]
  (hinterior : ∀ (y : U) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
variable (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ U)
Lean source · statement
def kummerGeometricRootAction :
    MulAction (rootsOfUnity (n : ℕ) K) ((FiniteEtale.fiber ξ).obj (M.openKummerCover S n hn a j
        hj hinterior))
theorem

kummerGeometricRootAction_commutes

L195 ↗
AlgebraicCurve.CurveModel.OpenKummer.kummerGeometricRootAction_commutes
Documentation

Geometric monodromy commutes with root scaling, because every root scaling is a morphism of the original finite étale cover.

Source context 8 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia TopologicalSpace
open JacobianVarieties.Kummer
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 : ℕ+)
  (a : Pic0.openKummerUnits K F S n)
  {U : Scheme.{u}} [IsIntegral U] (j : U ⟶ M.C) [IsOpenImmersion j]
  (hj : DenseRange j)
variable [CompactSpace U]
  (hinterior : ∀ (y : U) (x : closedPoints M.C),
    x.val = j y → M.placeOfPoint x ∉ S)
variable (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ U)
Lean source · full declaration
theorem kummerGeometricRootAction_commutes :
    let := kummerGeometricRootAction M S n a j hj hinterior hn ξ
    SMulCommClass (Aut (FiniteEtale.fiber ξ)) (rootsOfUnity (n : ℕ) K)
      ((FiniteEtale.fiber ξ).obj (M.openKummerCover S n hn a j hj hinterior)) := by
  let := kummerGeometricRootAction M S n a j hj hinterior hn ξ
  constructor
  intro g ζ x
  change g.hom.app (M.openKummerCover S n hn a j hj hinterior)
      ((FiniteEtale.fiber ξ).map (kummerCoverRootScale M S n a j hj hinterior hn ζ).hom x) =
    (FiniteEtale.fiber ξ).map (kummerCoverRootScale M S n a j hj hinterior hn ζ).hom
      (g.hom.app (M.openKummerCover S n hn a j hj hinterior) x)
  exact ConcreteCategory.congr_hom
    (g.hom.naturality (kummerCoverRootScale M S n a j hj hinterior hn ζ).hom) x

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