MonodromyAtom.lean

1 import PaperXI.MonodromyChain
2 import Mathlib.RepresentationTheory.Intertwining
3 import Mathlib.LinearAlgebra.Dimension.Constructions
4 
5 /-! Literal monodromy blocks underlying the formal reconstruction contract.
6 For ν(Φ)=q the action on the i-th copy is ν(g)^i ρ(g); the identity
7 R(g) N R(g)⁻¹ = ν(g)⁻¹ N fixes the normalization explicitly.
8 No assertion of irreducibility or a decomposition classification is assumed here. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.MonodromyAtom
12 open PaperXI.MonodromyChain
13 
14 variable {G V W : Type*} [Group G]
15 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
16 
17 /-- A representation and a nilpotent operator with the indicated covariance. -/
18 structure Datum (ν : G →* ℂˣ) (V : Type*) [AddCommGroup V] [Module ℂ V] where
19   action : Representation ℂ G V
20   monodromy : Module.End ℂ V
21   nilpotent : IsNilpotent monodromy
22   covariance : ∀ g, action g * monodromy =
23     (ν g : ℂ)⁻¹ • (monodromy * action g)
24 
25 def action (ν : G →* ℂˣ) (ρ : Representation ℂ G V) (m : ℕ) :
26     Representation ℂ G (Fin m → V) where
27   toFun g :=
28     { toFun := fun x i => (ν g : ℂ) ^ i.val • ρ g (x i)
29       map_add' := by intros; funext i; simp [map_add, smul_add]
30       map_smul' := by intros; funext i; simp [smul_smul, mul_comm] }
31   map_one' := by ext x i; simp
32   map_mul' g h := by
33     apply LinearMap.ext
34     intro x
35     funext i
36     change (ν (g*h) : ℂ)^i.val • ρ (g*h) (x i) =
37       (ν g : ℂ)^i.val • ρ g ((ν h : ℂ)^i.val • ρ h (x i))
38     simp only [map_mul, Units.val_mul, mul_pow, Module.End.mul_apply, map_smul, smul_smul]
39 
40 @[simp] theorem action_apply (ν : G →* ℂˣ) (ρ : Representation ℂ G V)
41     (m : ℕ) (g : G) (x : Fin m → V) (i : Fin m) :
42     action ν ρ m g x i = (ν g : ℂ) ^ i.val • ρ g (x i) := rfl
43 
44 def monodromy (m : ℕ) : Module.End ℂ (Fin m → V) := shift (fun _ => 1)
45 
46 theorem nilpotence (m : ℕ) : (monodromy (V := V) m)^m = 0 :=
47   nilpotent_bound _
48 
49 /-- The powers and group action are calculated on actual vectors. -/
50 theorem commutation (ν : G →* ℂˣ) (ρ : Representation ℂ G V) (m : ℕ) (g : G) :
51     monodromy m * action ν ρ m g = (ν g : ℂ) • (action ν ρ m g * monodromy m) := by
52   apply LinearMap.ext
53   intro x
54   funext i
55   change shift (fun _ => (1 : Module.End ℂ V)) (action ν ρ m g x) i =
56     (ν g : ℂ) • ((ν g : ℂ)^i.val • ρ g (shift (fun _ => (1 : Module.End ℂ V)) x i))
57   rw [shift_apply]
58   by_cases hi : i.val + 1 < m
59   · rw [dite_eq_left hi]
60     simp [shift_apply, hi, action_apply, pow_succ, smul_smul, mul_comm]
61   · rw [dite_eq_right hi]
62     simp [shift_apply, hi]
63 
64 theorem covariance (ν : G →* ℂˣ) (ρ : Representation ℂ G V) (m : ℕ) (g : G) :
65     action ν ρ m g * monodromy m =
66       (ν g : ℂ)⁻¹ • (monodromy m * action ν ρ m g) := by
67   rw [commutation, smul_smul, inv_mul_cancel₀ (Units.ne_zero _), one_smul]
68 
69 /-- A literal Weil--Deligne-type datum; ν is the inverse norm convention. -/
70 def sp (ν : G →* ℂˣ) (ρ : Representation ℂ G V) (m : ℕ) :
71     Datum ν (Fin m → V) where
72   action := action ν ρ m
73   monodromy := monodromy m
74   nilpotent := ⟨m, nilpotence m⟩
75   covariance := covariance ν ρ m
76 
77 /-- The size of a monodromy block is not merely its chain length. -/
78 theorem dimension [FiniteDimensional ℂ V] (m : ℕ) :
79     Module.finrank ℂ (Fin m → V) = m * Module.finrank ℂ V := by
80   simpa using (Module.finrank_pi_fintype (R := ℂ) (M := fun _ : Fin m => V))
81 
82 /-- An equivalence of Weil atoms lifts pointwise to the actual block action. -/
83 def mapEquiv (ν : G →* ℂˣ) {ρ : Representation ℂ G V} {σ : Representation ℂ G W}
84     (e : Representation.Equiv ρ σ) (m : ℕ) :
85     Representation.Equiv (action ν ρ m) (action ν σ m) :=
86   Representation.Equiv.mk (LinearEquiv.piCongrRight (fun _ : Fin m => e.toLinearEquiv))
87     (fun g => by
88       apply LinearMap.ext
89       intro x
90       funext i
91       change e ((ν g : ℂ)^i.val • ρ g (x i)) = (ν g : ℂ)^i.val • σ g (e (x i))
92       rw [map_smul]
93       congr 1
94       exact LinearMap.congr_fun (e.isIntertwining' g) (x i))
95 
96 /-- The same lifted map also intertwines monodromy, not just the Weil action. -/
97 theorem mapEquiv_monodromy (ν : G →* ℂˣ) {ρ : Representation ℂ G V}
98     {σ : Representation ℂ G W} (e : Representation.Equiv ρ σ) (m : ℕ)
99     (x : Fin m → V) :
100     mapEquiv ν e m (monodromy m x) = monodromy m (mapEquiv ν e m x) := by
101   funext i
102   change e (shift (fun _ => (1 : Module.End ℂ V)) x i) =
103     shift (fun _ => (1 : Module.End ℂ W)) (fun j => e (x j)) i
104   simp only [shift_apply]
105   split <;> simp_all
106 
107 /-- Twisting an atom twists the entire block, while leaving N fixed. -/
108 theorem scalar_twist (ν μ : G →* ℂˣ) (ρ σ : Representation ℂ G V)
109     (hσ : ∀ g, σ g = (μ g : ℂ) • ρ g) (m : ℕ) (g : G) :
110     action ν σ m g = (μ g : ℂ) • action ν ρ m g := by
111   apply LinearMap.ext
112   intro x
113   funext i
114   simp only [action_apply, hσ, LinearMap.smul_apply, Pi.smul_apply, smul_smul]
115   rw [mul_comm]
116 
117 end PaperXI.MonodromyAtom

Back to source controls