AuxiliaryCyclotomicBaseChange.lean

1 import PaperX.AuxiliaryCyclotomicExistence
2 
3 /-! Base change of a disjoint cyclic auxiliary extension. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperX.AuxiliaryCyclotomicBaseChange
7 open IntermediateField
8 
9 variable {k M : Type*} [Field k] [Field M] [Algebra k M]
10 
11 /-- The compositum, viewed as an extension of the new base field. -/
12 def compositumOver (K A : IntermediateField k M) : IntermediateField K M :=
13   IntermediateField.extendScalars (show K ≤ A ⊔ K from le_sup_right)
14 
15 theorem compositumOver_restrictScalars (K A : IntermediateField k M) :
16     (compositumOver K A).restrictScalars k = A ⊔ K := rfl
17 
18 theorem compositumOver_isGalois (K A : IntermediateField k M)
19     [FiniteDimensional k A] [IsGalois k A] :
20     IsGalois K (compositumOver K A) := by
21   let D : IntermediateField k M := A ⊔ K
22   let : Algebra K D := (IntermediateField.inclusion (show K ≤ D from le_sup_right)).toAlgebra
23   let A' : IntermediateField k D := A.restrict le_sup_left
24   let K' : IntermediateField k D := K.restrict le_sup_right
25   have hgal : IsGalois k A' := IsGalois.of_algEquiv (restrictAlgEquiv le_sup_left)
26   have : FiniteDimensional k A' :=
27     (restrictAlgEquiv (show A ≤ D from le_sup_left)).toLinearEquiv.finiteDimensional
28   have hsup : A' ⊔ K' = ⊤ := by
29     apply IntermediateField.lift_injective D
30     simp only [lift_sup, A', K', lift_restrict, lift_top, D]
31   have : IsGalois K' D := IsGalois.sup_right A' K' hsup
32   apply IsGalois.of_equiv_equiv (F := K') (E := D)
33     (f := (restrictAlgEquiv (show K ≤ D from le_sup_right)).symm.toRingEquiv)
34     (g := RingEquiv.refl D)
35   apply RingHom.ext
36   intro x
37   exact congrArg Subtype.val ((restrictAlgEquiv (show K ≤ D from le_sup_right)).apply_symm_apply x)
38 
39 theorem compositumOver_isCyclic (K A : IntermediateField k M)
40     [FiniteDimensional k A] [IsGalois k A] [IsCyclic Gal(A/k)] :
41     IsCyclic Gal((compositumOver K A)/K) := by
42   let D : IntermediateField k M := A ⊔ K
43   let : Algebra K D := (IntermediateField.inclusion (show K ≤ D from le_sup_right)).toAlgebra
44   let A' : IntermediateField k D := A.restrict le_sup_left
45   let K' : IntermediateField k D := K.restrict le_sup_right
46   let eK : K ≃ₐ[k] K' := restrictAlgEquiv le_sup_right
47   have hgal : IsGalois k A' := IsGalois.of_algEquiv (restrictAlgEquiv le_sup_left)
48   have : Normal k A' := hgal.to_normal
49   have : IsCyclic Gal(A'/k) := isCyclic_of_surjective
50     (restrictAlgEquiv (show A ≤ D from le_sup_left)).autCongr
51     (restrictAlgEquiv (show A ≤ D from le_sup_left)).autCongr.surjective
52   have hsup : A' ⊔ K' = ⊤ := by
53     apply IntermediateField.lift_injective D
54     simp only [lift_sup, A', K', lift_restrict, lift_top, D]
55   have hcycD : IsCyclic Gal(D/K') := isCyclic_of_injective
56     (restrictRestrictAlgEquivMapHom k A' K' D)
57     (restrictRestrictAlgEquivMapHom_injective A' K' hsup)
58   let : Algebra K' K := eK.symm.toAlgHom.toAlgebra
59   let : Algebra K' (compositumOver K A) := inferInstanceAs (Algebra K' D)
60   have : IsScalarTower K' K (compositumOver K A) :=
61     IsScalarTower.of_algebraMap_eq (fun x =>
62       (congrArg Subtype.val (eK.apply_symm_apply x)).symm)
63   have : IsCyclic Gal((compositumOver K A)/K') := hcycD
64   exact isCyclic_of_injective
65     (MulSemiringAction.toAlgAut Gal((compositumOver K A)/K) K' (compositumOver K A))
66     (fun f g h => AlgEquiv.ext (fun x => DFunLike.congr_fun h x))
67 
68 theorem compositumOver_eq_adjoin (K A : IntermediateField k M) :
69     compositumOver K A = IntermediateField.adjoin K (A : Set M) := by
70   apply IntermediateField.restrictScalars_injective k
71   rw [compositumOver_restrictScalars, restrictScalars_adjoin,
72     adjoin_union, adjoin_self, adjoin_self, sup_comm]
73 
74 /-- Disjoint base change preserves the degree of the original extension. -/
75 theorem compositumOver_finrank (K A : IntermediateField k M)
76     [FiniteDimensional k A] (h : A.LinearDisjoint K) :
77     Module.finrank K (compositumOver K A) = Module.finrank k A := by
78   rw [compositumOver_eq_adjoin]
79   exact congrArg Cardinal.toNat h.adjoin_rank_eq_rank_left_of_isAlgebraic_left
80 
81 /-- Base change inside the second field preserves linear disjointness. -/
82 theorem compositumOver_linearDisjoint (K A L : IntermediateField k M)
83     [FiniteDimensional k K] [FiniteDimensional k A] [FiniteDimensional k L]
84     (hKL : K ≤ L) (h : A.LinearDisjoint L) :
85     (compositumOver K A).LinearDisjoint (IntermediateField.extendScalars hKL) := by
86   let B := compositumOver K A
87   let L' := IntermediateField.extendScalars hKL
88   have : FiniteDimensional k B := inferInstanceAs (FiniteDimensional k (A ⊔ K : IntermediateField k M))
89   have : FiniteDimensional K B := FiniteDimensional.right k K B
90   have : FiniteDimensional k L' := inferInstanceAs (FiniteDimensional k L)
91   have : FiniteDimensional K L' := FiniteDimensional.right k K L'
92   have : FiniteDimensional K (B ⊔ L' : IntermediateField K M) :=
93     IntermediateField.finiteDimensional_sup B L'
94   have : Module.Free K (B ⊔ L' : IntermediateField K M) := Module.Free.of_divisionRing K _
95   have : FiniteDimensional k (B ⊔ L' : IntermediateField K M) :=
96     Module.Finite.trans K (B ⊔ L' : IntermediateField K M)
97   have hsup : (B ⊔ L' : IntermediateField K M).restrictScalars k = A ⊔ L := by
98     rw [← restrictScalars_sup, compositumOver_restrictScalars, extendScalars_restrictScalars]
99     exact sup_assoc A K L ▸ congrArg (fun E : IntermediateField k M => A ⊔ E)
100       (sup_eq_right.mpr hKL)
101   have htotal : Module.finrank k (B ⊔ L' : IntermediateField K M) =
102       Module.finrank k A * Module.finrank k L := by
103     change Module.finrank k ((B ⊔ L' : IntermediateField K M).restrictScalars k) = _
104     rw [hsup]
105     exact h.finrank_sup
106   have hB : Module.finrank K B = Module.finrank k A :=
107     compositumOver_finrank K A (h.of_le_right hKL)
108   have hL := Module.finrank_mul_finrank k K L'
109   have htot := Module.finrank_mul_finrank k K (B ⊔ L' : IntermediateField K M)
110   have hK : 0 < Module.finrank k K := Module.finrank_pos
111   apply IntermediateField.LinearDisjoint.of_finrank_sup
112   change Module.finrank K (B ⊔ L' : IntermediateField K M) = _
113   rw [hB]
114   change Module.finrank k K * Module.finrank K L' = Module.finrank k L at hL
115   nlinarith
116 
117 end PaperX.AuxiliaryCyclotomicBaseChange

Back to source controls