Module

RootScaling.lean

Nyll.EtaleFundamentalGroups.Kummer.AdjoinRoot.RootScaling

6 declarations indexed from sourceView source ↗

Module documentation

Actual root-of-unity automorphisms of the Kummer algebra

Multiplication of the adjoined root by a root of unity gives an actual algebra automorphism. No irreducibility or domain hypothesis on the Kummer algebra is needed, so the construction includes disconnected Kummer covers.

Imports3

Mathlib.RingTheory.AdjoinRoot
Mathlib.RingTheory.RootsOfUnity.Basic
Mathlib.Algebra.Algebra.Equiv

Imported by5

theorem

kummerRoot_pow

L28 ↗

JacobianVarieties.Kummer.kummerRoot_pow

Source context 4 commands

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

noncomputable section
universe u
namespace JacobianVarieties.Kummer
variable {R : Type u} [CommRing R] (n : ℕ) (a : R)

Lean source · statement

theorem kummerRoot_pow :
    AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a : Polynomial R) ^ n =
      algebraMap R (AdjoinRoot (Polynomial.X ^ n - Polynomial.C a : Polynomial R)) a

def

kummerRootScale

L37 ↗

JacobianVarieties.Kummer.kummerRootScale

Documentation

Scale the adjoined Kummer root by the specified root of unity.

Source context 4 commands

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

noncomputable section
universe u
namespace JacobianVarieties.Kummer
variable {R : Type u} [CommRing R] (n : ℕ) (a : R)

Lean source · statement

def kummerRootScale (ζ : rootsOfUnity n R) :
    AdjoinRoot (Polynomial.X ^ n - Polynomial.C a : Polynomial R) →ₐ[R]
      AdjoinRoot (Polynomial.X ^ n - Polynomial.C a : Polynomial R)

theorem

kummerRootScale_root

L48 ↗

JacobianVarieties.Kummer.kummerRootScale_root

Documentation

The constructed algebra endomorphism sends the actual root to its scale.

Source context 4 commands

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

noncomputable section
universe u
namespace JacobianVarieties.Kummer
variable {R : Type u} [CommRing R] (n : ℕ) (a : R)

Lean source · statement

theorem kummerRootScale_root (ζ : rootsOfUnity n R) :
    kummerRootScale n a ζ (AdjoinRoot.root _) =
      algebraMap R _ (ζ.val : R) * AdjoinRoot.root _

theorem

kummerRootScale_one

L54 ↗

JacobianVarieties.Kummer.kummerRootScale_one

Documentation

Scaling by one is the identity on the original Kummer algebra.

Source context 4 commands

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

noncomputable section
universe u
namespace JacobianVarieties.Kummer
variable {R : Type u} [CommRing R] (n : ℕ) (a : R)

Lean source · statement

theorem kummerRootScale_one : kummerRootScale n a 1 = AlgHom.id R _

theorem

kummerRootScale_mul

L61 ↗

JacobianVarieties.Kummer.kummerRootScale_mul

Documentation

Composition of the actual root scalings is multiplication of their coefficients.

Source context 4 commands

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

noncomputable section
universe u
namespace JacobianVarieties.Kummer
variable {R : Type u} [CommRing R] (n : ℕ) (a : R)

Lean source · statement

theorem kummerRootScale_mul (ζ η : rootsOfUnity n R) :
    kummerRootScale n a (ζ * η) = (kummerRootScale n a ζ).comp (kummerRootScale n a η)

def

kummerRootScaleEquiv

L71 ↗

JacobianVarieties.Kummer.kummerRootScaleEquiv

Documentation

Every root scaling is an algebra automorphism, with inverse scaling by the inverse root.

Source context 4 commands

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

noncomputable section
universe u
namespace JacobianVarieties.Kummer
variable {R : Type u} [CommRing R] (n : ℕ) (a : R)

Lean source · statement

def kummerRootScaleEquiv (ζ : rootsOfUnity n R) :
    AdjoinRoot (Polynomial.X ^ n - Polynomial.C a : Polynomial R) ≃ₐ[R]
      AdjoinRoot (Polynomial.X ^ n - Polynomial.C a : Polynomial R)

Module documentation

Actual root-of-unity automorphisms of the Kummer algebra

Declarations

kummerRoot_pow

kummerRootScale

kummerRootScale_root

kummerRootScale_one

kummerRootScale_mul

kummerRootScaleEquiv