AuxiliaryCyclotomicDegree.lean

1 import Mathlib.FieldTheory.Galois.Abelian
2 import Mathlib.GroupTheory.SpecificGroups.Cyclic
3 import Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
4 
5 /-! Construct a cyclic intermediate field of any degree dividing a finite
6 cyclic extension. The construction uses the fixed field of nth powers. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.AuxiliaryCyclotomicDegree
10 open IntermediateField
11 
12 section Cyclic
13 variable (K C : Type*) [Field K] [Field C] [Algebra K C]
14   [FiniteDimensional K C] [IsGalois K C] [IsCyclic Gal(C/K)]
15 
16 /-- Every divisor of the degree of a finite cyclic extension occurs as the
17 degree of an actual cyclic intermediate field. -/
18 theorem exists_cyclic_subfield (n : ℕ) (hn : n ∣ Module.finrank K C) :
19     ∃ A : IntermediateField K C, Module.finrank K A = n ∧
20       IsGalois K A ∧ IsCyclic Gal(A/K) := by
21   let : CommGroup Gal(C/K) := IsCyclic.commGroup
22   let H : Subgroup Gal(C/K) := (powMonoidHom n : Gal(C/K) →* Gal(C/K)).range
23   let A : IntermediateField K C := fixedField H
24   have hA : IsGalois K A := inferInstance
25   have hcyc : IsCyclic Gal(A/K) :=
26     isCyclic_of_surjective (AlgEquiv.restrictNormalHom A)
27       (AlgEquiv.restrictNormalHom_surjective C)
28   refine ⟨A, ?_, hA, hcyc⟩
29   rw [IntermediateField.finrank_eq_fixingSubgroup_index,
30     IntermediateField.fixingSubgroup_fixedField,
31     IsCyclic.index_powMonoidHom_range, IsGalois.card_aut_eq_finrank,
32     Nat.gcd_eq_right hn]
33 
34 end Cyclic
35 
36 section PrimeCyclotomic
37 variable (q : ℕ) [Fact q.Prime] (C : Type*) [Field C] [NumberField C]
38   [IsCyclotomicExtension {q} ℚ C]
39 
40 include q in
41 /-- The prime-conductor cyclotomic Galois group is cyclic. -/
42 theorem prime_cyclotomic_galois_isCyclic : IsCyclic Gal(C/ℚ) := by
43   have : NeZero q := ⟨(Fact.out : q.Prime).ne_zero⟩
44   exact isCyclic_of_injective (IsCyclotomicExtension.Rat.galEquivZMod q C).toMonoidHom
45     (IsCyclotomicExtension.Rat.galEquivZMod q C).injective
46 
47 /-- Prime conductors yield an actual cyclic subfield of each degree dividing q-1. -/
48 theorem exists_prime_cyclotomic_subfield (n : ℕ) (hn : n ∣ q - 1) :
49     ∃ A : IntermediateField ℚ C, Module.finrank ℚ A = n ∧
50       IsGalois ℚ A ∧ IsCyclic Gal(A/ℚ) := by
51   have : NeZero q := ⟨(Fact.out : q.Prime).ne_zero⟩
52   have : IsCyclic Gal(C/ℚ) := prime_cyclotomic_galois_isCyclic q C
53   have : IsGalois ℚ C := IsCyclotomicExtension.isGalois {q} ℚ C
54   apply exists_cyclic_subfield ℚ C n
55   simpa only [IsCyclotomicExtension.Rat.finrank q, Nat.totient_prime (Fact.out : q.Prime)]
56     using hn
57 
58 end PrimeCyclotomic
59 end PaperX.AuxiliaryCyclotomicDegree

Back to source controls