CyclotomicCrossingPair.lean

1 import PaperX.CyclotomicCrossingCore
2 import Mathlib.FieldTheory.LinearDisjoint
3 
4 /-!
5 # Constructing the crossing automorphism from a disjoint compositum
6 
7 Both Galois intermediate fields are supplied, together with their disjointness
8 and compositum equality. The automorphism with prescribed restrictions is
9 constructed from the actual restriction homomorphism.
10 -/
11 
12 set_option autoImplicit false
13 
14 noncomputable section
15 
16 namespace PaperX.CyclotomicCrossing
17 
18 open IntermediateField
19 
20 variable {K T : Type*} [Field K] [Field T] [Algebra K T]
21 
22 /-- The pair of actual restrictions to two normal intermediate fields. -/
23 def restrictionPair (L A : IntermediateField K T) [Normal K L] [Normal K A] :
24     (T ≃ₐ[K] T) →* ((L ≃ₐ[K] L) × (A ≃ₐ[K] A)) :=
25   (AlgEquiv.restrictNormalHom L).prod (AlgEquiv.restrictNormalHom A)
26 
27 /-- Restrictions determine an automorphism when the two fields generate `T`. -/
28 theorem restrictionPair_injective (L A : IntermediateField K T)
29     [Normal K L] [Normal K A] (hsup : L ⊔ A = ⊤) :
30     Function.Injective (restrictionPair L A) := by
31   apply (MonoidHom.ker_eq_bot_iff _).mp
32   rw [restrictionPair, MonoidHom.ker_prod, L.restrictNormalHom_ker,
33     A.restrictNormalHom_ker, ← fixingSubgroup_sup, hsup, fixingSubgroup_top]
34 
35 variable [FiniteDimensional K T] [IsGalois K T]
36 
37 /-- Linear disjointness upgrades the injective restriction pair to a bijection. -/
38 theorem restrictionPair_bijective (L A : IntermediateField K T)
39     [IsGalois K L] [IsGalois K A]
40     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤) :
41     Function.Bijective (restrictionPair L A) := by
42   apply (Nat.bijective_iff_injective_and_card _).mpr
43   refine ⟨restrictionPair_injective L A hsup, ?_⟩
44   rw [Nat.card_prod, IsGalois.card_aut_eq_finrank, IsGalois.card_aut_eq_finrank,
45     IsGalois.card_aut_eq_finrank]
46   have hdim := hdisj.finrank_sup
47   rw [hsup, finrank_top'] at hdim
48   exact hdim
49 
50 /-- The actual Galois group of a disjoint compositum is the product of the
51 two factor Galois groups, via restriction. -/
52 def restrictionPairEquiv (L A : IntermediateField K T)
53     [IsGalois K L] [IsGalois K A]
54     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤) :
55     (T ≃ₐ[K] T) ≃* ((L ≃ₐ[K] L) × (A ≃ₐ[K] A)) :=
56   MulEquiv.ofBijective (restrictionPair L A) (restrictionPair_bijective L A hdisj hsup)
57 
58 /-- The chosen automorphism on the compositum with the prescribed two restrictions. -/
59 def crossingAutomorphism (L A : IntermediateField K T)
60     [IsGalois K L] [IsGalois K A]
61     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤)
62     (sigma : L ≃ₐ[K] L) (eta : A ≃ₐ[K] A) : T ≃ₐ[K] T :=
63   (restrictionPairEquiv L A hdisj hsup).symm (sigma, eta)
64 
65 /-- The constructed automorphism restricts to the prescribed pair. -/
66 theorem restrictionPair_crossingAutomorphism (L A : IntermediateField K T)
67     [IsGalois K L] [IsGalois K A]
68     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤)
69     (sigma : L ≃ₐ[K] L) (eta : A ≃ₐ[K] A) :
70     restrictionPair L A (crossingAutomorphism L A hdisj hsup sigma eta) = (sigma, eta) :=
71   (restrictionPairEquiv L A hdisj hsup).apply_symm_apply _
72 
73 /-- If the order on the first factor divides that on the auxiliary factor,
74 restriction to the auxiliary field preserves the crossing automorphism's order. -/
75 theorem crossingAutomorphism_order (L A : IntermediateField K T)
76     [IsGalois K L] [IsGalois K A]
77     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤)
78     (sigma : L ≃ₐ[K] L) (eta : A ≃ₐ[K] A)
79     (horder : orderOf sigma ∣ orderOf eta) :
80     orderOf (crossingAutomorphism L A hdisj hsup sigma eta) = orderOf eta := by
81   rw [← orderOf_injective (restrictionPair L A) (restrictionPair_injective L A hsup),
82     restrictionPair_crossingAutomorphism, Prod.orderOf_mk, Nat.lcm_eq_right horder]
83 
84 /-- The field-crossing identity `T = E A`, for the actual fixed field of the
85 constructed automorphism. -/
86 theorem crossing_fixedField_sup_eq_top (L A : IntermediateField K T)
87     [IsGalois K L] [IsGalois K A]
88     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤)
89     (sigma : L ≃ₐ[K] L) (eta : A ≃ₐ[K] A)
90     (horder : orderOf sigma ∣ orderOf eta) :
91     fixedField (Subgroup.zpowers (crossingAutomorphism L A hdisj hsup sigma eta)) ⊔ A = ⊤ := by
92   apply fixedField_zpowers_sup_eq_top
93   rw [crossingAutomorphism_order L A hdisj hsup sigma eta horder]
94   exact congrArg (fun p => orderOf p.2)
95     (restrictionPair_crossingAutomorphism L A hdisj hsup sigma eta)
96 
97 /-- A supplied cyclic auxiliary field of the matching degree produces the
98 crossing automorphism, fixed-field identity, cyclic extension, and exact
99 relative degree without supplying a chosen auxiliary generator. -/
100 theorem exists_crossing_of_cyclic_auxiliary (L A : IntermediateField K T)
101     [IsGalois K L] [IsGalois K A] [IsCyclic (A ≃ₐ[K] A)]
102     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤)
103     (sigma : L ≃ₐ[K] L) (hdegree : Module.finrank K A = orderOf sigma) :
104     ∃ rho : T ≃ₐ[K] T,
105       AlgEquiv.restrictNormalHom L rho = sigma ∧
106       fixedField (Subgroup.zpowers rho) ⊔ A = ⊤ ∧
107       IsCyclic (T ≃ₐ[fixedField (Subgroup.zpowers rho)] T) ∧
108       Module.finrank (fixedField (Subgroup.zpowers rho)) T = orderOf sigma := by
109   obtain ⟨eta, heta⟩ := isCyclic_iff_exists_zpowers_eq_top.mp
110     (inferInstance : IsCyclic (A ≃ₐ[K] A))
111   have heta_order : orderOf eta = orderOf sigma := by
112     rw [orderOf_eq_card_of_forall_mem_zpowers (fun x => by rw [heta]; exact Subgroup.mem_top x),
113       IsGalois.card_aut_eq_finrank, hdegree]
114   have hdiv : orderOf sigma ∣ orderOf eta := by rw [heta_order]
115   let rho := crossingAutomorphism L A hdisj hsup sigma eta
116   refine ⟨rho, ?_, crossing_fixedField_sup_eq_top L A hdisj hsup sigma eta hdiv,
117     isCyclic_fixedField_zpowers rho, ?_⟩
118   · exact congrArg Prod.fst (restrictionPair_crossingAutomorphism L A hdisj hsup sigma eta)
119   · rw [finrank_fixedField_zpowers,
120       crossingAutomorphism_order L A hdisj hsup sigma eta hdiv, heta_order]
121 
122 end PaperX.CyclotomicCrossing

Back to source controls