NYLL
Module

CoprimePowerDescent.lean

Nyll.AnabelianGeometry.KummerTheory.CoprimePowerDescent
2 declarations indexed from sourceView source ↗

Module documentation

Exact power descent under coprimality

Norms descend powers across extensions of coprime degree. A central cyclotomic automorphism gives a second exact descent criterion when its displacement is coprime to the exponent.

Imports3
Imported by1

Declarations

theorem

exists_pow_eq_of_coprime_finrank

L25 ↗
AnabelianGeometry.KummerTheory.exists_pow_eq_of_coprime_finrank
Documentation

A power relation over a finite extension of degree coprime to its exponent already has a witness over the original field.

Source context 2 commands

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

namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_pow_eq_of_coprime_finrank [FiniteDimensional K L]
    (n : ℕ) (a : K) (r : L) (hr : r ^ n = algebraMap K L a)
    (hcop : (Module.finrank K L).Coprime n) :
    ∃ c : K, c ^ n = a
theorem

exists_pow_eq_of_coprime_central_cyclotomic

L36 ↗
AnabelianGeometry.KummerTheory.exists_pow_eq_of_coprime_central_cyclotomic
Documentation

A cyclotomic displacement prime to the exponent removes the entire power-class kernel, without a residual roots-of-unity factor.

Source context 2 commands

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

namespace AnabelianGeometry.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_pow_eq_of_coprime_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))
    (hcop : m.Coprime n) :
    ∃ c : K, c ^ n = a

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