CompositionStack.lean

1 import KomorebiSpace.StandardDescentBridge
2 
3 set_option autoImplicit false
4 set_option backward.isDefEq.respectTransparency false
5 
6 /-!
7 # The ordinary cocycle stack on the composition site
8 
9 The actual patch pseudofunctor is shown to satisfy mathlib's standard
10 IsStack predicate. The proof translates standard overlap data to the
11 already checked concrete nonabelian descent construction, then retains
12 all morphisms through a proved inverse to standard restriction.
13 -/
14 universe u v w z
15 namespace KomorebiSpace
16 open CategoryTheory Opposite Bicategory
17 namespace GroupViewSystem
18 variable {V : Type u} [Category.{v} V]
19 variable {G : V → Type w} [∀ a, Group (G a)]
20 variable (F : GroupViewSystem V G)
21 namespace StandardDescent
22 variable {I : Type z} {W : Set V} {U : I → Set V} (hU : ∀ i, U i ⊆ W)
23 
24 /-- The concrete effectuation supplies a standard local gauge comparison. -/
25 def localRealizationHom {D : Data F hU} (E : (toConcrete F hU D).Effectuation) (i : I) :
26     (F.patchRestrict (hU i)).obj E.object ⟶ D.obj i where
27   change := ⟨fun x => E.compare i ⟨⟨x.val,hU i x.property⟩,x.property⟩, by
28     intro x; exact False.elim x.property⟩
29   target := by
30     apply Cocycle.ext
31     intro x y f
32     exact E.local_eq i ⟨⟨x.val,hU i x.property⟩,x.property⟩
33       ⟨⟨y.val,hU i y.property⟩,y.property⟩ (InducedCategory.homMk f.hom)
34 
35 @[simp] theorem localRealizationHom_value {D : Data F hU}
36     (E : (toConcrete F hU D).Effectuation) (i : I) (x : PatchViews (U i)) :
37     (localRealizationHom F hU E i).change.val x =
38       E.compare i ⟨⟨x.val,hU i x.property⟩,x.property⟩ := rfl
39 
40 /-- The local identifications respect every standard overlap pullback. -/
41 def realizationIso {D : Data F hU} (E : (toConcrete F hU D).Effectuation) :
42     (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj E.object ≅ D := by
43   refine Pseudofunctor.DescentData.isoMk
44     (fun i => (Groupoid.isoEquivHom (C := (F.onPatch (U i)).GaugeObject ∅) _ _).symm (localRealizationHom F hU E i)) ?_
45   intro Y q i j fi fj hfi hfj
46   apply GaugeObject.Hom.ext
47   apply Subtype.ext
48   funext x
49   dsimp only [Groupoid.isoEquivHom, Equiv.symm, Equiv.coe_fn_mk]
50   change (D.hom q fi fj hfi hfj).change.val x *
51     ((F.patchRestrict (leOfHom fi)).map (localRealizationHom F hU E i)).change.val x =
52     ((F.patchRestrict (leOfHom fj)).map (localRealizationHom F hU E j)).change.val x *
53     ((Pseudofunctor.DescentData.ofObj (F := F.patchPseudofunctor)
54       (f := fun i => homOfLE (hU i)) E.object).hom q fi fj hfi hfj).change.val x
55   rw [ofObj_hom_value F hU E.object q fi fj x, mul_one]
56   change (D.hom q fi fj hfi hfj).change.val x *
57     E.compare i ⟨⟨x.val,leOfHom q x.property⟩,leOfHom fi x.property⟩ =
58     E.compare j ⟨⟨x.val,leOfHom q x.property⟩,leOfHom fj x.property⟩
59   rw [hom_value F hU D q fi fj x]
60   exact (E.overlap i j ⟨x.val,leOfHom q x.property⟩
61     (leOfHom fi x.property) (leOfHom fj x.property)).symm
62 
63 /-- Essential surjectivity in the standard library's descent category. -/
64 theorem essentially_surjective (h : CompositionSite.FamilyCovers W U) (D : Data F hU) :
65     ∃ c : (F.onPatch W).GaugeObject ∅,
66       Nonempty ((F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj c ≅ D) := by
67   let E := (toConcrete F hU D).effectuate
68     ((CompositionSite.familyCovers_iff_compositionCover W U).mp h)
69   exact ⟨E.object, ⟨realizationIso F hU E⟩⟩
70 
71 /-- Standard descent arrows yield matching gauge values on the original view patches. -/
72 def restrictedMatching {c d : (F.onPatch W).GaugeObject ∅}
73     (b : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj c ⟶
74       (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj d) :
75     GaugeMatching (G := fun x : PatchViews W => G x.val) (CompositionSite.inside W U) where
76   value i x := (b.hom i).change.val ⟨x.val.val,x.property⟩
77   agree := by
78     intro i j x hi hj
79     let q := singletonInclusion x.property
80     let fi := singletonInclusion (show x.val ∈ U i from hi)
81     let fj := singletonInclusion (show x.val ∈ U j from hj)
82     have hc := b.comm q fi fj (Subsingleton.elim _ _) (Subsingleton.elim _ _)
83     have he := congrArg (fun a => a.change.val ⟨x.val,Set.mem_singleton x.val⟩) hc
84     change
85       ((Pseudofunctor.DescentData.ofObj (F := F.patchPseudofunctor)
86         (f := fun i => homOfLE (hU i)) d).hom q fi fj (Subsingleton.elim _ _) (Subsingleton.elim _ _)).change.val ⟨x.val,Set.mem_singleton x.val⟩ *
87           (b.hom i).change.val ⟨x.val,hi⟩ =
88       (b.hom j).change.val ⟨x.val,hj⟩ *
89         ((Pseudofunctor.DescentData.ofObj (F := F.patchPseudofunctor)
90           (f := fun i => homOfLE (hU i)) c).hom q fi fj (Subsingleton.elim _ _) (Subsingleton.elim _ _)).change.val ⟨x.val,Set.mem_singleton x.val⟩ at he
91     rw [ofObj_hom_value F hU d, ofObj_hom_value F hU c, one_mul, mul_one] at he
92     exact he
93 
94 /-- The standard local morphisms satisfy the earlier actual gauge-descent equations. -/
95 def restrictedFramedDescent {c d : (F.onPatch W).GaugeObject ∅}
96     (b : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj c ⟶
97       (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj d) :
98     GaugeMatching.FramedDescent (F.onPatch W) (CompositionSite.inside W U) ∅ c d where
99   matching := restrictedMatching F hU b
100   relates := by
101     intro i x y f
102     exact congrArg (fun z => z.edge
103       (a := (⟨x.val.val,x.property⟩ : PatchViews (U i)))
104       (b := (⟨y.val.val,y.property⟩ : PatchViews (U i)))
105       (InducedCategory.homMk f.hom)) (b.hom i).target
106   based := by intro i x hi hx; exact False.elim hx
107 
108 /-- Lift a standard descent arrow to a genuine global gauge. -/
109 noncomputable def liftHom (h : CompositionSite.FamilyCovers W U)
110     {c d : (F.onPatch W).GaugeObject ∅}
111     (b : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj c ⟶
112       (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj d) : c ⟶ d :=
113   (restrictedFramedDescent F hU b).glueHom
114     ((CompositionSite.familyCovers_iff_compositionCover W U).mp h).transitionCover
115 
116 @[simp] theorem liftHom_local (h : CompositionSite.FamilyCovers W U)
117     {c d : (F.onPatch W).GaugeObject ∅}
118     (b : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj c ⟶
119       (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj d)
120     (i : I) (x : PatchViews (U i)) :
121     (liftHom F hU h b).change.val ⟨x.val,hU i x.property⟩ =
122       (b.hom i).change.val x :=
123   (restrictedFramedDescent F hU b).glueHom_local
124     ((CompositionSite.familyCovers_iff_compositionCover W U).mp h).transitionCover
125     i ⟨x.val,hU i x.property⟩ x.property
126 
127 /-- Standard restriction loses no global gauge on a composition cover. -/
128 theorem restriction_injective (h : CompositionSite.FamilyCovers W U)
129     {c d : (F.onPatch W).GaugeObject ∅} (a b : c ⟶ d)
130     (he : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).map a =
131       (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).map b) : a = b := by
132   apply GaugeObject.Hom.ext
133   apply Subtype.ext
134   funext x
135   obtain ⟨i,hi⟩ := CompositionSite.covers_objects h x.property
136   exact congrArg (fun z => (z.hom i).change.val ⟨x.val,hi⟩) he
137 
138 @[simp] theorem restrict_liftHom (h : CompositionSite.FamilyCovers W U)
139     {c d : (F.onPatch W).GaugeObject ∅}
140     (b : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj c ⟶
141       (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).obj d) :
142     (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).map
143       (liftHom F hU h b) = b := by
144   apply Pseudofunctor.DescentData.hom_ext
145   intro i
146   apply GaugeObject.Hom.ext
147   apply Subtype.ext
148   funext x
149   exact liftHom_local F hU h b i x
150 
151 @[simp] theorem liftHom_restrict (h : CompositionSite.FamilyCovers W U)
152     {c d : (F.onPatch W).GaugeObject ∅} (a : c ⟶ d) :
153     liftHom F hU h
154       ((F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).map a) = a := by
155   apply restriction_injective F hU h
156   exact restrict_liftHom F hU h _
157 
158 /-- An explicit inverse on the Hom sets of the standard descent functor. -/
159 noncomputable def fullyFaithful (h : CompositionSite.FamilyCovers W U) :
160     (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).FullyFaithful where
161   preimage := liftHom F hU h
162   map_preimage := restrict_liftHom F hU h
163   preimage_map := liftHom_restrict F hU h
164 
165 /-- Effective descent is now an equivalence for the actual mathlib descent interface. -/
166 theorem restriction_isEquivalence (h : CompositionSite.FamilyCovers W U) :
167     (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).IsEquivalence := by
168   let ff := fullyFaithful F hU h
169   let : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).Full := ff.full
170   let : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).Faithful := ff.faithful
171   let : (F.patchPseudofunctor.toDescentData (fun i => homOfLE (hU i))).EssSurj :=
172     ⟨essentially_surjective F hU h⟩
173   exact {}
174 
175 end StandardDescent
176 
177 /-- The cocycle pseudofunctor is an ordinary stack for the actual composition topology. -/
178 theorem patch_isStack : F.patchPseudofunctor.IsStack (CompositionSite.topology V) := by
179   apply Pseudofunctor.IsStack.of_isStackFor
180   intro W s hs
181   rw [Pseudofunctor.isStackFor_iff]
182   let U : s.arrows.category → Set V := fun t => t.obj.left
183   let hU : ∀ t, U t ⊆ W := fun t => leOfHom t.obj.hom
184   have hc : CompositionSite.FamilyCovers W U := by
185     intro q hq
186     let t : s.arrows.category := s.arrows.categoryMk (homOfLE hq) (hs q hq)
187     exact ⟨t, Set.Subset.refl q.support⟩
188   exact StandardDescent.restriction_isEquivalence F hU hc
189 
190 end GroupViewSystem
191 end KomorebiSpace

Back to source controls