PrimeDegreeFieldFrobenius.lean

1 import PaperX.PrimeDegreeSummabilityFrobenius
2 import Mathlib.FieldTheory.Galois.Basic
3 
4 /-!
5 # Frobenius descent for actual field automorphisms
6 
7 An actual E-linear field automorphism of T induces an actual O_E-linear
8 automorphism of O_T. This attachment commutes with scalar restriction.
9 Nonsummability is still assumed. Neither the Frobenius congruence nor this
10 attachment alone supplies unramifiedness.
11 -/
12 
13 noncomputable section
14 set_option autoImplicit false
15 
16 namespace PaperX.PrimeDegreeFieldFrobenius
17 
18 open NumberField IsDedekindDomain
19 
20 variable (E T : Type*) [Field E] [Field T] [Algebra E T]
21 
22 /-- Restrict an actual field automorphism to the actual ring of integers. -/
23 def integralAut (τ : T ≃ₐ[E] T) : (𝓞 T) ≃ₐ[𝓞 E] (𝓞 T) :=
24   RingOfIntegers.mapAlgEquiv τ
25 
26 /-- The integral action is literally the original field action on integral elements. -/
27 theorem integralAut_apply (τ : T ≃ₐ[E] T) (x : 𝓞 T) :
28     (integralAut E T τ x : T) = τ (x : T) := rfl
29 
30 /-- The prime set is defined using the integral action of the supplied field automorphism. -/
31 def prescribedPrimes (τ : T ≃ₐ[E] T) : Set (HeightOneSpectrum (𝓞 E)) :=
32   PrimeDegreeSummabilityFrobenius.prescribedPrimes E T (integralAut E T τ).toAlgHom
33 
34 variable (K : Type*) [Field K] [Algebra K E] [Algebra K T] [IsScalarTower K E T]
35 
36 /-- Integral attachment and restriction of scalars commute as algebra automorphisms. -/
37 theorem integralAut_restrictScalars (τ : T ≃ₐ[E] T) :
38     (integralAut E T τ).restrictScalars (𝓞 K) =
39       integralAut K T (τ.restrictScalars K) := rfl
40 
41 /-- The corresponding equality of algebra endomorphisms used by the Frobenius predicate. -/
42 theorem integralHom_restrictScalars (τ : T ≃ₐ[E] T) :
43     ((integralAut E T τ).toAlgHom).restrictScalars (𝓞 K) =
44       (integralAut K T (τ.restrictScalars K)).toAlgHom := rfl
45 
46 variable [NumberField K] [NumberField E]
47 
48 /-- Nonsummability of the actual field-automorphism prime set gives descended Frobenius. -/
49 theorem exists_descended_field_frobenius
50     (τ : T ≃ₐ[E] T)
51     (hdiv : ¬ Summable (fun q : prescribedPrimes E T τ => (q.1.asIdeal.absNorm : ℝ)⁻¹))
52     (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
53     ∃ Q : HeightOneSpectrum (𝓞 T), (Q.under (𝓞 E)).under (𝓞 K) ∉ bad ∧
54       (Q.asIdeal.under (𝓞 E)).inertiaDeg (𝓞 K) = 1 ∧
55       (integralAut K T (τ.restrictScalars K)).toAlgHom.IsArithFrobAt Q.asIdeal := by
56   simpa only [integralHom_restrictScalars] using
57     PrimeDegreeSummabilityFrobenius.exists_descended_frobenius K E T
58       (integralAut E T τ).toAlgHom hdiv bad hbad
59 
60 section FixedField
61 
62 variable (F U : Type*) [Field F] [Field U] [Algebra F U] [FiniteDimensional F U]
63 
64 /-- Regard an actual automorphism as linear over the fixed field of the subgroup it generates. -/
65 def overFixedField (ρ : U ≃ₐ[F] U) :
66     U ≃ₐ[IntermediateField.fixedField (Subgroup.zpowers ρ)] U :=
67   IntermediateField.subgroupEquivAlgEquiv (Subgroup.zpowers ρ)
68     ⟨ρ, Subgroup.mem_zpowers ρ⟩
69 
70 /-- The fixed-field automorphism has the original action on every field element. -/
71 theorem overFixedField_apply (ρ : U ≃ₐ[F] U) (x : U) :
72     overFixedField F U ρ x = ρ x := rfl
73 
74 /-- Returning to the original coefficient field recovers the original automorphism. -/
75 theorem overFixedField_restrictScalars (ρ : U ≃ₐ[F] U) :
76     (overFixedField F U ρ).restrictScalars F = ρ := by
77   ext x
78   rfl
79 
80 variable [NumberField F] [NumberField U]
81 
82 /-- The fixed-field construction attaches the original automorphism to descended Frobenius. -/
83 theorem exists_fixedField_descended_frobenius
84     (ρ : U ≃ₐ[F] U)
85     (hdiv : ¬ Summable
86       (fun q : prescribedPrimes (IntermediateField.fixedField (Subgroup.zpowers ρ)) U
87         (overFixedField F U ρ) => (q.1.asIdeal.absNorm : ℝ)⁻¹))
88     (bad : Set (HeightOneSpectrum (𝓞 F))) (hbad : bad.Finite) :
89     ∃ Q : HeightOneSpectrum (𝓞 U),
90       (Q.under (𝓞 (IntermediateField.fixedField (Subgroup.zpowers ρ)))).under (𝓞 F) ∉ bad ∧
91       (Q.asIdeal.under (𝓞 (IntermediateField.fixedField (Subgroup.zpowers ρ)))).inertiaDeg
92         (𝓞 F) = 1 ∧
93       (integralAut F U ρ).toAlgHom.IsArithFrobAt Q.asIdeal := by
94   simpa only [overFixedField_restrictScalars] using
95     exists_descended_field_frobenius
96       (IntermediateField.fixedField (Subgroup.zpowers ρ)) U F (overFixedField F U ρ)
97       hdiv bad hbad
98 
99 end FixedField
100 
101 end PaperX.PrimeDegreeFieldFrobenius

Back to source controls