TensorIntertwining107.lean

1 import PaperXI.TensorSlices107
2 import PaperXI.IntertwiningAlong105
3 
4 /-! The operator argument underlying BK 5.3.2. The arithmetic support and
5 one-dimensional Heisenberg-intertwining results are kept as explicit inputs. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TensorIntertwining107
9 open Representation IntertwiningAlong105 TensorSlices107
10 open scoped TensorProduct
11 variable {k K G Q W U : Type*} [Field k] [Group K] [Group G] [Group Q]
12   [AddCommGroup W] [Module k W] [AddCommGroup U] [Module k U]
13   (ι : K →* G) (N : Subgroup K) (q : K →* Q) (hN : N ≤ q.ker)
14   (κ : Representation k K W) (σ : Representation k Q U)
15 
16 include hN
17 
18 /-- Every coefficient of a tensor intertwiner intertwines the actual restricted
19 first-factor action; the quotient factor is trivial on the subgroup. -/
20 theorem slice_along (g : G) (T : W ⊗[k] U →ₗ[k] W ⊗[k] U)
21     (hT : Along ι (κ.tprod (σ.comp q)) g T) (u : U) (φ : Module.Dual k U) :
22     Along (ι.comp N.subtype) (κ.comp N.subtype) g (slice T u φ) := by
23   intro x y hxy w
24   have hx : q x = 1 := hN x.property
25   have hy : q y = 1 := hN y.property
26   have h := hT x y hxy (w ⊗ₜ[k] u)
27   change T (TensorProduct.map (κ x) (σ (q x)) (w ⊗ₜ[k] u)) =
28     TensorProduct.map (κ y) (σ (q y)) (T (w ⊗ₜ[k] u)) at h
29   rw [hx, hy, map_one] at h
30   change T (κ x w ⊗ₜ[k] u) =
31     TensorProduct.map (κ y) LinearMap.id (T (w ⊗ₜ[k] u)) at h
32   change right φ (T (κ x w ⊗ₜ[k] u)) = κ y (right φ (T (w ⊗ₜ[k] u)))
33   rw [← right_map]
34   exact congrArg (right φ) h
35 
36 theorem restrict_support (g : G) (h : ExistsAt ι (κ.tprod (σ.comp q)) g) :
37     ExistsAt (ι.comp N.subtype) (κ.comp N.subtype) g := by
38   obtain ⟨T, hT, ht⟩ := h
39   obtain ⟨u, φ, hn⟩ := exists_nonzero_slice T hT
40   exact ⟨slice T u φ, hn, slice_along ι N q hN κ σ g T ht u φ⟩
41 
42 omit N hN in
43 /-- Cancel a nonzero first-factor intertwiner using a separating functional,
44 without assuming the intertwiner is invertible. -/
45 theorem second_along (g : G) (S : W →ₗ[k] W) (hS : S ≠ 0)
46     (hs : Along ι κ g S) (R : U →ₗ[k] U)
47     (hT : Along ι (κ.tprod (σ.comp q)) g (TensorProduct.map S R)) :
48     Along ι (σ.comp q) g R := by
49   obtain ⟨w₀, hw₀⟩ : ∃ w₀, S w₀ ≠ 0 := by
50     by_contra h
51     push Not at h
52     exact hS (LinearMap.ext h)
53   intro x y hxy u
54   apply tmul_left_injective (k := k) (S w₀) hw₀
55   have h := hT x y hxy (κ x⁻¹ w₀ ⊗ₜ[k] u)
56   have he := hs x y hxy (κ x⁻¹ w₀)
57   simp only [act_mul_inv_cancel] at he
58   simpa only [Representation.tprod_apply, MonoidHom.comp_apply,
59     TensorProduct.map_tmul, act_mul_inv_cancel, ← he] using h
60 
61 omit N hN in
62 theorem map_along (g : G) (S : W →ₗ[k] W) (hs : Along ι κ g S)
63     (R : U →ₗ[k] U) (hr : Along ι (σ.comp q) g R) :
64     Along ι (κ.tprod (σ.comp q)) g (TensorProduct.map S R) := by
65   intro x y hxy t
66   induction t using TensorProduct.induction_on with
67   | zero => simp
68   | add a b ha hb => simp only [map_add, ha, hb]
69   | tmul w u =>
70     simpa only [Representation.tprod_apply, TensorProduct.map_tmul,
71       MonoidHom.comp_apply] using congrArg₂ (TensorProduct.tmul k)
72         (hs x y hxy w) (hr x y hxy u)
73 
74 /-- An exact factorization of every tensor intertwiner, given the restricted
75 Heisenberg intertwining line and its extension to the full first factor. -/
76 theorem factor_along (g : G) (S : W →ₗ[k] W) (hS : S ≠ 0)
77     (hs : Along ι κ g S)
78     (hline : ∀ A : W →ₗ[k] W,
79       Along (ι.comp N.subtype) (κ.comp N.subtype) g A → ∃ c : k, A = c • S)
80     (T : W ⊗[k] U →ₗ[k] W ⊗[k] U)
81     (hT : Along ι (κ.tprod (σ.comp q)) g T) :
82     ∃ R : U →ₗ[k] U, T = TensorProduct.map S R ∧ Along ι (σ.comp q) g R := by
83   obtain ⟨R, hr⟩ := factor_of_slice_line T S hS (fun u φ =>
84     hline _ (slice_along ι N q hN κ σ g T hT u φ))
85   exact ⟨R, hr, second_along ι q κ σ g S hS hs R (hr ▸ hT)⟩
86 
87 /-- Both directions of tensor-to-residue intertwining at a fixed element. -/
88 theorem existsAt_iff (g : G) (S : W →ₗ[k] W) (hS : S ≠ 0)
89     (hs : Along ι κ g S)
90     (hline : ∀ A : W →ₗ[k] W,
91       Along (ι.comp N.subtype) (κ.comp N.subtype) g A → ∃ c : k, A = c • S) :
92     ExistsAt ι (κ.tprod (σ.comp q)) g ↔ ExistsAt ι (σ.comp q) g := by
93   constructor
94   · rintro ⟨T, hT, ht⟩
95     obtain ⟨R, rfl, hr⟩ := factor_along ι N q hN κ σ g S hS hs hline T ht
96     refine ⟨R, ?_, hr⟩
97     intro hR
98     exact hT (by simp [hR])
99   · rintro ⟨R, hR, hr⟩
100     refine ⟨TensorProduct.map S R, ?_, map_along ι q κ σ g S hs R hr⟩
101     intro h
102     apply hR
103     apply map_left_injective S hS
104     simpa using h
105 
106 end PaperXI.TensorIntertwining107

Back to source controls