ModuleRationalCyclotomicTorsionField.lean
Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.RationalCyclotomicTorsionField
6 declarations indexed from sourceView source ↗ Module documentation
The torsion fixed field in the rational cyclotomic extension
The rational cyclotomic construction takes the fixed field of the closure of the torsion subgroup in Gal(ℚ(μ∞)/ℚ). This file defines that actual closed subgroup and fixed field. No copy of the Galois group is replaced definitionally by ℤ̂ˣ; the comparison with profinite units is a later theorem.
Declarations
KummerTheory.rationalCyclotomicTorsionClosure
DocumentationThe closure of the torsion subgroup in the actual Krull-topological Galois group of ℚ(μ∞)/ℚ.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
KummerTheory.rationalCyclotomicTorsionFixedField
DocumentationThe actual subfield of ℚ(μ∞) fixed by the closure of all finite-order cyclotomic automorphisms.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
KummerTheory.rationalCyclotomicTorsionFixedField_isIntegral
DocumentationThe torsion fixed field is integral over ℚ, since it is an intermediate field of the rational cyclotomic extension.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
KummerTheory.rationalCyclotomicTorsionFixedField_normal
DocumentationThe torsion fixed field is normal over ℚ: its defining closed subgroup is normal in the abelian cyclotomic Galois group.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
KummerTheory.rationalCyclotomicTorsionFixedField_isGalois
DocumentationThe torsion-fixed cyclotomic field is Galois over ℚ.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
KummerTheory.rationalCyclotomicTorsionFixedField_isAbelianGalois
DocumentationThe torsion-fixed subextension of the abelian rational cyclotomic extension is itself abelian Galois.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative