TameTensorSource.lean

1 import PaperXI.CyclicInducedCharacter
2 import PaperXI.TameTensorInduction
3 
4 /-! Source-facing tame tensor decomposition of genuine induced representations.
5 The Frobenius convention uses representatives `φ^(-i)` and hence the shifted
6 character `h ↦ η(φ^(-i) h φ^i)`. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TameTensorSource
10 open TameDegree
11 open scoped TensorProduct DirectSum Classical
12 
13 variable {G : Type*} [Group G] (ν : G →* Multiplicative ℤ) (φ : G)
14 variable (n m : ℕ)
15 variable (ξ : degreeSubgroup ν n →* ℂˣ) (η : degreeSubgroup ν m →* ℂˣ)
16 
17 /-- The literal product of the first restricted character and the second shifted restriction. -/
18 def interactionCharacter (i : Fin (Nat.gcd n m)) :
19     degreeSubgroup ν (Nat.lcm n m) →* ℂˣ :=
20   (ξ.comp (Subgroup.inclusion (degreeSubgroup_le ν n (Nat.lcm n m)
21     (Nat.dvd_lcm_left n m)))) *
22     (η.comp (conjugationInto ν m (Nat.lcm n m) (Nat.dvd_lcm_right n m)
23       (φ ^ (-(i.val : ℤ)))))
24 
25 @[simp] theorem interactionCharacter_apply (i : Fin (Nat.gcd n m))
26     (h : degreeSubgroup ν (Nat.lcm n m)) :
27     interactionCharacter ν φ n m ξ η i h =
28       ξ ⟨h, degreeSubgroup_le ν n (Nat.lcm n m) (Nat.dvd_lcm_left n m) h.property⟩ *
29       η (conjugationInto ν m (Nat.lcm n m) (Nat.dvd_lcm_right n m)
30         (φ ^ (-(i.val : ℤ))) h) := rfl
31 
32 /-- The character shift is an explicit conjugation, with no assumption of a scalar formula. -/
33 theorem interactionCharacter_literal (i : Fin (Nat.gcd n m))
34     (h : degreeSubgroup ν (Nat.lcm n m)) :
35     interactionCharacter ν φ n m ξ η i h =
36       ξ ⟨h, degreeSubgroup_le ν n (Nat.lcm n m) (Nat.dvd_lcm_left n m) h.property⟩ *
37       η ⟨φ ^ (-(i.val : ℤ)) * (h : G) * φ ^ (i.val : ℤ), by
38         have hp := (conjugationInto ν m (Nat.lcm n m) (Nat.dvd_lcm_right n m)
39           (φ ^ (-(i.val : ℤ))) h).property
40         simpa only [conjugationInto_apply, zpow_neg, inv_inv] using hp⟩ := by
41   rw [interactionCharacter_apply]
42   congr 1
43   apply congrArg η
44   apply Subtype.ext
45   simp [conjugationInto_apply, zpow_neg]
46 
47 variable [NeZero n] [NeZero m]
48 variable (hφ : ν φ = Multiplicative.ofAdd (1 : ℤ))
49 
50 omit [NeZero n] in
51 theorem representative_val (i : Fin (Nat.gcd n m)) : (i.val : ZMod m).val = i.val := by
52   rw [ZMod.val_natCast, Nat.mod_eq_of_lt]
53   exact i.isLt.trans_le (Nat.gcd_le_right n (Nat.pos_of_ne_zero (NeZero.ne m)))
54 
55 /-- The actual tensor-line coefficient equals the stated product of restricted characters. -/
56 theorem interactionCharacter_weight (i : Fin (Nat.gcd n m))
57     (h : degreeSubgroup ν (Nat.lcm n m)) :
58     (interactionCharacter ν φ n m ξ η i h : ℂ) =
59       (CyclicInduced.degreeWeight ν φ hφ n ξ h 0 : ℂ) *
60         (CyclicInduced.degreeWeight ν φ hφ m η h (i.val : ZMod m) : ℂ) := by
61   rw [CyclicInduced.degreeWeight_restrict_zero ν φ hφ n ξ (Nat.dvd_lcm_left n m),
62     CyclicInduced.degreeWeight_restrict ν φ hφ m η (Nat.dvd_lcm_right n m),
63     representative_val n m i, interactionCharacter_apply, Units.val_mul]
64 
65 /-- The gcd/lcm formula for the tensor product of two genuine induced representations. -/
66 def decomposition : Representation.Equiv
67     ((CyclicInduced.degreeInduced ν n ξ).tprod (CyclicInduced.degreeInduced ν m η))
68     (Representation.directSum (fun i : Fin (Nat.gcd n m) =>
69       CyclicInduced.degreeInduced ν (Nat.lcm n m) (interactionCharacter ν φ n m ξ η i))) :=
70   TameTensorInduction.decompositionWithCharacters ν n m
71     (CyclicInduced.degreeInduced ν n ξ) (CyclicInduced.degreeInduced ν m η)
72     (CyclicInduced.degreeBasis ν φ hφ n ξ) (CyclicInduced.degreeBasis ν φ hφ m η)
73     (CyclicInduced.degreeWeight ν φ hφ n ξ) (CyclicInduced.degreeWeight ν φ hφ m η)
74     (CyclicInduced.degreeBasis_action ν φ hφ n ξ)
75     (CyclicInduced.degreeBasis_action ν φ hφ m η) φ hφ
76     (interactionCharacter ν φ n m ξ η)
77     (fun i h => by simpa only [Units.val_mul] using
78       interactionCharacter_weight ν φ n m ξ η hφ i h)
79 
80 /-- The displayed decomposition is an actual group intertwiner. -/
81 theorem decomposition_intertwines (g : G)
82     (v : CyclicInduced.DegreeIndSpace ν n ξ ⊗[ℂ] CyclicInduced.DegreeIndSpace ν m η) :
83     decomposition ν φ n m ξ η hφ
84       (((CyclicInduced.degreeInduced ν n ξ).tprod (CyclicInduced.degreeInduced ν m η)) g v) =
85       (Representation.directSum (fun i : Fin (Nat.gcd n m) =>
86         CyclicInduced.degreeInduced ν (Nat.lcm n m) (interactionCharacter ν φ n m ξ η i))) g
87           (decomposition ν φ n m ξ η hφ v) :=
88   Representation.IntertwiningMap.isIntertwining _ _
89     (decomposition ν φ n m ξ η hφ).toIntertwiningMap g v
90 
91 include hφ in
92 /-- Each summand in the displayed genuine induction formula has dimension lcm. -/
93 theorem interaction_dimension (i : Fin (Nat.gcd n m)) :
94     Module.finrank ℂ (CyclicInduced.DegreeIndSpace ν (Nat.lcm n m)
95       (interactionCharacter ν φ n m ξ η i)) = Nat.lcm n m := by
96   simpa only [ZMod.card] using Module.finrank_eq_card_basis
97     (CyclicInduced.degreeBasis ν φ hφ (Nat.lcm n m) (interactionCharacter ν φ n m ξ η i))
98 
99 omit [NeZero n] [NeZero m] in
100 /-- The direct sum is indexed by exactly gcd-many interaction packets before merging. -/
101 theorem interaction_count : Fintype.card (Fin (Nat.gcd n m)) = Nat.gcd n m :=
102   Fintype.card_fin _
103 
104 include hφ in
105 /-- The dimensions of the actual induced summands, not hypothetical blocks, sum to `n*m`. -/
106 theorem interaction_dimension_sum :
107     (∑ i : Fin (Nat.gcd n m), Module.finrank ℂ
108       (CyclicInduced.DegreeIndSpace ν (Nat.lcm n m) (interactionCharacter ν φ n m ξ η i))) =
109       n*m := by
110   simp only [interaction_dimension ν φ n m ξ η hφ, Finset.sum_const,
111     Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
112   exact Nat.gcd_mul_lcm n m
113 
114 include hφ in
115 /-- The genuine tensor source has the same dimension as the constructed direct sum. -/
116 theorem tensor_dimension : Module.finrank ℂ
117     (CyclicInduced.DegreeIndSpace ν n ξ ⊗[ℂ] CyclicInduced.DegreeIndSpace ν m η) = n*m := by
118   simpa only [Fintype.card_prod, ZMod.card] using Module.finrank_eq_card_basis
119     ((CyclicInduced.degreeBasis ν φ hφ n ξ).tensorProduct
120       (CyclicInduced.degreeBasis ν φ hφ m η))
121 
122 end PaperXI.TameTensorSource

Back to source controls