InducedTwist.lean

1 import PaperXI.CharacterTwist
2 import PaperXI.CyclicInducedWrap
3 
4 /-! The projection formula on actual induced spaces, with inertia and return scalars. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.InducedTwist
8 open PaperXI.CyclicInduced
9 open PaperXI.CharacterTwist
10 variable {G Q : Type*} [Group G] [Group Q]
11 variable (d : G →* Q) (χ : d.ker →* ℂˣ) (ν : G →* ℂˣ)
12 
13 /-- The product character on the actual inducing subgroup. -/
14 def character : d.ker →* ℂˣ := χ * ν.comp d.ker.subtype
15 
16 @[simp] theorem character_apply (h : d.ker) :
17     character d χ ν h = χ h * ν h := rfl
18 
19 /-- Multiplication by the ambient character respects covariant-function equations. -/
20 def forward (f : CoindSpace d χ) : CoindSpace d (character d χ ν) :=
21   ⟨fun x => (ν x : ℂ) * f.1 x, by
22     intro h x
23     change (ν ((h : G) * x) : ℂ) * f.1 ((h : G) * x) =
24       ((χ h * ν h : ℂˣ) : ℂ) * ((ν x : ℂ) * f.1 x)
25     have hf := f.property h x
26     change f.1 ((h : G) * x) = (χ h : ℂ) * f.1 x at hf
27     rw [hf]
28     simp [mul_assoc, mul_comm, mul_left_comm]⟩
29 
30 /-- The inverse multiplies by the inverse ambient character pointwise. -/
31 def backward (f : CoindSpace d (character d χ ν)) : CoindSpace d χ :=
32   ⟨fun x => (ν x : ℂ)⁻¹ * f.1 x, by
33     intro h x
34     change (ν ((h : G) * x) : ℂ)⁻¹ * f.1 ((h : G) * x) =
35       (χ h : ℂ) * ((ν x : ℂ)⁻¹ * f.1 x)
36     have hf := f.property h x
37     change f.1 ((h : G) * x) = ((χ h * ν h : ℂˣ) : ℂ) * f.1 x at hf
38     rw [hf]
39     simp only [map_mul, Units.val_mul, mul_inv_rev]
40     field_simp⟩
41 
42 /-- A linear equivalence between the actual covariant function spaces. -/
43 def coindLinearEquiv : CoindSpace d χ ≃ₗ[ℂ] CoindSpace d (character d χ ν) where
44   toFun := forward d χ ν
45   invFun := backward d χ ν
46   left_inv f := by apply Subtype.ext; funext x; simp [forward, backward]
47   right_inv f := by apply Subtype.ext; funext x; simp [forward, backward]
48   map_add' f g := by apply Subtype.ext; funext x; simp [forward, mul_add]
49   map_smul' a f := by apply Subtype.ext; funext x; simp [forward, mul_left_comm]
50 
51 /-- Right translation intertwines the pointwise multiplier with scalar twisting. -/
52 def coindEquiv : Representation.Equiv (twist ν (coinduced d χ))
53     (coinduced d (character d χ ν)) :=
54   Representation.Equiv.mk (coindLinearEquiv d χ ν) (fun g => by
55     ext f x
56     change (ν x : ℂ) * ((ν g : ℂ) * f.1 (x*g)) = (ν (x*g) : ℂ) * f.1 (x*g)
57     simp [mul_assoc])
58 
59 variable [Fintype Q]
60 
61 /-- The projection formula for genuine Mathlib induction from the finite-index kernel. -/
62 def inducedEquiv : Representation.Equiv
63     ((induced d χ).tprod (scalar ν)) (induced d (character d χ ν)) :=
64   (tensorEquiv ν (induced d χ)).trans
65     ((mapEquiv ν (indCoind d χ)).trans
66       ((coindEquiv d χ ν).trans (indCoind d (character d χ ν)).symm))
67 
68 section Degree
69 variable (δ : G →* Multiplicative ℤ) (φ : G)
70 variable (hφ : δ φ = Multiplicative.ofAdd (1 : ℤ)) (n : ℕ) [NeZero n]
71 variable (ξ : TameDegree.degreeSubgroup δ n →* ℂˣ)
72 
73 /-- The unramified-twist induction formula for the degree-divisibility subgroup. -/
74 def degreeEquiv : Representation.Equiv
75     ((degreeInduced δ n ξ).tprod (scalar ν))
76     (degreeInduced δ n (character (TameDegree.degreeMod δ n) ξ ν)) :=
77   inducedEquiv (TameDegree.degreeMod δ n) ξ ν
78 
79 omit [NeZero n] in
80 /-- The value at the genuine period element is multiplied by the n-th character power. -/
81 theorem period_value :
82     character (TameDegree.degreeMod δ n) ξ ν (degreePeriod φ δ hφ) =
83       ξ (degreePeriod φ δ hφ) * ν φ ^ n := by
84   change ξ (degreePeriod φ δ hφ) * ν (φ ^ (n : ℤ)) = _
85   simp
86 
87 /-- The closing scalar is computed on the last basis vector of the twisted induction. -/
88 theorem closing_basis (j : ZMod n) (hj : j.val + 1 = n) :
89     degreeInduced δ n (character (TameDegree.degreeMod δ n) ξ ν) φ
90       (degreeBasis δ φ hφ n (character (TameDegree.degreeMod δ n) ξ ν) j) =
91     ((ξ (degreePeriod φ δ hφ) * ν φ ^ n : ℂˣ) : ℂ) •
92       degreeBasis δ φ hφ n (character (TameDegree.degreeMod δ n) ξ ν) 0 := by
93   erw [degreeBasis_phi_of_last φ δ hφ _ j hj, period_value]
94 
95 omit [NeZero n] in
96 /-- Unramified means trivial on the specified inertia subgroup; its action is unchanged. -/
97 theorem inertia_unchanged (I : Subgroup G) (hν : ∀ h : I, ν h = 1) :
98     (twist ν (degreeInduced δ n ξ)).comp I.subtype =
99       (degreeInduced δ n ξ).comp I.subtype :=
100   restrict_eq ν (degreeInduced δ n ξ) I hν
101 
102 end Degree
103 end PaperXI.InducedTwist

Back to source controls