SiteDescent.lean

1 import KomorebiSpace.CompositionSite
2 import KomorebiSpace.PatchViewSystem
3 import KomorebiSpace.DescentEquivalence
4 import Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
5 
6 set_option autoImplicit false
7 set_option backward.isDefEq.respectTransparency false
8 
9 /-!
10 # Effective descent over every patch and every composition-covering sieve
11 
12 The topology and the restricted groupoids are constructed independently.
13 This file proves their cover condition agrees with the existing descent
14 hypothesis, then applies the actual groupoid equivalence on any patch.
15 It does not identify our explicit descent-data type with mathlib's
16 Pseudofunctor.DescentData. That comparison is a separate formal interface.
17 -/
18 universe u v w z
19 namespace KomorebiSpace
20 open CategoryTheory Opposite Bicategory
21 namespace CompositionSite
22 variable {V : Type u} [Category.{v} V]
23 
24 /-- A subpatch expressed in the full category on the ambient patch W. -/
25 def inside {I : Type z} (W : Set V) (U : I → Set V) : I → Set (PatchViews W) :=
26   fun i => {x | x.val ∈ U i}
27 
28 /-- The relative family condition is precisely the old full-patch composition cover. -/
29 theorem familyCovers_iff_compositionCover {I : Type z} (W : Set V) (U : I → Set V) :
30     FamilyCovers W U ↔ GroupViewSystem.CompositionCover (inside W U) := by
31   constructor
32   · intro h a b c f g
33     let q : Triangle V := ⟨a.val, b.val, c.val, f.hom, g.hom⟩
34     have hq : q.support ⊆ W := (q.support_le_iff W).mpr
35       ⟨a.property, b.property, c.property⟩
36     obtain ⟨i, hi⟩ := h q hq
37     exact ⟨i, hi q.a_mem, hi q.b_mem, hi q.c_mem⟩
38   · intro h q hq
39     let a : PatchViews W := ⟨q.a, hq q.a_mem⟩
40     let b : PatchViews W := ⟨q.b, hq q.b_mem⟩
41     let c : PatchViews W := ⟨q.c, hq q.c_mem⟩
42     obtain ⟨i, hi, hj, hk⟩ := h a b c
43       (InducedCategory.homMk q.first) (InducedCategory.homMk q.second)
44     exact ⟨i, (q.support_le_iff (U i)).mpr ⟨hi, hj, hk⟩⟩
45 
46 end CompositionSite
47 
48 namespace GroupViewSystem
49 variable {V : Type u} [Category.{v} V]
50 variable {G : V → Type w} [∀ a, Group (G a)]
51 variable (F : GroupViewSystem V G)
52 
53 /-- The strict restriction diagram supplies the standard pseudofunctor interface. -/
54 def patchPseudofunctor : Pseudofunctor (LocallyDiscrete (Set V)ᵒᵖ) Cat :=
55   LocallyDiscrete.mkPseudofunctor
56     (fun W => F.patchDiagram.obj W)
57     (fun h => F.patchDiagram.map h)
58     (fun _ => Iso.refl _) (fun _ _ => Iso.refl _)
59     (by intros; ext c; apply GaugeObject.Hom.ext; apply Subtype.ext; funext x
60         dsimp [patchDiagram, patchRestrict, GaugeObject.compose, GaugeObject.identity]
61         simp)
62     (by intros; ext c; apply GaugeObject.Hom.ext; apply Subtype.ext; funext x
63         dsimp [patchDiagram, patchRestrict, GaugeObject.compose, GaugeObject.identity]
64         simp)
65     (by intros; ext c; apply GaugeObject.Hom.ext; apply Subtype.ext; funext x
66         dsimp [patchDiagram, patchRestrict, GaugeObject.compose, GaugeObject.identity]
67         simp)
68 
69 /-- Every covering family on every ambient patch admits effective groupoid descent. -/
70 noncomputable def siteDescent {I : Type z} (W : Set V) (U : I → Set V)
71     (h : CompositionSite.FamilyCovers W U) :
72     (F.onPatch W).GaugeObject ∅ ≌
73       (F.onPatch W).CocycleDescentData (CompositionSite.inside W U) :=
74   CocycleDescentData.descentEquivalence (F.onPatch W) (CompositionSite.inside W U)
75     ((CompositionSite.familyCovers_iff_compositionCover W U).mp h)
76 
77 /-- The equivalence uses the actual restriction functor, not an arbitrary equivalent map. -/
78 @[simp] theorem siteDescent_functor {I : Type z} (W : Set V) (U : I → Set V)
79     (h : CompositionSite.FamilyCovers W U) :
80     (F.siteDescent W U h).functor =
81       CocycleDescentData.restrictionFunctor (F.onPatch W) (CompositionSite.inside W U) := rfl
82 
83 /-- In particular, the theorem applies to every covering sieve of the constructed topology. -/
84 noncomputable def coveringSieveDescent (W : Set V) (s : Sieve W)
85     (hs : s ∈ CompositionSite.topology V W) :
86     (F.onPatch W).GaugeObject ∅ ≌
87       (F.onPatch W).CocycleDescentData
88         (CompositionSite.inside W (fun Z : CompositionSite.sievePatches s => Z.val)) :=
89   F.siteDescent W _ (CompositionSite.sieve_family_covers hs)
90 
91 /-- After any base change, the same coefficients admit descent for the intersected cover. -/
92 noncomputable def baseChangeDescent {I : Type z} {W Z : Set V} (hZW : Z ⊆ W)
93     (U : I → Set V) (h : CompositionSite.FamilyCovers W U) :
94     (F.onPatch Z).GaugeObject ∅ ≌
95       (F.onPatch Z).CocycleDescentData
96         (CompositionSite.inside Z (fun i => U i ∩ Z)) :=
97   F.siteDescent Z _ (CompositionSite.intersection_cover hZW h)
98 
99 /-- A cover refined by covers has the same effective reconstruction theorem. -/
100 noncomputable def compositeDescent {I : Type z} {J : I → Type z} (W : Set V)
101     (U : I → Set V) (T : ∀ i, J i → Set V)
102     (h : CompositionSite.FamilyCovers W U)
103     (k : ∀ i, CompositionSite.FamilyCovers (U i) (T i)) :
104     (F.onPatch W).GaugeObject ∅ ≌
105       (F.onPatch W).CocycleDescentData
106         (CompositionSite.inside W (fun ij : Sigma J => T ij.1 ij.2)) :=
107   F.siteDescent W _ (CompositionSite.composite_cover h k)
108 
109 end GroupViewSystem
110 end KomorebiSpace

Back to source controls