Module

CyclotomicPowerDescent.lean

Nyll.AnabelianGeometry.KummerTheory.CyclotomicPowerDescent

4 declarations indexed from sourceView source ↗

Module documentation

Descent of powers from a cyclotomic action

A central Galois automorphism acting on n-th roots of unity by the (m + 1)-st power forces an n-th radical from the base to descend after raising its power class to m. The proof is the explicit radical-cocycle calculation and the Galois fixed-field theorem. It does not assume a uniform bound on m or a number-field cyclotomic image theorem.

Imports3

Nyll.AnabelianGeometry.KummerTheory.RootCocycle
Mathlib.FieldTheory.Galois.Infinite
Mathlib.Tactic.Ring

Imported by4

theorem

rootRatio_central_cyclotomic

L29 ↗

AnabelianGeometry.KummerTheory.rootRatio_central_cyclotomic

Documentation

A central automorphism with specified cyclotomic action controls the Galois change of its own radical ratio.

Source context 3 commands

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

open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootRatio_central_cyclotomic
    {r : L} (hr : r ≠ 0) {n m : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a) (σ τ : L ≃ₐ[K] L)
    (hcomm : σ * τ = τ * σ)
    (hσ : ∀ ξ : L, ξ ^ n = 1 → σ ξ = ξ ^ (m + 1)) :
    τ (rootRatio r σ) = rootRatio r τ ^ m * rootRatio r σ

theorem

radical_power_div_ratio_fixed

L47 ↗

AnabelianGeometry.KummerTheory.radical_power_div_ratio_fixed

Documentation

An explicit root-of-unity correction makes a power of the radical fixed by every Galois automorphism.

Source context 3 commands

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

open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem radical_power_div_ratio_fixed
    {r : L} (hr : r ≠ 0) {n m : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a) (σ : L ≃ₐ[K] L)
    (hcentral : ∀ τ : L ≃ₐ[K] L, σ * τ = τ * σ)
    (hσ : ∀ ξ : L, ξ ^ n = 1 → σ ξ = ξ ^ (m + 1))
    (τ : L ≃ₐ[K] L) :
    τ (r ^ m / rootRatio r σ) = r ^ m / rootRatio r σ

theorem

exists_power_eq_of_central_cyclotomic

L61 ↗

AnabelianGeometry.KummerTheory.exists_power_eq_of_central_cyclotomic

Documentation

The cyclotomic displacement m annihilates the kernel of the n-th power class map for radicals contained in this Galois extension.

Source context 3 commands

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

open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem exists_power_eq_of_central_cyclotomic [IsGalois K L]
    {r : L} (hr : r ≠ 0) {n m : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a) (σ : L ≃ₐ[K] L)
    (hcentral : ∀ τ : L ≃ₐ[K] L, σ * τ = τ * σ)
    (hσ : ∀ ξ : L, ξ ^ n = 1 → σ ξ = ξ ^ (m + 1)) :
    ∃ c : K, c ^ n = a ^ m

theorem

exists_unit_power_eq_of_abelian_cyclotomic

L77 ↗

AnabelianGeometry.KummerTheory.exists_unit_power_eq_of_abelian_cyclotomic

Documentation

In an abelian Galois extension, the same calculation gives an actual unit of the original field witnessing the annihilated power class.

Source context 3 commands

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

open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem exists_unit_power_eq_of_abelian_cyclotomic [IsGalois K L]
    [IsMulCommutative (L ≃ₐ[K] L)]
    (n : ℕ+) (m : ℕ) (a : Kˣ) (r : L) (hr : r ≠ 0)
    (ha : r ^ (n : ℕ) = algebraMap K L (a : K)) (σ : L ≃ₐ[K] L)
    (hσ : ∀ ξ : L, ξ ^ (n : ℕ) = 1 → σ ξ = ξ ^ (m + 1)) :
    ∃ c : Kˣ, c ^ (n : ℕ) = a ^ m

Module documentation

Descent of powers from a cyclotomic action

Declarations

rootRatio_central_cyclotomic

radical_power_div_ratio_fixed

exists_power_eq_of_central_cyclotomic

exists_unit_power_eq_of_abelian_cyclotomic