ReconstructionTopology.lean

1 import PaperX.MonodromyReconstruction
2 import Mathlib.Topology.Algebra.Module.Basic
3 
4 /-! Joint continuity of the finite exponential construction. Nilpotence replaces
5 all analytic convergence requirements. Continuity of the original action, the
6 nilpotent operator, and the chosen cocycle remains explicit. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.ReconstructionTopology
10 open PaperX.NilpotentExponential PaperX.WeilData PaperX.MonodromyReconstruction
11 variable {K V : Type*} [Field K] [CharZero K]
12   [AddCommGroup V] [Module K V]
13   [TopologicalSpace K] [ContinuousMul K]
14   [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul K V]
15 
16 omit [CharZero K] [TopologicalSpace K] [ContinuousMul K] [ContinuousAdd V]
17     [ContinuousSMul K V] in
18  theorem continuous_end_pow (N : Module.End K V) (hN : Continuous N) (j : ℕ) :
19     Continuous (fun x : V => (N ^ j) x) := by
20   induction j with
21   | zero =>
22     convert (continuous_id : Continuous (fun x : V => x)) using 1
23     ext x
24     simp
25   | succ j ih =>
26     convert hN.comp ih using 1
27     ext x
28     simp [pow_succ', Module.End.mul_apply]
29 
30 /-- The exponential action is jointly continuous in its scalar parameter and vector. -/
31 theorem continuous_expN (N : Module.End K V) (hnil : IsNilpotent N)
32     (hN : Continuous N) : Continuous (fun p : K × V => expN N p.1 p.2) := by
33   obtain ⟨d, hd⟩ := hnil
34   have he (p : K × V) : expN N p.1 p.2 =
35       ∑ j ∈ Finset.range d, (p.1 ^ j / (j.factorial : K)) • (N ^ j) p.2 := by
36     simp [expN_polynomial hd]
37   simp_rw [he]
38   apply continuous_finsetSum
39   intro j hj
40   have hc : Continuous (fun p : K × V => p.1 ^ j / (j.factorial : K)) := by
41     convert (continuous_fst.pow j).mul
42       (continuous_const (y := (j.factorial : K)⁻¹)) using 1
43     ext p
44     simp [div_eq_mul_inv]
45   exact hc.smul ((continuous_end_pow N hN j).comp continuous_snd)
46 
47 variable {G : Type*} [Group G] [TopologicalSpace G] {ν : G →* Kˣ}
48 
49 /-- No topology on endomorphism rings and no finite-dimensionality assumption is needed. -/
50 theorem continuous_reconstruct (D : Datum ν V) (t : TwistedCocycle ν)
51     (hN : Continuous D.N)
52     (hr : Continuous (fun p : G × V => D.r p.1 p.2))
53     (ht : Continuous t.value) :
54     Continuous (fun p : G × V => reconstruct D t p.1 p.2) := by
55   have he := (continuous_expN D.N D.nilpotent hN).comp
56     ((ht.comp continuous_fst).prodMk hr)
57   convert he using 1
58   rfl
59 
60 end PaperX.ReconstructionTopology

Back to source controls