MonomialInductionTransitive.lean

1 import PaperXI.MonomialInduction
2 
3 /-! The transitive weighted permutation criterion for actual induced representations. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.MonomialInduction
7 open Representation Module
8 variable {G X V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
9 variable (ρ : Representation ℂ G V) (b : Basis X ℂ V)
10   (p : G →* Equiv.Perm X) (c : G → X → ℂˣ)
11   (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x)) (x₀ : X)
12 
13 include hρ in
14 /-- The actual line stabilizer equals the stabilizer of the basis index. -/
15 theorem mem_lineStabilizer_iff (g : G) :
16     g ∈ LineCharacter.lineStabilizer ρ (b x₀) ↔ p g x₀ = x₀ := by
17   constructor
18   · rintro ⟨d, hd⟩
19     by_contra hne
20     have he : (c g x₀ : ℂ) • b (p g x₀) = d • b x₀ := (hρ g x₀).symm.trans hd
21     have hc := congrArg (fun w => (b.repr w) (p g x₀)) he
22     simp [hne] at hc
23   · intro hg
24     exact ⟨(c g x₀ : ℂ), by simpa [hg] using hρ g x₀⟩
25 
26 include hρ in
27 /-- On that subgroup, the scalar character is the supplied actual basis weight. -/
28 theorem character_eq_weight (g : LineCharacter.lineStabilizer ρ (b x₀)) :
29     (LineCharacter.character ρ (b x₀) (b.ne_zero x₀) g : ℂ) = c (g : G) x₀ := by
30   apply LineCharacter.scalar_unique (b.ne_zero x₀)
31   rw [← LineCharacter.character_action]
32   have hg := (mem_lineStabilizer_iff ρ b p c hρ x₀ (g : G)).mp g.property
33   simpa [hg] using hρ (g : G) x₀
34 
35 variable (htrans : ∀ x : X, ∃ g : G, p g x₀ = x)
36 
37 /-- Representatives are chosen from transitivity, not assumed to index cosets. -/
38 def representative : X → G := fun x => Classical.choose (htrans x)
39 
40 theorem representative_spec (x : X) : p (representative p x₀ htrans x) x₀ = x :=
41   Classical.choose_spec (htrans x)
42 
43 include hρ in
44 theorem representative_action (x : X) :
45     ρ (representative p x₀ htrans x) (b x₀) =
46       (c (representative p x₀ htrans x) x₀ : ℂ) • b x := by
47   rw [hρ, representative_spec]
48 
49 include hρ in
50 theorem orbit_is_monomial (g : G) :
51     ∃ x : X, ∃ d : ℂˣ, ρ g (b x₀) = (d : ℂ) • b x :=
52   ⟨p g x₀, c g x₀, hρ g x₀⟩
53 
54 /-- Actual Mathlib induction of the point-stabilizer line character is isomorphic
55  to any representation with a transitive monomial basis. -/
56 def transitiveEquivalence : Representation.Equiv
57     (induced ρ (b x₀) (b.ne_zero x₀)) ρ :=
58   equivalence ρ (b x₀) (b.ne_zero x₀) b (representative p x₀ htrans)
59     (fun x => c (representative p x₀ htrans x) x₀)
60     (representative_action ρ b p c hρ x₀ htrans)
61     (orbit_is_monomial ρ b p c hρ x₀)
62 
63 @[simp] theorem transitiveEquivalence_mk (g : G) (z : ℂ) :
64     transitiveEquivalence ρ b p c hρ x₀ htrans
65       (IndV.mk (stabilizer ρ (b x₀)).subtype
66         (lineRepresentation ρ (b x₀) (b.ne_zero x₀)) g z) = z • ρ g⁻¹ (b x₀) :=
67   evaluation_mk ρ (b x₀) (b.ne_zero x₀) g z
68 
69 end PaperXI.MonomialInduction

Back to source controls