Intersecting the composita of the full root fields of c * x and c * y over all nonzero base-field twists c recovers the full root field of y / x. Roots of unity are retained throughout, so the base need not contain them.
The intermediate field generated by the roots of unity of a fixed order.
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 rootsOfUnityField (n : ℕ) : IntermediateField K LSplit the root field into its roots-of-unity and single-radical parts.
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 rootField_eq_sup (n : ℕ) (x : K) (a : L)
(ha : a ≠ 0) (hap : a ^ n = algebraMap K L x) :
rootField (L := L) n x = rootsOfUnityField n ⊔ IntermediateField.adjoin K {a}The compositum of two full root fields is generated by both radicals and the common roots of unity.
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 rootFields_sup_eq (n : ℕ) (x y : K) (a b : L)
(ha : a ≠ 0) (hb : b ≠ 0)
(hap : a ^ n = algebraMap K L x) (hbp : b ^ n = algebraMap K L y) :
rootField (L := L) n x ⊔ rootField (L := L) n y =
rootsOfUnityField n ⊔ IntermediateField.adjoin K ({a, b} : Set L)Keeping any fixed intermediate field in every simultaneous twist preserves the attained minimum at the inverse of the first coordinate.
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_sup_twistField_eq (E : IntermediateField K L) (a b : L) (n : ℕ)
(ha : a ≠ 0) (han : a ^ n ∈ (⊥ : IntermediateField K L)) :
(⨅ r : {r : L // r ≠ 0 ∧ r ^ n ∈ (⊥ : IntermediateField K L)},
E ⊔ twistField K a b r.1) = E ⊔ IntermediateField.adjoin K ({b / a} : Set L)The field of the ratio is the intersection of all simultaneously twisted full root fields, indexed by actual nonzero base-field scalars.
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_twisted_rootFields_eq [IsAlgClosed L]
(n : ℕ) (hn : 0 < n) (x y : Kˣ) :
(⨅ c : Kˣ, rootField (L := L) n ((c * x : Kˣ) : K) ⊔
rootField (L := L) n ((c * y : Kˣ) : K)) =
rootField (L := L) n ((y / x : Kˣ) : K)