GroupViewSystems.lean

1 import KomorebiSpace.ViewSections
2 import Mathlib.Algebra.Group.Pi.Basic
3 import Mathlib.Algebra.Group.Subgroup.Basic
4 import Mathlib.Tactic.Group
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Group-valued views and nonabelian coherence
10 
11 Groups need not commute. Cocycle labels obey a transported multiplication law.
12 The associated twisted set-valued system and its sections are constructed from
13 these labels. No site, stackification or higher category is asserted here.
14 -/
15 universe u v w
16 namespace KomorebiSpace
17 open CategoryTheory
18 
19 structure GroupViewSystem (V : Type u) [Category.{v} V]
20     (G : V → Type w) [∀ a, Group (G a)] where
21   pull : {a b : V} → (a ⟶ b) → (G b →* G a)
22   pull_id : ∀ a (x : G a), pull (𝟙 a) x = x
23   pull_comp : ∀ {a b c : V} (f : a ⟶ b) (g : b ⟶ c) (x : G c),
24     pull (f ≫ g) x = pull f (pull g x)
25 
26 namespace GroupViewSystem
27 variable {V : Type u} [Category.{v} V]
28 variable {G : V → Type w} [∀ a, Group (G a)]
29 variable (F : GroupViewSystem V G)
30 
31 /-- Underlying strict set-valued view system. -/
32 abbrev views : ViewSystem V where
33   Obj := G
34   pull := fun f => F.pull f
35   pull_id := F.pull_id
36   pull_comp := F.pull_comp
37 
38 /-- Multiplicative transition data, including normalization and all composable pairs. -/
39 structure Cocycle where
40   edge : ∀ {a b : V}, (a ⟶ b) → G a
41   edge_id : ∀ a, edge (𝟙 a) = 1
42   edge_comp : ∀ {a b c : V} (f : a ⟶ b) (g : b ⟶ c),
43     edge (f ≫ g) = edge f * F.pull f (edge g)
44 
45 namespace Cocycle
46 variable {F}
47 @[ext] theorem ext {c d : F.Cocycle}
48     (h : ∀ a b (f : a ⟶ b), c.edge f = d.edge f) : c = d := by
49   cases c with
50   | mk ce ci cc =>
51     cases d with
52     | mk de di dc =>
53       have he : @ce = @de := by funext a b f; exact h a b f
54       cases he
55       rfl
56 end Cocycle
57 
58 /-- Trivial transition labels, not an assumed preferred trivialization. -/
59 def trivial : F.Cocycle where
60   edge := fun _ => 1
61   edge_id := by intros; rfl
62   edge_comp := by intros; simp
63 
64 /-- A raw viewwise change of trivialization acts on a cocycle. -/
65 def gauge (a : ∀ v, G v) (c : F.Cocycle) : F.Cocycle where
66   edge := fun {v w} f => a v * c.edge f * (F.pull f (a w))⁻¹
67   edge_id := by intro v; rw [c.edge_id, F.pull_id]; simp
68   edge_comp := by
69     intro v w z f g
70     simp only [c.edge_comp, F.pull_comp, map_mul, map_inv]
71     group
72 
73 @[simp] theorem gauge_edge (a : ∀ v, G v) (c : F.Cocycle)
74     {v w : V} (f : v ⟶ w) :
75     (F.gauge a c).edge f = a v * c.edge f * (F.pull f (a w))⁻¹ := rfl
76 
77 @[simp] theorem gauge_one (c : F.Cocycle) : F.gauge 1 c = c := by
78   apply Cocycle.ext
79   intro v w f
80   simp [gauge]
81 
82 theorem gauge_mul (a b : ∀ v, G v) (c : F.Cocycle) :
83     F.gauge a (F.gauge b c) = F.gauge (a * b) c := by
84   apply Cocycle.ext
85   intro v w f
86   simp only [gauge_edge, Pi.mul_apply, map_mul]
87   group
88 
89 @[simp] theorem gauge_inv_gauge (a : ∀ v, G v) (c : F.Cocycle) :
90     F.gauge a⁻¹ (F.gauge a c) = c := by rw [F.gauge_mul]; simp
91 
92 @[simp] theorem gauge_gauge_inv (a : ∀ v, G v) (c : F.Cocycle) :
93     F.gauge a (F.gauge a⁻¹ c) = c := by rw [F.gauge_mul]; simp
94 
95 /-- The cocycle is used in the restriction functions, not hidden in a truth flag. -/
96 abbrev twistedViews (c : F.Cocycle) : ViewSystem V where
97   Obj := G
98   pull := fun f x => c.edge f * F.pull f x
99   pull_id := by intro v x; rw [c.edge_id, F.pull_id, one_mul]
100   pull_comp := by
101     intro v w z f g x
102     simp only [c.edge_comp, F.pull_comp, map_mul, mul_assoc]
103 
104 @[simp] theorem twisted_pull (c : F.Cocycle) {v w : V} (f : v ⟶ w) (x : G w) :
105     (F.twistedViews c).pull f x = c.edge f * F.pull f x := rfl
106 
107 theorem twisted_coherent_iff (c : F.Cocycle) (x : ∀ v, G v) :
108     (∀ v w (f : v ⟶ w), (F.twistedViews c).pull f (x w) = x v) ↔
109       ∀ v w (f : v ⟶ w), c.edge f = x v * (F.pull f (x w))⁻¹ := by
110   constructor
111   · intro h v w f
112     have he := h v w f
113     change c.edge f * F.pull f (x w) = x v at he
114     exact (eq_mul_inv_iff_mul_eq).mpr he
115   · intro h v w f
116     change c.edge f * F.pull f (x w) = x v
117     rw [h v w f]
118     group
119 
120 /-- An invertible coordinate change induces an equivalence of actual section sets. -/
121 def gaugeSections (a : ∀ v, G v) (c : F.Cocycle) :
122     (F.twistedViews c).Ambient ≃ (F.twistedViews (F.gauge a c)).Ambient where
123   toFun x := ⟨fun v => a v * x.val v, by
124     intro v w f
125     change (a v * c.edge f * (F.pull f (a w))⁻¹) *
126       F.pull f (a w * x.val w) = a v * x.val v
127     rw [map_mul]
128     have hx := x.property v w f
129     change c.edge f * F.pull f (x.val w) = x.val v at hx
130     calc
131       _ = a v * (c.edge f * F.pull f (x.val w)) := by group
132       _ = _ := by rw [hx]⟩
133   invFun y := ⟨fun v => (a v)⁻¹ * y.val v, by
134     intro v w f
135     change c.edge f * F.pull f ((a w)⁻¹ * y.val w) = (a v)⁻¹ * y.val v
136     have hy := y.property v w f
137     change (a v * c.edge f * (F.pull f (a w))⁻¹) *
138       F.pull f (y.val w) = y.val v at hy
139     rw [map_mul, map_inv]
140     calc
141       _ = (a v)⁻¹ * ((a v * c.edge f * (F.pull f (a w))⁻¹) *
142         F.pull f (y.val w)) := by group
143       _ = _ := by rw [hy]⟩
144   left_inv x := by apply ViewSystem.Ambient.ext; intro v; change _⁻¹ * (_ * _) = _; group
145   right_inv x := by apply ViewSystem.Ambient.ext; intro v; change _ * (_⁻¹ * _) = _; group
146 
147 @[simp] theorem gaugeSections_coordinate (a : ∀ v, G v) (c : F.Cocycle)
148     (x : (F.twistedViews c).Ambient) (v : V) :
149     ((F.gaugeSections a c) x).val v = a v * x.val v := rfl
150 
151 /-- Flattening labels and solving the twisted section equations are equivalent. -/
152 theorem flatten_iff_section (a : ∀ v, G v) (c : F.Cocycle) :
153     F.gauge a c = F.trivial ↔
154       ∀ v w (f : v ⟶ w), c.edge f * F.pull f ((a w)⁻¹) = (a v)⁻¹ := by
155   constructor
156   · intro h v w f
157     have he := congrArg (fun t : F.Cocycle => t.edge f) h
158     change a v * c.edge f * (F.pull f (a w))⁻¹ = 1 at he
159     rw [map_inv]
160     calc
161       _ = (a v)⁻¹ * (a v * c.edge f * (F.pull f (a w))⁻¹) := by group
162       _ = _ := by rw [he, mul_one]
163   · intro h
164     apply Cocycle.ext
165     intro v w f
166     change a v * c.edge f * (F.pull f (a w))⁻¹ = 1
167     have he := h v w f
168     rw [map_inv] at he
169     calc
170       _ = a v * (c.edge f * (F.pull f (a w))⁻¹) := by group
171       _ = _ := by rw [he]; group
172 
173 end GroupViewSystem
174 end KomorebiSpace

Back to source controls