CyclotomicCrossingCore.lean

1 import Mathlib.FieldTheory.Galois.Basic
2 import Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
3 import Mathlib.GroupTheory.OrderOfElement
4 
5 /-!
6 # The fixed-field step in cyclotomic field crossing
7 
8 The auxiliary field and the automorphism are supplied. No auxiliary-field existence,
9 prime occurrence, or distribution assertion is included in these statements.
10 -/
11 
12 set_option autoImplicit false
13 
14 noncomputable section
15 
16 namespace PaperX.CyclotomicCrossing
17 
18 open IntermediateField
19 
20 section Groups
21 
22 variable {G H : Type*} [Group G] [Group H]
23 
24 /-- Preservation of the order of one element makes the homomorphism faithful
25 on its cyclic subgroup. -/
26 theorem eq_one_of_mem_zpowers_of_map_eq_one (f : G →* H) (g : G)
27     (horder : orderOf (f g) = orderOf g) {x : G}
28     (hx : x ∈ Subgroup.zpowers g) (hfx : f x = 1) : x = 1 := by
29   obtain ⟨n, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
30   apply orderOf_dvd_iff_zpow_eq_one.mp
31   rw [← horder]
32   exact orderOf_dvd_iff_zpow_eq_one.mpr (by simpa only [map_zpow] using hfx)
33 
34 /-- An order-preserving restriction is injective on the cyclic subgroup. -/
35 theorem injective_on_zpowers_of_orderOf_eq (f : G →* H) (g : G)
36     (horder : orderOf (f g) = orderOf g) :
37     Function.Injective (f.comp (Subgroup.zpowers g).subtype) := by
38   apply (MonoidHom.ker_eq_bot_iff _).mp
39   apply le_antisymm
40   · intro x hx
41     apply Subgroup.mem_bot.mpr
42     apply Subtype.ext
43     exact eq_one_of_mem_zpowers_of_map_eq_one f g horder x.property hx
44   · exact bot_le
45 
46 end Groups
47 
48 section Fields
49 
50 variable {K T : Type*} [Field K] [Field T] [Algebra K T]
51 variable [FiniteDimensional K T] [IsGalois K T]
52 
53 /-- If restriction to `A` preserves the order of `rho`, adjoining `A` to the
54 fixed field of `rho` recovers the entire ambient field. -/
55 theorem fixedField_zpowers_sup_eq_top
56     (A : IntermediateField K T) [Normal K A] (rho : T ≃ₐ[K] T)
57     (horder : orderOf (AlgEquiv.restrictNormalHom A rho) = orderOf rho) :
58     fixedField (Subgroup.zpowers rho) ⊔ A = ⊤ := by
59   have hinf : Subgroup.zpowers rho ⊓ A.fixingSubgroup = ⊥ := by
60     apply le_antisymm
61     · intro x hx
62       apply Subgroup.mem_bot.mpr
63       apply eq_one_of_mem_zpowers_of_map_eq_one (AlgEquiv.restrictNormalHom A)
64         rho horder hx.1
65       exact show x ∈ (AlgEquiv.restrictNormalHom A).ker from
66         (A.restrictNormalHom_ker.symm ▸ hx.2)
67     · exact bot_le
68   calc
69     fixedField (Subgroup.zpowers rho) ⊔ A =
70         fixedField (fixingSubgroup (fixedField (Subgroup.zpowers rho) ⊔ A)) :=
71       (IsGalois.fixedField_fixingSubgroup _).symm
72     _ = ⊤ := by
73       rw [fixingSubgroup_sup, fixingSubgroup_fixedField, hinf, fixedField_bot]
74 
75 omit [FiniteDimensional K T] in
76 /-- The extension over the fixed field of one automorphism is Galois. -/
77 theorem isGalois_fixedField_zpowers (rho : T ≃ₐ[K] T) :
78     IsGalois (fixedField (Subgroup.zpowers rho)) T := inferInstance
79 
80 omit [IsGalois K T] in
81 /-- Its actual automorphism group is cyclic. -/
82 theorem isCyclic_fixedField_zpowers (rho : T ≃ₐ[K] T) :
83     IsCyclic (T ≃ₐ[fixedField (Subgroup.zpowers rho)] T) := by
84   exact isCyclic_of_surjective (subgroupEquivAlgEquiv (Subgroup.zpowers rho))
85     (subgroupEquivAlgEquiv (Subgroup.zpowers rho)).surjective
86 
87 omit [IsGalois K T] in
88 /-- The relative degree over the cyclic fixed field is the automorphism's order. -/
89 theorem finrank_fixedField_zpowers (rho : T ≃ₐ[K] T) :
90     Module.finrank (fixedField (Subgroup.zpowers rho)) T = orderOf rho := by
91   rw [finrank_fixedField_eq_card, Nat.card_zpowers]
92 
93 /-- Any intermediate field containing both the fixed field and the auxiliary
94 field is already the entire ambient extension. -/
95 theorem eq_top_of_contains_crossing
96     (A : IntermediateField K T) [Normal K A] (rho : T ≃ₐ[K] T)
97     (horder : orderOf (AlgEquiv.restrictNormalHom A rho) = orderOf rho)
98     (C : IntermediateField K T)
99     (hE : fixedField (Subgroup.zpowers rho) ≤ C) (hA : A ≤ C) : C = ⊤ := by
100   apply top_unique
101   rw [← fixedField_zpowers_sup_eq_top A rho horder]
102   exact sup_le hE hA
103 
104 end Fields
105 
106 end PaperX.CyclotomicCrossing

Back to source controls