CocycleCommutator.lean

1 import Mathlib.GroupTheory.QuotientGroup.Basic
2 import Mathlib.Tactic.Ext
3 
4 /-! Paper XI, Propositions 8.1–8.2. Multiplicative notation for the abelian
5 index group. Values may lie in any commutative group, including ℂˣ. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CocycleCommutator
9 
10 variable {A C : Type*} [CommGroup A] [CommGroup C]
11 
12 /-- The associativity identity for scalar coefficients of a twisted product.
13 Normalization is separate: arbitrary changes of basis need not preserve it. -/
14 structure Cocycle (A C : Type*) [CommGroup A] [CommGroup C] where
15   coeff : A → A → C
16   assoc : ∀ a b d, coeff a b * coeff (a * b) d = coeff b d * coeff a (b * d)
17 
18 def Normalized (c : Cocycle A C) : Prop :=
19   (∀ a, c.coeff 1 a = 1) ∧ (∀ a, c.coeff a 1 = 1)
20 
21 /-- A change of scalar choices changes coefficients by this coboundary. -/
22 def rescale (c : Cocycle A C) (s : A → C) : Cocycle A C where
23   coeff a b := s a * s b / s (a * b) * c.coeff a b
24   assoc a b d := by
25     calc
26       _ = (s a * s b * s d / s (a * (b * d))) *
27           (c.coeff a b * c.coeff (a * b) d) := by
28             rw [mul_assoc a b d]
29             simp [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
30       _ = (s a * s b * s d / s (a * (b * d))) *
31           (c.coeff b d * c.coeff a (b * d)) := by rw [c.assoc]
32       _ = _ := by simp [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
33 
34 /-- The scalar commutator. -/
35 def commutator (c : Cocycle A C) (a b : A) : C := c.coeff a b / c.coeff b a
36 
37 @[simp] theorem commutator_self (c : Cocycle A C) (a : A) :
38     commutator c a a = 1 := by simp [commutator]
39 
40 theorem commutator_swap (c : Cocycle A C) (a b : A) :
41     commutator c b a = (commutator c a b)⁻¹ := by simp [commutator]
42 
43 theorem commutator_rescale (c : Cocycle A C) (s : A → C) (a b : A) :
44     commutator (rescale c s) a b = commutator c a b := by
45   simp only [commutator, rescale, mul_comm b a]
46   simp [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
47 
48 theorem commutator_mul_left (c : Cocycle A C) (a b d : A) :
49     commutator c (a * b) d = commutator c a d * commutator c b d := by
50   have h₁ := c.assoc a b d
51   have h₂ := c.assoc d a b
52   have h₃ := c.assoc a d b
53   simp only [commutator]
54   rw [mul_comm d a] at h₂
55   rw [mul_comm d b] at h₃
56   have h₁' : c.coeff (a * b) d = c.coeff b d * c.coeff a (b * d) / c.coeff a b := by
57     apply (eq_div_iff_mul_eq').2
58     simpa [mul_comm] using h₁
59   have h₂' : c.coeff d (a * b) = c.coeff d a * c.coeff (a * d) b / c.coeff a b := by
60     apply (eq_div_iff_mul_eq').2
61     simpa [mul_comm] using h₂.symm
62   have h₃' : c.coeff a (b * d) = c.coeff a d * c.coeff (a * d) b / c.coeff d b := by
63     apply (eq_div_iff_mul_eq').2
64     simpa [mul_comm] using h₃.symm
65   rw [h₁', h₂', h₃']
66   simp [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
67 
68 theorem commutator_mul_right (c : Cocycle A C) (a b d : A) :
69     commutator c a (b * d) = commutator c a b * commutator c a d := by
70   rw [commutator_swap, commutator_mul_left]
71   simp [commutator, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
72 
73 @[simp] theorem commutator_one_left (c : Cocycle A C) (a : A) :
74     commutator c 1 a = 1 := by
75   have h := commutator_mul_left c 1 1 a
76   simpa only [one_mul, left_eq_mul] using h
77 
78 @[simp] theorem commutator_one_right (c : Cocycle A C) (a : A) :
79     commutator c a 1 = 1 := by rw [commutator_swap, commutator_one_left, inv_one]
80 
81 /-- The commutator as a homomorphism into the character group. -/
82 def characterMap (c : Cocycle A C) : A →* (A →* C) where
83   toFun a :=
84     { toFun := commutator c a
85       map_one' := commutator_one_right c a
86       map_mul' := commutator_mul_right c a }
87   map_one' := by ext a; exact commutator_one_left c a
88   map_mul' a b := by ext d; exact commutator_mul_left c a b d
89 
90 @[simp] theorem characterMap_apply (c : Cocycle A C) (a b : A) :
91     characterMap c a b = commutator c a b := rfl
92 
93 /-- The radical is a subgroup, defined as the kernel of the character map. -/
94 def radical (c : Cocycle A C) : Subgroup A := (characterMap c).ker
95 
96 @[simp] theorem mem_radical_iff (c : Cocycle A C) (a : A) :
97     a ∈ radical c ↔ ∀ b, commutator c a b = 1 := by
98   change characterMap c a = 1 ↔ _
99   constructor
100   · intro h b; exact DFunLike.congr_fun h b
101   · intro h; exact MonoidHom.ext h
102 
103 theorem radical_rescale (c : Cocycle A C) (s : A → C) :
104     radical (rescale c s) = radical c := by
105   ext a
106   simp only [mem_radical_iff, commutator_rescale]
107 
108 /-- Rescaling preserves normalized coefficients precisely when the scalar at
109 identity is 1. This hypothesis is unnecessary for commutator invariance. -/
110 theorem normalized_rescale (c : Cocycle A C) (hc : Normalized c)
111     (s : A → C) (hs : s 1 = 1) : Normalized (rescale c s) := by
112   constructor <;> intro a <;> simp [rescale, hc.1, hc.2, hs]
113 
114 theorem normalized_rescale_iff (c : Cocycle A C) (hc : Normalized c)
115     (s : A → C) : Normalized (rescale c s) ↔ s 1 = 1 := by
116   constructor
117   · intro h
118     have h₁ := h.1 1
119     simpa [rescale, hc.1, hc.2] using h₁
120   · exact normalized_rescale c hc s
121 
122 end PaperXI.CocycleCommutator

Back to source controls