StandardDescentBridge.lean

1 import KomorebiSpace.SiteDescent
2 import Mathlib.CategoryTheory.Sites.Descent.IsStack
3 
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 
7 /-!
8 # Comparison with mathlib's standard descent-data interface
9 
10 All standard pullbacks are the actual restriction functors on gauge
11 families. The lemmas below expose their coordinate actions before invoking
12 any standard stack interface.
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 open Pseudofunctor.LocallyDiscreteOpToCat
23 
24 /-- Coordinate formula for the standard pseudofunctor pullback of a gauge arrow. -/
25 theorem pullHom_value {X₁ X₂ Y Y' : Set V}
26     {M₁ : (F.onPatch X₁).GaugeObject ∅} {M₂ : (F.onPatch X₂).GaugeObject ∅}
27     {f₁ : Y ⟶ X₁} {f₂ : Y ⟶ X₂}
28     (a : (F.patchRestrict (leOfHom f₁)).obj M₁ ⟶
29       (F.patchRestrict (leOfHom f₂)).obj M₂)
30     (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂)
31     (x : PatchViews Y') :
32     (pullHom (F := F.patchPseudofunctor) (f₁ := f₁) (f₂ := f₂) a g gf₁ gf₂
33       (Subsingleton.elim _ _) (Subsingleton.elim _ _)).change.val x =
34       a.change.val ⟨x.val, leOfHom g x.property⟩ := by
35   simp [pullHom, Pseudofunctor.mapComp', patchPseudofunctor,
36     LocallyDiscrete.mkPseudofunctor, pseudofunctorOfIsLocallyDiscrete]
37   dsimp [patchDiagram, patchRestrict]
38   simp
39 
40 variable {I : Type z} {W : Set V} {U : I → Set V} (hU : ∀ i, U i ⊆ W)
41 
42 abbrev Data := F.patchPseudofunctor.DescentData (fun i => homOfLE (hU i))
43 
44 /-- Canonical descent of a global object has identity comparison gauges. -/
45 theorem ofObj_hom_value (c : (F.onPatch W).GaugeObject ∅)
46     {Y : Set V} (q : Y ⟶ W) {i j : I} (fi : Y ⟶ U i) (fj : Y ⟶ U j)
47     (x : PatchViews Y) :
48     ((Pseudofunctor.DescentData.ofObj (F := F.patchPseudofunctor)
49       (f := fun i => homOfLE (hU i)) c).hom q fi fj
50         (Subsingleton.elim _ _) (Subsingleton.elim _ _)).change.val x = 1 := by
51   simp [Pseudofunctor.DescentData.ofObj, Pseudofunctor.mapComp',
52     patchPseudofunctor, LocallyDiscrete.mkPseudofunctor,
53     pseudofunctorOfIsLocallyDiscrete]
54   dsimp [patchDiagram, patchRestrict]
55   simp
56 
57 /-- A singleton inclusion for a known membership. -/
58 def singletonInclusion {Z : Set V} {x : V} (h : x ∈ Z) : ({x} : Set V) ⟶ Z :=
59   homOfLE (by intro y hy; rw [Set.mem_singleton_iff.mp hy]; exact h)
60 
61 /-- The comparison value at a view, extracted from standard descent on its singleton. -/
62 def label (D : Data F hU) (i j : I) (x : V) (hi : x ∈ U i) (hj : x ∈ U j) : G x :=
63   (D.hom (singletonInclusion (hU i hi)) (singletonInclusion hi)
64     (singletonInclusion hj) (Subsingleton.elim _ _) (Subsingleton.elim _ _)).change.val
65       ⟨x, Set.mem_singleton x⟩
66 
67 /-- Naturality makes the singleton label agree with evaluation on every common subpatch. -/
68 theorem hom_value (D : Data F hU) {Y : Set V} (q : Y ⟶ W) {i j : I}
69     (fi : Y ⟶ U i) (fj : Y ⟶ U j) (x : PatchViews Y) :
70     (D.hom q fi fj (Subsingleton.elim _ _) (Subsingleton.elim _ _)).change.val x =
71       label F hU D i j x.val (leOfHom fi x.property) (leOfHom fj x.property) := by
72   let g := singletonInclusion x.property
73   let gi := singletonInclusion (leOfHom fi x.property)
74   let gj := singletonInclusion (leOfHom fj x.property)
75   have hp := D.pullHom_hom g q (singletonInclusion (leOfHom q x.property))
76     (Subsingleton.elim _ _) fi fj (Subsingleton.elim _ _) (Subsingleton.elim _ _)
77     gi gj (Subsingleton.elim _ _) (Subsingleton.elim _ _)
78   have hv := congrArg (fun a => a.change.val ⟨x.val, Set.mem_singleton x.val⟩) hp
79   have he := pullHom_value F (f₁ := fi) (f₂ := fj)
80     (D.hom q fi fj (Subsingleton.elim _ _) (Subsingleton.elim _ _))
81     g gi gj ⟨x.val, Set.mem_singleton x.val⟩
82   exact he.symm.trans hv
83 
84 /-- The standard triple-overlap equation is the noncommutative label equation. -/
85 theorem label_comp (D : Data F hU) (i j k : I) (x : V)
86     (hi : x ∈ U i) (hj : x ∈ U j) (hk : x ∈ U k) :
87     label F hU D i k x hi hk =
88       label F hU D j k x hj hk * label F hU D i j x hi hj := by
89   have hc := D.hom_comp (singletonInclusion (hU i hi))
90     (singletonInclusion hi) (singletonInclusion hj) (singletonInclusion hk)
91     (Subsingleton.elim _ _) (Subsingleton.elim _ _) (Subsingleton.elim _ _)
92   have hv := congrArg (fun a => a.change.val ⟨x, Set.mem_singleton x⟩) hc
93   exact hv.symm
94 
95 /-- Standard overlap maps give the required relation between every pair of local labels. -/
96 theorem label_edge (D : Data F hU) (i j : I) (x y : V)
97     (hxi : x ∈ U i) (hyi : y ∈ U i) (hxj : x ∈ U j) (hyj : y ∈ U j)
98     (f : x ⟶ y) :
99     label F hU D i j x hxi hxj *
100         (D.obj i).labels.edge (a := ⟨x,hxi⟩) (b := ⟨y,hyi⟩) (InducedCategory.homMk f) *
101         (F.pull f (label F hU D i j y hyi hyj))⁻¹ =
102       (D.obj j).labels.edge (a := ⟨x,hxj⟩) (b := ⟨y,hyj⟩) (InducedCategory.homMk f) := by
103   let qi : (U i ∩ U j) ⟶ U i := homOfLE Set.inter_subset_left
104   let qj : (U i ∩ U j) ⟶ U j := homOfLE Set.inter_subset_right
105   let q : (U i ∩ U j) ⟶ W := homOfLE (Set.inter_subset_left.trans (hU i))
106   let a := D.hom q qi qj (Subsingleton.elim _ _) (Subsingleton.elim _ _)
107   have he := congrArg (fun c => c.edge
108     (a := (⟨x, hxi, hxj⟩ : PatchViews (U i ∩ U j)))
109     (b := (⟨y, hyi, hyj⟩ : PatchViews (U i ∩ U j)))
110     (InducedCategory.homMk f)) a.target
111   change a.change.val ⟨x,hxi,hxj⟩ * _ * (F.pull f (a.change.val ⟨y,hyi,hyj⟩))⁻¹ = _ at he
112   have hx := hom_value F hU D q qi qj ⟨x,hxi,hxj⟩
113   have hy := hom_value F hU D q qi qj ⟨y,hyi,hyj⟩
114   change a.change.val ⟨x,hxi,hxj⟩ = _ at hx
115   change a.change.val ⟨y,hyi,hyj⟩ = _ at hy
116   rw [hx, hy] at he
117   exact he
118 
119 /-- Standard descent data retain exactly the previously implemented overlap labels. -/
120 def toConcrete (D : Data F hU) :
121     (F.onPatch W).CocycleDescentData (CompositionSite.inside W U) where
122   patch i :=
123     { edge := fun {a b} f => (D.obj i).labels.edge
124         (a := ⟨a.val.val,a.property⟩) (b := ⟨b.val.val,b.property⟩)
125         (InducedCategory.homMk f.hom)
126       edge_id := fun a => (D.obj i).labels.edge_id ⟨a.val.val,a.property⟩
127       edge_comp := by
128         intro a b c f g
129         exact (D.obj i).labels.edge_comp
130           (a := ⟨a.val.val,a.property⟩) (b := ⟨b.val.val,b.property⟩)
131           (c := ⟨c.val.val,c.property⟩)
132           (InducedCategory.homMk f.hom) (InducedCategory.homMk g.hom) }
133   change := fun i j x hi hj => label F hU D i j x.val hi hj
134   change_edge := fun i j x y hxi hyi hxj hyj f =>
135     label_edge F hU D i j x.val y.val hxi hyi hxj hyj f.hom
136   change_comp := fun i j k x hi hj hk => label_comp F hU D i j k x.val hi hj hk
137 
138 end StandardDescent
139 end GroupViewSystem
140 end KomorebiSpace

Back to source controls