Module

RootChoice.lean

Nyll.AnabelianGeometry.KummerTheory.RootChoice

2 declarations indexed from sourceView source ↗

Module documentation

Independence of radical cocycles from the choice of root

Over a base containing the relevant roots of unity, replacing a radical by another root of the same power equation leaves its Galois cocycle unchanged.

Imports1

Nyll.AnabelianGeometry.KummerTheory.RootCocycle

Imported by1

Nyll.AnabelianGeometry.KummerTheory.All

theorem

rootRatio_eq_of_pow_eq

L24 ↗

AnabelianGeometry.KummerTheory.rootRatio_eq_of_pow_eq

Documentation

Roots of the same power equation have identical radical cocycles when all roots of unity of that order lie in the base field.

Source context 3 commands

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

namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem rootRatio_eq_of_pow_eq {r s : L} (hr : r ≠ 0) (hs : s ≠ 0)
    {n : ℕ} (hpow : s ^ n = r ^ n)
    (hroots : ∀ ξ : L, ξ ^ n = 1 → ∃ b : K, algebraMap K L b = ξ)
    (σ : L ≃ₐ[K] L) : rootRatio r σ = rootRatio s σ

theorem

rootRatio_pow

L40 ↗

AnabelianGeometry.KummerTheory.rootRatio_pow