MonomialDual.lean

1 import PaperXI.MonomialAction
2 import Mathlib.LinearAlgebra.Dual.Basis
3 
4 /-! The contragredient of a genuine monomial representation on the dual basis. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.MonomialDual
8 open scoped Classical
9 variable {G X V : Type*} [Group G] [Fintype X]
10 variable [AddCommGroup V] [Module ℂ V]
11 variable (ρ : Representation ℂ G V) (b : Module.Basis X ℂ V)
12 variable (p : G →* Equiv.Perm X) (c : G → X → ℂˣ)
13 variable (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x))
14 
15 include hρ in
16 omit [Fintype X] in
17 /-- Inverse-step coefficients are consequences of the original representation law. -/
18 theorem inverse_weight (g : G) (j : X) :
19     c g⁻¹ (p g j) = (c g j)⁻¹ := by
20   apply eq_inv_iff_mul_eq_one.mpr
21   rw [← MonomialAction.weight_mul b p c ρ hρ, inv_mul_cancel,
22     MonomialAction.weight_one b p c ρ hρ]
23 
24 include hρ in
25 /-- This identity uses the actual contragredient action, not merely inverse labels. -/
26 theorem dual_basis_action (g : G) (j : X) :
27     ρ.dual g (b.dualBasis j) = ((c g j)⁻¹ : ℂˣ) • b.dualBasis (p g j) := by
28   apply b.ext
29   intro k
30   change b.dualBasis j (ρ g⁻¹ (b k)) =
31     (((c g j)⁻¹ : ℂˣ) : ℂ) * b.dualBasis (p g j) (b k)
32   rw [hρ, map_smul, b.dualBasis_apply_self, b.dualBasis_apply_self]
33   by_cases hk : k = p g j
34   · subst k
35     have hp : p g⁻¹ (p g j) = j := by simp
36     rw [hp, inverse_weight ρ b p c hρ]
37     simp
38   · have hn : p g⁻¹ k ≠ j := by
39       intro h
40       apply hk
41       have hh := congrArg (p g) h
42       simpa using hh
43     rw [ite_eq_right hn, ite_eq_right hk]
44     simp
45 
46 end PaperXI.MonomialDual

Back to source controls