IntertwiningSpace107.lean

1 import PaperXI.TensorIntertwining107
2 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
3 
4 /-! A linear equivalence of actual intertwining spaces on the same embedded
5 compact group. Identification with a smaller integral subgroup is separate. -/
6 set_option autoImplicit false
7 set_option maxHeartbeats 100000
8 noncomputable section
9 namespace PaperXI.IntertwiningSpace107
10 open Representation IntertwiningAlong105 TensorIntertwining107 TensorSlices107
11 open scoped TensorProduct
12 variable {k K G Q W U V : Type*} [Field k] [Group K] [Group G] [Group Q]
13   [AddCommGroup W] [Module k W] [AddCommGroup U] [Module k U]
14   [AddCommGroup V] [Module k V]
15 
16 def space (ι : K →* G) (ρ : Representation k K V) (g : G) :
17     Submodule k (V →ₗ[k] V) where
18   carrier := {T | Along ι ρ g T}
19   zero_mem' := by intro x y hxy v; simp
20   add_mem' := by
21     intro A B hA hB x y hxy v
22     simp only [LinearMap.add_apply, map_add, hA x y hxy v, hB x y hxy v]
23   smul_mem' := by
24     intro c A hA x y hxy v
25     simp only [LinearMap.smul_apply, map_smul, hA x y hxy v]
26 
27 variable (ι : K →* G) (N : Subgroup K) (q : K →* Q) (hN : N ≤ q.ker)
28   (κ : Representation k K W) (σ : Representation k Q U)
29   (g : G) (S : W →ₗ[k] W) (hS : S ≠ 0) (hs : Along ι κ g S)
30   (hline : ∀ A : W →ₗ[k] W,
31     Along (ι.comp N.subtype) (κ.comp N.subtype) g A → ∃ c : k, A = c • S)
32 
33 def tensorMap : space ι (σ.comp q) g →ₗ[k] space ι (κ.tprod (σ.comp q)) g where
34   toFun R := ⟨TensorProduct.map S R, map_along ι q κ σ g S hs R R.property⟩
35   map_add' R R' := by
36     apply Subtype.ext
37     exact TensorProduct.map_add_right S (R : U →ₗ[k] U) (R' : U →ₗ[k] U)
38   map_smul' c R := by
39     apply Subtype.ext
40     exact TensorProduct.map_smul_right c S (R : U →ₗ[k] U)
41 
42 /-- Literal operator spaces, with forward map R ↦ S ⊗ R. -/
43 def equivalence : space ι (σ.comp q) g ≃ₗ[k] space ι (κ.tprod (σ.comp q)) g :=
44   LinearEquiv.ofBijective (tensorMap ι q κ σ g S hs) ⟨by
45     intro R R' h
46     apply Subtype.ext
47     apply map_left_injective S hS
48     exact congrArg Subtype.val h, by
49     intro T
50     obtain ⟨R, hr, hR⟩ := factor_along ι N q hN κ σ g S hS hs hline T T.property
51     exact ⟨⟨R, hR⟩, Subtype.ext hr.symm⟩⟩
52 
53 include hN hS hs hline in
54 theorem finrank_eq :
55     Module.finrank k (space ι (σ.comp q) g) =
56       Module.finrank k (space ι (κ.tprod (σ.comp q)) g) :=
57   (equivalence ι N q hN κ σ g S hS hs hline).finrank_eq
58 
59 /-- The line certificate follows from the literal dimension-one statement and
60 the defining centralizer-intertwining property of a beta extension. -/
61 theorem line_of_dimension
62     (hdim : Module.finrank k (space (ι.comp N.subtype) (κ.comp N.subtype) g) = 1)
63     (hκ : ExistsAt ι κ g) :
64     ∃ S : W →ₗ[k] W, S ≠ 0 ∧ Along ι κ g S ∧
65       ∀ A : W →ₗ[k] W,
66         Along (ι.comp N.subtype) (κ.comp N.subtype) g A → ∃ c : k, A = c • S := by
67   obtain ⟨S, hn, hs⟩ := hκ
68   have hsr : Along (ι.comp N.subtype) (κ.comp N.subtype) g S := by
69     intro x y hxy w
70     exact hs x y hxy w
71   let v : space (ι.comp N.subtype) (κ.comp N.subtype) g := ⟨S, hsr⟩
72   have hv : v ≠ 0 := by
73     intro h
74     exact hn (congrArg Subtype.val h)
75   refine ⟨S, hn, hs, ?_⟩
76   intro A hA
77   obtain ⟨c, hc⟩ := exists_smul_eq_of_finrank_eq_one hdim hv
78     (⟨A, hA⟩ : space (ι.comp N.subtype) (κ.comp N.subtype) g)
79   exact ⟨c, (congrArg Subtype.val hc).symm⟩
80 
81 end PaperXI.IntertwiningSpace107

Back to source controls