TameTensorInduction.lean

1 import PaperXI.TameTensorPackets
2 import PaperXI.MonomialInductionSubgroup
3 
4 /-! Actual induction of the interaction packets and the tensor decomposition. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.TameTensorInduction
8 open scoped DirectSum Classical
9 
10 variable {G V W : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
11 variable [AddCommGroup W] [Module ℂ W]
12 variable (ν : G →* Multiplicative ℤ) (n m : ℕ) [NeZero n] [NeZero m]
13 variable (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
14 variable (b : Module.Basis (ZMod n) ℂ V) (d : Module.Basis (ZMod m) ℂ W)
15 variable (a : G → ZMod n → ℂˣ) (w : G → ZMod m → ℂˣ)
16 variable (hρ : ∀ g x, ρ g (b x) = (a g x : ℂ) • b (TameDegree.translationAction ν n g x))
17 variable (hσ : ∀ g y, σ g (d y) = (w g y : ℂ) • d (TameDegree.translationAction ν m g y))
18 
19 /-- The product weight on the interaction line is an actual group character. -/
20 def character (i : Fin (Nat.gcd n m)) :
21     TameDegree.degreeSubgroup ν (Nat.lcm n m) →* ℂˣ where
22   toFun g := a g 0 * w g (i.val : ZMod m)
23   map_one' := by
24     apply Units.ext
25     apply LineCharacter.scalar_unique ((Pi.basisFun ℂ (ZMod (Nat.lcm n m))).ne_zero 0)
26     rw [← TameTensorPackets.packet_zero ν n m ρ σ b d a w hρ hσ i 1]
27     simp
28   map_mul' g h := by
29     apply Units.ext
30     apply LineCharacter.scalar_unique ((Pi.basisFun ℂ (ZMod (Nat.lcm n m))).ne_zero 0)
31     rw [← TameTensorPackets.packet_zero ν n m ρ σ b d a w hρ hσ i (g*h)]
32     change TameTensorPackets.packet ν n m ρ σ b d a w hρ hσ i ((g : G)*(h : G))
33       (Pi.basisFun ℂ (ZMod (Nat.lcm n m)) 0) = _
34     rw [map_mul, Module.End.mul_apply,
35       TameTensorPackets.packet_zero ν n m ρ σ b d a w hρ hσ i h, map_smul,
36       TameTensorPackets.packet_zero ν n m ρ σ b d a w hρ hσ i g]
37     simp [smul_smul, mul_comm]
38 
39 @[simp] theorem character_apply (i : Fin (Nat.gcd n m))
40     (g : TameDegree.degreeSubgroup ν (Nat.lcm n m)) :
41     character ν n m ρ σ b d a w hρ hσ i g = a g 0 * w g (i.val : ZMod m) := rfl
42 
43 variable (φ : G) (hφ : ν φ = Multiplicative.ofAdd (1 : ℤ))
44 
45 omit [NeZero n] [NeZero m] in
46 include hφ in
47 /-- Degree-one powers act transitively on the actual lcm cycle. -/
48 theorem cycle_transitive (x : ZMod (Nat.lcm n m)) :
49     ∃ g : G, TameDegree.translationAction ν (Nat.lcm n m) g 0 = x := by
50   obtain ⟨k, hk⟩ := ZMod.intCast_surjective x
51   refine ⟨φ ^ k, ?_⟩
52   rw [TameDegree.translationAction_phi_zpow ν φ hφ, zero_add, hk]
53 
54 /-- Each packet is the actual induced representation of its interaction character. -/
55 def packetEquivalence (i : Fin (Nat.gcd n m)) : Representation.Equiv
56     (Representation.ind (TameDegree.degreeSubgroup ν (Nat.lcm n m)).subtype
57       (MonomialInduction.scalarRepresentation (character ν n m ρ σ b d a w hρ hσ i)))
58     (TameTensorPackets.packet ν n m ρ σ b d a w hρ hσ i) :=
59   MonomialInduction.transitiveEquivalenceOfSubgroupAction
60     (TameTensorPackets.packet ν n m ρ σ b d a w hρ hσ i)
61     (Pi.basisFun ℂ (ZMod (Nat.lcm n m))) (TameDegree.translationAction ν (Nat.lcm n m))
62     (fun g y => TameTensorPackets.coefficient n m a w g (TameTensorOrbits.orbitEquiv n m (i,y)))
63     (TameTensorPackets.packet_basis ν n m ρ σ b d a w hρ hσ i) 0
64     (cycle_transitive ν n m φ hφ) (TameDegree.degreeSubgroup ν (Nat.lcm n m))
65     (character ν n m ρ σ b d a w hρ hσ i)
66     (fun g => (TameDegree.translationAction_fixed_iff ν (Nat.lcm n m) g 0).symm)
67     (TameTensorPackets.packet_zero ν n m ρ σ b d a w hρ hσ i)
68 
69 /-- Component representation equivalences induce an actual direct sum equivalence. -/
70 def directSumEquiv {I : Type*} {A B : I → Type*}
71     [∀ i, AddCommGroup (A i)] [∀ i, Module ℂ (A i)]
72     [∀ i, AddCommGroup (B i)] [∀ i, Module ℂ (B i)]
73     (α : ∀ i, Representation ℂ G (A i)) (β : ∀ i, Representation ℂ G (B i))
74     (e : ∀ i, Representation.Equiv (α i) (β i)) :
75     Representation.Equiv (Representation.directSum α) (Representation.directSum β) :=
76   Representation.Equiv.mk (DFinsupp.mapRange.linearEquiv (fun i => (e i).toLinearEquiv))
77     (fun g => by
78       apply LinearMap.ext
79       intro x
80       apply DFinsupp.ext
81       intro i
82       change e i (α i g (x i)) = β i g (e i (x i))
83       exact LinearMap.congr_fun ((e i).isIntertwining' g) (x i))
84 
85 /-- The literal tensor decomposes into the actual induced interaction representations. -/
86 def decomposition : Representation.Equiv (ρ.tprod σ)
87     (Representation.directSum (fun i : Fin (Nat.gcd n m) =>
88       Representation.ind (TameDegree.degreeSubgroup ν (Nat.lcm n m)).subtype
89         (MonomialInduction.scalarRepresentation (character ν n m ρ σ b d a w hρ hσ i)))) :=
90   (TameTensorPackets.decomposition ν n m ρ σ b d a w hρ hσ).trans
91     (directSumEquiv _ _ (fun i => (packetEquivalence ν n m ρ σ b d a w hρ hσ φ hφ i).symm))
92 
93 /-- A supplied formula for the actual interaction characters can replace their
94 constructed definitions in the final induced decomposition. -/
95 def decompositionWithCharacters
96     (χ : Fin (Nat.gcd n m) → TameDegree.degreeSubgroup ν (Nat.lcm n m) →* ℂˣ)
97     (hχ : ∀ i g, (χ i g : ℂ) = ((a g 0 * w g (i.val : ZMod m) : ℂˣ) : ℂ)) :
98     Representation.Equiv (ρ.tprod σ)
99       (Representation.directSum (fun i : Fin (Nat.gcd n m) =>
100         Representation.ind (TameDegree.degreeSubgroup ν (Nat.lcm n m)).subtype
101           (MonomialInduction.scalarRepresentation (χ i)))) := by
102   have he : χ = character ν n m ρ σ b d a w hρ hσ := by
103     funext i
104     apply MonoidHom.ext
105     intro g
106     apply Units.ext
107     exact hχ i g
108   subst χ
109   exact decomposition ν n m ρ σ b d a w hρ hσ φ hφ
110 
111 end PaperXI.TameTensorInduction

Back to source controls