ProjectorTransport.lean

1 import Mathlib.LinearAlgebra.Pi
2 import Mathlib.Tactic
3 
4 /-! Exact reindexing law underlying the Frobenius covariance in Proposition 3.1.
5 This does not yet prove Fourier idempotence or the Weil-group realization.
6 The character weight transforms by the inverse permutation. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.ProjectorTransport
10 open scoped BigOperators
11 
12 variable {K V G : Type*} [Field K] [AddCommGroup V] [Module K V] [Fintype G]
13 
14 theorem weighted_sum_conjugation (e : G ≃ G) (F : V ≃ₗ[K] V)
15     (T : G → Module.End K V) (w : G → K)
16     (h : ∀ g, F.conj (T g) = T (e g)) :
17     F.conj (∑ g, w g • T g) = ∑ g, w (e.symm g) • T g := by
18   simp only [map_sum, map_smul, h]
19   simpa using (Equiv.sum_comp e (fun g => w (e.symm g) • T g))
20 
21 theorem normalized_sum_conjugation (e : G ≃ G) (F : V ≃ₗ[K] V)
22     (T : G → Module.End K V) (w : G → K) (c : K)
23     (h : ∀ g, F.conj (T g) = T (e g)) :
24     F.conj (c • ∑ g, w g • T g) = c • ∑ g, w (e.symm g) • T g := by
25   rw [map_smul, weighted_sum_conjugation e F T w h]
26 
27 end PaperXI.ProjectorTransport

Back to source controls