FullIntertwiningLocus69.lean

1 import PaperXI.InductionIrreducibility
2 
3 /-! Exact convention adapter for the full extended-type intertwining locus. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.FullIntertwiningLocus69
7 open Representation PaperXI.InductionIrreducibility
8 
9 variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
10   (H : Subgroup G) (σ : Representation k H V)
11 
12 /-- Actual full intertwining locus, with the intersection and conjugation of the
13 coefficient-model Mackey theorem, not a compact-subgroup substitute. -/
14 def locus : Set G :=
15   {g | ∃ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
16     (σ.comp (intersectionConjugation H g)), A ≠ 0}
17 
18 /-- An element of H intertwines by its own representation operator. -/
19 def internalIntertwiner (g : H) :
20     IntertwiningMap (σ.comp (intersectionSubgroup H (g : G)).subtype)
21       (σ.comp (intersectionConjugation H (g : G))) where
22   toLinearMap := σ g
23   isIntertwining' h := by
24     change σ g * σ (h : H) = σ (intersectionConjugation H (g : G) h) * σ g
25     rw [← map_mul, ← map_mul]
26     congr 1
27     apply Subtype.ext
28     simp [intersectionConjugation, mul_assoc]
29 
30 theorem internalIntertwiner_ne_zero [Nontrivial V] (g : H) :
31     internalIntertwiner H σ g ≠ 0 := by
32   intro he
33   obtain ⟨v, hv⟩ := exists_ne (0 : V)
34   have hz := congrArg (fun A => σ g⁻¹ (A v)) he
35   have hz' : σ g⁻¹ (σ g v) = 0 := by simpa [internalIntertwiner] using hz
36   have hi : σ g⁻¹ (σ g v) = v := by
37     rw [← Module.End.mul_apply, ← map_mul, inv_mul_cancel, map_one]
38     rfl
39   exact hv (hi.symm.trans hz')
40 
41 theorem subgroup_subset [Nontrivial V] :
42     (H : Set G) ⊆ locus H σ := by
43   intro g hg
44   exact ⟨internalIntertwiner H σ ⟨g,hg⟩, internalIntertwiner_ne_zero H σ ⟨g,hg⟩⟩
45 
46 /-- A genuine full-locus equality is exactly the hypothesis used by the
47 compact-mod-center induction theorem. -/
48 theorem locus_eq_iff [Nontrivial V] :
49     locus H σ = (H : Set G) ↔
50       ∀ g : G, g ∉ H →
51         ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
52           (σ.comp (intersectionConjugation H g)), A = 0 := by
53   constructor
54   · intro he g hg A
55     by_contra hA
56     have hm : g ∈ locus H σ := ⟨A,hA⟩
57     rw [he] at hm
58     exact hg hm
59   · intro h
60     apply Set.Subset.antisymm
61     · intro g hg
62       by_contra hgn
63       obtain ⟨A,hA⟩ := hg
64       exact hA (h g hgn A)
65     · exact subgroup_subset H σ
66 
67 
68 /-- The opposite common conjugation convention: its subgroup is
69 H intersect g H g-inverse and its conjugate operator is sigma(g-inverse h g).
70 This is the present literal coefficient convention at g-inverse. -/
71 def standardLocus : Set G := {g | g⁻¹ ∈ locus H σ}
72 
73 /-- Full subgroup equality is independent of the two inverse conventions.
74 This does not identify individual Hom spaces by assuming invertible maps. -/
75 theorem standardLocus_eq_iff :
76     standardLocus H σ = (H : Set G) ↔ locus H σ = (H : Set G) := by
77   constructor
78   · intro he
79     ext g
80     have ht := Set.ext_iff.mp he g⁻¹
81     simpa [standardLocus] using ht
82   · intro he
83     ext g
84     simp [standardLocus, he]
85 
86 /-- A source using the conventional inverse-conjugation definition supplies
87 exactly the full off-H premise of the existing Mackey construction. -/
88 theorem off_subgroup_of_standard_locus [Nontrivial V]
89     (hI : standardLocus H σ = (H : Set G)) :
90     ∀ g : G, g ∉ H →
91       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
92         (σ.comp (intersectionConjugation H g)), A = 0 :=
93   (locus_eq_iff H σ).mp ((standardLocus_eq_iff H σ).mp hI)
94 
95 end PaperXI.FullIntertwiningLocus69

Back to source controls