CyclicInducedCoordinates.lean

1 import Mathlib.RepresentationTheory.FiniteIndex
2 import Mathlib.LinearAlgebra.StdBasis
3 import Mathlib.Basic.Complex.Basic
4 
5 /-! Coordinates for genuine induction from the kernel of a finite quotient.
6 The representative indexed by `q` lies over `q⁻¹`, so the basis action is left translation.
7 -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CyclicInduced
11 open Representation
12 open scoped Classical
13 variable {G Q : Type*} [Group G] [Group Q]
14 variable (d : G →* Q) (r : Q → G) (hr : ∀ q, d (r q) = q⁻¹)
15 
16 /-- The one dimensional representation defined by a unit-valued character. -/
17 def scalar {H : Type*} [Group H] (χ : H →* ℂˣ) : Representation ℂ H ℂ where
18   toFun h := (χ h : ℂ) • LinearMap.id
19   map_one' := by ext; simp
20   map_mul' h k := by ext; simp [smul_smul, mul_comm]
21 
22 @[simp] theorem scalar_apply {H : Type*} [Group H] (χ : H →* ℂˣ)
23     (h : H) (a : ℂ) : scalar χ h a = (χ h : ℂ) * a := rfl
24 
25 /-- Kernel component in the decomposition `x = residual x * r ((d x)⁻¹)`. -/
26 def residual (x : G) : d.ker :=
27   ⟨x * (r (d x)⁻¹)⁻¹, by simp [MonoidHom.mem_ker, hr]⟩
28 
29 @[simp] theorem residual_rep (q : Q) : residual d r hr (r q) = 1 := by
30   apply Subtype.ext
31   simp [residual, hr]
32 
33 @[simp] theorem residual_mul (h : d.ker) (x : G) :
34     residual d r hr ((h : G) * x) = h * residual d r hr x := by
35   apply Subtype.ext
36   have hh : d h = 1 := h.property
37   simp [residual, hh, mul_assoc]
38 
39 variable (χ : d.ker →* ℂˣ)
40 abbrev CoindSpace := coindV d.ker.subtype (scalar χ)
41 abbrev coinduced := coind d.ker.subtype (scalar χ)
42 abbrev IndSpace := IndV d.ker.subtype (scalar χ)
43 abbrev induced := ind d.ker.subtype (scalar χ)
44 
45 /-- The covariant function reconstructed from its values on the representatives. -/
46 def extend (a : Q → ℂ) : CoindSpace d χ :=
47   ⟨fun x => (χ (residual d r hr x) : ℂ) * a (d x)⁻¹, by
48     intro h x
49     have hh : d h = 1 := h.property
50     simp [residual_mul, hh, scalar_apply, mul_assoc]⟩
51 
52 @[simp] theorem extend_rep (a : Q → ℂ) (q : Q) :
53     (extend d r hr χ a).1 (r q) = a q := by
54   simp [extend, hr]
55 
56 /-- Evaluation identifies the actual coinduced space with the coordinate space. -/
57 def coordinates : CoindSpace d χ ≃ₗ[ℂ] (Q → ℂ) where
58   toFun f q := f.1 (r q)
59   invFun := extend d r hr χ
60   left_inv f := by
61     apply Subtype.ext
62     funext x
63     change (χ (residual d r hr x) : ℂ) * f.1 (r (d x)⁻¹) = f.1 x
64     have h := f.property (residual d r hr x) (r (d x)⁻¹)
65     simpa [residual, scalar_apply] using h.symm
66   right_inv a := by funext q; exact extend_rep d r hr χ a q
67   map_add' f g := by rfl
68   map_smul' c f := by rfl
69 
70 @[simp] theorem coordinates_apply (f : CoindSpace d χ) (q : Q) :
71     coordinates d r hr χ f q = f.1 (r q) := rfl
72 
73 /-- The actual scalar in the monomial action, read from the group extension. -/
74 def weight (g : G) (q : Q) : ℂˣ :=
75   χ (residual d r hr (r (d g * q) * g))
76 
77 variable [Fintype Q]
78 
79 /-- The representative delta functions form a basis of actual coinduction. -/
80 def coindBasis : Module.Basis Q ℂ (CoindSpace d χ) :=
81   (Pi.basisFun ℂ Q).map (coordinates d r hr χ).symm
82 
83 @[simp] theorem coindBasis_rep (j q : Q) :
84     (coindBasis d r hr χ j).1 (r q) = if q = j then 1 else 0 := by
85   classical
86   change (extend d r hr χ ((Pi.basisFun ℂ Q) j)).1 (r q) = _
87   rw [extend_rep]
88   simp only [Pi.basisFun_apply]
89   by_cases h : q = j
90   · subst q; simp
91   · rw [ite_eq_right h, Pi.single_eq_of_ne h]
92 
93 /-- Monomial action on the genuine covariant-function basis. -/
94 theorem coindBasis_action (g : G) (j : Q) :
95     coinduced d χ g (coindBasis d r hr χ j) =
96       (weight d r hr χ g j : ℂ) • coindBasis d r hr χ (d g * j) := by
97   classical
98   apply (coordinates d r hr χ).injective
99   funext q
100   change (coindBasis d r hr χ j).1 (r q * g) =
101     (weight d r hr χ g j : ℂ) * (coindBasis d r hr χ (d g * j)).1 (r q)
102   have h := (coindBasis d r hr χ j).property
103     (residual d r hr (r q * g)) (r (d (r q * g))⁻¹)
104   have hv : (coindBasis d r hr χ j).1 (r q * g) =
105       (χ (residual d r hr (r q * g)) : ℂ) *
106       (if (d g)⁻¹ * q = j then 1 else 0) := by
107     simpa [residual, scalar_apply, hr, coindBasis_rep] using h
108   rw [hv, coindBasis_rep]
109   by_cases hq : q = d g * j
110   · subst q
111     simp [weight]
112   · have hn : (d g)⁻¹ * q ≠ j := by
113       intro he
114       apply hq
115       calc q = d g * ((d g)⁻¹ * q) := by simp
116            _ = d g * j := by rw [he]
117     simp [hq, hn]
118 
119 /-- The standard finite-index induction/coinduction equivalence. -/
120 def indCoind : (induced d χ).Equiv (coinduced d χ) := by
121   classical
122   exact Representation.equivOfIso (Rep.indCoindIso (Rep.of (scalar χ)))
123 
124 /-- An actual basis of induction, obtained from the canonical finite-index isomorphism. -/
125 def basis : Module.Basis Q ℂ (IndSpace d χ) :=
126   (coindBasis d r hr χ).map (indCoind d χ).toLinearEquiv.symm
127 
128 /-- Formula for the action on the actual induced representation, not an assumed model. -/
129 theorem basis_action (g : G) (j : Q) :
130     induced d χ g (basis d r hr χ j) =
131       (weight d r hr χ g j : ℂ) • basis d r hr χ (d g * j) := by
132   apply (indCoind d χ).injective
133   have hi := Representation.IntertwiningMap.isIntertwining (induced d χ) (coinduced d χ)
134     (indCoind d χ).toIntertwiningMap g (basis d r hr χ j)
135   change (indCoind d χ).toLinearEquiv _ = coinduced d χ g ((indCoind d χ).toLinearEquiv _) at hi
136   rw [hi]
137   simp only [basis, Module.Basis.map_apply, LinearEquiv.apply_symm_apply,
138     map_smul]
139   exact coindBasis_action d r hr χ g j
140 
141 /-- Conjugation by a representative restricts to the normal kernel. -/
142 def conjugate (q : Q) : d.ker →* d.ker where
143   toFun h := ⟨r q * (h : G) * (r q)⁻¹, by
144     have hh : d h = 1 := h.property
145     simp [MonoidHom.mem_ker, hh]⟩
146   map_one' := by apply Subtype.ext; simp
147   map_mul' h k := by apply Subtype.ext; simp [mul_assoc]
148 
149 /-- The inertia character visible on the corresponding basis line. -/
150 def conjugateCharacter (q : Q) : d.ker →* ℂˣ :=
151   χ.comp (conjugate d r q)
152 
153 omit [Fintype Q] in
154 @[simp] theorem weight_kernel (h : d.ker) (j : Q) :
155     weight d r hr χ h j = conjugateCharacter d r χ j h := by
156   have hh : d h = 1 := h.property
157   change χ (residual d r hr (r (d h * j) * h)) = χ (conjugate d r j h)
158   apply congrArg χ
159   apply Subtype.ext
160   simp [residual, conjugate, hh, hr]
161 
162 /-- Kernel elements act diagonally by the conjugated character. -/
163 theorem basis_action_kernel (h : d.ker) (j : Q) :
164     induced d χ h (basis d r hr χ j) =
165       (conjugateCharacter d r χ j h : ℂ) • basis d r hr χ j := by
166   have hh : d h = 1 := h.property
167   simpa [hh] using basis_action d r hr χ (h : G) j
168 
169 /-- With the identity representative normalized, its line carries the original character. -/
170 theorem basis_action_origin (hr1 : r 1 = 1) (h : d.ker) :
171     induced d χ h (basis d r hr χ 1) = (χ h : ℂ) • basis d r hr χ 1 := by
172   rw [basis_action_kernel]
173   have hc : conjugateCharacter d r χ 1 h = χ h := by
174     apply congrArg χ
175     apply Subtype.ext
176     simp [conjugate, hr1]
177   rw [hc]
178 
179 end PaperXI.CyclicInduced

Back to source controls