ReconstructionExamples.lean

1 import PaperX.AffineMonodromy
2 import PaperX.NilpotentExponential
3 import PaperX.MonodromyReconstruction
4 
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.ReconstructionExamples
8 open PaperX.AffineMonodromy PaperX.WeilSpecialChain PaperX.SpecialMonodromy
9 open PaperX.MonodromyReconstruction
10 
11 def chosenCocycle : TwistedCocycle ν := ⟨t, cocycle_identity⟩
12 def good3 : Representation ℚ G (Fin 3 → ℚ) := reconstruct datum3 chosenCocycle
13 
14 theorem exponential_coordinates (s : ℚ) (x : Fin 3 → ℚ) :
15     PaperX.NilpotentExponential.expN datum3.N s x =
16       ![x 0 + s * x 1 + (s ^ 2 / 2) * x 2, x 1 + s * x 2, x 2] := by
17   rw [PaperX.NilpotentExponential.expN_sum nonzero_monodromy.2]
18   funext j
19   fin_cases j <;>
20     simp [Finset.sum_range_succ, smul_pow, datum3, chain, chainDatum,
21       shift_pow_apply]
22   ring
23 
24 theorem translated_coordinates (x : Fin 3 → ℚ) :
25     good3 u x = ![x 0 + x 1 + (1/2) * x 2, x 1 + x 2, x 2] := by
26   simp [good3, chosenCocycle, reconstruct_apply, unipotent,
27     translation_value.1, translation_action, exponential_coordinates]
28 
29 theorem dilated_coordinates (x : Fin 3 → ℚ) :
30     good3 d x = ![x 0, 3 * x 1, 9 * x 2] := by
31   simp only [good3, reconstruct_apply, chosenCocycle, dilation_value.1,
32     unipotent_zero, Module.End.one_apply]
33   funext j
34   fin_cases j <;> norm_num [dilation_action]
35   rfl
36 
37 theorem translation_is_nontrivial : good3 u ≠ 1 := by
38   intro h
39   have he := congrArg (fun A : Module.End ℚ (Fin 3 → ℚ) => A ![0, 1, 0] 0) h
40   simp [translated_coordinates] at he
41 
42 theorem dilation_translation_coordinates (x : Fin 3 → ℚ) :
43     good3 (d * u) x = ![x 0 + x 1 + (1/2) * x 2, 3 * x 1 + 3 * x 2, 9 * x 2] := by
44   rw [map_mul, Module.End.mul_apply, translated_coordinates, dilated_coordinates]
45   ext j
46   fin_cases j <;> simp
47   ring
48 
49 theorem translation_dilation_coordinates (x : Fin 3 → ℚ) :
50     good3 (u * d) x = ![x 0 + 3 * x 1 + (9/2) * x 2, 3 * x 1 + 9 * x 2, 9 * x 2] := by
51   rw [map_mul, Module.End.mul_apply, dilated_coordinates, translated_coordinates]
52   ext j
53   fin_cases j <;> simp
54   ring
55 
56 theorem exact_group_inverse (g : G) : good3 g * good3 g⁻¹ = 1 :=
57   reconstruct_inverse datum3 chosenCocycle g
58 
59 theorem quadratic_term_required : good3 u ≠ 1 + datum3.N := by
60   intro h
61   have he := congrArg (fun A : Module.End ℚ (Fin 3 → ℚ) => A ![0, 0, 1] 0) h
62   simp [translated_coordinates, datum3, chain, chainDatum, shift_apply] at he
63 
64 theorem ordinary_additivity_fails : t (d * u) ≠ t d + t u := by
65   rw [product_values.1, dilation_value.1, translation_value.1]
66   norm_num
67 
68 def wrongOrder (g : G) : Module.End ℚ (Fin 3 → ℚ) :=
69   datum3.r g * PaperX.NilpotentExponential.expN datum3.N (t g)
70 
71 theorem wrong_order_fails : wrongOrder (u * d) ≠ wrongOrder u * wrongOrder d := by
72   intro h
73   have he := congrArg (fun A : Module.End ℚ (Fin 3 → ℚ) => A ![0, 1, 0] 0) h
74   simp only [wrongOrder, map_mul, Module.End.mul_apply, product_values.2,
75     translation_value.1, dilation_value.1, translation_action,
76     PaperX.NilpotentExponential.expN_zero, Module.End.one_apply] at he
77   simp [exponential_coordinates, dilation_action] at he
78 
79 
80 end PaperX.ReconstructionExamples

Back to source controls