AbsoluteFrobeniusWitnesses.lean

1 import PaperX.AbsoluteIntegralFrobenius
2 import Mathlib.RepresentationTheory.Character
3 
4 /-! Actual absolute arithmetic Frobenius witnesses indexed by rational primes.
5 The prime ideal, stabilizer membership and residue action are stored together.
6 These records do not assert that their global elements are unramified in Qbar. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.AbsoluteFrobeniusWitnesses
10 open PaperX.AbsoluteIntegralFrobenius
11 open scoped Pointwise
12 
13 abbrev RationalPrime := {p : ℕ // p.Prime}
14 
15 /-- Arithmetic p-power Frobenius at an actual prime of the algebraic integers. -/
16 structure Witness (p : ℕ) where
17   primeIdeal : Ideal IntegralClosure
18   isMaximal : primeIdeal.IsMaximal
19   liesOver : primeIdeal.LiesOver (Ideal.span {(p : ℤ)})
20   element : GQ
21   stabilizes : element ∈ MulAction.stabilizer GQ primeIdeal
22   residue : ∀ x : IntegralClosure, Ideal.Quotient.mk primeIdeal (element • x) =
23     (Ideal.Quotient.mk primeIdeal x) ^ p
24 
25 /-- Existence is derived from the actual integral-closure construction. -/
26 theorem witness_nonempty (p : ℕ) [Fact p.Prime] : Nonempty (Witness p) := by
27   obtain ⟨Q, hQ, hQp, σ, hσ⟩ := exists_frobenius p
28   exact ⟨⟨Q, hQ, hQp, σ.val, σ.property, hσ⟩⟩
29 
30 /-- A fixed prime-indexed choice of actual arithmetic witnesses. -/
31 def chosenWitness (p : RationalPrime) : Witness p.val := by
32   let : Fact p.val.Prime := ⟨p.property⟩
33   exact Classical.choice (witness_nonempty p.val)
34 
35 section Conjugation
36 variable {R G : Type*} [CommRing R] [Group G] [MulSemiringAction G R]
37 
38 /-- Conjugating an arithmetic residue action conjugates its prime ideal. -/
39 theorem residue_conjugate (Q : Ideal R) (p : ℕ) (γ a : G)
40     (hγ : ∀ x : R, Ideal.Quotient.mk Q (γ • x) = (Ideal.Quotient.mk Q x) ^ p) :
41     ∀ x : R, Ideal.Quotient.mk (a • Q) ((a * γ * a⁻¹) • x) =
42       (Ideal.Quotient.mk (a • Q) x) ^ p := by
43   intro x
44   rw [← map_pow, Ideal.Quotient.eq]
45   rw [Ideal.mem_pointwise_smul_iff_inv_smul_mem, smul_sub, smul_pow']
46   have h' := hγ (a⁻¹ • x)
47   rw [← map_pow] at h'
48   have h := Ideal.Quotient.eq.mp h'
49   simpa only [mul_smul, inv_smul_smul] using h
50 
51 /-- Equal residue actions at a fixed actual prime differ by its inertia. -/
52 theorem same_residue_div_mem_inertia (Q : Ideal R) (γ δ : G)
53     (hγ : γ ∈ MulAction.stabilizer G Q)
54     (h : ∀ x : R, Ideal.Quotient.mk Q (δ • x) = Ideal.Quotient.mk Q (γ • x)) :
55     γ⁻¹ * δ ∈ Q.inertia G := by
56   intro x
57   change (γ⁻¹ * δ) • x - x ∈ Q
58   have hm : δ • x - γ • x ∈ Q := Ideal.Quotient.eq.mp (h x)
59   have hs : γ⁻¹ • Q = Q := (MulAction.stabilizer G Q).inv_mem hγ
60   have hh := Ideal.smul_mem_pointwise_smul γ⁻¹ _ Q hm
61   simpa only [hs, smul_sub, inv_smul_smul, mul_smul] using hh
62 
63 end Conjugation
64 end PaperX.AbsoluteFrobeniusWitnesses

Back to source controls