ProjectiveCocycle.lean

1 import PaperXI.CocycleCommutator
2 import PaperXI.SchurScalar
3 
4 /-! Scalar cocycles extracted from the multiplication of actual nonzero operators.
5 Associativity and normalization are conclusions of operator identities. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.ProjectiveCocycle
9 
10 open CocycleCommutator
11 variable {A V : Type*} [CommGroup A] [AddCommGroup V] [Module ℂ V]
12 
13 /-- Nonzero operators make their scalar multipliers identifiable. -/
14 theorem scalar_injective (F : Module.End ℂ V) (hF : F ≠ 0) :
15     Function.Injective (fun c : ℂˣ => (c : ℂ) • F) := by
16   intro c d h
17   apply Units.ext
18   exact (smul_left_injective ℂ hF) h
19 
20 /-- The scalar multiplication law of actual operators forces the cocycle identity. -/
21 def cocycle (T : A → Module.End ℂ V) (hT : ∀ a, T a ≠ 0)
22     (c : A → A → ℂˣ)
23     (hmul : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b)) : Cocycle A ℂˣ where
24   coeff := c
25   assoc a b d := by
26     apply scalar_injective (T (a * (b * d))) (hT _)
27     have h := mul_assoc (T a) (T b) (T d)
28     simpa only [hmul, smul_mul_assoc, mul_smul_comm, hmul, smul_smul,
29       Units.val_mul, mul_assoc a b d] using h
30 
31 /-- Identity operators force both scalar normalizations. -/
32 theorem normalized (T : A → Module.End ℂ V) (hT : ∀ a, T a ≠ 0)
33     (c : A → A → ℂˣ)
34     (hmul : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b))
35     (hone : T 1 = 1) : Normalized (cocycle T hT c hmul) := by
36   constructor
37   · intro a
38     apply scalar_injective (T a) (hT a)
39     simpa [hone, cocycle] using (hmul 1 a).symm
40   · intro a
41     apply scalar_injective (T a) (hT a)
42     simpa [hone, cocycle] using (hmul a 1).symm
43 
44 /-- Equality of all multiplication coefficients follows from equality of the operators. -/
45 theorem coefficient_unique (T : A → Module.End ℂ V) (hT : ∀ a, T a ≠ 0)
46     (c d : A → A → ℂˣ)
47     (hc : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b))
48     (hd : ∀ a b, T a * T b = (d a b : ℂ) • T (a * b)) : c = d := by
49   funext a b
50   exact scalar_injective (T (a * b)) (hT _) ((hc a b).symm.trans (hd a b))
51 
52 /-- Rescaling the actual operators changes their scalar cocycle by the stated coboundary. -/
53 theorem rescale_coefficients (T U : A → Module.End ℂ V) (hT : ∀ a, T a ≠ 0)
54     (c d : A → A → ℂˣ)
55     (hc : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b))
56     (hd : ∀ a b, U a * U b = (d a b : ℂ) • U (a * b))
57     (s : A → ℂˣ) (hs : ∀ a, U a = (s a : ℂ) • T a) (a b : A) :
58     d a b = s a * s b / s (a * b) * c a b := by
59   have h : ((d a b * s (a * b) : ℂˣ) : ℂ) • T (a * b) =
60       ((s a * s b * c a b : ℂˣ) : ℂ) • T (a * b) := by
61     simpa only [hs, smul_mul_assoc, mul_smul_comm, hc, smul_smul,
62       Units.val_mul, mul_assoc, mul_left_comm] using (hd a b).symm
63   have he := scalar_injective (T (a * b)) (hT _) h
64   calc
65     d a b = (s a * s b * c a b) / s (a * b) :=
66       by
67         have hh := congrArg (fun x : ℂˣ => x / s (a * b)) he
68         simpa using hh
69     _ = _ := by simp [div_eq_mul_inv, mul_assoc, mul_comm]
70 
71 /-- Two actual projective families related by a cochain have equal commutators. -/
72 theorem commutator_rescale_operators
73     (T U : A → Module.End ℂ V) (hT : ∀ a, T a ≠ 0) (hU : ∀ a, U a ≠ 0)
74     (c d : A → A → ℂˣ)
75     (hc : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b))
76     (hd : ∀ a b, U a * U b = (d a b : ℂ) • U (a * b))
77     (s : A → ℂˣ) (hs : ∀ a, U a = (s a : ℂ) • T a) (a b : A) :
78     commutator (cocycle U hU d hd) a b = commutator (cocycle T hT c hc) a b := by
79   calc
80     _ = commutator (rescale (cocycle T hT c hc) s) a b := by
81       change d a b / d b a = _
82       rw [rescale_coefficients T U hT c d hc hd s hs a b,
83         rescale_coefficients T U hT c d hc hd s hs b a]
84       rfl
85     _ = _ := commutator_rescale _ s a b
86 
87 
88 /-- The operator cochain comparison gives equality of the actual cocycle structures. -/
89 theorem cocycle_rescale_operators
90     (T U : A → Module.End ℂ V) (hT : ∀ a, T a ≠ 0) (hU : ∀ a, U a ≠ 0)
91     (c d : A → A → ℂˣ)
92     (hc : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b))
93     (hd : ∀ a b, U a * U b = (d a b : ℂ) • U (a * b))
94     (s : A → ℂˣ) (hs : ∀ a, U a = (s a : ℂ) • T a) :
95     cocycle U hU d hd = rescale (cocycle T hT c hc) s := by
96   have h := funext (fun a => funext (rescale_coefficients T U hT c d hc hd s hs a))
97   unfold cocycle rescale
98   congr 1
99 
100 /-- Normalized actual families force the comparing cochain to be normalized. -/
101 theorem cochain_one (T U : A → Module.End ℂ V) (hT : T 1 ≠ 0)
102     (hT1 : T 1 = 1) (hU1 : U 1 = 1)
103     (s : A → ℂˣ) (hs : ∀ a, U a = (s a : ℂ) • T a) : s 1 = 1 := by
104   apply scalar_injective (T 1) hT
105   simpa [hT1, hU1] using (hs 1).symm
106 
107 
108 /-- A cochain change of actual operators realizes the rescaled scalar cocycle. -/
109 theorem rescaledFamily_mul (T U : A → Module.End ℂ V) (c : Cocycle A ℂˣ)
110     (hc : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b))
111     (s : A → ℂˣ) (hs : ∀ a, U a = (s a : ℂ) • T a) (a b : A) :
112     U a * U b = ((rescale c s).coeff a b : ℂ) • U (a * b) := by
113   have he : s b * (s a * c.coeff a b) =
114       (s a * s b / s (a * b) * c.coeff a b) * s (a * b) := by
115     simp [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
116   simp only [hs, smul_mul_assoc, mul_smul_comm, hc, smul_smul, rescale]
117   exact congrArg (fun z : ℂˣ => (z : ℂ) • T (a * b)) he
118 
119 section Conjugation
120 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
121 
122 /-- Simultaneous change of coordinates preserves actual scalar multiplication. -/
123 theorem conjugate_mul (T : A → Module.End ℂ V) (c : A → A → ℂˣ)
124     (hc : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b))
125     (e : V ≃ₗ[ℂ] W) (a b : A) :
126     e.conj (T a) * e.conj (T b) = (c a b : ℂ) • e.conj (T (a * b)) := by
127   have h := congrArg e.conj (hc a b)
128   change e.conj ((T a).comp (T b)) = _ at h
129   rw [LinearEquiv.conj_comp, map_smul] at h
130   exact h
131 
132 /-- A conjugation followed by a scalar change has the same explicit coboundary. -/
133 theorem conjugate_rescale_coefficients
134     (T : A → Module.End ℂ V) (U : A → Module.End ℂ W) (hT : ∀ a, T a ≠ 0)
135     (c d : A → A → ℂˣ)
136     (hc : ∀ a b, T a * T b = (c a b : ℂ) • T (a * b))
137     (hd : ∀ a b, U a * U b = (d a b : ℂ) • U (a * b))
138     (e : V ≃ₗ[ℂ] W) (s : A → ℂˣ)
139     (hs : ∀ a, U a = (s a : ℂ) • e.conj (T a)) (a b : A) :
140     d a b = s a * s b / s (a * b) * c a b := by
141   apply rescale_coefficients (fun a => e.conj (T a)) U _ c d
142     (conjugate_mul T c hc e) hd s hs a b
143   intro a h
144   exact hT a (e.conj.injective (h.trans e.conj.map_zero.symm))
145 
146 
147 /-- Actual simultaneous conjugation, reindexing and a scalar cochain preserve
148 commutators on the corresponding elements of the two index groups. -/
149 theorem conjugate_rescale_commutator {B : Type*} [CommGroup B]
150     (T : A → Module.End ℂ V) (U : B → Module.End ℂ W) (hT : ∀ a, T a ≠ 0)
151     (c : Cocycle A ℂˣ) (d : Cocycle B ℂˣ)
152     (hc : ∀ a b, T a * T b = (c.coeff a b : ℂ) • T (a * b))
153     (hd : ∀ a b, U a * U b = (d.coeff a b : ℂ) • U (a * b))
154     (e : V ≃ₗ[ℂ] W) (r : A ≃* B) (s : A → ℂˣ)
155     (hs : ∀ a, U (r a) = (s a : ℂ) • e.conj (T a)) (a b : A) :
156     commutator d (r a) (r b) = commutator c a b := by
157   have hp (x y : A) : U (r x) * U (r y) =
158       (d.coeff (r x) (r y) : ℂ) • U (r (x * y)) := by
159     simpa only [map_mul] using hd (r x) (r y)
160   have hh := conjugate_rescale_coefficients T (fun x => U (r x)) hT c.coeff
161     (fun x y => d.coeff (r x) (r y)) hc hp e s hs
162   calc
163     _ = commutator (rescale c s) a b := by
164       change d.coeff (r a) (r b) / d.coeff (r b) (r a) = _
165       rw [hh a b, hh b a]
166       rfl
167     _ = _ := commutator_rescale c s a b
168 
169 end Conjugation
170 end PaperXI.ProjectiveCocycle
171 

Back to source controls