SchurScalar.lean

1 import PaperXI.GeneratedIrreducibility
2 import Mathlib.Analysis.Complex.Polynomial.Basic
3 
4 /-! Scalar commutants and uniqueness of actual irreducible representation bridges. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.SchurScalar
8 open PaperXI.GeneratedIrreducibility
9 variable {G V W : Type*} [Group G]
10 variable [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
11 variable [AddCommGroup W] [Module ℂ W]
12 
13 theorem commuting_scalar (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
14     (F : Module.End ℂ V) (hF : ∀ g x, F (ρ g x) = ρ g (F x)) :
15     ∃ c : ℂ, F = c • LinearMap.id := by
16   let f : Representation.IntertwiningMap ρ ρ :=
17     ⟨F, fun g => LinearMap.ext (hF g)⟩
18   obtain ⟨c, hc⟩ := (Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed
19     (ρ := ρ)).surjective f
20   refine ⟨c, ?_⟩
21   have h := congrArg Representation.IntertwiningMap.toLinearMap hc
22   exact h.symm
23 
24 omit [FiniteDimensional ℂ V] in
25 theorem scalar_unique (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
26     (F : Module.End ℂ V) {c d : ℂ} (hc : F = c • LinearMap.id) (hd : F = d • LinearMap.id) : c = d := by
27   have : Nontrivial V := nontrivial_space ρ
28   obtain ⟨v, hv⟩ := exists_ne (0 : V)
29   have h := LinearMap.congr_fun (hc.symm.trans hd) v
30   exact (smul_left_injective ℂ hv) h
31 
32 /-- An invertible operator in the commutant has a nonzero scalar. -/
33 theorem commuting_unit (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
34     (F : V ≃ₗ[ℂ] V) (hF : ∀ g x, F (ρ g x) = ρ g (F x)) :
35     ∃ c : ℂˣ, ∀ x, F x = (c : ℂ) • x := by
36   obtain ⟨c, hc⟩ := commuting_scalar ρ F.toLinearMap hF
37   have : Nontrivial V := nontrivial_space ρ
38   obtain ⟨v, hv⟩ := exists_ne (0 : V)
39   have hc0 : c ≠ 0 := by
40     intro hz
41     have h : F v = 0 := by simpa [hz] using LinearMap.congr_fun hc v
42     exact hv (F.injective (h.trans F.map_zero.symm))
43   exact ⟨Units.mk0 c hc0, fun x => LinearMap.congr_fun hc x⟩
44 
45 /-- Two actual invertible intertwiners differ by a unique nonzero scalar. -/
46 theorem bridge_unique (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
47     (σ : Representation ℂ G W) (U T : V ≃ₗ[ℂ] W)
48     (hU : ∀ g x, U (ρ g x) = σ g (U x))
49     (hT : ∀ g x, T (ρ g x) = σ g (T x)) :
50     ∃! c : ℂˣ, ∀ x, T x = (c : ℂ) • U x := by
51   have hcomm (g : G) (x : V) : (T.trans U.symm) (ρ g x) = ρ g ((T.trans U.symm) x) := by
52     apply U.injective
53     simp only [LinearEquiv.trans_apply, U.apply_symm_apply, hT, hU]
54   obtain ⟨c, hc⟩ := commuting_unit ρ (T.trans U.symm) hcomm
55   have hct (x : V) : T x = (c : ℂ) • U x := by
56     have h := congrArg U (hc x)
57     simpa using h
58   refine ⟨c, hct, ?_⟩
59   intro d hd
60   have : Nontrivial V := nontrivial_space ρ
61   obtain ⟨v, hv⟩ := exists_ne (0 : V)
62   have hUv : U v ≠ 0 := fun h => hv (U.injective (h.trans U.map_zero.symm))
63   apply Units.ext
64   exact (smul_left_injective ℂ hUv) ((hd v).symm.trans (hct v))
65 
66 end PaperXI.SchurScalar

Back to source controls