CharacterGenerators.lean

1 import PaperXI.CyclicBridge
2 import Mathlib.Algebra.Group.Subgroup.Basic
3 
4 /-! Triviality of the actual stabilizer discrepancy on a generating set. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CharacterGenerators
8 
9 variable {C D : Type*} [Group C] [Group D]
10 
11 /-- Kernel membership propagates from generators through the subgroup closure. -/
12 theorem eq_one_on_closure (δ : C →* D) (S : Set C)
13     (hS : ∀ g ∈ S, δ g = 1) : ∀ g ∈ Subgroup.closure S, δ g = 1 := by
14   have hle : Subgroup.closure S ≤ δ.ker := (Subgroup.closure_le δ.ker).mpr hS
15   exact fun g hg => hle hg
16 
17 /-- The arbitrary generating-set test, including noncyclic stabilizers. -/
18 theorem trivial (δ : C →* D) (S : Set C) (hgen : Subgroup.closure S = ⊤)
19     (hS : ∀ g ∈ S, δ g = 1) : ∀ g, δ g = 1 := by
20   intro g
21   apply eq_one_on_closure δ S hS
22   rw [hgen]
23   trivial
24 
25 theorem trivial_iff (δ : C →* D) (S : Set C) (hgen : Subgroup.closure S = ⊤) :
26     (∀ g, δ g = 1) ↔ ∀ g ∈ S, δ g = 1 :=
27   ⟨fun h g _ => h g, trivial δ S hgen⟩
28 
29 variable {H V W : Type*} [Group H]
30 variable [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
31 variable [AddCommGroup W] [Module ℂ W]
32 
33 /-- Actual honest stabilizer actions produce the character. Generator values
34 of this character close the whole semidirect-product bridge. -/
35 theorem bridge_from_actions
36     (ρ : Representation ℂ H V) [Representation.IsIrreducible ρ]
37     (σ : Representation ℂ H W) (U : V ≃ₗ[ℂ] W)
38     (hU : ∀ h x, U (ρ h x) = σ h (U x))
39     (α : C →* MulAut H) (R : Representation ℂ C V) (T : Representation ℂ C W)
40     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x))
41     (hT : ∀ g h x, T g (σ h x) = σ (α g h) (T g x))
42     (S : Set C) (hgen : Subgroup.closure S = ⊤) :
43     ∃ δ : C →* ℂˣ,
44       (∀ g x, U (R g x) = (δ g : ℂ) • T g (U x)) ∧
45       ((∀ g ∈ S, δ g = 1) → ∀ a x,
46         U (CyclicBridge.semidirectRepresentation α ρ R hR a x) =
47           CyclicBridge.semidirectRepresentation α σ T hT a (U x)) := by
48   obtain ⟨δ, hδ⟩ := DiscrepancyCharacter.exists_character ρ σ U hU α R T hR hT
49   refine ⟨δ, hδ, ?_⟩
50   intro hs
51   apply CyclicBridge.semidirect_intertwining α
52     (CyclicBridge.semidirectRepresentation α ρ R hR)
53     (CyclicBridge.semidirectRepresentation α σ T hT) U
54   · simpa only [CyclicBridge.semidirectRepresentation_inl] using hU
55   · intro g x
56     simpa only [CyclicBridge.semidirectRepresentation_inr, trivial δ S hgen hs g,
57       Units.val_one, one_smul] using hδ g x
58 
59 end PaperXI.CharacterGenerators

Back to source controls