FiniteProfileBridge109.lean

1 import PaperXI.HeisenbergTrace108
2 import PaperXI.CharacterPairing108
3 import PaperXI.FiniteJointQuotient108
4 import Mathlib.GroupTheory.Index
5 
6 /-! Bounded auxiliary results for the next finite-profile bridge. These prove
7 generic algebraic descent prerequisites, not the actual simple-character
8 profile or the BK lattice-index equality. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.FiniteProfileBridge109
12 open Representation
13 
14 variable {K W : Type*} [Group K] [AddCommGroup W] [Module ℂ W]
15   [FiniteDimensional ℂ W]
16 
17 /-- Positive degree and vanishing off H force the action kernel into H.
18 No scalar restriction or irreducibility is needed for this implication. -/
19 theorem kernel_le_of_trace_support
20     (ρ : Representation ℂ K W) (H : Subgroup K)
21     (hd : 0 < Module.finrank ℂ W)
22     (hz : ∀ x : K, x ∉ H → ρ.character x = 0) : ρ.ker ≤ H := by
23   intro x hx
24   by_contra h
25   have he : ρ.character x = (Module.finrank ℂ W : ℂ) := by
26     simp [Representation.character, MonoidHom.mem_ker.mp hx]
27   have hdim : (Module.finrank ℂ W : ℂ) ≠ 0 := by
28     exact_mod_cast hd.ne'
29   exact hdim (he.symm.trans (hz x h))
30 
31 /-- A scalar character is trivial on elements that act identically, provided
32 the original carrier has positive degree. -/
33 theorem scalar_character_eq_one_on_kernel
34     (ρ : Representation ℂ K W) (H : Subgroup K) (θ : H →* ℂˣ)
35     (hd : 0 < Module.finrank ℂ W)
36     (hscalar : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
37     (h : H) (hk : (h : K) ∈ ρ.ker) : θ h = 1 := by
38   have he := HeisenbergTrace108.character_on_subgroup H θ ρ hscalar h
39   have ht : ρ.character h = (Module.finrank ℂ W : ℂ) := by
40     simp [Representation.character, MonoidHom.mem_ker.mp hk]
41   have hdim : (Module.finrank ℂ W : ℂ) ≠ 0 := by
42     exact_mod_cast hd.ne'
43   apply Units.ext
44   apply mul_left_cancel₀ hdim
45   simpa using he.symm.trans ht
46 
47 /-- Both trace profiles put the actual joint kernel in their intersection. -/
48 theorem joint_kernel_le
49     (ρ σ : Representation ℂ K W) (H₁ H₂ : Subgroup K)
50     (hd : 0 < Module.finrank ℂ W)
51     (hz₁ : ∀ x : K, x ∉ H₁ → ρ.character x = 0)
52     (hz₂ : ∀ x : K, x ∉ H₂ → σ.character x = 0) :
53     FiniteJointQuotient108.kernel ρ σ ≤ H₁ ⊓ H₂ := by
54   exact inf_le_inf (kernel_le_of_trace_support ρ H₁ hd hz₁)
55     (kernel_le_of_trace_support σ H₂ hd hz₂)
56 
57 variable {Q : Type*} [Group Q]
58 
59 /-- The actual image map of a scalar subgroup. -/
60 def imageMap (q : K →* Q) (H : Subgroup K) : H →* H.map q where
61   toFun h := ⟨q h, Subgroup.mem_map_of_mem q h.property⟩
62   map_one' := Subtype.ext (map_one q)
63   map_mul' a b := Subtype.ext (map_mul q (a : K) (b : K))
64 
65 theorem imageMap_surjective (q : K →* Q) (H : Subgroup K) :
66     Function.Surjective (imageMap q H) := by
67   rintro ⟨x, hx⟩
68   obtain ⟨p, hp, rfl⟩ := hx
69   exact ⟨⟨p, hp⟩, rfl⟩
70 
71 /-- Positive degree makes a scalar character factor through the actual image
72 of any quotient map through which the representation already factors. -/
73 theorem imageMap_kernel_le_character_kernel
74     (q : K →* Q) (ρ : Representation ℂ Q W)
75     (H : Subgroup K) (θ : H →* ℂˣ)
76     (hd : 0 < Module.finrank ℂ W)
77     (hscalar : ∀ h : H, (ρ.comp q) h = (θ h : ℂ) • LinearMap.id) :
78     (imageMap q H).ker ≤ θ.ker := by
79   intro h hh
80   have he : q (h : K) = 1 := congrArg Subtype.val (MonoidHom.mem_ker.mp hh)
81   have hk : (h : K) ∈ (ρ.comp q).ker := by
82     apply MonoidHom.mem_ker.mpr
83     change ρ (q (h : K)) = 1
84     simp [he]
85   exact MonoidHom.mem_ker.mpr
86     (scalar_character_eq_one_on_kernel (ρ.comp q) H θ hd hscalar h hk)
87 
88 /-- Character descent onto the named subgroup H.map q, rather than onto a
89 different finite quotient or an unrelated isomorphic subgroup. -/
90 def imageCharacter (q : K →* Q) (H : Subgroup K) (θ : H →* ℂˣ)
91     (hθ : (imageMap q H).ker ≤ θ.ker) : H.map q →* ℂˣ :=
92   (imageMap q H).liftOfSurjective (imageMap_surjective q H) ⟨θ, hθ⟩
93 
94 @[simp] theorem imageCharacter_apply (q : K →* Q) (H : Subgroup K) (θ : H →* ℂˣ)
95     (hθ : (imageMap q H).ker ≤ θ.ker) (h : H) :
96     imageCharacter q H θ hθ (imageMap q H h) = θ h := by
97   exact (imageMap q H).liftOfRightInverse_comp_apply
98     (Function.surjInv (imageMap_surjective q H))
99     (Function.rightInverse_surjInv (imageMap_surjective q H)) ⟨θ, hθ⟩ h
100 
101 omit [FiniteDimensional ℂ W] in
102 theorem image_scalar (q : K →* Q) (ρ : Representation ℂ Q W)
103     (H : Subgroup K) (θ : H →* ℂˣ)
104     (hθ : (imageMap q H).ker ≤ θ.ker)
105     (hscalar : ∀ h : H, (ρ.comp q) h = (θ h : ℂ) • LinearMap.id)
106     (h : H.map q) :
107     ρ h = (imageCharacter q H θ hθ h : ℂ) • LinearMap.id := by
108   obtain ⟨p, rfl⟩ := imageMap_surjective q H h
109   rw [imageCharacter_apply]
110   exact hscalar p
111 
112 omit [FiniteDimensional ℂ W] in
113 theorem image_trace_zero (q : K →* Q) (hq : Function.Surjective q)
114     (ρ : Representation ℂ Q W) (H : Subgroup K)
115     (hz : ∀ x : K, x ∉ H → Representation.character (ρ.comp q) x = 0)
116     (x : Q) (hx : x ∉ H.map q) : ρ.character x = 0 := by
117   obtain ⟨p, rfl⟩ := hq x
118   exact hz p (fun hp => hx (Subgroup.mem_map_of_mem q hp))
119 
120 theorem image_intersection (q : K →* Q) (hq : Function.Surjective q)
121     (H₁ H₂ : Subgroup K) (hk₁ : q.ker ≤ H₁) (hk₂ : q.ker ≤ H₂) :
122     (H₁ ⊓ H₂).map q = H₁.map q ⊓ H₂.map q := by
123   apply Subgroup.comap_injective hq
124   rw [Subgroup.comap_inf, Subgroup.comap_map_eq_self hk₁,
125     Subgroup.comap_map_eq_self hk₂,
126     Subgroup.comap_map_eq_self (le_inf hk₁ hk₂)]
127 
128 /-- The finite image subgroup has the same index as the original subgroup;
129 no cardinality of the original possibly infinite group is used. -/
130 theorem image_index (q : K →* Q) (hq : Function.Surjective q)
131     (H : Subgroup K) (hk : q.ker ≤ H) : (H.map q).index = H.index := by
132   rw [← (H.map q).index_comap_of_surjective hq, Subgroup.comap_map_eq_self hk]
133 
134 theorem image_characters_compatible (q : K →* Q) (hq : Function.Surjective q)
135     (H₁ H₂ : Subgroup K) (θ₁ : H₁ →* ℂˣ) (θ₂ : H₂ →* ℂˣ)
136     (hk₁ : q.ker ≤ H₁) (hk₂ : q.ker ≤ H₂)
137     (ht₁ : (imageMap q H₁).ker ≤ θ₁.ker)
138     (ht₂ : (imageMap q H₂).ker ≤ θ₂.ker)
139     (hc : ∀ p : K, ∀ h₁ : p ∈ H₁, ∀ h₂ : p ∈ H₂,
140       θ₁ ⟨p, h₁⟩ = θ₂ ⟨p, h₂⟩) :
141     ∀ x : Q, ∀ h₁ : x ∈ H₁.map q, ∀ h₂ : x ∈ H₂.map q,
142       imageCharacter q H₁ θ₁ ht₁ ⟨x, h₁⟩ =
143         imageCharacter q H₂ θ₂ ht₂ ⟨x, h₂⟩ := by
144   intro x hx₁ hx₂
145   obtain ⟨p, rfl⟩ := hq x
146   have hp₁ : p ∈ H₁ := by
147     have : p ∈ (H₁.map q).comap q := hx₁
148     rwa [Subgroup.comap_map_eq_self hk₁] at this
149   have hp₂ : p ∈ H₂ := by
150     have : p ∈ (H₂.map q).comap q := hx₂
151     rwa [Subgroup.comap_map_eq_self hk₂] at this
152   change imageCharacter q H₁ θ₁ ht₁ (imageMap q H₁ ⟨p, hp₁⟩) =
153     imageCharacter q H₂ θ₂ ht₂ (imageMap q H₂ ⟨p, hp₂⟩)
154   rw [imageCharacter_apply, imageCharacter_apply]
155   exact hc p hp₁ hp₂
156 
157 omit [FiniteDimensional ℂ W] in
158 theorem quotient_kernel_le_action_kernel (q : K →* Q) (ρ : Representation ℂ Q W) :
159     q.ker ≤ (ρ.comp q).ker := by
160   intro p hp
161   apply MonoidHom.mem_ker.mpr
162   change ρ (q p) = 1
163   simp [MonoidHom.mem_ker.mp hp]
164 
165 /-- The finite criterion can be fed only profiles on the original actions.
166 All subgroup-image, character-descent, and compatibility obligations are
167 discharged generically; the actual profiles and index identity remain inputs. -/
168 theorem dimension_one_iff_of_original_profiles [Fintype Q]
169     (q : K →* Q) (hq : Function.Surjective q)
170     (ρ σ : Representation ℂ Q W)
171     (H₁ H₂ : Subgroup K) (θ₁ : H₁ →* ℂˣ) (θ₂ : H₂ →* ℂˣ)
172     (hd : 0 < Module.finrank ℂ W)
173     (h₁ : ∀ h : H₁, (ρ.comp q) h = (θ₁ h : ℂ) • LinearMap.id)
174     (h₂ : ∀ h : H₂, (σ.comp q) h = (θ₂ h : ℂ) • LinearMap.id)
175     (hz₁ : ∀ p : K, p ∉ H₁ → Representation.character (ρ.comp q) p = 0)
176     (hz₂ : ∀ p : K, p ∉ H₂ → Representation.character (σ.comp q) p = 0)
177     (hc : ∀ p : K, ∀ h₁ : p ∈ H₁, ∀ h₂ : p ∈ H₂,
178       θ₁ ⟨p, h₁⟩ = θ₂ ⟨p, h₂⟩) :
179     Module.finrank ℂ (IntertwiningMap ρ σ) = 1 ↔
180       Module.finrank ℂ W * Module.finrank ℂ W * Nat.card ((H₁ ⊓ H₂).map q) =
181         Nat.card Q := by
182   have hk₁ : q.ker ≤ H₁ := (quotient_kernel_le_action_kernel q ρ).trans
183     (kernel_le_of_trace_support (ρ.comp q) H₁ hd hz₁)
184   have hk₂ : q.ker ≤ H₂ := (quotient_kernel_le_action_kernel q σ).trans
185     (kernel_le_of_trace_support (σ.comp q) H₂ hd hz₂)
186   have ht₁ := imageMap_kernel_le_character_kernel q ρ H₁ θ₁ hd h₁
187   have ht₂ := imageMap_kernel_le_character_kernel q σ H₂ θ₂ hd h₂
188   have he := CharacterPairing108.dimension_one_iff ρ σ (H₁.map q) (H₂.map q)
189     (imageCharacter q H₁ θ₁ ht₁) (imageCharacter q H₂ θ₂ ht₂)
190     (image_scalar q ρ H₁ θ₁ ht₁ h₁) (image_scalar q σ H₂ θ₂ ht₂ h₂)
191     (image_trace_zero q hq ρ H₁ hz₁) (image_trace_zero q hq σ H₂ hz₂)
192     (image_characters_compatible q hq H₁ H₂ θ₁ θ₂ hk₁ hk₂ ht₁ ht₂ hc)
193   rwa [← image_intersection q hq H₁ H₂ hk₁ hk₂] at he
194 
195 end PaperXI.FiniteProfileBridge109

Back to source controls