CentralExtensionComparison.lean

1 import PaperXI.CentralExtensionUniqueness
2 import PaperXI.HeisenbergTransport
3 
4 /-! The initial representation comparison along an actual extension lift,
5 without an odd-characteristic or coordinate-group restriction. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CentralExtensionComparison
9 open CentralExtension CocycleCommutator HeisenbergTransport
10 
11 variable {Z H A G V W : Type*} [CommGroup Z] [Group H] [CommGroup A] [Fintype A]
12 variable [Group G] [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
13 
14 /-- Construct the first representation equivalence along the actual group lift. -/
15 def equivAlong (D : Datum Z H A) (ζ : Z →* ℂˣ)
16     (hnd : radical (scalarCocycle D ζ) = ⊥) (e : H ≃* G)
17     (ρ : Representation ℂ H V) (σ : Representation ℂ G W)
18     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
19     (hρ : ∀ z, ρ (D.i z) = (ζ z : ℂ) • LinearMap.id)
20     (hσ : ∀ z, σ (e (D.i z)) = (ζ z : ℂ) • LinearMap.id) :
21     Representation.Equiv ρ (pullback e σ) := by
22   letI := pullback_irreducible e σ
23   exact CentralExtensionUniqueness.equiv D ζ hnd ρ (pullback e σ) hρ hσ
24 
25 theorem equivAlong_intertwines (D : Datum Z H A) (ζ : Z →* ℂˣ)
26     (hnd : radical (scalarCocycle D ζ) = ⊥) (e : H ≃* G)
27     (ρ : Representation ℂ H V) (σ : Representation ℂ G W)
28     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
29     (hρ : ∀ z, ρ (D.i z) = (ζ z : ℂ) • LinearMap.id)
30     (hσ : ∀ z, σ (e (D.i z)) = (ζ z : ℂ) • LinearMap.id) (h : H) (v : V) :
31     equivAlong D ζ hnd e ρ σ hρ hσ (ρ h v) =
32       σ (e h) (equivAlong D ζ hnd e ρ σ hρ hσ v) :=
33   Representation.IntertwiningMap.isIntertwining ρ (pullback e σ)
34     (equivAlong D ζ hnd e ρ σ hρ hσ).toIntertwiningMap h v
35 
36 /-- An actual lift and matching central actions determine an invertible
37 intertwiner, unique up to a unique nonzero complex scalar. -/
38 theorem exists_unique_along (D : Datum Z H A) (ζ : Z →* ℂˣ)
39     (hnd : radical (scalarCocycle D ζ) = ⊥) (e : H ≃* G)
40     (ρ : Representation ℂ H V) (σ : Representation ℂ G W)
41     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
42     (hρ : ∀ z, ρ (D.i z) = (ζ z : ℂ) • LinearMap.id)
43     (hσ : ∀ z, σ (e (D.i z)) = (ζ z : ℂ) • LinearMap.id) :
44     ∃ U : V ≃ₗ[ℂ] W, U.toLinearMap ≠ 0 ∧
45       (∀ h v, U (ρ h v) = σ (e h) (U v)) ∧
46       ∀ T : V ≃ₗ[ℂ] W, (∀ h v, T (ρ h v) = σ (e h) (T v)) →
47         ∃! c : ℂˣ, ∀ v, T v = (c : ℂ) • U v := by
48   let U := (equivAlong D ζ hnd e ρ σ hρ hσ).toLinearEquiv
49   have hU : ∀ h v, U (ρ h v) = σ (e h) (U v) :=
50     equivAlong_intertwines D ζ hnd e ρ σ hρ hσ
51   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space ρ
52   let : FiniteDimensional ℂ V := CentralExtensionUniqueness.finiteDimensional D ζ hnd ρ hρ
53   refine ⟨U, ?_, hU, ?_⟩
54   · intro h
55     obtain ⟨v, hv⟩ := exists_ne (0 : V)
56     have hz : U v = 0 := LinearMap.congr_fun h v
57     exact hv (U.injective (hz.trans U.map_zero.symm))
58   · intro T hT
59     exact SchurScalar.bridge_unique ρ (pullback e σ) U T hU hT
60 
61 end PaperXI.CentralExtensionComparison

Back to source controls