FiniteSampleRecovery.lean

1 import PaperX.GeneralReconstructionRecovery
2 import PaperX.WeilSmooth
3 import Mathlib.GroupTheory.OrderOfElement
4 
5 /-! Finite original inertia actions supply a common unipotent sample after taking
6 an explicitly positive power. The norm character and a nonzero cocycle value
7 are still hypotheses on the supplied element; no arithmetic attachment is asserted. -/
8 set_option autoImplicit false
9 noncomputable section
10 
11 namespace PaperX.FiniteSampleRecovery
12 
13 open PaperX.WeilData PaperX.MonodromyReconstruction
14 
15 variable {K G : Type*} [Field K] [CharZero K] [Group G] {ν : G →* Kˣ}
16 variable {V W : Type*} [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
17 
18 /-- On the kernel of the norm character the twisted cocycle is additive on powers. -/
19 theorem cocycle_pow (t : TwistedCocycle ν) (u : G) (hν : ν u = 1) (n : ℕ) :
20     t.value (u ^ n) = (n : K) * t.value u := by
21   induction n with
22   | zero => simp
23   | succ n ih =>
24     rw [pow_succ, t.mul_value, ih, map_pow, hν]
25     simp only [one_pow, Units.val_one, one_mul, Nat.cast_add, Nat.cast_one]
26     ring
27 
28 /-- Positive powers retain the nonzero cocycle value in characteristic zero. -/
29 theorem cocycle_pow_ne_zero (t : TwistedCocycle ν) (u : G) (hν : ν u = 1)
30     (htu : t.value u ≠ 0) {n : ℕ} (hn : 0 < n) : t.value (u ^ n) ≠ 0 := by
31   rw [cocycle_pow t u hν]
32   exact mul_ne_zero (Nat.cast_ne_zero.mpr (Nat.ne_of_gt hn)) htu
33 
34 /-- Two finite-order original actions become trivial at one positive common power. -/
35 theorem exists_common_sample {D : Datum ν V} {E : Datum ν W}
36     (t : TwistedCocycle ν) (u : G) (hν : ν u = 1) (htu : t.value u ≠ 0)
37     (hD : IsOfFinOrder (D.r u)) (hE : IsOfFinOrder (E.r u)) :
38     ∃ n : ℕ, 0 < n ∧ D.r (u ^ n) = 1 ∧ E.r (u ^ n) = 1 ∧ t.value (u ^ n) ≠ 0 := by
39   obtain ⟨d, hd, hdp⟩ := hD.exists_pow_eq_one
40   obtain ⟨e, he, hep⟩ := hE.exists_pow_eq_one
41   refine ⟨d * e, Nat.mul_pos hd he, ?_, ?_,
42     cocycle_pow_ne_zero t u hν htu (Nat.mul_pos hd he)⟩
43   · rw [map_pow, pow_mul, hdp, one_pow]
44   · rw [map_pow, Nat.mul_comm d e, pow_mul, hep, one_pow]
45 
46 /-- Full reconstruction faithfulness when the sampled original actions have finite order. -/
47 theorem reconstruct_intertwiner_iff_of_finite_order {D : Datum ν V} {E : Datum ν W}
48     (t : TwistedCocycle ν) (u : G) (hν : ν u = 1) (htu : t.value u ≠ 0)
49     (hD : IsOfFinOrder (D.r u)) (hE : IsOfFinOrder (E.r u)) (f : V →ₗ[K] W) :
50     (∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) ↔
51       (∀ g x, f (D.r g x) = E.r g (f x)) ∧ E.N ∘ₗ f = f ∘ₗ D.N := by
52   obtain ⟨n, _, hDn, hEn, htn⟩ := exists_common_sample t u hν htu hD hE
53   exact GeneralReconstructionRecovery.reconstruct_intertwiner_iff t (u ^ n) hDn hEn htn f
54 
55 omit [CharZero K] in
56 /-- Finite actual image on a subgroup makes each restricted action element finite order. -/
57 theorem action_finite_order_of_finite_image (ρ : Representation K G V) (H : Subgroup G)
58     (hfinite : Set.Finite (Set.range (fun g : H => ρ g))) (u : H) :
59     IsOfFinOrder (ρ u) := by
60   have hmem (n : ℕ) : (ρ u) ^ n ∈ Set.range (fun g : H => ρ g) := by
61     refine ⟨u ^ n, ?_⟩
62     simp
63   obtain ⟨m, n, hmn, hpow⟩ := hfinite.exists_lt_map_eq_of_forall_mem hmem
64   apply isOfFinOrder_iff_pow_eq_one.mpr
65   refine ⟨n - m, Nat.sub_pos_of_lt hmn, ?_⟩
66   have hm : IsUnit ((ρ u) ^ m) := by
67     rw [← map_pow]
68     exact ⟨ρ.toHomUnits ((u : G) ^ m), rfl⟩
69   apply hm.mul_left_cancel
70   rw [← pow_add, Nat.add_sub_of_le hmn.le, mul_one]
71   exact hpow.symm
72 
73 /-- Actual finite inertia images supply the common sample needed for full faithfulness. -/
74 theorem reconstruct_intertwiner_iff_of_finite_inertia {D : Datum ν V} {E : Datum ν W}
75     (t : TwistedCocycle ν) (H : Subgroup G) (u : H)
76     (hν : ν u = 1) (htu : t.value u ≠ 0)
77     (hD : Set.Finite (Set.range (fun g : H => D.r g)))
78     (hE : Set.Finite (Set.range (fun g : H => E.r g))) (f : V →ₗ[K] W) :
79     (∀ g x, f (reconstruct D t g x) = reconstruct E t g (f x)) ↔
80       (∀ g x, f (D.r g x) = E.r g (f x)) ∧ E.N ∘ₗ f = f ∘ₗ D.N := by
81   exact reconstruct_intertwiner_iff_of_finite_order t u hν htu
82     (action_finite_order_of_finite_image D.r H hD u)
83     (action_finite_order_of_finite_image E.r H hE u) f
84 
85 end PaperX.FiniteSampleRecovery

Back to source controls