EffectiveCocycleDescent.lean

1 import KomorebiSpace.CocycleDescent
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Effective descent of cocycles with specified overlap isomorphisms
7 
8 Patches need not have equal labels. An overlap gauge from patch i to patch j
9 has values a_ij, with a_ik = a_jk * a_ij. A composition cover lets us choose
10 local reference frames, strictify the labels, and invoke strict cocycle gluing.
11 The result includes its local gauges and their compatibility with the supplied
12 overlap gauges. No site, topology, or unrestricted stack condition is assumed.
13 -/
14 universe u v w z
15 namespace KomorebiSpace
16 open CategoryTheory
17 namespace GroupViewSystem
18 variable {V : Type u} [Category.{v} V]
19 variable {G : V → Type w} [∀ a, Group (G a)]
20 variable {I : Type z}
21 variable (F : GroupViewSystem V G)
22 
23 namespace PatchCocycle
24 variable {F}
25 
26 /-- A change of frame inside a full patch. -/
27 def gauge {S : Set V} (a : ∀ x : S, G x.val) (c : F.PatchCocycle S) :
28     F.PatchCocycle S where
29   edge := fun {x y} f => a x * c.edge f * (F.pull f (a y))⁻¹
30   edge_id := by intro x; rw [c.edge_id, F.pull_id]; simp
31   edge_comp := by
32     intro x y z f g
33     simp only [c.edge_comp, F.pull_comp, map_mul, map_inv]
34     group
35 
36 @[simp] theorem gauge_edge {S : Set V} (a : ∀ x : S, G x.val)
37     (c : F.PatchCocycle S) {x y : S} (f : x.val ⟶ y.val) :
38     (c.gauge a).edge f = a x * c.edge f * (F.pull f (a y))⁻¹ := rfl
39 end PatchCocycle
40 
41 /-- Descent data with actual overlap gauges, not just pairwise existence of an isomorphism. -/
42 structure CocycleDescentData (U : I → Set V) where
43   patch : ∀ i, F.PatchCocycle (U i)
44   change : ∀ (i j : I) (x : V), x ∈ U i → x ∈ U j → G x
45   change_edge : ∀ (i j : I) (x y : V) (hxi : x ∈ U i) (hyi : y ∈ U i)
46       (hxj : x ∈ U j) (hyj : y ∈ U j) (f : x ⟶ y),
47     change i j x hxi hxj * (patch i).edge (a := ⟨x,hxi⟩) (b := ⟨y,hyi⟩) f *
48         (F.pull f (change i j y hyi hyj))⁻¹ =
49       (patch j).edge (a := ⟨x,hxj⟩) (b := ⟨y,hyj⟩) f
50   change_comp : ∀ (i j k : I) (x : V) (hi : x ∈ U i) (hj : x ∈ U j) (hk : x ∈ U k),
51     change i k x hi hk = change j k x hj hk * change i j x hi hj
52 
53 namespace CocycleDescentData
54 variable {F} {U : I → Set V}
55 
56 /-- Identity and inverse overlap laws follow from the triple-overlap equation. -/
57 theorem change_self (D : F.CocycleDescentData U) (i : I) (x : V) (hi : x ∈ U i) :
58     D.change i i x hi hi = 1 := by
59   have h := D.change_comp i i i x hi hi hi
60   have h' : D.change i i x hi hi * 1 = D.change i i x hi hi * D.change i i x hi hi := by
61     simpa only [mul_one] using h
62   exact (mul_left_cancel h').symm
63 
64 theorem change_reverse (D : F.CocycleDescentData U) (i j : I) (x : V)
65     (hi : x ∈ U i) (hj : x ∈ U j) :
66     D.change j i x hj hi = (D.change i j x hi hj)⁻¹ := by
67   have h := D.change_comp i j i x hi hj hi
68   rw [D.change_self] at h
69   exact eq_inv_of_mul_eq_one_left h.symm
70 
71 /-- A global representative with isomorphisms to all local cocycles. -/
72 structure Effectuation (D : F.CocycleDescentData U) where
73   global : F.Cocycle
74   compare : ∀ i, ∀ x : U i, G x.val
75   local_eq : ∀ (i : I) (x y : U i) (f : x.val ⟶ y.val),
76     compare i x * global.edge f * (F.pull f (compare i y))⁻¹ = (D.patch i).edge f
77   overlap : ∀ (i j : I) (x : V) (hi : x ∈ U i) (hj : x ∈ U j),
78     compare j ⟨x,hj⟩ = D.change i j x hi hj * compare i ⟨x,hi⟩
79 
80 /-- Choose a reference patch independently at each view. This is choice data. -/
81 noncomputable def reference (h : ViewSystem.ObjectCover U) (x : V) : I :=
82   Classical.choose (h x)
83 
84 omit [Category.{v} V] in
85 theorem reference_mem (h : ViewSystem.ObjectCover U) (x : V) :
86     x ∈ U (reference h x) := Classical.choose_spec (h x)
87 
88 /-- The gauge from the selected reference frame at x into patch i. -/
89 noncomputable def frame (D : F.CocycleDescentData U) (h : ViewSystem.ObjectCover U)
90     (i : I) (x : U i) : G x.val :=
91   D.change (reference h x.val) i x.val (reference_mem h x.val) x.property
92 
93 theorem frame_overlap (D : F.CocycleDescentData U) (h : ViewSystem.ObjectCover U)
94     (i j : I) (x : V) (hi : x ∈ U i) (hj : x ∈ U j) :
95     D.frame h j ⟨x,hj⟩ = D.change i j x hi hj * D.frame h i ⟨x,hi⟩ :=
96   D.change_comp (reference h x) i j x (reference_mem h x) hi hj
97 
98 /-- Rewrite every patch in the independently selected reference frames. -/
99 noncomputable def strictify (D : F.CocycleDescentData U) (h : ViewSystem.ObjectCover U) :
100     F.CocycleMatching U where
101   patch := fun i => (D.patch i).gauge (fun x => (D.frame h i x)⁻¹)
102   agree := by
103     intro i j x y hxi hyi hxj hyj f
104     simp only [PatchCocycle.gauge_edge, map_inv, inv_inv]
105     rw [D.frame_overlap h i j x hxi hxj, D.frame_overlap h i j y hyi hyj,
106       ← D.change_edge i j x y hxi hyi hxj hyj f, map_mul]
107     group
108 
109 /-- Construct an effectuation from arbitrary coherent overlap isomorphisms. -/
110 noncomputable def effectuate (D : F.CocycleDescentData U) (h : CompositionCover U) :
111     D.Effectuation where
112   global := (D.strictify (ViewSystem.TransitionCover.objectCover U h.transitionCover)).glue h
113   compare := D.frame (ViewSystem.TransitionCover.objectCover U h.transitionCover)
114   local_eq := by
115     intro i x y f
116     let ho := ViewSystem.TransitionCover.objectCover U h.transitionCover
117     have he := (D.strictify ho).assembleEdge_local h.transitionCover i x.val y.val
118       x.property y.property f
119     change D.frame ho i x * (D.strictify ho).assembleEdge h.transitionCover f *
120       (F.pull f (D.frame ho i y))⁻¹ = (D.patch i).edge f
121     rw [he]
122     simp only [strictify, PatchCocycle.gauge_edge, map_inv, inv_inv]
123     group
124   overlap := D.frame_overlap (ViewSystem.TransitionCover.objectCover U h.transitionCover)
125 
126 /-- The existence conclusion is derived, not a field in descent data. -/
127 theorem effective (D : F.CocycleDescentData U) (h : CompositionCover U) :
128     Nonempty D.Effectuation := ⟨D.effectuate h⟩
129 
130 /-- Each local identification satisfies the original overlap law. -/
131 theorem effectuate_overlap (D : F.CocycleDescentData U) (h : CompositionCover U)
132     (i j : I) (x : V) (hi : x ∈ U i) (hj : x ∈ U j) :
133     (D.effectuate h).compare j ⟨x,hj⟩ =
134       D.change i j x hi hj * (D.effectuate h).compare i ⟨x,hi⟩ :=
135   (D.effectuate h).overlap i j x hi hj
136 
137 /-- Inverse form of the local comparison equation, useful for uniqueness. -/
138 theorem Effectuation.global_local {D : F.CocycleDescentData U} (E : D.Effectuation)
139     (i : I) (x y : U i) (f : x.val ⟶ y.val) :
140     E.global.edge f = (E.compare i x)⁻¹ * (D.patch i).edge f * F.pull f (E.compare i y) := by
141   rw [← E.local_eq i x y f]
142   group
143 
144 end CocycleDescentData
145 end GroupViewSystem
146 end KomorebiSpace

Back to source controls