NonabelianExtension.lean

1 import KomorebiSpace.CocycleGaugeGroupoid
2 
3 set_option autoImplicit false
4 
5 /-!
6 # A nonabelian relative obstruction to extending a twisted section
7 
8 A raw extension normalizes a fixed cocycle. Its orbit under gauge changes
9 which equal identity on the prescribed domain is independent of the raw
10 extension. Being in the neutral orbit is equivalent to actual extension.
11 No abelian quotient-group structure or decision procedure is asserted.
12 -/
13 universe u v w
14 namespace KomorebiSpace
15 open CategoryTheory
16 namespace GroupViewSystem
17 variable {V : Type u} [Category.{v} V]
18 variable {G : V → Type w} [∀ a, Group (G a)]
19 variable (F : GroupViewSystem V G)
20 
21 /-- Normalize the transition labels by a raw family of local trivializations. -/
22 def normalize (c : F.Cocycle) (q : ∀ v, G v) : F.Cocycle := F.gauge q⁻¹ c
23 
24 @[simp] theorem normalize_edge (c : F.Cocycle) (q : ∀ v, G v)
25     {v w : V} (f : v ⟶ w) :
26     (F.normalize c q).edge f = (q v)⁻¹ * c.edge f * F.pull f (q w) := by
27   simp [normalize]
28 
29 theorem normalize_trivial_iff (c : F.Cocycle) (q : ∀ v, G v) :
30     F.normalize c q = F.trivial ↔
31       ∀ v w (f : v ⟶ w), c.edge f * F.pull f (q w) = q v := by
32   simpa [normalize] using F.flatten_iff_section q⁻¹ c
33 
34 /-- Raw normalization changes by an allowed gauge when observations agree. -/
35 theorem normalization_independent (c : F.Cocycle) (U : Set V)
36     (q t : ∀ v, G v) (h : ∀ v : U, q v.val = t v.val) :
37     F.orbitClass U (F.normalize c q) = F.orbitClass U (F.normalize c t) := by
38   rw [F.orbitClass_eq_iff]
39   let a : F.basedGauge U := ⟨t⁻¹ * q, by
40     intro v
41     change (t v.val)⁻¹ * q v.val = 1
42     rw [h v]; group⟩
43   refine ⟨a, ?_⟩
44   change F.gauge (t⁻¹ * q) (F.gauge q⁻¹ c) = F.gauge t⁻¹ c
45   rw [F.gauge_mul]
46   have he : (t⁻¹ * q) * q⁻¹ = t⁻¹ := by group
47   rw [he]
48 
49 /-- The orbit condition is equivalent to solving the original equations with fixed data. -/
50 theorem normalized_class_neutral_iff (c : F.Cocycle) (U : Set V) (q : ∀ v, G v) :
51     F.orbitClass U (F.normalize c q) = F.neutralClass U ↔
52       ∃ x : (F.twistedViews c).Ambient, ∀ v : U, x.val v.val = q v.val := by
53   change F.orbitClass U (F.normalize c q) = F.orbitClass U F.trivial ↔ _
54   rw [F.orbitClass_eq_iff]
55   constructor
56   · rintro ⟨a, ha⟩
57     have he : F.gauge (a.val * q⁻¹) c = F.trivial := by
58       rw [← F.gauge_mul]
59       exact ha
60     have hx := (F.flatten_iff_section (a.val * q⁻¹) c).mp he
61     refine ⟨⟨fun v => ((a.val * q⁻¹) v)⁻¹, hx⟩, ?_⟩
62     intro v
63     change (a.val v.val * (q v.val)⁻¹)⁻¹ = q v.val
64     rw [a.property v]
65     simp
66   · rintro ⟨x, hx⟩
67     let a : F.basedGauge U := ⟨x.val⁻¹ * q, by
68       intro v
69       change (x.val v.val)⁻¹ * q v.val = 1
70       rw [hx v]; group⟩
71     refine ⟨a, ?_⟩
72     change F.gauge (x.val⁻¹ * q) (F.gauge q⁻¹ c) = F.trivial
73     rw [F.gauge_mul]
74     have he : (x.val⁻¹ * q) * q⁻¹ = x.val⁻¹ := by group
75     rw [he]
76     apply (F.normalize_trivial_iff c x.val).mpr
77     exact x.property
78 
79 /-- Identity outside the prescribed domain is one raw extension, usually noncoherent. -/
80 noncomputable def rawSection (c : F.Cocycle) (U : Set V)
81     (s : (F.twistedViews c).Partial U) : ∀ v, G v := by
82   classical
83   exact fun v => if h : v ∈ U then s.val ⟨v, h⟩ else 1
84 
85 @[simp] theorem rawSection_prescribed (c : F.Cocycle) (U : Set V)
86     (s : (F.twistedViews c).Partial U) (v : U) :
87     F.rawSection c U s v.val = s.val v := by
88   classical
89   simp [rawSection, v.property]
90 
91 noncomputable def extensionOrbit (c : F.Cocycle) (U : Set V)
92     (s : (F.twistedViews c).Partial U) : F.Orbit U :=
93   F.orbitClass U (F.normalize c (F.rawSection c U s))
94 
95 /-- Actual extension is equivalent to neutrality of the independently defined orbit. -/
96 theorem extensionOrbit_neutral_iff (c : F.Cocycle) (U : Set V)
97     (s : (F.twistedViews c).Partial U) :
98     F.extensionOrbit c U s = F.neutralClass U ↔
99       Nonempty ((F.twistedViews c).Extensions U s) := by
100   change F.orbitClass U (F.normalize c (F.rawSection c U s)) = F.neutralClass U ↔ _
101   rw [F.normalized_class_neutral_iff]
102   constructor
103   · rintro ⟨x, hx⟩
104     refine ⟨⟨x, ?_⟩⟩
105     apply ViewSystem.Partial.ext
106     intro v
107     exact (hx v).trans (F.rawSection_prescribed c U s v)
108   · rintro ⟨⟨x, hx⟩⟩
109     refine ⟨x, ?_⟩
110     intro v
111     have he := congrArg (fun t : (F.twistedViews c).Partial U => t.val v) hx
112     exact he.trans (F.rawSection_prescribed c U s v).symm
113 
114 theorem extensionOrbit_independent (c : F.Cocycle) (U : Set V)
115     (s : (F.twistedViews c).Partial U) (q : ∀ v, G v)
116     (hq : ∀ v : U, q v.val = s.val v) :
117     F.orbitClass U (F.normalize c q) = F.extensionOrbit c U s := by
118   apply F.normalization_independent
119   intro v
120   exact (hq v).trans (F.rawSection_prescribed c U s v).symm
121 
122 /-- Coherence of the prescribed partial section trivializes internal transition labels. -/
123 theorem normalized_internal_edge (c : F.Cocycle) (U : Set V)
124     (s : (F.twistedViews c).Partial U) (v w : U) (f : v.val ⟶ w.val) :
125     (F.normalize c (F.rawSection c U s)).edge f = 1 := by
126   rw [F.normalize_edge, F.rawSection_prescribed, F.rawSection_prescribed]
127   have hs := s.property v w f
128   change c.edge f * F.pull f (s.val w) = s.val v at hs
129   calc
130     _ = (s.val v)⁻¹ * (c.edge f * F.pull f (s.val w)) := by group
131     _ = 1 := by rw [hs]; group
132 
133 end GroupViewSystem
134 end KomorebiSpace

Back to source controls