MonomialInductionSubgroup.lean

1 import PaperXI.MonomialInductionTransitive
2 
3 /-! Induction from a specified subgroup and its actual scalar character. -/
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 
10 /-- A supplied character that acts on the nonzero line equals its actual scalar
11 character once the supplied subgroup is identified with the line stabilizer. -/
12 def equivalenceOfSubgroup
13     (ρ : Representation ℂ G V) (v : V) (hv : v ≠ 0)
14     (b : Basis X ℂ V) (r : X → G) (a : X → ℂˣ)
15     (hr : ∀ i, ρ (r i) v = (a i : ℂ) • b i)
16     (hmono : ∀ g : G, ∃ i : X, ∃ d : ℂˣ, ρ g v = (d : ℂ) • b i)
17     (S : Subgroup G) (χ : S →* ℂˣ) (hS : S = stabilizer ρ v)
18     (hχ : ∀ s : S, ρ (s : G) v = (χ s : ℂ) • v) :
19     Representation.Equiv (Representation.ind S.subtype (scalarRepresentation χ)) ρ := by
20   subst S
21   have he : χ = character ρ v hv := by
22     apply MonoidHom.ext
23     intro s
24     apply Units.ext
25     apply LineCharacter.scalar_unique hv
26     rw [← hχ s, ← LineCharacter.character_action]
27   subst χ
28   exact equivalence ρ v hv b r a hr hmono
29 
30 /-- The transitive criterion accepts the actual scalar action on the base line. -/
31 def transitiveEquivalenceOfSubgroupAction
32     (ρ : Representation ℂ G V) (b : Basis X ℂ V)
33     (p : G →* Equiv.Perm X) (c : G → X → ℂˣ)
34     (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x)) (x₀ : X)
35     (htrans : ∀ x : X, ∃ g : G, p g x₀ = x)
36     (S : Subgroup G) (χ : S →* ℂˣ)
37     (hS : ∀ g : G, g ∈ S ↔ p g x₀ = x₀)
38     (hχ : ∀ s : S, ρ (s : G) (b x₀) = (χ s : ℂ) • b x₀) :
39     Representation.Equiv (Representation.ind S.subtype (scalarRepresentation χ)) ρ := by
40   apply equivalenceOfSubgroup ρ (b x₀) (b.ne_zero x₀) b
41     (representative p x₀ htrans) (fun x => c (representative p x₀ htrans x) x₀)
42     (representative_action ρ b p c hρ x₀ htrans)
43     (orbit_is_monomial ρ b p c hρ x₀) S χ
44   · ext g
45     rw [hS, mem_lineStabilizer_iff ρ b p c hρ x₀]
46   · exact hχ
47 
48 /-- The transitive monomial criterion with an independently specified subgroup
49 and character.  Subgroup equality is proved from its point-stabilizer formula. -/
50 def transitiveEquivalenceOfSubgroup
51     (ρ : Representation ℂ G V) (b : Basis X ℂ V)
52     (p : G →* Equiv.Perm X) (c : G → X → ℂˣ)
53     (hρ : ∀ g x, ρ g (b x) = (c g x : ℂ) • b (p g x)) (x₀ : X)
54     (htrans : ∀ x : X, ∃ g : G, p g x₀ = x)
55     (S : Subgroup G) (χ : S →* ℂˣ)
56     (hS : ∀ g : G, g ∈ S ↔ p g x₀ = x₀)
57     (hχ : ∀ s : S, (χ s : ℂ) = c (s : G) x₀) :
58     Representation.Equiv (Representation.ind S.subtype (scalarRepresentation χ)) ρ := by
59   apply equivalenceOfSubgroup ρ (b x₀) (b.ne_zero x₀) b
60     (representative p x₀ htrans) (fun x => c (representative p x₀ htrans x) x₀)
61     (representative_action ρ b p c hρ x₀ htrans)
62     (orbit_is_monomial ρ b p c hρ x₀) S χ
63   · ext g
64     rw [hS, mem_lineStabilizer_iff ρ b p c hρ x₀]
65   · intro s
66     have hs := (hS (s : G)).mp s.property
67     rw [hρ, hs, hχ]
68 
69 end PaperXI.MonomialInduction

Back to source controls