CentralExtensionCocycle.lean

1 import PaperXI.CentralExtension
2 import Mathlib.Analysis.Complex.Basic
3 
4 /-! The normalized central and scalar cocycles of an actual central extension.
5 The defect and its cocycle law are derived from group multiplication. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CentralExtension
9 
10 open CocycleCommutator
11 variable {Z H A : Type*} [CommGroup Z] [Group H] [CommGroup A]
12 variable (D : Datum Z H A)
13 
14 /-- The actual central coordinate of the section's multiplicative defect. -/
15 def defect (a b : A) : Z := coordinate D (sectionMap D a * sectionMap D b)
16 
17 theorem section_mul (a b : A) :
18     sectionMap D a * sectionMap D b = D.i (defect D a b) * sectionMap D (a * b) := by
19   simpa only [defect, map_mul, q_section] using
20     normal_form D (sectionMap D a * sectionMap D b)
21 
22 @[simp] theorem defect_one_left (a : A) : defect D 1 a = 1 := by
23   simp [defect]
24 
25 @[simp] theorem defect_one_right (a : A) : defect D a 1 = 1 := by
26   simp [defect]
27 
28 theorem normal_form_mul (z w : Z) (a b : A) :
29     (D.i z * sectionMap D a) * (D.i w * sectionMap D b) =
30       D.i (z * w * defect D a b) * sectionMap D (a * b) := by
31   calc
32     _ = (D.i z * D.i w) * (sectionMap D a * sectionMap D b) := by
33       rw [mul_assoc (D.i z), ← mul_assoc (sectionMap D a), ← D.central]
34       simp only [mul_assoc]
35     _ = _ := by rw [section_mul]; simp only [map_mul, mul_assoc]
36 
37 /-- The central coordinate multiplication law, derived from the actual group. -/
38 theorem coordinate_mul (h k : H) :
39     coordinate D (h * k) =
40       coordinate D h * coordinate D k * defect D (D.q h) (D.q k) := by
41   apply coordinate_eq_of_eq D (h * k) _ (D.q h * D.q k)
42   calc
43     h * k = (D.i (coordinate D h) * sectionMap D (D.q h)) *
44         (D.i (coordinate D k) * sectionMap D (D.q k)) :=
45       congrArg₂ (fun x y : H => x * y) (normal_form D h) (normal_form D k)
46     _ = _ := normal_form_mul D _ _ _ _
47 
48 /-- Associativity in the middle group forces the central cocycle identity. -/
49 theorem defect_assoc (a b d : A) :
50     defect D a b * defect D (a * b) d = defect D b d * defect D a (b * d) := by
51   have h := congrArg (coordinate D)
52     (mul_assoc (sectionMap D a) (sectionMap D b) (sectionMap D d))
53   simpa only [coordinate_mul, coordinate_section, q_section, map_mul, one_mul, mul_one] using h
54 
55 /-- The actual central-valued normalized cocycle attached to the section. -/
56 def centralCocycle : Cocycle A Z where
57   coeff := defect D
58   assoc := defect_assoc D
59 
60 theorem normalized_centralCocycle : Normalized (centralCocycle D) :=
61   ⟨defect_one_left D, defect_one_right D⟩
62 
63 /-- Apply the actual central character to the actual section defect. -/
64 def scalarCocycle (ζ : Z →* ℂˣ) : Cocycle A ℂˣ where
65   coeff a b := ζ (defect D a b)
66   assoc a b d := by
67     simpa only [map_mul] using congrArg ζ (defect_assoc D a b d)
68 
69 @[simp] theorem scalarCocycle_coeff (ζ : Z →* ℂˣ) (a b : A) :
70     (scalarCocycle D ζ).coeff a b = ζ (defect D a b) := rfl
71 
72 theorem normalized_scalarCocycle (ζ : Z →* ℂˣ) : Normalized (scalarCocycle D ζ) := by
73   constructor <;> intro a <;> simp
74 
75 /-- Normal-form multiplication expressed directly for two middle-group elements. -/
76 theorem product_normal_form (h k : H) :
77     h * k = D.i (coordinate D h * coordinate D k * defect D (D.q h) (D.q k)) *
78       sectionMap D (D.q h * D.q k) := by
79   simpa only [map_mul, coordinate_mul] using normal_form D (h * k)
80 
81 /-- The two actual lifts commute by the quotient's central defect ratio. -/
82 theorem lift_commutation (h k : H) :
83     h * k = D.i (defect D (D.q h) (D.q k) / defect D (D.q k) (D.q h)) * (k * h) := by
84   have hz : (defect D (D.q h) (D.q k) / defect D (D.q k) (D.q h)) *
85       (coordinate D k * coordinate D h * defect D (D.q k) (D.q h)) =
86       coordinate D h * coordinate D k * defect D (D.q h) (D.q k) := by
87     simp [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
88   calc
89     h * k = D.i (coordinate D h * coordinate D k * defect D (D.q h) (D.q k)) *
90         sectionMap D (D.q h * D.q k) := product_normal_form D h k
91     _ = D.i (defect D (D.q h) (D.q k) / defect D (D.q k) (D.q h)) *
92         (D.i (coordinate D k * coordinate D h * defect D (D.q k) (D.q h)) *
93           sectionMap D (D.q k * D.q h)) := by
94       rw [← mul_assoc, ← D.i.map_mul, hz, mul_comm (D.q k) (D.q h)]
95     _ = _ := congrArg
96       (fun t => D.i (defect D (D.q h) (D.q k) / defect D (D.q k) (D.q h)) * t)
97       (product_normal_form D k h).symm
98 
99 /-- The central preimage of the commutator, with convention `[h,k]=h k h⁻¹ k⁻¹`. -/
100 def centralCommutator (h k : H) : Z := coordinate D (h * k * h⁻¹ * k⁻¹)
101 
102 theorem centralCommutator_eq (h k : H) :
103     centralCommutator D h k = defect D (D.q h) (D.q k) / defect D (D.q k) (D.q h) := by
104   have heq : h * k * h⁻¹ * k⁻¹ =
105       D.i (defect D (D.q h) (D.q k) / defect D (D.q k) (D.q h)) := by
106     rw [lift_commutation D h k]
107     group
108   simp only [centralCommutator, heq, coordinate_i]
109 
110 theorem i_centralCommutator (h k : H) :
111     D.i (centralCommutator D h k) = h * k * h⁻¹ * k⁻¹ := by
112   rw [centralCommutator_eq, lift_commutation D h k]
113   group
114 
115 /-- Changing either lift leaves the actual central commutator unchanged. -/
116 theorem centralCommutator_lift_independent (h h' k k' : H)
117     (hh : D.q h = D.q h') (hk : D.q k = D.q k') :
118     centralCommutator D h k = centralCommutator D h' k' := by
119   simp only [centralCommutator_eq, hh, hk]
120 
121 /-- The scalar bicharacter is the central character evaluated on the actual
122 commutator of any two lifts. -/
123 theorem scalar_commutator (ζ : Z →* ℂˣ) (h k : H) :
124     commutator (scalarCocycle D ζ) (D.q h) (D.q k) = ζ (centralCommutator D h k) := by
125   simp only [CocycleCommutator.commutator, scalarCocycle_coeff, centralCommutator_eq, map_div]
126 
127 end PaperXI.CentralExtension

Back to source controls