DiscrepancyCharacter.lean

1 import PaperXI.SchurScalar
2 
3 /-! Discrepancy of honest stabilizer actions is a character, derived from Schur. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.DiscrepancyCharacter
7 open PaperXI.GeneratedIrreducibility
8 variable {H C V W : Type*} [Group H] [Group C]
9 variable [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
10 variable [AddCommGroup W] [Module ℂ W]
11 
12 /-- No cyclicity is needed until the later generator test. -/
13 theorem exists_character (ρ : Representation ℂ H V) [Representation.IsIrreducible ρ]
14     (σ : Representation ℂ H W) (U : V ≃ₗ[ℂ] W)
15     (hU : ∀ h x, U (ρ h x) = σ h (U x))
16     (α : C →* MulAut H) (R : Representation ℂ C V) (S : Representation ℂ C W)
17     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x))
18     (hS : ∀ g h x, S g (σ h x) = σ (α g h) (S g x)) :
19     ∃ δ : C →* ℂˣ, ∀ g x, U (R g x) = (δ g : ℂ) • S g (U x) := by
20   have hs (g : C) : ∃! c : ℂˣ, ∀ x, U (R g x) = (c : ℂ) • S g (U x) := by
21     let σg : Representation ℂ H W := σ.comp (α g).toMonoidHom
22     have hB (h : H) (x : V) : (U.trans (actionEquiv S g)) (ρ h x) =
23         σg h ((U.trans (actionEquiv S g)) x) := by
24       change S g (U (ρ h x)) = σ (α g h) (S g (U x))
25       rw [hU, hS]
26     have hA (h : H) (x : V) : ((actionEquiv R g).trans U) (ρ h x) =
27         σg h (((actionEquiv R g).trans U) x) := by
28       change U (R g (ρ h x)) = σ (α g h) (U (R g x))
29       rw [hR, hU]
30     exact PaperXI.SchurScalar.bridge_unique ρ σg (U.trans (actionEquiv S g))
31       ((actionEquiv R g).trans U) hB hA
32   choose d hd hu using hs
33   have hone : d 1 = 1 := by
34     symm
35     apply hu 1 1
36     intro x
37     simp
38   have hmul (g h : C) : d (g * h) = d g * d h := by
39     symm
40     apply hu (g * h) (d g * d h)
41     intro x
42     calc
43       U (R (g * h) x) = U (R g (R h x)) := by rw [map_mul]; rfl
44       _ = (d g : ℂ) • S g (U (R h x)) := hd g (R h x)
45       _ = (d g : ℂ) • S g ((d h : ℂ) • S h (U x)) := by rw [hd h]
46       _ = ((d g * d h : ℂˣ) : ℂ) • S (g * h) (U x) := by
47         simp [map_mul, Module.End.mul_apply, smul_smul]
48   exact ⟨{ toFun := d, map_one' := hone, map_mul' := hmul }, hd⟩
49 
50 end PaperXI.DiscrepancyCharacter

Back to source controls