GlobalHeisenbergBridge112.lean

1 import PaperXI.HeisenbergCharacterProfile111
2 import PaperXI.FiniteRepresentation
3 import PaperXI.TypeSideDescent
4 import PaperXI.SchurScalar
5 import Mathlib.LinearAlgebra.Determinant
6 import Mathlib.GroupTheory.OrderOfElement
7 
8 /-! A literal global central lift produces the Heisenberg representation bridge;
9 the target representation equivalence is a conclusion. The actual quotient
10 endpoint retains the original theta and eta on its original carrier. Existence
11 of the canonical global quotient lift is not asserted here. -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.GlobalHeisenbergBridge112
15 open Representation HeisenbergCharacterProfile111
16 
17 section FiniteUniqueness
18 variable {P V W : Type*} [Group P] [Finite P]
19   [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
20 
21 /-- The common original scalar/trace profile forces a nonzero actual Hom.
22 Neither representation equivalence nor target Hom dimension is an input. -/
23 theorem equiv_of_common_profile
24     (H : Subgroup P) (θ : H →* ℂˣ)
25     (ρ : Representation ℂ P V) (σ : Representation ℂ P W)
26     [IsIrreducible ρ] [IsIrreducible σ]
27     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
28     (hσ : ∀ h : H, σ h = (θ h : ℂ) • LinearMap.id)
29     (hzρ : ∀ p : P, p ∉ H → Representation.character ρ p = 0)
30     (hzσ : ∀ p : P, p ∉ H → Representation.character σ p = 0) :
31     Nonempty (Representation.Equiv ρ σ) := by
32   classical
33   let : Fintype P := Fintype.ofFinite P
34   let : FiniteDimensional ℂ V := FiniteRepresentation.finiteDimensional ρ
35   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional σ
36   have he := CharacterPairing108.dimension_formula ρ σ H H θ θ hρ hσ hzρ hzσ
37     (fun _ _ _ => rfl)
38   have hp : 0 < Module.finrank ℂ V * Module.finrank ℂ W * Nat.card H :=
39     Nat.mul_pos (Nat.mul_pos (FiniteRepresentation.finrank_pos ρ)
40       (FiniteRepresentation.finrank_pos σ)) (Nat.card_pos (α := H))
41   have hhom : 0 < Module.finrank ℂ (IntertwiningMap ρ σ) := by
42     by_contra hn
43     have hh : Module.finrank ℂ (IntertwiningMap ρ σ) = 0 := Nat.eq_zero_of_not_pos hn
44     rw [hh, mul_zero, inf_idem] at he
45     exact (Nat.ne_of_gt hp) he.symm
46   let : Nontrivial (IntertwiningMap ρ σ) := Module.nontrivial_of_finrank_pos hhom
47   obtain ⟨T, hT⟩ := exists_ne (0 : IntertwiningMap ρ σ)
48   exact ⟨T.ofBijective ((IsIrreducible.bijective_or_eq_zero T).resolve_right hT)⟩
49 
50 variable {k X : Type*} [Field k] [AddCommGroup X] [Module k X]
51 
52 /-- Nondegenerate original commutator data derive both profiles and hence the
53 global representation equivalence, without separate break embeddings. -/
54 theorem equiv_of_common_quotient_form
55     (H : Subgroup P) [H.Normal] (θ : H →* ℂˣ)
56     (τ : (P ⧸ H) ≃* Multiplicative X)
57     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
58     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
59     (hform : ∀ p q : P, ψ (B (coordinate H τ p) (coordinate H τ q)) =
60       characterCommutator H τ θ p q)
61     (ρ : Representation ℂ P V) (σ : Representation ℂ P W)
62     [IsIrreducible ρ] [IsIrreducible σ]
63     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
64     (hσ : ∀ h : H, σ h = (θ h : ℂ) • LinearMap.id) :
65     Nonempty (Representation.Equiv ρ σ) :=
66   equiv_of_common_profile H θ ρ σ hρ hσ
67     (trace_support_of_nondegenerate_form H τ θ B ψ hψ hnd hform ρ hρ)
68     (trace_support_of_nondegenerate_form H τ θ B ψ hψ hnd hform σ hσ)
69 
70 /-- A global central-extension group lift preserving the original scalar
71 character gives the desired representation bridge. No target iso is a field. -/
72 theorem equiv_of_global_central_lift
73     {Q : Type*} [Group Q] (H : Subgroup P) [H.Normal] (N : Subgroup Q)
74     (θ : H →* ℂˣ) (φ : N →* ℂˣ) (ℓ : P ≃* Q)
75     (ζ : H →* N) (hℓ : ∀ h : H, ℓ (h : P) = (ζ h : Q))
76     (hchar : ∀ h : H, θ h = φ (ζ h))
77     (τ : (P ⧸ H) ≃* Multiplicative X)
78     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
79     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
80     (hform : ∀ p q : P, ψ (B (coordinate H τ p) (coordinate H τ q)) =
81       characterCommutator H τ θ p q)
82     (ρ : Representation ℂ P V) (σ : Representation ℂ Q W)
83     [IsIrreducible ρ] [IsIrreducible σ]
84     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
85     (hσ : ∀ z : N, σ z = (φ z : ℂ) • LinearMap.id) :
86     Nonempty (Representation.Equiv ρ (σ.comp ℓ.toMonoidHom)) := by
87   let : IsIrreducible (σ.comp ℓ.toMonoidHom) :=
88     (QuotientRepresentation.irreducible_comp_iff ℓ.toMonoidHom ℓ.surjective σ).mpr
89       inferInstance
90   apply equiv_of_common_quotient_form H θ τ B ψ hψ hnd hform ρ
91     (σ.comp ℓ.toMonoidHom) hρ
92   intro h
93   change σ (ℓ (h : P)) = _
94   rw [hℓ, hσ, hchar]
95 
96 end FiniteUniqueness
97 
98 section ActualQuotient
99 variable {G P V W k X : Type*} [Group G] [Group P] [Finite P]
100   [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
101   [Field k] [AddCommGroup X] [Module k X]
102 
103 /-- The target is the literal action descended from the prescribed actual eta
104 to J¹/ker(theta), on the same W. Scalar action is derived from occurrence. -/
105 theorem actual_eta_bridge_of_global_lift
106     (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
107     (hinv : TypeSideDescent.Invariant D θ)
108     (η : Representation ℂ G W) [IsIrreducible η]
109     (hcontains : TypeSideDescent.Contains D θ η)
110     (H : Subgroup P) [H.Normal] (χ : H →* ℂˣ)
111     (ℓ : P ≃* (G ⧸ TypeSideDescent.characterKernel D θ hinv))
112     (ζ : H →* (D ⧸ θ.ker))
113     (hℓ : ∀ h : H, ℓ (h : P) = TypeSideDescent.centerInclusion D θ hinv (ζ h))
114     (hchar : ∀ h : H, χ h = TypeSideDescent.centralCharacter D θ (ζ h))
115     (τ : (P ⧸ H) ≃* Multiplicative X)
116     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
117     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
118     (hform : ∀ p q : P, ψ (B (coordinate H τ p) (coordinate H τ q)) =
119       characterCommutator H τ χ p q)
120     (ρ : Representation ℂ P V) [IsIrreducible ρ]
121     (hρ : ∀ h : H, ρ h = (χ h : ℂ) • LinearMap.id) :
122     Nonempty (Representation.Equiv ρ
123       ((TypeSideDescent.representation D θ hinv η hcontains).comp ℓ.toMonoidHom)) := by
124   let σ := TypeSideDescent.representation D θ hinv η hcontains
125   let : IsIrreducible σ := TypeSideDescent.representation_irreducible D θ hinv η hcontains
126   let : IsIrreducible (σ.comp ℓ.toMonoidHom) :=
127     (QuotientRepresentation.irreducible_comp_iff ℓ.toMonoidHom ℓ.surjective σ).mpr
128       inferInstance
129   apply equiv_of_common_quotient_form H χ τ B ψ hψ hnd hform ρ (σ.comp ℓ.toMonoidHom) hρ
130   intro h
131   change σ (ℓ (h : P)) = _
132   rw [hℓ]
133   exact (TypeSideDescent.central_action D θ hinv η hcontains (ζ h)).trans
134     (by rw [hchar])
135 
136 end ActualQuotient
137 
138 section GeneratorPhase
139 variable {P V W : Type*} [Group P]
140   [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
141   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
142 
143 omit [FiniteDimensional ℂ W] in
144 /-- Two actual implementers of the same lifted automorphism differ by a scalar
145 after the global Heisenberg bridge. Schur applies to the whole irreducible rho. -/
146 theorem generator_discrepancy
147     (ρ : Representation ℂ P V) (σ : Representation ℂ P W) [IsIrreducible ρ]
148     (U : V ≃ₗ[ℂ] W) (hU : ∀ p v, U (ρ p v) = σ p (U v))
149     (α : MulAut P) (A : V ≃ₗ[ℂ] V) (B : W ≃ₗ[ℂ] W)
150     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v))
151     (hB : ∀ p v, B (σ p v) = σ (α p) (B v)) :
152     ∃ c : ℂˣ, ∀ v, U (A v) = (c : ℂ) • B (U v) := by
153   have hBi (p : P) (w : W) : B.symm (σ (α p) w) = σ p (B.symm w) := by
154     apply B.injective
155     rw [B.apply_symm_apply, hB, B.apply_symm_apply]
156   let T := (A.trans U).trans B.symm
157   have hT : ∀ p v, T (ρ p v) = σ p (T v) := by
158     intro p v
159     simp only [T, LinearEquiv.trans_apply, hA, hU, hBi]
160   obtain ⟨c, hc, _⟩ := SchurScalar.bridge_unique ρ σ U T hU hT
161   refine ⟨c, fun v => ?_⟩
162   simpa only [T, LinearEquiv.trans_apply, B.apply_symm_apply, map_smul] using
163     congrArg B (hc v)
164 
165 omit [FiniteDimensional ℂ V] [FiniteDimensional ℂ W] in
166 /-- The scalar discrepancy propagates through actual powers of honest
167 generator operators, with the same direction as the original bridge. -/
168 theorem generator_discrepancy_pow
169     (U : V ≃ₗ[ℂ] W) (A : V ≃ₗ[ℂ] V) (B : W ≃ₗ[ℂ] W) (c : ℂˣ)
170     (hc : ∀ v, U (A v) = (c : ℂ) • B (U v)) (n : ℕ) (v : V) :
171     U ((A ^ n) v) = ((c ^ n : ℂˣ) : ℂ) • (B ^ n) (U v) := by
172   induction n generalizing v with
173   | zero => simp
174   | succ n ih =>
175     rw [pow_succ, LinearEquiv.mul_apply, ih, hc, map_smul]
176     simp only [pow_succ, Units.val_mul, smul_smul, LinearEquiv.mul_apply]
177 
178 /-- Two coprime exact scalar power conditions eliminate every residual phase. -/
179 theorem unit_eq_one_of_coprime_powers (c : ℂˣ) (n d : ℕ)
180     (hcop : Nat.Coprime n d) (hn : c ^ n = 1) (hd : c ^ d = 1) : c = 1 := by
181   apply orderOf_eq_one_iff.mp
182   exact Nat.eq_one_of_dvd_coprimes hcop (orderOf_dvd_of_pow_eq_one hn)
183     (orderOf_dvd_of_pow_eq_one hd)
184 
185 omit [FiniteDimensional ℂ W] in
186 /-- Matching determinants kill the generator phase when its honest order and
187 the original Heisenberg dimension are coprime. A nonzero trace is unnecessary. -/
188 theorem generator_phase_eq_one_of_det_coprime [Nontrivial V]
189     (U : V ≃ₗ[ℂ] W) (A : V ≃ₗ[ℂ] V) (B : W ≃ₗ[ℂ] W) (c : ℂˣ)
190     (hc : ∀ v, U (A v) = (c : ℂ) • B (U v))
191     (n : ℕ) (hA : A ^ n = 1) (hB : B ^ n = 1)
192     (hdet : LinearEquiv.det A = LinearEquiv.det B)
193     (hcop : Nat.Coprime n (Module.finrank ℂ V)) : c = 1 := by
194   have hcn : c ^ n = 1 := by
195     obtain ⟨v, hv⟩ := exists_ne (0 : V)
196     have huv : U v ≠ 0 := fun h => hv (U.injective (h.trans U.map_zero.symm))
197     have hp := generator_discrepancy_pow U A B c hc n v
198     rw [hA, hB] at hp
199     have hs : ((c ^ n : ℂˣ) : ℂ) = 1 :=
200       (smul_left_injective ℂ huv) (by simpa only [LinearEquiv.coe_one, id_eq, one_smul] using hp.symm)
201     exact Units.ext hs
202   let B' := (U.trans B).trans U.symm
203   have ha : A.toLinearMap = (c : ℂ) • B'.toLinearMap := by
204     ext v
205     apply U.injective
206     change U (A v) = U ((c : ℂ) • B' v)
207     simp only [B', LinearEquiv.trans_apply, map_smul, U.apply_symm_apply]
208     exact hc v
209   have hbd : LinearMap.det B'.toLinearMap = (LinearEquiv.det B : ℂ) := by
210     simpa only [B', LinearEquiv.symm_symm, LinearEquiv.coe_det] using
211       congrArg Units.val (LinearEquiv.det_conj B U.symm)
212   have hcd : c ^ Module.finrank ℂ V = 1 := by
213     have hd := congrArg LinearMap.det ha
214     rw [LinearMap.det_smul, hbd, ← LinearEquiv.coe_det A] at hd
215     rw [hdet] at hd
216     apply Units.ext
217     exact mul_right_cancel₀ (Units.ne_zero (LinearEquiv.det B))
218       (by simpa only [Units.val_one, one_mul, Units.val_pow_eq_pow_val] using hd.symm)
219   exact unit_eq_one_of_coprime_powers c n (Module.finrank ℂ V) hcop hcn hcd
220 
221 omit [FiniteDimensional ℂ W] in
222 /-- The derived Heisenberg bridge intertwines the honest generator when the
223 same lifted automorphism and determinant normalization have been attached. -/
224 theorem generator_equivariant_of_det_coprime
225     (ρ : Representation ℂ P V) (σ : Representation ℂ P W) [IsIrreducible ρ]
226     (U : V ≃ₗ[ℂ] W) (hU : ∀ p v, U (ρ p v) = σ p (U v))
227     (α : MulAut P) (A : V ≃ₗ[ℂ] V) (B : W ≃ₗ[ℂ] W)
228     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v))
229     (hB : ∀ p v, B (σ p v) = σ (α p) (B v))
230     (n : ℕ) (hAn : A ^ n = 1) (hBn : B ^ n = 1)
231     (hdet : LinearEquiv.det A = LinearEquiv.det B)
232     (hcop : Nat.Coprime n (Module.finrank ℂ V)) :
233     ∀ v, U (A v) = B (U v) := by
234   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space ρ
235   obtain ⟨c, hc⟩ := generator_discrepancy ρ σ U hU α A B hA hB
236   have he := generator_phase_eq_one_of_det_coprime U A B c hc n hAn hBn hdet hcop
237   simpa only [he, Units.val_one, one_smul] using hc
238 
239 end GeneratorPhase
240 
241 section CyclicAction
242 variable {C V W : Type*} [Group C]
243   [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
244 
245 /-- A bridge for one declared cyclic generator is a bridge for every element
246 of the same honest cyclic action. The cyclic generation datum is explicit. -/
247 theorem cyclic_equivariant_of_generator
248     (Ωρ : C →* (V ≃ₗ[ℂ] V)) (Ωσ : C →* (W ≃ₗ[ℂ] W))
249     (c : C) (hgen : ∀ g : C, ∃ n : ℕ, g = c ^ n)
250     (U : V ≃ₗ[ℂ] W) (hU : ∀ v, U (Ωρ c v) = Ωσ c (U v)) :
251     ∀ g v, U (Ωρ g v) = Ωσ g (U v) := by
252   intro g v
253   obtain ⟨n, rfl⟩ := hgen g
254   simpa only [map_pow, one_pow, Units.val_one, one_smul] using
255     generator_discrepancy_pow U (Ωρ c) (Ωσ c) 1
256       (fun v => by simpa only [Units.val_one, one_smul] using hU v) n v
257 
258 end CyclicAction
259 
260 section GlobalEquivariantBridge
261 variable {P C V W k X : Type*} [Group P] [Finite P] [Group C]
262   [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
263   [Field k] [AddCommGroup X] [Module k X]
264 
265 /-- The equivariant global bridge is derived from nondegenerate original
266 Heisenberg data and actual honest generator actions. Neither a representation
267 equivalence nor a target eta intertwiner is a premise. -/
268 theorem equivariant_bridge_of_common_quotient_form
269     (H : Subgroup P) [H.Normal] (θ : H →* ℂˣ)
270     (τ : (P ⧸ H) ≃* Multiplicative X)
271     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
272     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
273     (hform : ∀ p q : P, ψ (B (coordinate H τ p) (coordinate H τ q)) =
274       characterCommutator H τ θ p q)
275     (ρ : Representation ℂ P V) (σ : Representation ℂ P W)
276     [IsIrreducible ρ] [IsIrreducible σ]
277     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
278     (hσ : ∀ h : H, σ h = (θ h : ℂ) • LinearMap.id)
279     (Ωρ : C →* (V ≃ₗ[ℂ] V)) (Ωσ : C →* (W ≃ₗ[ℂ] W))
280     (c : C) (hgen : ∀ g : C, ∃ n : ℕ, g = c ^ n)
281     (α : MulAut P)
282     (hA : ∀ p v, Ωρ c (ρ p v) = ρ (α p) (Ωρ c v))
283     (hB : ∀ p v, Ωσ c (σ p v) = σ (α p) (Ωσ c v))
284     (n : ℕ) (hn : c ^ n = 1)
285     (hdet : LinearEquiv.det (Ωρ c) = LinearEquiv.det (Ωσ c))
286     (hcop : Nat.Coprime n (Module.finrank ℂ V)) :
287     ∃ U : Representation.Equiv ρ σ,
288       ∀ g v, U (Ωρ g v) = Ωσ g (U v) := by
289   let : FiniteDimensional ℂ V := FiniteRepresentation.finiteDimensional ρ
290   obtain ⟨U⟩ := equiv_of_common_quotient_form H θ τ B ψ hψ hnd hform ρ σ hρ hσ
291   have hU : ∀ p v, U.toLinearEquiv (ρ p v) = σ p (U.toLinearEquiv v) :=
292     U.toIntertwiningMap.isIntertwining
293   have hAn : Ωρ c ^ n = 1 := by rw [← map_pow, hn, map_one]
294   have hBn : Ωσ c ^ n = 1 := by rw [← map_pow, hn, map_one]
295   have hc := generator_equivariant_of_det_coprime ρ σ U.toLinearEquiv hU
296     α (Ωρ c) (Ωσ c) hA hB n hAn hBn hdet hcop
297   exact ⟨U, cyclic_equivariant_of_generator Ωρ Ωσ c hgen U.toLinearEquiv hc⟩
298 
299 end GlobalEquivariantBridge
300 
301 end PaperXI.GlobalHeisenbergBridge112

Back to source controls