InducedClassification.lean

1 import PaperXI.InducedDual
2 import PaperXI.CyclicInducedWrap
3 
4 /-! Classification uses the full subgroup characters, including return values.
5 No assertion identifies an abstract degree subgroup with a local Weil group. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.InducedClassification
9 open PaperXI.CyclicInduced PaperXI.InducedDual
10 open scoped Classical
11 variable {G Q : Type*} [Group G] [Group Q] [Fintype Q]
12 variable (d : G →* Q) (r : Q → G) (hr : ∀ q, d (r q) = q⁻¹)
13 
14 omit [Fintype Q] in
15 include hr in
16 theorem index_transitive (j k : Q) : ∃ g : G, indexAction d g j = k := by
17   refine ⟨(r (k * j⁻¹))⁻¹, ?_⟩
18   change d ((r (k * j⁻¹))⁻¹) * j = k
19   simp [hr, mul_assoc]
20 
21 omit [Fintype Q] in
22 theorem index_stabilizer (j : Q) (g : G) : g ∈ d.ker ↔ indexAction d g j = j := by
23   change d g = 1 ↔ d g * j = j
24   constructor
25   · intro h; simp [h]
26   · intro h; exact mul_right_cancel (h.trans (one_mul j).symm)
27 
28 /-- Changing the distinguished coset line gives actual induction of its conjugate character. -/
29 def conjugateEquiv (ψ : d.ker →* ℂˣ) (j : Q) :
30     Representation.Equiv (induced d (conjugateCharacter d r ψ j)) (induced d ψ) :=
31   MonomialInduction.transitiveEquivalenceOfSubgroupAction
32     (induced d ψ) (basis d r hr ψ) (indexAction d) (weight d r hr ψ)
33     (fun g k => basis_action d r hr ψ g k) j
34     (index_transitive d r hr j) d.ker (conjugateCharacter d r ψ j)
35     (index_stabilizer d j) (fun h => basis_action_kernel d r hr ψ h j)
36 
37 /-- Coefficients of a subgroup action are its actual diagonal characters. -/
38 theorem coefficient_action (ψ : d.ker →* ℂˣ) (h : d.ker) (j : Q) (v : IndSpace d ψ) :
39     (basis d r hr ψ).repr (induced d ψ h v) j =
40       (conjugateCharacter d r ψ j h : ℂ) * (basis d r hr ψ).repr v j := by
41   have he : ((basis d r hr ψ).coord j).comp (induced d ψ h) =
42       (conjugateCharacter d r ψ j h : ℂ) • (basis d r hr ψ).coord j := by
43     apply (basis d r hr ψ).ext
44     intro k
45     change (basis d r hr ψ).repr (induced d ψ h (basis d r hr ψ k)) j =
46       (conjugateCharacter d r ψ j h : ℂ) * (basis d r hr ψ).repr (basis d r hr ψ k) j
47     rw [basis_action_kernel]
48     by_cases hk : k = j
49     · subst k
50       simp
51     · simp [hk]
52   exact LinearMap.congr_fun he v
53 
54 include hr in
55 /-- A nonzero coefficient of the image of the original character line detects a conjugate. -/
56 theorem character_of_equiv (hr1 : r 1 = 1) (χ ψ : d.ker →* ℂˣ)
57     (e : Representation.Equiv (induced d χ) (induced d ψ)) :
58     ∃ j : Q, χ = conjugateCharacter d r ψ j := by
59   have hv : e (basis d r hr χ 1) ≠ 0 := by
60     intro h
61     exact (basis d r hr χ).ne_zero 1 (e.injective (h.trans e.map_zero.symm))
62   obtain ⟨j, hj⟩ : ∃ j : Q, (basis d r hr ψ).repr (e (basis d r hr χ 1)) j ≠ 0 := by
63     by_contra hn
64     simp only [not_exists, not_not] at hn
65     apply hv
66     apply (basis d r hr ψ).repr.injective
67     ext j
68     simpa using hn j
69   refine ⟨j, ?_⟩
70   apply MonoidHom.ext
71   intro h
72   apply Units.ext
73   have he := LinearMap.congr_fun (e.isIntertwining' (h : G)) (basis d r hr χ 1)
74   change e (induced d χ h (basis d r hr χ 1)) =
75     induced d ψ h (e (basis d r hr χ 1)) at he
76   rw [basis_action_origin d r hr χ hr1, map_smul] at he
77   have hc := congrArg (fun v => (basis d r hr ψ).repr v j) he
78   rw [coefficient_action d r hr ψ] at hc
79   simp only [map_smul, Finsupp.smul_apply, smul_eq_mul] at hc
80   exact mul_right_cancel₀ hj hc
81 
82 include hr in
83 /-- Equality of induction classes is exactly conjugacy of full inducing characters. -/
84 theorem equiv_iff (hr1 : r 1 = 1) (χ ψ : d.ker →* ℂˣ) :
85     Nonempty (Representation.Equiv (induced d χ) (induced d ψ)) ↔
86       ∃ j : Q, χ = conjugateCharacter d r ψ j := by
87   constructor
88   · rintro ⟨e⟩; exact character_of_equiv d r hr hr1 χ ψ e
89   · rintro ⟨j, rfl⟩; exact ⟨conjugateEquiv d r hr ψ j⟩
90 
91 include hr in
92 /-- Dual induction together with classification gives the full self-duality criterion. -/
93 theorem selfDual_iff (hr1 : r 1 = 1) (χ : d.ker →* ℂˣ) :
94     Nonempty (Representation.Equiv (induced d χ).dual (induced d χ)) ↔
95       ∃ j : Q, χ⁻¹ = conjugateCharacter d r χ j := by
96   constructor
97   · rintro ⟨e⟩
98     exact (equiv_iff d r hr hr1 (χ⁻¹) χ).mp
99       ⟨(inverseCharacterEquiv d r hr χ).trans e⟩
100   · intro h
101     obtain ⟨e⟩ := (equiv_iff d r hr hr1 (χ⁻¹) χ).mpr h
102     exact ⟨(inverseCharacterEquiv d r hr χ).symm.trans e⟩
103 
104 section Degree
105 variable (δ : G →* Multiplicative ℤ) (φ : G)
106 variable (hφ : δ φ = Multiplicative.ofAdd (1 : ℤ)) (n : ℕ) [NeZero n]
107 variable (ξ : TameDegree.degreeSubgroup δ n →* ℂˣ)
108 
109 /-- Source-facing dual equivalence on the degree-subgroup induction. -/
110 def degreeDualEquiv : Representation.Equiv
111     (degreeInduced δ n ξ).dual (degreeInduced δ n (ξ⁻¹)) :=
112   (inverseCharacterEquiv (TameDegree.degreeMod δ n) (cyclicRep φ)
113     (cyclicRep_degree _ φ (by
114       change Multiplicative.ofAdd (((δ φ).toAdd : ℤ) : ZMod n) = _
115       rw [hφ]
116       simp)) ξ).symm
117 
118 include hφ in
119 /-- Full character equality, not equality merely on inertia, detects self-duality. -/
120 theorem degreeSelfDual_iff :
121     Nonempty (Representation.Equiv (degreeInduced δ n ξ).dual (degreeInduced δ n ξ)) ↔
122       ∃ j : ZMod n, ξ⁻¹ = degreeCharacter δ φ n ξ j := by
123   have hh := selfDual_iff (TameDegree.degreeMod δ n) (cyclicRep φ)
124     (cyclicRep_degree _ φ (by
125       change Multiplicative.ofAdd (((δ φ).toAdd : ℤ) : ZMod n) = _
126       rw [hφ]
127       simp)) (cyclicRep_one φ) ξ
128   constructor
129   · intro h
130     obtain ⟨j, hj⟩ := hh.mp h
131     exact ⟨j.toAdd, hj⟩
132   · rintro ⟨j, hj⟩
133     exact hh.mpr ⟨Multiplicative.ofAdd j, hj⟩
134 
135 end Degree
136 end PaperXI.InducedClassification

Back to source controls