CentralCharacterRepresentation.lean

1 import PaperXI.CentralCharacterAction
2 
3 /-! Reconstruction of the actual central-character representation from an
4 algebra action, with both action roundtrips. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CentralCharacter
8 open PaperXI.CentralExtension
9 variable {Z H A W : Type*} [CommGroup Z] [Group H] [CommGroup A] [Fintype A]
10 variable [AddCommGroup W] [Module ℂ W]
11 
12 /-- Reconstruct the actual group action from the central coordinate and
13 canonical quotient-basis operators. -/
14 def ofAlgebraAction (D : Datum Z H A) (ζ : Z →* ℂˣ)
15     (φ : Algebra D ζ →ₐ[ℂ] Module.End ℂ W) : Representation ℂ H W where
16   toFun h := (ζ (coordinate D h) : ℂ) • φ (basis D ζ (D.q h))
17   map_one' := by
18     simp [basis]
19   map_mul' h k := by
20     rw [coordinate_mul, D.q.map_mul, ζ.map_mul, ζ.map_mul]
21     simp only [Units.val_mul]
22     rw [smul_mul_assoc, mul_smul_comm, ← map_mul φ (basis D ζ (D.q h)) (basis D ζ (D.q k)),
23       TwistedAlgebra.basis_mul,
24       map_smul]
25     simp only [scalarCocycle_coeff, smul_smul, mul_assoc]
26 
27 @[simp] theorem ofAlgebraAction_apply (D : Datum Z H A) (ζ : Z →* ℂˣ)
28     (φ : Algebra D ζ →ₐ[ℂ] Module.End ℂ W) (h : H) :
29     ofAlgebraAction D ζ φ h =
30       (ζ (coordinate D h) : ℂ) • φ (basis D ζ (D.q h)) := rfl
31 
32 /-- The reconstructed action has the prescribed character on the distinguished central inclusion. -/
33 theorem ofAlgebraAction_central (D : Datum Z H A) (ζ : Z →* ℂˣ)
34     (φ : Algebra D ζ →ₐ[ℂ] Module.End ℂ W) (z : Z) :
35     ofAlgebraAction D ζ φ (D.i z) = (ζ z : ℂ) • LinearMap.id := by
36   simp [basis]
37   rfl
38 
39 /-- Section elements recover the original canonical basis operators. -/
40 @[simp] theorem ofAlgebraAction_section (D : Datum Z H A) (ζ : Z →* ℂˣ)
41     (φ : Algebra D ζ →ₐ[ℂ] Module.End ℂ W) (a : A) :
42     ofAlgebraAction D ζ φ (sectionMap D a) = φ (basis D ζ a) := by
43   simp
44 
45 /-- Every reconstructed group operator is invertible. -/
46 theorem ofAlgebraAction_isUnit (D : Datum Z H A) (ζ : Z →* ℂˣ)
47     (φ : Algebra D ζ →ₐ[ℂ] Module.End ℂ W) (h : H) :
48     IsUnit (ofAlgebraAction D ζ φ h) := by
49   rw [← Representation.asGroupHom_apply (ofAlgebraAction D ζ φ) h]
50   exact ((ofAlgebraAction D ζ φ).asGroupHom h).isUnit
51 
52 /-- Forward algebra action and reconstruction recover every original group operator. -/
53 @[simp] theorem of_toAlgebraAction (D : Datum Z H A) (ζ : Z →* ℂˣ)
54     (σ : Representation ℂ H W)
55     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
56     ofAlgebraAction D ζ (toAlgebraAction D ζ σ hcentral) = σ := by
57   apply MonoidHom.ext
58   intro h
59   exact (action_normal_form D ζ σ hcentral h).symm
60 
61 /-- Reconstruction and forward extension recover the original algebra homomorphism. -/
62 @[simp] theorem to_ofAlgebraAction (D : Datum Z H A) (ζ : Z →* ℂˣ)
63     (φ : Algebra D ζ →ₐ[ℂ] Module.End ℂ W) :
64     toAlgebraAction D ζ (ofAlgebraAction D ζ φ) (ofAlgebraAction_central D ζ φ) = φ := by
65   apply AlgHom.toLinearMap_injective
66   apply (basis D ζ).ext
67   intro a
68   change toAlgebraAction D ζ (ofAlgebraAction D ζ φ)
69       (ofAlgebraAction_central D ζ φ) (basis D ζ a) = φ (basis D ζ a)
70   rw [toAlgebraAction_basis, ofAlgebraAction_section]
71 
72 /-- The actual central-character representations on a fixed complex vector
73 space are equivalent to the actual twisted-algebra actions on that space. -/
74 def actionEquiv (D : Datum Z H A) (ζ : Z →* ℂˣ) :
75     {σ : Representation ℂ H W //
76       ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id} ≃
77         (Algebra D ζ →ₐ[ℂ] Module.End ℂ W) where
78   toFun σ := toAlgebraAction D ζ σ.val σ.property
79   invFun φ := ⟨ofAlgebraAction D ζ φ, ofAlgebraAction_central D ζ φ⟩
80   left_inv σ := Subtype.ext (of_toAlgebraAction D ζ σ.val σ.property)
81   right_inv φ := to_ofAlgebraAction D ζ φ
82 
83 end PaperXI.CentralCharacter

Back to source controls