HeisenbergReduction107.lean

1 import PaperXI.TensorIntertwining107
2 
3 /-! Assemble the operator proof and two-sided compact transport. The only
4 arithmetic inputs are support and line structure for the restricted first factor. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.HeisenbergReduction107
8 open Representation IntertwiningAlong105 TensorIntertwining107
9 open scoped TensorProduct
10 variable {k K G Q B L W U : Type*} [Field k] [Group K] [Group G] [Group Q]
11   [Group B] [Group L] [AddCommGroup W] [Module k W] [AddCommGroup U] [Module k U]
12 
13 /-- Pull the second-factor intertwiner back to an actual embedded integral
14 subgroup of the centralizer, with both maps and actions checked literally. -/
15 theorem pullback (ι : K →* G) (b : B →* G) (a : L →* B) (j : L →* K)
16     (hcompat : ∀ x, ι (j x) = b (a x))
17     (ρ : Representation k K U) (τ : Representation k L U)
18     (hρ : ∀ x, ρ (j x) = τ x) (y : B)
19     (h : ExistsAt ι ρ (b y)) : ExistsAt a τ y := by
20   obtain ⟨T, hn, ht⟩ := h
21   refine ⟨T, hn, ?_⟩
22   intro x z hxz u
23   have he : ι (j z) = b y * ι (j x) * (b y)⁻¹ := by
24     rw [hcompat, hcompat, hxz, map_mul, map_mul, map_inv]
25   simpa only [hρ] using ht (j x) (j z) he u
26 
27 theorem double_coset_reduction
28     (ι : K →* G) (N : Subgroup K) (q : K →* Q) (hN : N ≤ q.ker)
29     (κ : Representation k K W) (σ : Representation k Q U) (b : B →* G)
30     (hsupport : ∀ g, ExistsAt (ι.comp N.subtype) (κ.comp N.subtype) g →
31       ∃ j₁ j₂ : K, ∃ y : B, g = ι j₁ * b y * ι j₂)
32     (hlines : ∀ y : B, ∃ S : W →ₗ[k] W, S ≠ 0 ∧ Along ι κ (b y) S ∧
33       ∀ A : W →ₗ[k] W,
34         Along (ι.comp N.subtype) (κ.comp N.subtype) (b y) A → ∃ c : k, A = c • S)
35     (g : G) (hg : ExistsAt ι (κ.tprod (σ.comp q)) g) :
36     ∃ j₁ j₂ : K, ∃ y : B, g = ι j₁ * b y * ι j₂ ∧
37       ExistsAt ι (σ.comp q) (b y) := by
38   obtain ⟨j₁, j₂, y, he⟩ := hsupport g (restrict_support ι N q hN κ σ g hg)
39   have ht := existsAt_of_left_right ι (κ.tprod (σ.comp q)) j₁ j₂ (b y) (he ▸ hg)
40   obtain ⟨S, hn, hs, hl⟩ := hlines y
41   exact ⟨j₁, j₂, y, he, (existsAt_iff ι N q hN κ σ (b y) S hn hs hl).mp ht⟩
42 
43 theorem integral_reduction
44     (ι : K →* G) (N : Subgroup K) (q : K →* Q) (hN : N ≤ q.ker)
45     (κ : Representation k K W) (σ : Representation k Q U)
46     (b : B →* G) (a : L →* B) (j : L →* K) (r : L →* Q)
47     (hcompat : ∀ x, ι (j x) = b (a x)) (hred : ∀ x, q (j x) = r x)
48     (hsupport : ∀ g, ExistsAt (ι.comp N.subtype) (κ.comp N.subtype) g →
49       ∃ j₁ j₂ : K, ∃ y : B, g = ι j₁ * b y * ι j₂)
50     (hlines : ∀ y : B, ∃ S : W →ₗ[k] W, S ≠ 0 ∧ Along ι κ (b y) S ∧
51       ∀ A : W →ₗ[k] W,
52         Along (ι.comp N.subtype) (κ.comp N.subtype) (b y) A → ∃ c : k, A = c • S)
53     (g : G) (hg : ExistsAt ι (κ.tprod (σ.comp q)) g) :
54     ∃ j₁ j₂ : K, ∃ y : B, g = ι j₁ * b y * ι j₂ ∧ ExistsAt a (σ.comp r) y := by
55   obtain ⟨j₁, j₂, y, he, hy⟩ := double_coset_reduction ι N q hN κ σ b hsupport hlines g hg
56   refine ⟨j₁, j₂, y, he, pullback ι b a j hcompat (σ.comp q) (σ.comp r) ?_ y hy⟩
57   intro x
58   change σ (q (j x)) = σ (r x)
59   rw [hred]
60 
61 end PaperXI.HeisenbergReduction107

Back to source controls