After choosing one nonzero root, adjoining all roots of the equation is exactly adjoining that root and all roots of unity of the same order. The equality is proved inside the given ambient field without assuming that roots of unity already lie in the base.
The field generated by all roots in the ambient field of one Kummer equation.
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 rootField (n : ℕ) (a : K) : IntermediateField K LOne nonzero root and the roots of unity generate exactly the full root 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 rootField_eq_adjoin_root_rootsOfUnity (n : ℕ) (a : K) (r : L)
(hr : r ≠ 0) (hpow : r ^ n = algebraMap K L a) :
rootField (L := L) n a =
IntermediateField.adjoin K (insert r {ξ : L | ξ ^ n = 1})Extending the coefficient field takes the compositum with the original root field. This comparison uses all roots and is independent of choices.
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_restrictScalars (C : IntermediateField K L) (n : ℕ) (a : K) :
(rootField (L := L) n (algebraMap K C a)).restrictScalars K =
C ⊔ rootField (L := L) n aEquality of full root fields persists after any intermediate-field extension of the base.
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_baseChange_eq (C : IntermediateField K L) (n : ℕ) (a b : K)
(h : rootField (L := L) n a = rootField (L := L) n b) :
rootField (L := L) n (algebraMap K C a) =
rootField (L := L) n (algebraMap K C b)