CyclotomicCrossingContainment.lean

1 import PaperX.CyclotomicCrossingPair
2 import Mathlib.NumberTheory.Cyclotomic.Basic
3 
4 /-!
5 # Embedding the crossed extension in a cyclotomic extension
6 
7 The auxiliary field need only be contained in a cyclotomic extension. The root
8 of unity may lie in a larger ambient field than the original compositum.
9 -/
10 
11 set_option autoImplicit false
12 
13 noncomputable section
14 
15 namespace PaperX.CyclotomicCrossing
16 
17 open IntermediateField
18 
19 variable {K T Ω : Type*} [Field K] [Field T] [Field Ω]
20 variable [Algebra K T] [Algebra K Ω]
21 
22 /-- Mapping the ambient top field is exactly the image of the embedding. -/
23 theorem map_top_eq_fieldRange (i : T →ₐ[K] Ω) :
24     (⊤ : IntermediateField K T).map i = i.fieldRange := by
25   ext x
26   simp only [mem_map, mem_top, true_and, AlgHom.mem_fieldRange]
27 
28 /-- An equality of composita gives an actual inclusion into an adjunction
29 over the image of the first field. -/
30 theorem fieldRange_le_adjoin_of_sup_eq_top
31     (E A : IntermediateField K T) (hsup : E ⊔ A = ⊤)
32     (i : T →ₐ[K] Ω) (ζ : Ω) (hA : A.map i ≤ adjoin K ({ζ} : Set Ω)) :
33     i.fieldRange ≤ (adjoin (E.map i) ({ζ} : Set Ω)).restrictScalars K := by
34   rw [restrictScalars_adjoin_eq_sup, ← map_top_eq_fieldRange i, ← hsup,
35     IntermediateField.map_sup]
36   exact sup_le_sup_left hA _
37 
38 variable [FiniteDimensional K T] [IsGalois K T]
39 
40 /-- The crossed extension embeds into `E(ζ)` whenever the auxiliary field
41 embeds into `K(ζ)`. This statement does not require `ζ` to belong to `T`. -/
42 theorem crossing_fieldRange_le_adjoin
43     (L A : IntermediateField K T) [IsGalois K L] [IsGalois K A]
44     (hdisj : L.LinearDisjoint A) (hsup : L ⊔ A = ⊤)
45     (sigma : L ≃ₐ[K] L) (eta : A ≃ₐ[K] A)
46     (horder : orderOf sigma ∣ orderOf eta)
47     (i : T →ₐ[K] Ω) (ζ : Ω) (hA : A.map i ≤ adjoin K ({ζ} : Set Ω)) :
48     i.fieldRange ≤
49       (adjoin ((fixedField (Subgroup.zpowers
50         (crossingAutomorphism L A hdisj hsup sigma eta))).map i)
51           ({ζ} : Set Ω)).restrictScalars K := by
52   exact fieldRange_le_adjoin_of_sup_eq_top _ A
53     (crossing_fixedField_sup_eq_top L A hdisj hsup sigma eta horder) i ζ hA
54 
55 omit [FiniteDimensional K T] [IsGalois K T] in
56 /-- Adjoining the supplied primitive root is genuinely a cyclotomic extension
57 over the changed base field. -/
58 theorem adjoin_isCyclotomic_over_mapped_base
59     (E : IntermediateField K T) (i : T →ₐ[K] Ω)
60     {n : ℕ} [NeZero n] (ζ : Ω) (hζ : IsPrimitiveRoot ζ n) :
61     IsCyclotomicExtension {n} (E.map i) (adjoin (E.map i) ({ζ} : Set Ω)) := by
62   exact (IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin
63     n (E.map i) Ω (adjoin (E.map i) ({ζ} : Set Ω)) hζ).mpr rfl
64 
65 end PaperX.CyclotomicCrossing

Back to source controls