MonomialOrbit.lean

1 import PaperXI.MonomialAction
2 import Mathlib.RepresentationTheory.Intertwining
3 import Mathlib.LinearAlgebra.StdBasis
4 import Mathlib.LinearAlgebra.DirectSum.Basis
5 
6 /-! Decomposition of an actual monomial representation along actual invariant
7 basis orbits. The direct sum and its representation equivalence are constructed. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.MonomialOrbit
11 open scoped DirectSum
12 open scoped Classical
13 
14 variable {G X I Y V : Type*} [Group G] [Fintype Y]
15 variable [AddCommGroup V] [Module ℂ V]
16 variable (ρ : Representation ℂ G V) (b : Module.Basis X ℂ V)
17 variable (p : G →* Equiv.Perm X) (c : G → X → ℂˣ)
18 variable (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x))
19 variable (e : I × Y ≃ X) (q : I → G →* Equiv.Perm Y)
20 variable (he : ∀ g i y, p g (e (i,y)) = e (i,q i g y))
21 
22 /-- Each invariant orbit has the actual restricted basis action. -/
23 def block (i : I) : Representation ℂ G (Y → ℂ) :=
24   MonomialAction.representation (Pi.basisFun ℂ Y) (q i) (fun g y => c g (e (i,y)))
25     (fun y => MonomialAction.weight_one b p c ρ hρ (e (i,y)))
26     (fun g h y => by
27       rw [MonomialAction.weight_mul b p c ρ hρ, he])
28 
29 @[simp] theorem block_basis (i : I) (g : G) (y : Y) :
30     block ρ b p c hρ e q he i g (Pi.basisFun ℂ Y y) =
31       (c g (e (i,y)) : ℂ) • Pi.basisFun ℂ Y (q i g y) :=
32   MonomialAction.representation_basis _ _ _ _ _ g y
33 
34 @[simp] theorem block_single (i : I) (g : G) (y : Y) :
35     block ρ b p c hρ e q he i g (Pi.single y 1) =
36       (c g (e (i,y)) : ℂ) • Pi.single (q i g y) 1 := by
37   simpa only [Pi.basisFun_apply] using block_basis ρ b p c hρ e q he i g y
38 
39 /-- The basis of the literal direct sum of orbit spaces. -/
40 def sumBasis : Module.Basis (I × Y) ℂ (⨁ _ : I, Y → ℂ) :=
41   (DFinsupp.basis (fun _ : I => Pi.basisFun ℂ Y)).reindex (Equiv.sigmaEquivProd I Y)
42 
43 @[simp] theorem sumBasis_apply (i : I) (y : Y) :
44     sumBasis (I := I) (Y := Y) (i,y) =
45       DirectSum.lof ℂ I (fun _ => Y → ℂ) i (Pi.basisFun ℂ Y y) := by
46   simp [sumBasis, DFinsupp.basis]
47   rfl
48 
49 /-- The actual basis reindexing, not a dimension-only comparison. -/
50 def linearEquiv : V ≃ₗ[ℂ] (⨁ _ : I, Y → ℂ) :=
51   b.equiv sumBasis e.symm
52 
53 @[simp] theorem linearEquiv_basis (i : I) (y : Y) :
54     linearEquiv b e (b (e (i,y))) = sumBasis (I := I) (Y := Y) (i,y) := by
55   simp [linearEquiv]
56 
57 /-- Every original group operator is intertwined with the direct sum of
58 constructed orbit actions. -/
59 theorem intertwines (g : G) (v : V) :
60     linearEquiv b e (ρ g v) =
61       Representation.directSum (block ρ b p c hρ e q he) g (linearEquiv b e v) := by
62   have h : (linearEquiv b e).toLinearMap.comp (ρ g) =
63       (Representation.directSum (block ρ b p c hρ e q he) g).comp
64         (linearEquiv b e).toLinearMap := by
65     apply b.ext
66     intro x
67     obtain ⟨⟨i,y⟩, rfl⟩ := e.surjective x
68     simp [hρ, he, Representation.directSum]
69   exact DFunLike.congr_fun h v
70 
71 /-- Representation equivalence with the actual direct sum of orbit modules. -/
72 def representationEquiv : Representation.Equiv ρ
73     (Representation.directSum (block ρ b p c hρ e q he)) := by
74   let F : Representation.IntertwiningMap ρ (Representation.directSum (block ρ b p c hρ e q he)) :=
75     ⟨(linearEquiv b e).toLinearMap, fun g => LinearMap.ext (intertwines ρ b p c hρ e q he g)⟩
76   exact F.ofBijective (linearEquiv b e).bijective
77 
78 /-- Each constructed interaction summand has the actual coordinate dimension. -/
79 theorem block_finrank : Module.finrank ℂ (Y → ℂ) = Fintype.card Y := by
80   simp
81 
82 end PaperXI.MonomialOrbit

Back to source controls