IntertwiningAlong105.lean

1 import Mathlib.RepresentationTheory.Basic
2 import Mathlib.Tactic.Group
3 
4 /-! Intertwining on a literal embedded subgroup, with exact carrier maps and
5 transport through both compact factors. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.IntertwiningAlong105
9 open Representation
10 variable {k K G V : Type*} [Field k] [Group K] [Group G]
11   [AddCommGroup V] [Module k V]
12 
13 theorem act_mul (ρ : Representation k K V) (a b : K) (v : V) :
14     ρ (a * b) v = ρ a (ρ b v) := by rw [map_mul, Module.End.mul_apply]
15 
16 theorem act_inv_cancel (ρ : Representation k K V) (a : K) (v : V) :
17     ρ a⁻¹ (ρ a v) = v := by
18   rw [← act_mul, inv_mul_cancel, map_one, Module.End.one_apply]
19 
20 theorem act_mul_inv_cancel (ρ : Representation k K V) (a : K) (v : V) :
21     ρ a (ρ a⁻¹ v) = v := by
22   rw [← act_mul, mul_inv_cancel, map_one, Module.End.one_apply]
23 
24 /-- All pairs of original subgroup elements, not an abstract support label. -/
25 def Along (ι : K →* G) (ρ : Representation k K V) (g : G)
26     (T : V →ₗ[k] V) : Prop :=
27   ∀ x y : K, ι y = g * ι x * g⁻¹ → ∀ v, T (ρ x v) = ρ y (T v)
28 
29 def ExistsAt (ι : K →* G) (ρ : Representation k K V) (g : G) : Prop :=
30   ∃ T : V →ₗ[k] V, T ≠ 0 ∧ Along ι ρ g T
31 
32 theorem left_right (ι : K →* G) (ρ : Representation k K V)
33     (a b : K) (g : G) (T : V →ₗ[k] V)
34     (hT : Along ι ρ (ι a * g * ι b) T) :
35     Along ι ρ g ((ρ a⁻¹).comp (T.comp (ρ b⁻¹))) := by
36   intro x y hxy v
37   have hrel : ι (a * y * a⁻¹) =
38       (ι a * g * ι b) * ι (b⁻¹ * x * b) * (ι a * g * ι b)⁻¹ := by
39     simp only [map_mul, map_inv]
40     rw [hxy]
41     group
42   have h := hT (b⁻¹ * x * b) (a * y * a⁻¹) hrel (ρ b⁻¹ v)
43   have h' := congrArg (fun w => ρ a⁻¹ w) h
44   simpa only [LinearMap.comp_apply, act_mul, act_inv_cancel, act_mul_inv_cancel] using h'
45 
46 theorem left_right_ne_zero (ρ : Representation k K V)
47     (a b : K) (T : V →ₗ[k] V) (hT : T ≠ 0) :
48     (ρ a⁻¹).comp (T.comp (ρ b⁻¹)) ≠ 0 := by
49   intro he
50   apply hT
51   ext v
52   have h := congrArg (fun f : V →ₗ[k] V => ρ a (f (ρ b v))) he
53   simpa only [LinearMap.comp_apply, LinearMap.zero_apply, map_zero,
54     act_mul_inv_cancel, act_inv_cancel] using h
55 
56 theorem existsAt_of_left_right (ι : K →* G) (ρ : Representation k K V)
57     (a b : K) (g : G) (h : ExistsAt ι ρ (ι a * g * ι b)) :
58     ExistsAt ι ρ g := by
59   obtain ⟨T, hT, h⟩ := h
60   exact ⟨_, left_right_ne_zero ρ a b T hT, left_right ι ρ a b g T h⟩
61 
62 theorem remove_central (ι : K →* G) (ρ : Representation k K V)
63     (c g : G) (hc : ∀ x : G, Commute c x) (T : V →ₗ[k] V)
64     (hT : Along ι ρ (c * g) T) : Along ι ρ g T := by
65   intro x y hxy v
66   apply hT x y _ v
67   calc
68     ι y = g * ι x * g⁻¹ := hxy
69     _ = c * (g * ι x * g⁻¹) * c⁻¹ := by rw [(hc _).eq]; simp
70     _ = (c * g) * ι x * (c * g)⁻¹ := by group
71 
72 theorem existsAt_remove_central (ι : K →* G) (ρ : Representation k K V)
73     (c g : G) (hc : ∀ x : G, Commute c x)
74     (h : ExistsAt ι ρ (c * g)) : ExistsAt ι ρ g := by
75   obtain ⟨T, hn, ht⟩ := h
76   exact ⟨T, hn, remove_central ι ρ c g hc T ht⟩
77 
78 end PaperXI.IntertwiningAlong105

Back to source controls