AbsoluteIntegralFrobenius.lean

1 import PaperX.AbsoluteGaloisRestriction
2 import Mathlib.FieldTheory.Galois.IsGaloisGroup
3 import Mathlib.FieldTheory.Galois.Profinite
4 import Mathlib.RingTheory.Invariant.Profinite
5 import Mathlib.RingTheory.Localization.Integral
6 import Mathlib.FieldTheory.Perfect
7 import Mathlib.Topology.Algebra.MulAction
8 import Mathlib.NumberTheory.NumberField.Basic
9 import Mathlib.RingTheory.Ideal.Int
10 
11 /-! Actual arithmetic Frobenius elements in decomposition groups of the algebraic
12 integers in the fixed algebraic closure of Q. The prime ideal and the absolute
13 Galois automorphism are constructed. No Frobenius lift or residue-surjectivity
14 hypothesis is supplied. The residue convention is the arithmetic p-power map. -/
15 set_option autoImplicit false
16 noncomputable section
17 namespace PaperX.AbsoluteIntegralFrobenius
18 open scoped Pointwise
19 
20 abbrev Qbar := AlgebraicClosure ℚ
21 abbrev GQ := Gal(Qbar/ℚ)
22 abbrev IntegralClosure := integralClosure ℤ Qbar
23 
24 instance algebraic_int : Algebra.IsAlgebraic ℤ Qbar :=
25   IsFractionRing.comap_isAlgebraic_iff.mpr (inferInstance : Algebra.IsAlgebraic ℚ Qbar)
26 
27 instance fractionRing : IsFractionRing IntegralClosure Qbar :=
28   integralClosure.isFractionRing_of_algebraic (A := ℤ)
29     (fun _ hx => (FaithfulSMul.algebraMap_injective ℤ Qbar) (hx.trans (map_zero _).symm))
30 
31 instance galoisGroup_integral : IsGaloisGroup GQ ℤ IntegralClosure :=
32   IsGaloisGroup.of_isFractionRing GQ ℤ IntegralClosure ℚ Qbar
33 
34 local instance : TopologicalSpace IntegralClosure := ⊥
35 local instance : DiscreteTopology IntegralClosure := ⟨rfl⟩
36 
37 /-- The actual absolute Galois action on the algebraic integers is continuous
38 when the algebraic integers carry the discrete topology. -/
39 theorem continuous_integral_action : ContinuousSMul GQ IntegralClosure := by
40   apply continuousSMul_iff_stabilizer_isOpen.mpr
41   intro x
42   convert stabilizer_isOpen_of_isIntegral (K := ℚ) (x : Qbar) using 1
43   ext σ
44   simp only [SetLike.mem_coe, MulAction.mem_stabilizer_iff, Subtype.ext_iff]
45   rfl
46 
47 attribute [local instance] continuous_integral_action
48 
49 variable (p : ℕ) [hp : Fact p.Prime]
50   (Q : Ideal IntegralClosure) [Q.IsMaximal] [Q.LiesOver (Ideal.span {(p : ℤ)})]
51 
52 attribute [local instance] Ideal.Quotient.field
53 
54 /-- A prime ideal of the algebraic integers above p has residue characteristic p. -/
55 theorem residue_charP : CharP (IntegralClosure ⧸ Q) p := by
56   apply (CharP.charP_iff_prime_eq_zero hp.out).mpr
57   have hm : (p : IntegralClosure) ∈ Q := by
58     change algebraMap ℤ IntegralClosure (p : ℤ) ∈ Q
59     rw [← Ideal.mem_under, ← Ideal.over_def Q (Ideal.span {(p : ℤ)})]
60     exact Ideal.subset_span (Set.mem_singleton _)
61   simpa only [map_natCast] using (Ideal.Quotient.eq_zero_iff_mem.mpr hm)
62 
63 
64 /-- The p-power map on this actual residue field is bijective. Roots in Qbar
65 remain integral because their p-th powers are integral. -/
66 theorem residue_perfect : PerfectRing (IntegralClosure ⧸ Q) p := by
67   let : CharP (IntegralClosure ⧸ Q) p := residue_charP p Q
68   refine ⟨⟨frobenius_inj (IntegralClosure ⧸ Q) p, ?_⟩⟩
69   intro x
70   obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective x
71   obtain ⟨y, hy⟩ := IsAlgClosed.exists_pow_nat_eq (b : Qbar) hp.out.pos
72   have hi : IsIntegral ℤ y := IsIntegral.of_pow hp.out.pos (by rw [hy]; exact b.property)
73   let c : IntegralClosure := ⟨y, (mem_integralClosure_iff ℤ Qbar).mpr hi⟩
74   refine ⟨Ideal.Quotient.mk Q c, ?_⟩
75   change Ideal.Quotient.mk Q c ^ p = Ideal.Quotient.mk Q b
76   rw [← map_pow]
77   apply congrArg (Ideal.Quotient.mk Q)
78   exact Subtype.ext hy
79 
80 
81 /-- Arithmetic Frobenius as an automorphism of the actual residue extension. -/
82 def residueFrobenius :
83     (IntegralClosure ⧸ Q) ≃ₐ[ℤ ⧸ Ideal.span {(p : ℤ)}] (IntegralClosure ⧸ Q) := by
84   let : CharP (IntegralClosure ⧸ Q) p := residue_charP p Q
85   let : PerfectRing (IntegralClosure ⧸ Q) p := residue_perfect p Q
86   exact
87     { __ := frobeniusEquiv (IntegralClosure ⧸ Q) p
88       commutes' := by
89         intro x
90         obtain ⟨z, rfl⟩ := Ideal.Quotient.mk_surjective x
91         change frobeniusEquiv (IntegralClosure ⧸ Q) p (z : IntegralClosure ⧸ Q) =
92           (z : IntegralClosure ⧸ Q)
93         exact map_intCast (frobeniusEquiv (IntegralClosure ⧸ Q) p) z }
94 
95 /-- The chosen residue automorphism is exactly the p-power map. -/
96 theorem residueFrobenius_apply (x : IntegralClosure ⧸ Q) :
97     residueFrobenius p Q x = x ^ p := rfl
98 
99 /-- Every actual prime ideal above p admits an arithmetic Frobenius lift in its
100 actual absolute Galois decomposition group. -/
101 theorem exists_frobenius_at :
102     ∃ σ : MulAction.stabilizer GQ Q, ∀ x : IntegralClosure,
103       Ideal.Quotient.mk Q (σ.val • x) = (Ideal.Quotient.mk Q x) ^ p := by
104   obtain ⟨σ, hσ⟩ := Ideal.Quotient.stabilizerHom_surjective_of_profinite
105     (G := GQ) (Ideal.span {(p : ℤ)}) Q (residueFrobenius p Q)
106   refine ⟨σ, fun x => ?_⟩
107   exact DFunLike.congr_fun hσ (Ideal.Quotient.mk Q x)
108 
109 /-- For each rational prime, an actual maximal ideal of the algebraic integers
110 and an actual absolute Frobenius element above it exist. -/
111 theorem exists_frobenius :
112     ∃ Q : Ideal IntegralClosure, Q.IsMaximal ∧ Q.LiesOver (Ideal.span {(p : ℤ)}) ∧
113       ∃ σ : MulAction.stabilizer GQ Q, ∀ x : IntegralClosure,
114         Ideal.Quotient.mk Q (σ.val • x) = (Ideal.Quotient.mk Q x) ^ p := by
115   let : (Ideal.span {(p : ℤ)}).IsMaximal := Int.ideal_span_isMaximal_of_prime p
116   obtain ⟨Q, hQ, hQP⟩ := Ideal.exists_maximal_ideal_liesOver_of_isIntegral
117     (S := IntegralClosure) (Ideal.span {(p : ℤ)})
118   let : Q.IsMaximal := hQ
119   let : Q.LiesOver (Ideal.span {(p : ℤ)}) := hQP
120   exact ⟨Q, hQ, hQP, exists_frobenius_at p Q⟩
121 
122 end PaperX.AbsoluteIntegralFrobenius

Back to source controls