DescentDataGroupoid.lean

1 import KomorebiSpace.DescentComparison
2 import Mathlib.CategoryTheory.Equivalence
3 
4 set_option autoImplicit false
5 
6 /-!
7 # The groupoid of nonabelian descent data
8 
9 Objects carry local cocycles and specified coherent overlap isomorphisms.
10 Morphisms are local gauges commuting with those overlap isomorphisms.
11 Restriction is a genuine functor from the existing global gauge groupoid.
12 -/
13 universe u v w z
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 {I : Type z} {F : GroupViewSystem V G} {U : I → Set V}
20 namespace CocycleDescentData
21 
22 /-- The overlap square for a morphism retains its noncommutative order. -/
23 structure Hom (D E : F.CocycleDescentData U) where
24   value : ∀ i, ∀ x : U i, G x.val
25   local_eq : ∀ (i : I) (x y : U i) (f : x.val ⟶ y.val),
26     value i x * (D.patch i).edge f * (F.pull f (value i y))⁻¹ = (E.patch i).edge f
27   overlap : ∀ (i j : I) (x : V) (hi : x ∈ U i) (hj : x ∈ U j),
28     value j ⟨x,hj⟩ * D.change i j x hi hj = E.change i j x hi hj * value i ⟨x,hi⟩
29 
30 @[ext] theorem Hom.ext {D E : F.CocycleDescentData U} {a b : Hom D E}
31     (h : ∀ i x, a.value i x = b.value i x) : a = b := by
32   cases a with
33   | mk av al ao =>
34     cases b with
35     | mk bv bl bo =>
36       have he : av = bv := by funext i x; exact h i x
37       cases he
38       rfl
39 
40 def identity (D : F.CocycleDescentData U) : Hom D D where
41   value := fun _ _ => 1
42   local_eq := by intros; simp
43   overlap := by intros; simp
44 
45 def compose {D E K : F.CocycleDescentData U} (a : Hom D E) (b : Hom E K) : Hom D K where
46   value := fun i x => b.value i x * a.value i x
47   local_eq := by
48     intro i x y f
49     rw [map_mul]
50     calc
51       _ = b.value i x * (a.value i x * (D.patch i).edge f *
52           (F.pull f (a.value i y))⁻¹) * (F.pull f (b.value i y))⁻¹ := by group
53       _ = _ := by rw [a.local_eq, b.local_eq]
54   overlap := by
55     intro i j x hi hj
56     calc
57       _ = b.value j ⟨x,hj⟩ * (a.value j ⟨x,hj⟩ * D.change i j x hi hj) := by group
58       _ = b.value j ⟨x,hj⟩ * (E.change i j x hi hj * a.value i ⟨x,hi⟩) := by rw [a.overlap]
59       _ = (b.value j ⟨x,hj⟩ * E.change i j x hi hj) * a.value i ⟨x,hi⟩ := by group
60       _ = _ := by rw [b.overlap]; group
61 
62 def reverse {D E : F.CocycleDescentData U} (a : Hom D E) : Hom E D where
63   value := fun i x => (a.value i x)⁻¹
64   local_eq := by
65     intro i x y f
66     rw [← a.local_eq i x y f, map_inv]
67     group
68   overlap := by
69     intro i j x hi hj
70     calc
71       _ = (a.value j ⟨x,hj⟩)⁻¹ *
72         (E.change i j x hi hj * a.value i ⟨x,hi⟩) * (a.value i ⟨x,hi⟩)⁻¹ := by group
73       _ = _ := by rw [← a.overlap]; group
74 
75 instance : Groupoid (F.CocycleDescentData U) where
76   Hom := Hom
77   id := identity
78   comp := compose
79   id_comp := by intro D E a; apply Hom.ext; intro i x; exact mul_one _
80   comp_id := by intro D E a; apply Hom.ext; intro i x; exact one_mul _
81   assoc := by intro D E K L a b c; apply Hom.ext; intro i x; exact (mul_assoc _ _ _).symm
82   inv := reverse
83   inv_comp := by intro D E a; apply Hom.ext; intro i x; exact mul_inv_cancel _
84   comp_inv := by intro D E a; apply Hom.ext; intro i x; exact inv_mul_cancel _
85 
86 @[simp] theorem composition_value {D E K : F.CocycleDescentData U}
87     (a : D ⟶ E) (b : E ⟶ K) (i : I) (x : U i) :
88     (a ≫ b).value i x = b.value i x * a.value i x := rfl
89 
90 /-- The canonical descent datum of a global cocycle has identity overlap gauges. -/
91 def ofGlobal (c : F.Cocycle) : F.CocycleDescentData U where
92   patch := fun i => F.restrictCocycle c (U i)
93   change := fun _ _ _ _ _ => 1
94   change_edge := by intros; simp [restrictCocycle]
95   change_comp := by intros; simp
96 
97 /-- Restrict an actual global gauge arrow to every patch. -/
98 def restrictHom {c d : F.GaugeObject (∅ : Set V)} (a : c ⟶ d) :
99     ofGlobal (U := U) c.labels ⟶ ofGlobal d.labels where
100   value := fun _ x => a.change.val x.val
101   local_eq := by
102     intro i x y f
103     exact congrArg (fun c : F.Cocycle => c.edge f) a.target
104   overlap := by intros; simp [ofGlobal]
105 
106 /-- Restriction into the descent-data groupoid. -/
107 def restrictionFunctor (F : GroupViewSystem V G) (U : I → Set V) :
108     F.GaugeObject (∅ : Set V) ⥤ F.CocycleDescentData U where
109   obj := fun c => ofGlobal c.labels
110   map := restrictHom
111   map_id := by intro c; apply Hom.ext; intros; rfl
112   map_comp := by intros; apply Hom.ext; intros; rfl
113 
114 @[simp] theorem restriction_value {c d : F.GaugeObject (∅ : Set V)}
115     (a : c ⟶ d) (i : I) (x : U i) :
116     ((restrictionFunctor F U).map a).value i x = a.change.val x.val := rfl
117 
118 /-- The chosen local comparisons give an isomorphism from restricted globalization to D. -/
119 def Effectuation.toDescentHom {D : F.CocycleDescentData U} (E : D.Effectuation) :
120     ofGlobal (U := U) E.global ⟶ D where
121   value := E.compare
122   local_eq := E.local_eq
123   overlap := by
124     intro i j x hi hj
125     change E.compare j ⟨x,hj⟩ * 1 = D.change i j x hi hj * E.compare i ⟨x,hi⟩
126     rw [mul_one, E.overlap]
127 
128 def Effectuation.toDescentIso {D : F.CocycleDescentData U} (E : D.Effectuation) :
129     ofGlobal (U := U) E.global ≅ D :=
130   (Groupoid.isoEquivHom _ _).symm E.toDescentHom
131 
132 /-- Explicit essential-surjectivity witnesses: no global cocycle is assumed in the input. -/
133 theorem restriction_essentially_surjective (h : CompositionCover U)
134     (D : F.CocycleDescentData U) :
135     ∃ c : F.GaugeObject (∅ : Set V), Nonempty ((restrictionFunctor F U).obj c ≅ D) :=
136   ⟨(D.effectuate h).object, ⟨(D.effectuate h).toDescentIso⟩⟩
137 
138 end CocycleDescentData
139 end GroupViewSystem
140 end KomorebiSpace

Back to source controls