CyclicLinearization.lean

1 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
2 import Mathlib.Analysis.Complex.Polynomial.Basic
3 import Mathlib.GroupTheory.SpecificGroups.Cyclic
4 
5 /-! A genuine projective representation of a finite cyclic group lifts to GL.
6 The projective representation is an actual homomorphism to Mathlib's PGL,
7 and equality after projection is the conclusion, not a hypothesis. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CyclicLinearization
11 open scoped MatrixGroups
12 
13 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
14 
15 /-- Every nonzero complex scalar has a nonzero root of any positive order. -/
16 theorem unit_root (a : ℂˣ) {m : ℕ} (hm : 0 < m) :
17     ∃ u : ℂˣ, u ^ m = a := by
18   obtain ⟨z, hz⟩ := IsAlgClosed.exists_pow_nat_eq (a : ℂ) hm
19   have hne : z ≠ 0 := by
20     intro h
21     rw [h, zero_pow (Nat.ne_of_gt hm)] at hz
22     exact a.ne_zero hz.symm
23   refine ⟨Units.mk0 z hne, ?_⟩
24   apply Units.ext
25   exact hz
26 
27 /-- A GL lift of a finite-order projective element can be rescaled to have
28 that finite order relation itself. -/
29 theorem rescale_generator (T : GL ι ℂ) {m : ℕ} (hm : 0 < m)
30     (hT : Matrix.ProjGenLinGroup.mk T ^ m = 1) :
31     ∃ S : GL ι ℂ, S ^ m = 1 ∧
32       Matrix.ProjGenLinGroup.mk S = Matrix.ProjGenLinGroup.mk T := by
33   have hc : T ^ m ∈ Subgroup.center (GL ι ℂ) := by
34     apply Matrix.ProjGenLinGroup.mk_eq_one.mp
35     simpa only [map_pow] using hT
36   rw [Matrix.GeneralLinearGroup.center_eq_range_scalar] at hc
37   obtain ⟨a, ha⟩ := hc
38   obtain ⟨u, hu⟩ := unit_root a⁻¹ hm
39   refine ⟨Matrix.GeneralLinearGroup.scalar ι u * T, ?_, ?_⟩
40   · have hcomm : Commute (Matrix.GeneralLinearGroup.scalar ι u) T :=
41       Matrix.GeneralLinearGroup.scalar_commute u T
42     rw [hcomm.mul_pow, ← map_pow, hu, ← ha, ← map_mul]
43     simp
44   · simp
45 
46 variable {G : Type*} [Group G]
47 
48 /-- A projective cyclic action lifts, using any explicitly supplied generator
49 of finite positive order. -/
50 theorem lift_of_generator (π : G →* PGL(ι, ℂ)) (g : G)
51     (hg : ∀ x, x ∈ Subgroup.zpowers g) (hm : 0 < orderOf g) :
52     ∃ ρ : G →* GL ι ℂ, Matrix.ProjGenLinGroup.mk.comp ρ = π := by
53   obtain ⟨T, hT⟩ := Matrix.ProjGenLinGroup.mk_surjective (π g)
54   have hp : Matrix.ProjGenLinGroup.mk T ^ orderOf g = 1 := by
55     rw [hT, ← map_pow, pow_orderOf_eq_one, map_one]
56   obtain ⟨S, hS, hproj⟩ := rescale_generator T hm hp
57   let ρ : G →* GL ι ℂ := monoidHomOfForallMemZpowers hg
58     (orderOf_dvd_of_pow_eq_one hS)
59   refine ⟨ρ, (MonoidHom.eq_iff_eq_on_generator hg _ _).mpr ?_⟩
60   change Matrix.ProjGenLinGroup.mk (ρ g) = π g
61   rw [monoidHomOfForallMemZpowers_apply_gen, hproj, hT]
62 
63 /-- Paper XI Lemma 11.4: every projective representation of a finite cyclic
64 group over the complex numbers is the projectivization of an honest action. -/
65 theorem finite_cyclic_linearization [Finite G] [IsCyclic G]
66     (π : G →* PGL(ι, ℂ)) :
67     ∃ ρ : G →* GL ι ℂ, Matrix.ProjGenLinGroup.mk.comp ρ = π := by
68   obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
69   exact lift_of_generator π g hg (orderOf_pos g)
70 
71 /-- Pointwise projective equality gives actual invertible scalar changes of
72 any chosen lifts of the input projective action. -/
73 theorem finite_cyclic_scalar_equivalence [Finite G] [IsCyclic G]
74     (π : G →* PGL(ι, ℂ)) (T : G → GL ι ℂ)
75     (hT : ∀ g, Matrix.ProjGenLinGroup.mk (T g) = π g) :
76     ∃ ρ : G →* GL ι ℂ, ∀ g, ∃ u : ℂˣ,
77       T g * Matrix.GeneralLinearGroup.scalar ι u = ρ g := by
78   obtain ⟨ρ, hρ⟩ := finite_cyclic_linearization π
79   refine ⟨ρ, fun g => Matrix.ProjGenLinGroup.mk_eq_mk_iff.mp ?_⟩
80   rw [hT g]
81   exact (DFunLike.congr_fun hρ g).symm
82 
83 end PaperXI.CyclicLinearization

Back to source controls