TameTensorPackets.lean

1 import PaperXI.MonomialOrbit
2 import PaperXI.TameDegree
3 
4 /-! Actual gcd/lcm decomposition of tensor representations with cyclic monomial
5 bases. The bases may belong to nonregular or reducible induced representations. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TameTensorPackets
9 open scoped TensorProduct DirectSum Classical
10 
11 variable {G V W : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
12 variable [AddCommGroup W] [Module ℂ W]
13 variable (ν : G →* Multiplicative ℤ) (n m : ℕ) [NeZero n] [NeZero m]
14 variable (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
15 variable (b : Module.Basis (ZMod n) ℂ V) (d : Module.Basis (ZMod m) ℂ W)
16 variable (a : G → ZMod n → ℂˣ) (w : G → ZMod m → ℂˣ)
17 variable (hρ : ∀ g x, ρ g (b x) = (a g x : ℂ) • b (TameDegree.translationAction ν n g x))
18 variable (hσ : ∀ g y, σ g (d y) = (w g y : ℂ) • d (TameDegree.translationAction ν m g y))
19 
20 /-- Coefficients of the actual tensor basis. -/
21 def coefficient (g : G) (x : ZMod n × ZMod m) : ℂˣ := a g x.1 * w g x.2
22 
23 include hρ hσ in
24 omit [NeZero n] [NeZero m] in
25 /-- The literal tensor basis is monomial for the actual simultaneous action. -/
26 theorem tensor_action (g : G) (x : ZMod n × ZMod m) :
27     (ρ.tprod σ) g (b.tensorProduct d x) =
28       (coefficient n m a w g x : ℂ) • b.tensorProduct d (TameDegree.pairAction ν n m g x) :=
29   MonomialAction.tensor_basis b (TameDegree.translationAction ν n) a ρ σ d
30     (TameDegree.translationAction ν m) w hρ hσ g x
31 
32 /-- The actual orbit equivalence respects the group action. -/
33 theorem orbit_covariance (g : G) (i : Fin (Nat.gcd n m)) (y : ZMod (Nat.lcm n m)) :
34     TameDegree.pairAction ν n m g (TameTensorOrbits.orbitEquiv n m (i,y)) =
35       TameTensorOrbits.orbitEquiv n m (i,TameDegree.translationAction ν (Nat.lcm n m) g y) :=
36   (TameDegree.orbitEquiv_intertwines ν n m g (i,y)).symm
37 
38 /-- One actual interaction representation for each gcd orbit. -/
39 def packet (i : Fin (Nat.gcd n m)) : Representation ℂ G (ZMod (Nat.lcm n m) → ℂ) :=
40   MonomialOrbit.block (ρ.tprod σ) (b.tensorProduct d) (TameDegree.pairAction ν n m)
41     (coefficient n m a w) (tensor_action ν n m ρ σ b d a w hρ hσ)
42     (TameTensorOrbits.orbitEquiv n m) (fun _ => TameDegree.translationAction ν (Nat.lcm n m))
43     (orbit_covariance ν n m) i
44 
45 /-- The decomposition is an equivalence of actual representations, not just dimensions. -/
46 def decomposition : Representation.Equiv (ρ.tprod σ)
47     (Representation.directSum (packet ν n m ρ σ b d a w hρ hσ)) :=
48   MonomialOrbit.representationEquiv (ρ.tprod σ) (b.tensorProduct d) (TameDegree.pairAction ν n m)
49     (coefficient n m a w) (tensor_action ν n m ρ σ b d a w hρ hσ)
50     (TameTensorOrbits.orbitEquiv n m) (fun _ => TameDegree.translationAction ν (Nat.lcm n m))
51     (orbit_covariance ν n m)
52 
53 /-- Exact action inside the interaction packet. -/
54 theorem packet_basis (i : Fin (Nat.gcd n m)) (g : G) (y : ZMod (Nat.lcm n m)) :
55     packet ν n m ρ σ b d a w hρ hσ i g (Pi.basisFun ℂ (ZMod (Nat.lcm n m)) y) =
56       (coefficient n m a w g (TameTensorOrbits.orbitEquiv n m (i,y)) : ℂ) •
57         Pi.basisFun ℂ (ZMod (Nat.lcm n m)) (TameDegree.translationAction ν (Nat.lcm n m) g y) :=
58   MonomialOrbit.block_basis _ _ _ _ _ _ _ _ i g y
59 
60 /-- The packet at orbit `(0,i)` has the product of the actual factor-line coefficients. -/
61 theorem packet_zero (i : Fin (Nat.gcd n m))
62     (g : TameDegree.degreeSubgroup ν (Nat.lcm n m)) :
63     packet ν n m ρ σ b d a w hρ hσ i g (Pi.basisFun ℂ (ZMod (Nat.lcm n m)) 0) =
64       ((a g 0 * w g (i.val : ZMod m) : ℂˣ) : ℂ) • Pi.basisFun ℂ (ZMod (Nat.lcm n m)) 0 := by
65   rw [packet_basis, (TameDegree.translationAction_fixed_iff ν _ g 0).mpr g.property]
66   simp [TameTensorOrbits.orbitMap_zero, coefficient]
67 
68 omit [NeZero n] [NeZero m] in
69 /-- There are exactly gcd-many constructed interaction summands. -/
70 theorem packet_count : Fintype.card (Fin (Nat.gcd n m)) = Nat.gcd n m := Fintype.card_fin _
71 
72 /-- Every actual interaction carrier has dimension lcm, including nonregular products. -/
73 theorem packet_dimension : Module.finrank ℂ (ZMod (Nat.lcm n m) → ℂ) = Nat.lcm n m := by simp
74 
75 /-- The dimensions of these constructed summands sum to the original tensor dimension. -/
76 theorem dimension_sum : (∑ _ : Fin (Nat.gcd n m),
77     Module.finrank ℂ (ZMod (Nat.lcm n m) → ℂ)) = n*m := by
78   simp only [packet_dimension, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
79   exact Nat.gcd_mul_lcm n m
80 
81 end PaperXI.TameTensorPackets

Back to source controls