HeisenbergTrace108.lean

1 import Mathlib.RepresentationTheory.Character
2 import Mathlib.Analysis.Complex.Basic
3 
4 /-! The finite Heisenberg character formula, derived from scalar restriction
5 and detection by actual commutators. No trace-support hypothesis is supplied. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.HeisenbergTrace108
9 open Representation
10 variable {K W : Type*} [Group K] [AddCommGroup W] [Module ℂ W]
11   [FiniteDimensional ℂ W]
12   (H : Subgroup K) (θ : H →* ℂˣ) (ρ : Representation ℂ K W)
13   (hscalar : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
14 
15 include hscalar in
16 theorem character_on_subgroup (h : H) :
17     ρ.character h = (Module.finrank ℂ W : ℂ) * (θ h : ℂ) := by
18   simp [Representation.character, hscalar, mul_comm]
19 
20 omit [FiniteDimensional ℂ W] in
21 include hscalar in
22 /-- A commutator with nontrivial central character forces trace zero. -/
23 theorem character_zero_of_commutator (x y : K) (z : H)
24     (he : y * x * y⁻¹ = (z : K) * x) (hz : θ z ≠ 1) : ρ.character x = 0 := by
25   have ht := ρ.char_conj x y
26   rw [he] at ht
27   have hs : ρ.character ((z : K) * x) = (θ z : ℂ) * ρ.character x := by
28     simp [Representation.character, map_mul, hscalar, Module.End.mul_eq_comp]
29   rw [hs] at ht
30   have hc : (θ z : ℂ) - 1 ≠ 0 := by
31     intro h
32     apply hz
33     apply Units.ext
34     exact sub_eq_zero.mp h
35   apply (mul_eq_zero.mp (show ((θ z : ℂ) - 1) * ρ.character x = 0 by
36     rw [sub_mul, one_mul, ht, sub_self])).resolve_left hc
37 
38 omit [FiniteDimensional ℂ W] in
39 include hscalar in
40 theorem character_off_subgroup
41     (hdetect : ∀ x : K, x ∉ H → ∃ y : K, ∃ z : H,
42       y * x * y⁻¹ = (z : K) * x ∧ θ z ≠ 1)
43     (x : K) (hx : x ∉ H) : ρ.character x = 0 := by
44   obtain ⟨y, z, he, hz⟩ := hdetect x hx
45   exact character_zero_of_commutator H θ ρ hscalar x y z he hz
46 
47 end PaperXI.HeisenbergTrace108

Back to source controls