AffineMonodromy.lean

1 import PaperX.WeilSpecialChain
2 import Mathlib.GroupTheory.SemidirectProduct
3 import Mathlib.Tactic.NormNum
4 
5 /-! A nonzero twisted cocycle on the actual affine group. This is an algebraic
6 model, with no asserted identification with an arithmetic Weil group. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.AffineMonodromy
10 open PaperX.WeilData PaperX.WeilSpecialChain PaperX.SpecialMonodromy
11 
12 variable (K : Type*) [Field K]
13 
14 def scaleAut (a : Kˣ) : MulAut (Multiplicative K) where
15   toFun x := Multiplicative.ofAdd ((a : K) * x.toAdd)
16   invFun x := Multiplicative.ofAdd ((a⁻¹ : Kˣ) * x.toAdd)
17   left_inv x := by simp
18   right_inv x := by simp
19   map_mul' x y := by
20     change Multiplicative.ofAdd ((a : K) * (x.toAdd + y.toAdd)) = _
21     simp [mul_add]
22 
23 def scaling : Kˣ →* MulAut (Multiplicative K) where
24   toFun := scaleAut K
25   map_one' := by ext x; simp [scaleAut]
26   map_mul' a b := by ext x; simp [scaleAut, mul_assoc]
27 
28 abbrev Affine := Multiplicative K ⋊[scaling K] Kˣ
29 
30 def norm : Affine K →* Kˣ := SemidirectProduct.rightHom
31 def coordinate (g : Affine K) : K := g.left.toAdd
32 
33 theorem coordinate_one : coordinate K 1 = 0 := rfl
34 
35 theorem coordinate_mul (g h : Affine K) :
36     coordinate K (g * h) = coordinate K g + (norm K g : K) * coordinate K h := rfl
37 
38 def translation (a : K) : Affine K := ⟨Multiplicative.ofAdd a, 1⟩
39 def dilation (a : Kˣ) : Affine K := ⟨1, a⟩
40 
41 theorem translation_coordinate (a : K) : coordinate K (translation K a) = a := rfl
42 theorem dilation_coordinate (a : Kˣ) : coordinate K (dilation K a) = 0 := rfl
43 theorem translation_norm (a : K) : norm K (translation K a) = 1 := rfl
44 theorem dilation_norm (a : Kˣ) : norm K (dilation K a) = a := rfl
45 
46 def chain (n : ℕ) : Datum (norm K) (Fin n → K) := chainDatum (norm K) 1 n
47 
48 abbrev G := Affine ℚ
49 def ν : G →* ℚˣ := norm ℚ
50 def t : G → ℚ := coordinate ℚ
51 def u : G := translation ℚ 1
52 def d : G := dilation ℚ (Units.mk0 (1/3) (by norm_num))
53 def datum3 : Datum ν (Fin 3 → ℚ) := chain ℚ 3
54 
55 theorem cocycle_identity (g h : G) : t (g * h) = t g + (ν g : ℚ) * t h := rfl
56 theorem translation_value : t u = 1 ∧ ν u = 1 := ⟨rfl, rfl⟩
57 theorem dilation_value : t d = 0 ∧ (ν d : ℚ) = 1/3 := ⟨rfl, rfl⟩
58 
59 theorem product_values : t (d * u) = 1/3 ∧ t (u * d) = 1 := by
60   constructor <;> norm_num [cocycle_identity, translation_value.1,
61     translation_value.2, dilation_value.1, dilation_value.2]
62 
63 theorem noncommuting_elements : d * u ≠ u * d := by
64   intro h
65   have ht := congrArg t h
66   rw [product_values.1, product_values.2] at ht
67   norm_num at ht
68 
69 theorem nonzero_monodromy : datum3.N ^ 2 ≠ 0 ∧ datum3.N ^ 3 = 0 :=
70   ⟨shift_previous_power_nonzero 3 (by decide), shift_nilpotent 3⟩
71 
72 theorem translation_action : datum3.r u = 1 := by
73   apply LinearMap.ext
74   intro x
75   funext j
76   simp [datum3, chain, chainDatum, chainRep, diagonalF, ν, norm, u, translation,
77     SemidirectProduct.rightHom]
78 
79 theorem dilation_action (x : Fin 3 → ℚ) (j : Fin 3) :
80     datum3.r d x j = 3 ^ j.val * x j := by
81   simp [datum3, chain, chainDatum, chainRep, diagonalF, ν, norm, d, dilation,
82     SemidirectProduct.rightHom]
83 
84 
85 end PaperX.AffineMonodromy

Back to source controls