CocycleDescent.lean

1 import KomorebiSpace.GaugeDescent
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Strict descent of cocycle objects
7 
8 Local cocycle labels on full view patches glue when they agree literally on
9 overlap arrows. To verify the cocycle law after gluing, every composable pair
10 must be visible inside one patch; this is stronger than covering arrows one at
11 a time. The result is an explicit equivalence between global cocycles and
12 strictly matching local cocycles under that cover hypothesis.
13 
14 This is strict object descent. Local cocycles related only by gauge
15 isomorphisms are not yet glued here.
16 -/
17 universe u v w z
18 namespace KomorebiSpace
19 open CategoryTheory
20 namespace GroupViewSystem
21 
22 variable {V : Type u} [Category.{v} V]
23 variable {G : V → Type w} [∀ a, Group (G a)]
24 variable {I : Type z}
25 variable (F : GroupViewSystem V G)
26 
27 /-- Cocycle data restricted to one full patch of view objects. -/
28 structure PatchCocycle (S : Set V) where
29   edge : ∀ {a b : S}, (a.val ⟶ b.val) → G a.val
30   edge_id : ∀ a : S, edge (𝟙 a.val) = 1
31   edge_comp : ∀ {a b c : S} (f : a.val ⟶ b.val) (g : b.val ⟶ c.val),
32     edge (f ≫ g) = edge f * F.pull f (edge g)
33 
34 namespace PatchCocycle
35 variable {F}
36 
37 @[ext] theorem ext {S : Set V} {c d : F.PatchCocycle S}
38     (h : ∀ (a b : S) (f : a.val ⟶ b.val), c.edge f = d.edge f) : c = d := by
39   cases c with
40   | mk ce ci cc =>
41     cases d with
42     | mk de di dc =>
43       have he : @ce = @de := by
44         funext a b f
45         exact h a b f
46       cases he
47       rfl
48 
49 end PatchCocycle
50 
51 /-- Restrict an already-global cocycle to a full patch. -/
52 def restrictCocycle (c : F.Cocycle) (S : Set V) : F.PatchCocycle S where
53   edge := fun f => c.edge f
54   edge_id := fun a => c.edge_id a.val
55   edge_comp := fun f g => c.edge_comp f g
56 
57 /-- Local cocycles which agree literally on every arrow visible in two patches. -/
58 structure CocycleMatching (U : I → Set V) where
59   patch : ∀ i, F.PatchCocycle (U i)
60   agree : ∀ (i j : I) (a b : V) (hai : a ∈ U i) (hbi : b ∈ U i)
61       (haj : a ∈ U j) (hbj : b ∈ U j) (f : a ⟶ b),
62     (patch i).edge (a := ⟨a, hai⟩) (b := ⟨b, hbi⟩) f =
63       (patch j).edge (a := ⟨a, haj⟩) (b := ⟨b, hbj⟩) f
64 
65 namespace CocycleMatching
66 variable {F} {U : I → Set V}
67 
68 @[ext] theorem ext {m n : F.CocycleMatching U}
69     (h : ∀ i, m.patch i = n.patch i) : m = n := by
70   cases m with
71   | mk mp ma =>
72     cases n with
73     | mk np na =>
74       have he : mp = np := funext h
75       cases he
76       rfl
77 
78 end CocycleMatching
79 
80 /-- Every composable pair is contained in one patch. -/
81 def CompositionCover (U : I → Set V) : Prop :=
82   ∀ (a b c : V) (_ : a ⟶ b) (_ : b ⟶ c),
83     ∃ i, a ∈ U i ∧ b ∈ U i ∧ c ∈ U i
84 
85 namespace CompositionCover
86 variable {U : I → Set V}
87 
88 /-- A composition cover in particular covers every individual transition. -/
89 theorem transitionCover (h : CompositionCover U) : ViewSystem.TransitionCover U := by
90   intro a b f
91   obtain ⟨i, ha, hb, _⟩ := h a b b f (𝟙 b)
92   exact ⟨i, ha, hb⟩
93 
94 end CompositionCover
95 
96 namespace CocycleMatching
97 variable {F} {U : I → Set V}
98 
99 /-- Assemble one global edge label using any patch which sees that arrow. -/
100 noncomputable def assembleEdge (h : ViewSystem.TransitionCover U)
101     (m : F.CocycleMatching U) {a b : V} (f : a ⟶ b) : G a :=
102   let witness := Classical.choose (h a b f)
103   let spec := Classical.choose_spec (h a b f)
104   (m.patch witness).edge
105     (a := ⟨a, spec.1⟩) (b := ⟨b, spec.2⟩) f
106 
107 /-- Assembly agrees with the label in every patch containing the arrow. -/
108 theorem assembleEdge_local (h : ViewSystem.TransitionCover U)
109     (m : F.CocycleMatching U) (i : I) (a b : V)
110     (ha : a ∈ U i) (hb : b ∈ U i) (f : a ⟶ b) :
111     m.assembleEdge h f =
112       (m.patch i).edge (a := ⟨a, ha⟩) (b := ⟨b, hb⟩) f := by
113   unfold assembleEdge
114   let j := Classical.choose (h a b f)
115   let hs := Classical.choose_spec (h a b f)
116   exact m.agree j i a b hs.1 hs.2 ha hb f
117 
118 /-- Strictly matching local cocycles glue to a global cocycle. -/
119 noncomputable def glue (h : CompositionCover U) (m : F.CocycleMatching U) : F.Cocycle where
120   edge := fun f => m.assembleEdge h.transitionCover f
121   edge_id := by
122     intro a
123     obtain ⟨i, ha⟩ := ViewSystem.TransitionCover.objectCover U h.transitionCover a
124     rw [m.assembleEdge_local h.transitionCover i a a ha ha (𝟙 a)]
125     exact (m.patch i).edge_id ⟨a, ha⟩
126   edge_comp := by
127     intro a b c f g
128     obtain ⟨i, ha, hb, hc⟩ := h a b c f g
129     rw [m.assembleEdge_local h.transitionCover i a c ha hc (f ≫ g),
130         m.assembleEdge_local h.transitionCover i a b ha hb f,
131         m.assembleEdge_local h.transitionCover i b c hb hc g]
132     exact (m.patch i).edge_comp (a := ⟨a, ha⟩) (b := ⟨b, hb⟩) (c := ⟨c, hc⟩) f g
133 
134 /-- A global cocycle gives a strictly matching family on every patch. -/
135 def ofGlobal (c : F.Cocycle) : F.CocycleMatching U where
136   patch := fun i => F.restrictCocycle c (U i)
137   agree := by intros; rfl
138 
139 /-- Gluing the restrictions of a global cocycle returns that cocycle. -/
140 theorem glue_ofGlobal (h : CompositionCover U) (c : F.Cocycle) :
141     (ofGlobal (U := U) c).glue h = c := by
142   apply Cocycle.ext
143   intro a b f
144   obtain ⟨i, ha, hb⟩ := h.transitionCover a b f
145   exact (ofGlobal (U := U) c).assembleEdge_local h.transitionCover i a b ha hb f
146 
147 /-- Restricting a glued strict matching family returns the original family. -/
148 theorem ofGlobal_glue (h : CompositionCover U) (m : F.CocycleMatching U) :
149     ofGlobal (U := U) (m.glue h) = m := by
150   apply CocycleMatching.ext
151   intro i
152   apply PatchCocycle.ext
153   intro a b f
154   exact m.assembleEdge_local h.transitionCover i a.val b.val a.property b.property f
155 
156 /-- Strict cocycle descent equivalence under a composable-triple cover. -/
157 noncomputable def descentEquiv (h : CompositionCover U) :
158     F.Cocycle ≃ F.CocycleMatching U where
159   toFun := ofGlobal (U := U)
160   invFun := fun m => m.glue h
161   left_inv := glue_ofGlobal h
162   right_inv := ofGlobal_glue h
163 
164 end CocycleMatching
165 end GroupViewSystem
166 end KomorebiSpace

Back to source controls