If a ^ n belongs to the base field, the intersection of the fields K(r * a, r * b), over nonzero r whose n-th power belongs to K, is exactly K(b / a). The proof constructs the normalizing twist r = a⁻¹. This is the field-theoretic calculation used to recover cross ratios from two fibres of a cyclic cover. It does not assert that these fields have already been reconstructed from an étale fundamental group.
The argument works over any field, hence in particular over number fields and their cyclotomic extensions.
The field generated by two elements after a common multiplicative twist.
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]def twistField (a b r : L) : IntermediateField K LThe ratio of two nonzero-twisted elements lies in their common field.
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]theorem ratio_mem_twistField (a b r : L) (hr : r ≠ 0) :
b / a ∈ twistField K a b rThe field of the ratio is contained in every nonzero simultaneous twist.
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]theorem adjoin_ratio_le_twistField (a b r : L) (hr : r ≠ 0) :
IntermediateField.adjoin K ({b / a} : Set L) ≤ twistField K a b rThe inverse of the first coordinate gives a twist attaining the lower bound.
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]theorem twistField_inv_eq_adjoin_ratio (a b : L) (ha : a ≠ 0) :
twistField K a b a⁻¹ = IntermediateField.adjoin K ({b / a} : Set L)The intersection over all twists with n-th power in the base field recovers the field generated by the radical ratio.
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]theorem iInf_twistField_eq_adjoin_ratio (a b : L) (n : ℕ)
(ha : a ≠ 0) (han : a ^ n ∈ (⊥ : IntermediateField K L)) :
(⨅ r : {r : L // r ≠ 0 ∧ r ^ n ∈ (⊥ : IntermediateField K L)},
twistField K a b r.1) = IntermediateField.adjoin K ({b / a} : Set L)The reconstructed ratio is an n-th root of the ratio of the original values.
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]theorem ratio_pow_eq {a b : L} {x y : K} {n : ℕ}
(ha : a ^ n = algebraMap K L x) (hb : b ^ n = algebraMap K L y) :
(b / a) ^ n = algebraMap K L (y / x)When the base field contains the n-th roots of unity, a nonzero radical generates a field independent of the chosen root.
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]theorem adjoin_eq_of_pow_eq {a b : L} {n : ℕ}
(ha : a ≠ 0) (hb : b ≠ 0) (hab : a ^ n = b ^ n)
(hroots : ∀ ζ : L, ζ ^ n = 1 → ζ ∈ (⊥ : IntermediateField K L)) :
IntermediateField.adjoin K ({a} : Set L) =
IntermediateField.adjoin K ({b} : Set L)