ScalarCovariance.lean

1 import PaperXI.MonodromyChain
2 
3 /-! Paper XI, Proposition 2.4. F = diag(1,q,...,q^(m-1)) as an actual
4 linear automorphism. q is a unit. The covariance factor is q⁻¹. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.ScalarCovariance
8 open PaperXI.MonodromyChain
9 
10 variable {K W : Type*} [Field K] [AddCommGroup W] [Module K W]
11 variable {m : ℕ}
12 
13 def frobenius (q : Kˣ) : (Fin m → W) ≃ₗ[K] (Fin m → W) where
14   toFun x i := (q : K) ^ i.val • x i
15   invFun x i := ((q⁻¹ : Kˣ) : K) ^ i.val • x i
16   left_inv x := by
17     funext i
18     simp [smul_smul]
19   right_inv x := by
20     funext i
21     simp [smul_smul]
22   map_add' x y := by funext i; exact smul_add _ _ _
23   map_smul' c x := by funext i; simp [smul_smul, mul_comm]
24 
25 @[simp] theorem frobenius_apply (q : Kˣ) (x : Fin m → W) (i : Fin m) :
26     frobenius q x i = (q : K) ^ i.val • x i := rfl
27 
28 /-- The pointwise covariance holds even for arbitrary linear transfers. -/
29 theorem covariance (q : Kˣ) (A : ℕ → Module.End K W) (x : Fin m → W) :
30     frobenius q (shift A x) = ((q⁻¹ : Kˣ) : K) • shift A (frobenius q x) := by
31   funext i
32   simp only [frobenius_apply, shift_apply, Pi.smul_apply]
33   split
34   · rename_i h
35     simp only [map_smul, smul_smul]
36     congr 1
37     simp [pow_succ, mul_comm]
38   · simp
39 
40 /-- Proposition 2.4, with F⁻¹ implemented by the inverse linear equivalence. -/
41 theorem conjugation (q : Kˣ) (A : ℕ → Module.End K W) :
42     (frobenius (m := m) q).conj (shift A) = ((q⁻¹ : Kˣ) : K) • shift A := by
43   apply LinearMap.ext
44   intro x
45   simpa using covariance q A ((frobenius q).symm x)
46 
47 /-- The printed scalar model is the case in which every transfer is the identity. -/
48 theorem scalar_model (q : Kˣ) :
49     (frobenius (W := K) (m := m) q).conj (shift fun _ => 1) =
50       ((q⁻¹ : Kˣ) : K) • (shift fun _ => 1) := conjugation q _
51 
52 end PaperXI.ScalarCovariance

Back to source controls