DescentComparison.lean

1 import KomorebiSpace.EffectiveCocycleDescent
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Uniqueness and choice-independence of effectuation
7 
8 Two globalizations of the same specified descent datum have a unique global
9 gauge compatible with their local identifications. This does not discard
10 ordinary automorphisms of the underlying global cocycle.
11 -/
12 universe u v w z
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace GroupViewSystem
16 variable {V : Type u} [Category.{v} V]
17 variable {G : V → Type w} [∀ a, Group (G a)]
18 variable {I : Type z} {F : GroupViewSystem V G} {U : I → Set V}
19 namespace CocycleDescentData
20 namespace Effectuation
21 variable {D : F.CocycleDescentData U}
22 
23 /-- Underlying object in the existing unframed gauge groupoid. -/
24 def object (E : D.Effectuation) : F.GaugeObject (∅ : Set V) := ⟨E.global⟩
25 
26 /-- Patchwise quotient of the two sets of local identifications. -/
27 def comparisonMatching (E E' : D.Effectuation) : GaugeMatching (G := G) U where
28   value := fun i x => (E'.compare i x)⁻¹ * E.compare i x
29   agree := by
30     intro i j x hi hj
31     rw [E.overlap i j x hi hj, E'.overlap i j x hi hj]
32     group
33 
34 /-- The quotient gauge really carries one global cocycle to the other. -/
35 theorem comparison_relates (E E' : D.Effectuation) :
36     GaugeMatching.Relates F (E.comparisonMatching E') E.global E'.global := by
37   intro i x y f
38   change ((E'.compare i x)⁻¹ * E.compare i x) * E.global.edge f *
39     (F.pull f ((E'.compare i y)⁻¹ * E.compare i y))⁻¹ = E'.global.edge f
40   rw [E.global_local i x y f, E'.global_local i x y f, map_mul, map_inv]
41   group
42 
43 /-- Assemble the comparison through the already checked morphism descent. -/
44 def comparisonDescent (E E' : D.Effectuation) :
45     GaugeMatching.FramedDescent F U (∅ : Set V) E.object E'.object where
46   matching := E.comparisonMatching E'
47   relates := E.comparison_relates E'
48   based := by intro i x hi hx; exact False.elim hx
49 
50 noncomputable def comparisonHom (E E' : D.Effectuation)
51     (h : ViewSystem.TransitionCover U) : E.object ⟶ E'.object :=
52   (E.comparisonDescent E').glueHom h
53 
54 @[simp] theorem comparisonHom_local (E E' : D.Effectuation)
55     (h : ViewSystem.TransitionCover U) (i : I) (x : U i) :
56     (E.comparisonHom E' h).change.val x.val = (E'.compare i x)⁻¹ * E.compare i x :=
57   (E.comparisonDescent E').glueHom_local h i x.val x.property
58 
59 /-- A comparison must respect the chosen local identifications. -/
60 def Compatible (E E' : D.Effectuation) (a : E.object ⟶ E'.object) : Prop :=
61   ∀ i (x : U i), E'.compare i x * a.change.val x.val = E.compare i x
62 
63 theorem comparisonHom_compatible (E E' : D.Effectuation)
64     (h : ViewSystem.TransitionCover U) : E.Compatible E' (E.comparisonHom E' h) := by
65   intro i x
66   rw [comparisonHom_local]
67   group
68 
69 theorem comparisonHom_unique (E E' : D.Effectuation)
70     (h : ViewSystem.TransitionCover U) (a : E.object ⟶ E'.object)
71     (ha : E.Compatible E' a) : a = E.comparisonHom E' h := by
72   apply (E.comparisonDescent E').glueHom_unique h a
73   intro i x
74   change a.change.val x.val = (E'.compare i x)⁻¹ * E.compare i x
75   rw [← ha i x]
76   group
77 
78 /-- Existence and uniqueness are for a fixed descent datum with its identifications. -/
79 theorem exists_unique_comparison (E E' : D.Effectuation)
80     (h : ViewSystem.TransitionCover U) :
81     ∃! a : E.object ⟶ E'.object, E.Compatible E' a := by
82   refine ⟨E.comparisonHom E' h, E.comparisonHom_compatible E' h, ?_⟩
83   intro a ha
84   exact E.comparisonHom_unique E' h a ha
85 
86 noncomputable def comparisonIso (E E' : D.Effectuation)
87     (h : ViewSystem.TransitionCover U) : E.object ≅ E'.object :=
88   (Groupoid.isoEquivHom E.object E'.object).symm (E.comparisonHom E' h)
89 
90 theorem orbit_independent (E E' : D.Effectuation) (h : ViewSystem.TransitionCover U) :
91     F.orbitClass ∅ E.global = F.orbitClass ∅ E'.global :=
92   (F.morphism_nonempty_iff_class ∅ E.object E'.object).mp ⟨E.comparisonHom E' h⟩
93 
94 theorem comparisonHom_self (E : D.Effectuation) (h : ViewSystem.TransitionCover U) :
95     E.comparisonHom E h = 𝟙 E.object := by
96   symm
97   apply E.comparisonHom_unique E h
98   intro i x
99   change E.compare i x * 1 = E.compare i x
100   exact mul_one _
101 
102 theorem comparisonHom_comp (E E' E'' : D.Effectuation)
103     (h : ViewSystem.TransitionCover U) :
104     E.comparisonHom E' h ≫ E'.comparisonHom E'' h = E.comparisonHom E'' h := by
105   apply E.comparisonHom_unique E'' h
106   intro i x
107   change E''.compare i x *
108     ((E'.comparisonHom E'' h).change.val x.val * (E.comparisonHom E' h).change.val x.val) = _
109   rw [comparisonHom_local, comparisonHom_local]
110   group
111 
112 end Effectuation
113 
114 /-- Effective descent, including uniqueness of each compatible global comparison. -/
115 theorem effective_descent (D : F.CocycleDescentData U) (h : CompositionCover U) :
116     ∃ E : D.Effectuation, ∀ E' : D.Effectuation,
117       ∃! a : E.object ⟶ E'.object, E.Compatible E' a := by
118   refine ⟨D.effectuate h, ?_⟩
119   intro E'
120   exact (D.effectuate h).exists_unique_comparison E' h.transitionCover
121 
122 end CocycleDescentData
123 end GroupViewSystem
124 end KomorebiSpace

Back to source controls