IrreducibleCharacterRigidity.lean

1 import PaperX.GeneralCharacters
2 
3 /-! Character rigidity for actual finite-dimensional irreducible representations.
4 The monoid need not be finite, and the characteristic-zero coefficient field need
5 not be algebraically closed. The topological consequence retains density of the
6 conjugacy-saturated samples as an explicit hypothesis. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.IrreducibleCharacterRigidity
10 universe u
11 
12 section Algebra
13 variable {K G : Type*} {V W : Type u} [Field K] [Monoid G]
14 variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
15 
16 /-- An actual equivariant linear isomorphism preserves the actual character. -/
17 theorem character_eq_of_equiv (ρ : Representation K G V) (τ : Representation K G W)
18     (h : Nonempty (ρ.Equiv τ)) : ρ.character = τ.character := by
19   obtain ⟨e⟩ := h
20   exact Representation.char_iso e
21 
22 variable [CharZero K] [FiniteDimensional K V] [FiniteDimensional K W]
23 
24 /-- Character equality detects equivalence of irreducible representations on
25 possibly different vector spaces, for an arbitrary acting monoid. -/
26 theorem equiv_iff_character_eq (ρ : Representation K G V) (τ : Representation K G W)
27     [ρ.IsIrreducible] [τ.IsIrreducible] :
28     Nonempty (ρ.Equiv τ) ↔ ρ.character = τ.character := by
29   constructor
30   · exact character_eq_of_equiv ρ τ
31   intro hchar
32   by_contra hno
33   let U : Bool → Type _ := fun b => match b with
34     | false => V
35     | true => W
36   let (b : Bool) : AddCommGroup (U b) := by
37     cases b <;> dsimp [U] <;> infer_instance
38   let (b : Bool) : Module K (U b) := by
39     cases b <;> dsimp [U] <;> infer_instance
40   let (b : Bool) : FiniteDimensional K (U b) := by
41     cases b <;> dsimp [U] <;> infer_instance
42   let R : (b : Bool) → Representation K G (U b) := fun b => match b with
43     | false => ρ
44     | true => τ
45   let (b : Bool) : (R b).IsIrreducible := by
46     cases b <;> dsimp [R] <;> infer_instance
47   have hne : ∀ i j, Nonempty ((R i).Equiv (R j)) → i = j := by
48     intro i j hij
49     cases i <;> cases j
50     · rfl
51     · exact False.elim (hno hij)
52     · obtain ⟨e⟩ := hij
53       exact False.elim (hno ⟨e.symm⟩)
54     · rfl
55   have hi := PaperX.GeneralCharacters.independent_irreducible_characters R hne
56   have hbad : false = true := hi.injective hchar
57   cases hbad
58 
59 end Algebra
60 
61 section Topological
62 variable {K G X : Type*} {V W : Type u} [Field K] [CharZero K] [Group G]
63 variable [AddCommGroup V] [Module K V] [FiniteDimensional K V]
64 variable [AddCommGroup W] [Module K W] [FiniteDimensional K W]
65 variable [TopologicalSpace G] [TopologicalSpace K] [T2Space K]
66 
67 omit [CharZero K] [FiniteDimensional K V] [FiniteDimensional K W] in
68 /-- Continuous actual characters agreeing on samples agree everywhere when
69 the conjugacy saturation of those samples is dense. -/
70 theorem character_eq_of_dense_samples
71     (ρ : Representation K G V) (τ : Representation K G W)
72     (hρ : Continuous ρ.character) (hτ : Continuous τ.character) (s : X → G)
73     (hd : DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹))
74     (he : ∀ x, ρ.character (s x) = τ.character (s x)) :
75     ρ.character = τ.character := by
76   apply hd.equalizer hρ hτ
77   funext p
78   simpa only [Function.comp_apply, Representation.char_conj] using he p.1
79 
80 /-- Dense conjugacy samples determine the equivalence class of an actual
81 irreducible representation. Arithmetic density is an input to this theorem. -/
82 theorem equiv_of_dense_character_eq
83     (ρ : Representation K G V) (τ : Representation K G W)
84     [ρ.IsIrreducible] [τ.IsIrreducible]
85     (hρ : Continuous ρ.character) (hτ : Continuous τ.character) (s : X → G)
86     (hd : DenseRange (fun p : X × G => p.2 * s p.1 * p.2⁻¹))
87     (he : ∀ x, ρ.character (s x) = τ.character (s x)) :
88     Nonempty (ρ.Equiv τ) :=
89   (equiv_iff_character_eq ρ τ).mpr
90     (character_eq_of_dense_samples ρ τ hρ hτ s hd he)
91 
92 end Topological
93 end PaperX.IrreducibleCharacterRigidity

Back to source controls