QuotientRepresentation.lean

1 import Mathlib.RepresentationTheory.Irreducible
2 import Mathlib.GroupTheory.QuotientGroup.Basic
3 
4 /-! Actual representation descent through a quotient group and preservation
5 of irreducibility and intertwining equations under a surjective group map. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.QuotientRepresentation
9 
10 variable {k G Q V W : Type*} [Field k] [Group G] [Group Q]
11 variable [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
12 
13 /-- Surjective pullback preserves precisely the actual stable subspaces. -/
14 def subrepresentationEquiv (q : G →* Q) (hq : Function.Surjective q)
15     (σ : Representation k Q V) :
16     Subrepresentation (σ.comp q) ≃o Subrepresentation σ where
17   toFun S := ⟨S.toSubmodule, fun a v hv => by
18     obtain ⟨g, rfl⟩ := hq a
19     exact S.apply_mem_toSubmodule g hv⟩
20   invFun S := ⟨S.toSubmodule, fun g _ hv => S.apply_mem_toSubmodule (q g) hv⟩
21   left_inv _ := Subrepresentation.toSubmodule_injective rfl
22   right_inv _ := Subrepresentation.toSubmodule_injective rfl
23   map_rel_iff' := Iff.rfl
24 
25 theorem irreducible_comp_iff (q : G →* Q) (hq : Function.Surjective q)
26     (σ : Representation k Q V) :
27     Representation.IsIrreducible (σ.comp q) ↔ Representation.IsIrreducible σ :=
28   (subrepresentationEquiv q hq σ).isSimpleOrder_iff
29 
30 theorem intertwines_comp_iff (q : G →* Q) (hq : Function.Surjective q)
31     (ρ : Representation k Q V) (σ : Representation k Q W) (F : V →ₗ[k] W) :
32     (∀ g v, F (ρ (q g) v) = σ (q g) (F v)) ↔
33       ∀ a v, F (ρ a v) = σ a (F v) := by
34   constructor
35   · intro h a v
36     obtain ⟨g, rfl⟩ := hq a
37     exact h g v
38   · intro h g v
39     exact h (q g) v
40 
41 /-- Descend the supplied action after proving the actual kernel condition. -/
42 def descend (N : Subgroup G) [N.Normal] (σ : Representation k G V)
43     (hN : N ≤ σ.ker) : Representation k (G ⧸ N) V :=
44   QuotientGroup.lift N σ hN
45 
46 @[simp] theorem descend_apply (N : Subgroup G) [N.Normal] (σ : Representation k G V)
47     (hN : N ≤ σ.ker) (g : G) : descend N σ hN (QuotientGroup.mk' N g) = σ g := rfl
48 
49 @[simp] theorem descend_comp (N : Subgroup G) [N.Normal] (σ : Representation k G V)
50     (hN : N ≤ σ.ker) : (descend N σ hN).comp (QuotientGroup.mk' N) = σ := rfl
51 
52 theorem descend_irreducible_iff (N : Subgroup G) [N.Normal] (σ : Representation k G V)
53     (hN : N ≤ σ.ker) :
54     Representation.IsIrreducible (descend N σ hN) ↔ Representation.IsIrreducible σ :=
55   (irreducible_comp_iff (QuotientGroup.mk' N) QuotientGroup.mk_surjective
56     (descend N σ hN)).symm
57 
58 theorem descend_irreducible (N : Subgroup G) [N.Normal] (σ : Representation k G V)
59     (hN : N ≤ σ.ker) [Representation.IsIrreducible σ] :
60     Representation.IsIrreducible (descend N σ hN) :=
61   (descend_irreducible_iff N σ hN).mpr inferInstance
62 
63 /-- The quotient action is determined by its evaluation on actual representatives. -/
64 theorem descend_unique (N : Subgroup G) [N.Normal] (σ : Representation k G V)
65     (hN : N ≤ σ.ker) (τ : Representation k (G ⧸ N) V)
66     (hτ : ∀ g, τ (QuotientGroup.mk' N g) = σ g) : τ = descend N σ hN := by
67   apply MonoidHom.ext
68   intro a
69   obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective a
70   exact hτ g
71 
72 end PaperXI.QuotientRepresentation

Back to source controls