HeisenbergComparison.lean

1 import PaperXI.HeisenbergTransport
2 import PaperXI.SchrodingerUniversal
3 
4 /-! The first actual intertwiner between arbitrary irreducible actions along
5 a group equivalence from the odd-characteristic coordinate Heisenberg group.
6 The coordinate isometry specialization constructs that group equivalence.
7 Abstract symplectic coordinates, source quotient actions, and the dyadic
8 extension branch are not supplied by this module. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.HeisenbergComparison
12 
13 open Heisenberg HeisenbergTransport
14 
15 variable {K X G V W : Type*} [Field K] [AddCommGroup X] [Module K X]
16 variable [Fintype X] [Fintype (Module.Dual K X)] [FiniteDimensional K X]
17 variable [Group G] [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
18 
19 /-- Construct the first equivalence between arbitrary irreducible actions,
20 by comparing both actions to the model after pulling back the second one. -/
21 def equivAlong (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
22     (e : Element K X ≃* G)
23     (ρ : Representation ℂ (Element K X) V) (σ : Representation ℂ G W)
24     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
25     (hρ : ∀ z, ρ (centralElement z) = ψ z • LinearMap.id)
26     (hσ : ∀ z, σ (e (centralElement z)) = ψ z • LinearMap.id) :
27     Representation.Equiv ρ (pullback e σ) := by
28   letI := pullback_irreducible e σ
29   exact (SchrodingerUniversal.equiv ψ hψ h2 ρ hρ).symm.trans
30     (SchrodingerUniversal.equiv ψ hψ h2 (pullback e σ) hσ)
31 
32 theorem equivAlong_intertwines (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
33     (e : Element K X ≃* G)
34     (ρ : Representation ℂ (Element K X) V) (σ : Representation ℂ G W)
35     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
36     (hρ : ∀ z, ρ (centralElement z) = ψ z • LinearMap.id)
37     (hσ : ∀ z, σ (e (centralElement z)) = ψ z • LinearMap.id)
38     (g : Element K X) (v : V) :
39     equivAlong ψ hψ h2 e ρ σ hρ hσ (ρ g v) =
40       σ (e g) (equivAlong ψ hψ h2 e ρ σ hρ hσ v) :=
41   Representation.IntertwiningMap.isIntertwining ρ (pullback e σ)
42     (equivAlong ψ hψ h2 e ρ σ hρ hσ).toIntertwiningMap g v
43 
44 /-- Existence does not assume a starting intertwiner or finite dimensionality
45 of either representation space. The scalar comparison is uniquely invertible. -/
46 theorem exists_unique_along (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
47     (e : Element K X ≃* G)
48     (ρ : Representation ℂ (Element K X) V) (σ : Representation ℂ G W)
49     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
50     (hρ : ∀ z, ρ (centralElement z) = ψ z • LinearMap.id)
51     (hσ : ∀ z, σ (e (centralElement z)) = ψ z • LinearMap.id) :
52     ∃ U : V ≃ₗ[ℂ] W, U.toLinearMap ≠ 0 ∧
53       (∀ g v, U (ρ g v) = σ (e g) (U v)) ∧
54       ∀ T : V ≃ₗ[ℂ] W, (∀ g v, T (ρ g v) = σ (e g) (T v)) →
55         ∃! c : ℂˣ, ∀ v, T v = (c : ℂ) • U v := by
56   let U := (equivAlong ψ hψ h2 e ρ σ hρ hσ).toLinearEquiv
57   have hU : ∀ g v, U (ρ g v) = σ (e g) (U v) :=
58     equivAlong_intertwines ψ hψ h2 e ρ σ hρ hσ
59   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space ρ
60   let : FiniteDimensional ℂ V := SchrodingerUniversal.finiteDimensional ψ hψ h2 ρ hρ
61   refine ⟨U, ?_, hU, ?_⟩
62   · intro h
63     obtain ⟨v, hv⟩ := exists_ne (0 : V)
64     have hz : U v = 0 := LinearMap.congr_fun h v
65     exact hv (U.injective (hz.trans U.map_zero.symm))
66   · intro T hT
67     exact SchurScalar.bridge_unique ρ (pullback e σ) U T hU hT
68 
69 section Coordinates
70 
71 variable {Y : Type*} [AddCommGroup Y] [Module K Y]
72 
73 /-- Lift the supplied form-preserving linear equivalence, then construct the
74 first nonzero intertwiner between the two actual arbitrary irreducibles. -/
75 theorem exists_unique_of_isometry
76     (e : (X × Module.Dual K X) ≃ₗ[K] (Y × Module.Dual K Y)) (he : PreservesForm e)
77     (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
78     (ρ : Representation ℂ (Element K X) V) (σ : Representation ℂ (Element K Y) W)
79     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
80     (hρ : ∀ z, ρ (centralElement z) = ψ z • LinearMap.id)
81     (hσ : ∀ z, σ (centralElement z) = ψ z • LinearMap.id) :
82     ∃ U : V ≃ₗ[ℂ] W, U.toLinearMap ≠ 0 ∧
83       (∀ g v, U (ρ g v) = σ (liftIsometry e he g) (U v)) ∧
84       ∀ T : V ≃ₗ[ℂ] W, (∀ g v, T (ρ g v) = σ (liftIsometry e he g) (T v)) →
85         ∃! c : ℂˣ, ∀ v, T v = (c : ℂ) • U v := by
86   apply exists_unique_along ψ hψ h2 (liftIsometry e he) ρ σ hρ
87   intro z
88   simpa using hσ z
89 
90 end Coordinates
91 
92 end PaperXI.HeisenbergComparison

Back to source controls