CentralExtension.lean

1 import PaperXI.CocycleCommutator
2 import Mathlib.Tactic.Group
3 
4 /-! An actual central extension and normalized coordinates on its middle group.
5 No characteristic, finiteness, or scalar-character assumption is used. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CentralExtension
9 
10 /-- A short exact sequence whose distinguished kernel lies in the center. -/
11 structure Datum (Z H A : Type*) [CommGroup Z] [Group H] [CommGroup A] where
12   i : Z →* H
13   q : H →* A
14   i_injective : Function.Injective i
15   q_surjective : Function.Surjective q
16   range_i_eq_ker_q : i.range = q.ker
17   central : ∀ z h, i z * h = h * i z
18 
19 variable {Z H A : Type*} [CommGroup Z] [Group H] [CommGroup A]
20 variable (D : Datum Z H A)
21 
22 @[simp] theorem q_i (z : Z) : D.q (D.i z) = 1 := by
23   have h : D.i z ∈ D.i.range := ⟨z, rfl⟩
24   rw [D.range_i_eq_ker_q] at h
25   exact h
26 
27 /-- A chosen quotient section, normalized at the identity. -/
28 def sectionMap (a : A) : H := by
29   classical
30   exact if a = 1 then 1 else Classical.choose (D.q_surjective a)
31 
32 @[simp] theorem section_one : sectionMap D 1 = 1 := by
33   simp [sectionMap]
34 
35 @[simp] theorem q_section (a : A) : D.q (sectionMap D a) = a := by
36   classical
37   by_cases ha : a = 1
38   · simp [ha]
39   · simpa [sectionMap, ha] using Classical.choose_spec (D.q_surjective a)
40 
41 theorem exists_coordinate (h : H) :
42     ∃ z : Z, D.i z = h * (sectionMap D (D.q h))⁻¹ := by
43   have hk : h * (sectionMap D (D.q h))⁻¹ ∈ D.q.ker := by
44     simp only [MonoidHom.mem_ker, map_mul, map_inv, q_section, mul_inv_cancel]
45   rw [← D.range_i_eq_ker_q] at hk
46   exact hk
47 
48 /-- The unique central coordinate of a group element relative to the section. -/
49 def coordinate (h : H) : Z := Classical.choose (exists_coordinate D h)
50 
51 theorem coordinate_spec (h : H) :
52     D.i (coordinate D h) = h * (sectionMap D (D.q h))⁻¹ :=
53   Classical.choose_spec (exists_coordinate D h)
54 
55 /-- Every group element has its actual central-times-section normal form. -/
56 theorem normal_form (h : H) :
57     h = D.i (coordinate D h) * sectionMap D (D.q h) := by
58   rw [coordinate_spec, inv_mul_cancel_right]
59 
60 theorem coordinate_eq_of_eq (h : H) (z : Z) (a : A)
61     (heq : h = D.i z * sectionMap D a) : coordinate D h = z := by
62   have hq : D.q h = a := by rw [heq, map_mul, q_i, q_section, one_mul]
63   have hn := normal_form D h
64   rw [hq] at hn
65   exact D.i_injective (mul_right_cancel (hn.symm.trans heq))
66 
67 @[simp] theorem coordinate_one : coordinate D 1 = 1 :=
68   coordinate_eq_of_eq D 1 1 1 (by simp)
69 
70 @[simp] theorem coordinate_section (a : A) : coordinate D (sectionMap D a) = 1 :=
71   coordinate_eq_of_eq D (sectionMap D a) 1 a (by simp)
72 
73 @[simp] theorem coordinate_i (z : Z) : coordinate D (D.i z) = z :=
74   coordinate_eq_of_eq D (D.i z) z 1 (by simp)
75 
76 /-- Both coordinates of the normal form are unique. -/
77 theorem normal_form_unique (h : H) (z : Z) (a : A) :
78     h = D.i z * sectionMap D a ↔ coordinate D h = z ∧ D.q h = a := by
79   constructor
80   · intro heq
81     exact ⟨coordinate_eq_of_eq D h z a heq, by rw [heq, map_mul, q_i, q_section, one_mul]⟩
82   · rintro ⟨hz, ha⟩
83     simpa only [hz, ha] using normal_form D h
84 
85 end PaperXI.CentralExtension

Back to source controls