Module

AbsoluteRootPowerAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteRootPowerAction

1 declaration indexed from sourceView source ↗

Module documentation

Power actions on roots in the algebraic closure

When a base automorphism acts by a specified power on the roots of unity, its chosen lift acts by that power on the same roots in the algebraic closure. The roots are descended using an actual primitive root in the base field.

Imports2

Imported by3

theorem

absoluteGaloisLift_nthRoot_eq_pow

L26 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteGaloisLift_nthRoot_eq_pow

Documentation

The chosen lift of a base automorphism has the same power action on the roots in the algebraic closure as on the roots in the base field.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]

Lean source · statement

theorem absoluteGaloisLift_nthRoot_eq_pow
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (a : ℕ)
    (hτ : ∀ ζ : K, ζ ^ (n : ℕ) = 1 → τ ζ = ζ ^ a)
    (z : nthRootsSubgroup (AlgebraicClosure K) (n : ℕ)) :
    Units.map (IsAlgClosure.equivOfEquiv (AlgebraicClosure K)
      (AlgebraicClosure K) τ).toMonoidHom (z : (AlgebraicClosure K)ˣ) =
        (z : (AlgebraicClosure K)ˣ) ^ a

Module documentation

Power actions on roots in the algebraic closure

Declarations

absoluteGaloisLift_nthRoot_eq_pow