NYLL
Module

CurveCoverAction.lean

Nyll.JacobianVarieties.Kummer.CurveCoverAction
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 by7

Declarations

def

scalarRoot

L34 ↗
AlgebraicCurve.CurveModel.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
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
def scalarRoot (ζ : rootsOfUnity (n : ℕ) K) :
    rootsOfUnity (n : ℕ) M.C.functionField
def

kummerGenericRootScale

L40 ↗
AlgebraicCurve.CurveModel.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
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
def kummerGenericRootScale (ζ : rootsOfUnity (n : ℕ) K) :
    Spec (.of (AdjoinRoot (Polynomial.X ^ (n : ℕ) -
        Polynomial.C (M.ffEquiv (u.val : F)) : Polynomial M.C.functionField))) ≅
      Spec (.of (AdjoinRoot (Polynomial.X ^ (n : ℕ) -
        Polynomial.C (M.ffEquiv (u.val : F)) : Polynomial M.C.functionField)))
theorem

kummerGenericRootScale_hom_over

L49 ↗
AlgebraicCurve.CurveModel.kummerGenericRootScale_hom_over
Documentation

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

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
theorem kummerGenericRootScale_hom_over (ζ : rootsOfUnity (n : ℕ) K) :
    (M.kummerGenericRootScale n u ζ).hom ≫ M.kummerGenericMap n u =
      M.kummerGenericMap n u
theorem

kummerGenericRootScale_one

L63 ↗
AlgebraicCurve.CurveModel.kummerGenericRootScale_one
Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
theorem kummerGenericRootScale_one :
    (M.kummerGenericRootScale n u 1).hom = 𝟙 _
theorem

kummerGenericRootScale_mul

L71 ↗
AlgebraicCurve.CurveModel.kummerGenericRootScale_mul
Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
theorem kummerGenericRootScale_mul (ζ η : rootsOfUnity (n : ℕ) K) :
    (M.kummerGenericRootScale n u (ζ * η)).hom =
      (M.kummerGenericRootScale n u η).hom ≫ (M.kummerGenericRootScale n u ζ).hom
def

kummerNormalizationRootScale

L92 ↗
AlgebraicCurve.CurveModel.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
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
def kummerNormalizationRootScale (ζ : rootsOfUnity (n : ℕ) K) :
    (M.kummerGenericMap n u).normalization ≅ (M.kummerGenericMap n u).normalization
theorem

toNormalization_kummerNormalizationRootScale

L99 ↗
AlgebraicCurve.CurveModel.toNormalization_kummerNormalizationRootScale
Documentation

The extension to normalization retains the original generic root scaling.

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
theorem toNormalization_kummerNormalizationRootScale (ζ : rootsOfUnity (n : ℕ) K) :
    (M.kummerGenericMap n u).toNormalization ≫ (M.kummerNormalizationRootScale n u ζ).hom =
      (M.kummerGenericRootScale n u ζ).hom ≫ (M.kummerGenericMap n u).toNormalization
theorem

kummerNormalizationRootScale_over

L104 ↗
AlgebraicCurve.CurveModel.kummerNormalizationRootScale_over
Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
theorem kummerNormalizationRootScale_over (ζ : rootsOfUnity (n : ℕ) K) :
    (M.kummerNormalizationRootScale n u ζ).hom ≫ (M.kummerGenericMap n u).fromNormalization =
      (M.kummerGenericMap n u).fromNormalization
theorem

kummerNormalizationRootScale_one

L109 ↗
AlgebraicCurve.CurveModel.kummerNormalizationRootScale_one
Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
theorem kummerNormalizationRootScale_one :
    (M.kummerNormalizationRootScale n u 1).hom = 𝟙 _
theorem

kummerNormalizationRootScale_mul

L118 ↗
AlgebraicCurve.CurveModel.kummerNormalizationRootScale_mul
Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
theorem kummerNormalizationRootScale_mul (ζ η : rootsOfUnity (n : ℕ) K) :
    (M.kummerNormalizationRootScale n u (ζ * η)).hom =
      (M.kummerNormalizationRootScale n u η).hom ≫
        (M.kummerNormalizationRootScale n u ζ).hom
def

kummerCoverRootScale

L132 ↗
AlgebraicCurve.CurveModel.kummerCoverRootScale
Documentation

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

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · statement
def kummerCoverRootScale (hn : IsUnit ((n : ℕ) : K)) (ζ : rootsOfUnity (n : ℕ) K) :
    Aut (M.kummerCover n hn u)
def

kummerCoverRootScaleHom

L139 ↗
AlgebraicCurve.CurveModel.kummerCoverRootScaleHom
Documentation

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

Source context 6 commands

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

noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Inertia
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
Lean source · full declaration
def kummerCoverRootScaleHom (hn : IsUnit ((n : ℕ) : K)) :
    rootsOfUnity (n : ℕ) K →* Aut (M.kummerCover n hn u) where
  toFun := M.kummerCoverRootScale n u hn
  map_one' := by
    apply Iso.ext
    apply MorphismProperty.Comma.Hom.ext'
    apply Over.OverMorphism.ext
    exact kummerNormalizationRootScale_one M n u
  map_mul' ζ η := by
    apply Iso.ext
    apply MorphismProperty.Comma.Hom.ext'
    apply Over.OverMorphism.ext
    exact kummerNormalizationRootScale_mul M n u ζ η
def

kummerGeometricRootAction

L159 ↗
AlgebraicCurve.CurveModel.kummerGeometricRootAction
Documentation

The root-of-unity action on the actual geometric fiber, obtained from the constructed automorphisms of the original 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
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
variable (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · statement
def kummerGeometricRootAction :
    MulAction (rootsOfUnity (n : ℕ) K) ((FiniteEtale.fiber ξ).obj (M.kummerCover n hn u))
theorem

kummerGeometricRootAction_commutes

L165 ↗
AlgebraicCurve.CurveModel.kummerGeometricRootAction_commutes
Documentation

Geometric monodromy commutes with root scaling, because every root scaling is a morphism of the original finite étale 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
open JacobianVarieties.Kummer
namespace AlgebraicCurve.CurveModel
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)
variable (hn : IsUnit ((n : ℕ) : K))
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ M.C)
Lean source · full declaration
theorem kummerGeometricRootAction_commutes :
    let := M.kummerGeometricRootAction n u hn ξ
    SMulCommClass (Aut (FiniteEtale.fiber ξ)) (rootsOfUnity (n : ℕ) K)
      ((FiniteEtale.fiber ξ).obj (M.kummerCover n hn u)) := by
  let := M.kummerGeometricRootAction n u hn ξ
  constructor
  intro g ζ x
  change g.hom.app (M.kummerCover n hn u)
      ((FiniteEtale.fiber ξ).map (M.kummerCoverRootScale n u hn ζ).hom x) =
    (FiniteEtale.fiber ξ).map (M.kummerCoverRootScale n u hn ζ).hom
      (g.hom.app (M.kummerCover n hn u) x)
  exact ConcreteCategory.congr_hom
    (g.hom.naturality (M.kummerCoverRootScale n u 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.