DescentEquivalence.lean

1 import KomorebiSpace.DescentDataGroupoid
2 
3 set_option autoImplicit false
4 
5 /-!
6 # An actual equivalence of the global gauge and descent-data groupoids
7 
8 Restriction is fully faithful under transition coverage and essentially
9 surjective under composition coverage. The equivalence is between the
10 specified strict coefficient/cocycle groupoids. No Grothendieck topology or
11 arbitrary higher-stack descent is asserted.
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 /-- A descent arrow between two restricted global cocycles has literally matching values. -/
23 def restrictedMatching {c d : F.GaugeObject (∅ : Set V)}
24     (b : ofGlobal (U := U) c.labels ⟶ ofGlobal d.labels) : GaugeMatching (G := G) U where
25   value := b.value
26   agree := by
27     intro i j x hi hj
28     have he := b.overlap i j x hi hj
29     change b.value j ⟨x,hj⟩ * 1 = 1 * b.value i ⟨x,hi⟩ at he
30     simpa only [mul_one, one_mul] using he.symm
31 
32 /-- The previous morphism-descent record, instantiated with the actual local arrow. -/
33 def restrictedDescent {c d : F.GaugeObject (∅ : Set V)}
34     (b : ofGlobal (U := U) c.labels ⟶ ofGlobal d.labels) :
35     GaugeMatching.FramedDescent F U (∅ : Set V) c d where
36   matching := restrictedMatching b
37   relates := b.local_eq
38   based := by intro i x hi hx; exact False.elim hx
39 
40 noncomputable def liftRestrictedHom (h : ViewSystem.TransitionCover U)
41     {c d : F.GaugeObject (∅ : Set V)}
42     (b : ofGlobal (U := U) c.labels ⟶ ofGlobal d.labels) : c ⟶ d :=
43   (restrictedDescent b).glueHom h
44 
45 @[simp] theorem liftRestrictedHom_value (h : ViewSystem.TransitionCover U)
46     {c d : F.GaugeObject (∅ : Set V)}
47     (b : ofGlobal (U := U) c.labels ⟶ ofGlobal d.labels) (i : I) (x : U i) :
48     (liftRestrictedHom h b).change.val x.val = b.value i x :=
49   (restrictedDescent b).glueHom_local h i x.val x.property
50 
51 /-- Restriction loses no arrow when the patches cover all view objects. -/
52 theorem restriction_injective (h : ViewSystem.ObjectCover U)
53     {c d : F.GaugeObject (∅ : Set V)}
54     (a b : c ⟶ d) (he : (restrictionFunctor F U).map a = (restrictionFunctor F U).map b) :
55     a = b := by
56   apply GaugeObject.Hom.ext
57   apply Subtype.ext
58   funext x
59   obtain ⟨i,hi⟩ := h x
60   exact congrArg (fun z : ofGlobal (U := U) c.labels ⟶ ofGlobal d.labels =>
61     z.value i ⟨x,hi⟩) he
62 
63 @[simp] theorem restrict_lift (h : ViewSystem.TransitionCover U)
64     {c d : F.GaugeObject (∅ : Set V)}
65     (b : ofGlobal (U := U) c.labels ⟶ ofGlobal d.labels) :
66     (restrictionFunctor F U).map (liftRestrictedHom h b) = b := by
67   apply Hom.ext
68   intro i x
69   exact liftRestrictedHom_value h b i x
70 
71 @[simp] theorem lift_restrict (h : ViewSystem.TransitionCover U)
72     {c d : F.GaugeObject (∅ : Set V)} (a : c ⟶ d) :
73     liftRestrictedHom h ((restrictionFunctor F U).map a) = a := by
74   apply restriction_injective (ViewSystem.TransitionCover.objectCover U h)
75   exact restrict_lift h _
76 
77 /-- Explicit inverse on every Hom set. -/
78 noncomputable def restrictionFullyFaithful (h : ViewSystem.TransitionCover U) :
79     (restrictionFunctor F U).FullyFaithful where
80   preimage := liftRestrictedHom h
81   map_preimage := restrict_lift h
82   preimage_map := lift_restrict h
83 
84 /-- Morphisms, including automorphisms, are retained by descent. -/
85 noncomputable def restrictionHomEquiv (h : ViewSystem.TransitionCover U)
86     (c d : F.GaugeObject (∅ : Set V)) :
87     (c ⟶ d) ≃ ((restrictionFunctor F U).obj c ⟶ (restrictionFunctor F U).obj d) where
88   toFun := (restrictionFunctor F U).map
89   invFun := liftRestrictedHom h
90   left_inv := lift_restrict h
91   right_inv := restrict_lift h
92 
93 /-- Full, faithful, and essentially surjective are all proved under the stated cover. -/
94 theorem restriction_isEquivalence (h : CompositionCover U) :
95     (restrictionFunctor F U).IsEquivalence := by
96   let ff := restrictionFullyFaithful (F := F) h.transitionCover
97   let : (restrictionFunctor F U).Full := ff.full
98   let : (restrictionFunctor F U).Faithful := ff.faithful
99   let : (restrictionFunctor F U).EssSurj :=
100     ⟨restriction_essentially_surjective h⟩
101   exact {}
102 
103 /-- Effective groupoid descent with genuine overlap isomorphisms. -/
104 noncomputable def descentEquivalence (F : GroupViewSystem V G)
105     (U : I → Set V) (h : CompositionCover U) :
106     F.GaugeObject (∅ : Set V) ≌ F.CocycleDescentData U := by
107   letI := restriction_isEquivalence (F := F) h
108   exact (restrictionFunctor F U).asEquivalence
109 
110 /-- The forward functor is the explicitly defined restriction functor. -/
111 @[simp] theorem descentEquivalence_functor (h : CompositionCover U) :
112     (descentEquivalence F U h).functor = restrictionFunctor F U := rfl
113 
114 end CocycleDescentData
115 end GroupViewSystem
116 end KomorebiSpace

Back to source controls