This file constructs the actual field ℚ(μ∞) inside SeparableClosure ℚ. It uses mathlib's general IsCyclotomicExtension API, so the infinite field and its finite cyclotomic levels are not replaced by abstract copies of their expected Galois groups.
The finite levels form the divisibility-directed system whose supremum is the whole cyclotomic field. This supplies the field-theoretic source for the rational cyclotomic calculation.
The actual field ℚ(μ∞) in a fixed separable closure of ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheorydef rationalCyclotomicField :
IntermediateField ℚ (SeparableClosure ℚ)The field ℚ(μ∞) is the cyclotomic extension generated by roots of unity of all positive orders.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheoryinstance rationalCyclotomicField_isCyclotomicExtension :
IsCyclotomicExtension (Set.univ : Set ℕ) ℚ
rationalCyclotomicFieldThe actual infinite rational cyclotomic extension is abelian Galois.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheoryinstance rationalCyclotomicField_isAbelianGalois :
IsAbelianGalois ℚ rationalCyclotomicFieldThe n-th finite cyclotomic level inside ℚ(μ∞). Positive naturals are used so that the zero-order degeneracy cannot enter the directed system.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheorydef rationalCyclotomicLevel (n : ℕ+) :
IntermediateField ℚ rationalCyclotomicFieldEach internal finite level is the standard singleton cyclotomic extension.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheoryinstance rationalCyclotomicLevel_isCyclotomicExtension
(n : ℕ+) :
IsCyclotomicExtension {(n : ℕ)} ℚ
(rationalCyclotomicLevel n)Every finite internal cyclotomic level is Galois over ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheoryinstance rationalCyclotomicLevel_isGalois
(n : ℕ+) :
IsGalois ℚ (rationalCyclotomicLevel n)A finite level of ℚ(μ∞) carries mathlib's standard number-field structure coming from its singleton cyclotomic presentation.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheoryinstance rationalCyclotomicLevel_numberField
(n : ℕ+) :
NumberField (rationalCyclotomicLevel n)Every unit modulo m is realized on all m-th roots of unity by an automorphism of the separable closure of ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheorytheorem exists_separableClosureRatAutomorphism_pow_of_unit
(m : ℕ) [NeZero m] (u : (ZMod m)ˣ) :
∃ σ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ,
∀ z : SeparableClosure ℚ, z ^ m = 1 →
σ z = z ^ u.val.valDivisibility of orders gives the canonical inclusion between internal cyclotomic levels.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheorytheorem rationalCyclotomicLevel_mono
{m n : ℕ+}
(h : (m : ℕ) ∣ (n : ℕ)) :
rationalCyclotomicLevel m ≤
rationalCyclotomicLevel nThe internal finite cyclotomic levels exhaust ℚ(μ∞).
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheorytheorem iSup_rationalCyclotomicLevel :
(⨆ n : ℕ+, rationalCyclotomicLevel n) = ⊤