FiniteResidueBaseChange.lean

1 import PaperXI.ResidueDegreeBaseChange
2 import Mathlib.FieldTheory.Finite.Basic
3 
4 /-! Genuine finite-residue Frobenius, base-field change, and period detection.
5 The chosen embeddings are inputs, not a constructed unramified extension of a
6 local field. Residue Frobenius is never replaced by an abstract cyclic label. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.FiniteResidueBaseChange
10 open PaperXI.ResidueWeil PaperXI.ResidueDegreeBaseChange
11 
12 variable (k L : Type*) [Field k] [Fintype k] [Field L] [Algebra k L]
13   [Algebra.IsAlgebraic k L]
14 
15 /-- The literal q-power automorphism, q = |k|. -/
16 def arithmetic : RingAut L :=
17   (FiniteField.frobeniusAlgEquivOfAlgebraic k L).toRingEquiv
18 
19 /-- The inverse q-power automorphism fixes the geometric convention. -/
20 def geometric : RingAut L := (arithmetic k L)⁻¹
21 
22 @[simp] theorem arithmetic_apply (x : L) : arithmetic k L x = x ^ Fintype.card k := rfl
23 
24 theorem arithmetic_pow_apply (n : ℕ) (x : L) :
25     (arithmetic k L ^ n) x = x ^ (Fintype.card k ^ n) := by
26   induction n with
27   | zero => simp
28   | succ n ih =>
29     rw [pow_succ']
30     change arithmetic k L ((arithmetic k L ^ n) x) = _
31     rw [arithmetic_apply, ih, ← pow_mul, pow_succ]
32 
33 @[simp] theorem geometric_inverse_power (x : L) :
34     (geometric k L x) ^ Fintype.card k = x :=
35   (arithmetic k L).apply_symm_apply x
36 
37 section Tower
38 variable (k' : Type*) [Field k'] [Fintype k'] [Algebra k k']
39   [Algebra k' L] [Algebra.IsAlgebraic k' L]
40 
41 /-- Finite-field cardinality supplies the exponent. No degree/Frobenius equality is assumed. -/
42 theorem arithmetic_tower :
43     arithmetic k L ^ Module.finrank k k' = arithmetic k' L := by
44   apply RingEquiv.ext
45   intro x
46   rw [arithmetic_pow_apply, arithmetic_apply]
47   rw [← Module.card_eq_pow_finrank (K := k) (V := k')]
48 
49 /-- Geometric Frobenius of the enlarged residue base is the f-th power. -/
50 theorem geometric_tower :
51     geometric k L ^ Module.finrank k k' = geometric k' L := by
52   unfold geometric
53   rw [inv_pow, arithmetic_tower k L k']
54 
55 /-- Base change in the residue Frobenius produces an actual degree-divisible group. -/
56 def pullbackEquiv {D : Type*} [Group D] (r : D →* RingAut L) :
57     Pullback r (geometric k' L) ≃*
58       periodSubgroup r (geometric k L) (Module.finrank k k') := by
59   rw [← geometric_tower k L k']
60   exact periodEquiv r (geometric k L) (Module.finrank_pos.ne')
61 end Tower
62 
63 section Order
64 variable [Finite L]
65 
66 /-- Forgetting scalar-fixing data is an injective automorphism-group homomorphism. -/
67 def forget : (L ≃ₐ[k] L) →* RingAut L where
68   toFun e := e.toRingEquiv
69   map_one' := rfl
70   map_mul' _ _ := rfl
71 
72 omit [Fintype k] [Algebra.IsAlgebraic k L] [Finite L] in
73 theorem forget_injective : Function.Injective (forget k L) := by
74   intro a b h
75   apply AlgEquiv.ext
76   intro x
77   exact RingEquiv.congr_fun h x
78 
79 /-- Exact field degree, rather than an assumed period certificate. -/
80 theorem geometric_order : orderOf (geometric k L) = Module.finrank k L := by
81   rw [geometric, orderOf_inv]
82   exact (orderOf_injective (forget k L) (forget_injective k L) _).trans
83     (FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic k L)
84 
85 /-- Includes zero and negative exponents. -/
86 theorem geometric_zpow_eq_one (m : ℤ) :
87     geometric k L ^ m = 1 ↔ (Module.finrank k L : ℤ) ∣ m := by
88   rw [← orderOf_dvd_iff_zpow_eq_one, geometric_order]
89 end Order
90 
91 end PaperXI.FiniteResidueBaseChange

Back to source controls