InducedDual.lean

1 import PaperXI.MonomialDual
2 import PaperXI.CyclicInducedCoordinates
3 import PaperXI.MonomialInductionSubgroup
4 
5 /-! Duality and the full-character classification for induction from a finite normal quotient. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.InducedDual
9 open PaperXI.CyclicInduced
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 /-- The index permutation is genuine left multiplication in the quotient. -/
15 def indexAction : G →* Equiv.Perm Q where
16   toFun g := Equiv.mulLeft (d g)
17   map_one' := by ext q; simp
18   map_mul' g h := by ext q; simp
19 
20 omit [Fintype Q] in
21 @[simp] theorem indexAction_apply (g : G) (q : Q) : indexAction d g q = d g * q := rfl
22 
23 variable (χ : d.ker →* ℂˣ)
24 
25 /-- Induction of the inverse character identifies with the actual dual representation. -/
26 def inverseCharacterEquiv : Representation.Equiv (induced d (χ⁻¹)) (induced d χ).dual :=
27   Representation.Equiv.mk
28     ((basis d r hr (χ⁻¹)).equiv (basis d r hr χ).dualBasis (Equiv.refl Q))
29     (fun g => by
30       apply (basis d r hr (χ⁻¹)).ext
31       intro j
32       change (basis d r hr (χ⁻¹)).equiv (basis d r hr χ).dualBasis (Equiv.refl Q)
33         (induced d (χ⁻¹) g (basis d r hr (χ⁻¹) j)) =
34         (induced d χ).dual g
35           ((basis d r hr (χ⁻¹)).equiv (basis d r hr χ).dualBasis (Equiv.refl Q)
36             (basis d r hr (χ⁻¹) j))
37       rw [basis_action, map_smul, Module.Basis.equiv_apply, Module.Basis.equiv_apply]
38       rw [MonomialDual.dual_basis_action (induced d χ) (basis d r hr χ)
39         (indexAction d) (weight d r hr χ) (fun g j => basis_action d r hr χ g j)]
40       rfl)
41 
42 end PaperXI.InducedDual

Back to source controls