GaugeDescent.lean

1 import KomorebiSpace.CocycleGaugeGroupoid
2 import KomorebiSpace.SectionGluing
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Descent of gauge transformations across a view cover
8 
9 This module proves the morphism half of a stack-like descent statement for the
10 existing nonabelian cocycle groupoid. Local gauge changes which agree on
11 view-overlaps glue to one global gauge. If each local gauge carries one fixed
12 cocycle to another on every transition visible in its patch, then the glued
13 gauge carries the first global cocycle to the second globally, provided the
14 patches cover transitions. A framed version produces an actual morphism in the
15 existing `GaugeObject` groupoid.
16 
17 The cocycle objects in this theorem are already global. Thus this is descent of
18 morphisms, not yet effective descent of locally supplied cocycle objects.
19 -/
20 universe u v w z
21 namespace KomorebiSpace
22 open CategoryTheory
23 namespace GroupViewSystem
24 
25 variable {V : Type u}
26 variable {G : V → Type w}
27 variable {I : Type z}
28 
29 /-- A family of local gauge values which agrees literally on common views. -/
30 structure GaugeMatching (U : I → Set V) where
31   value : ∀ (i : I) (a : U i), G a.val
32   agree : ∀ (i j : I) (a : V) (hi : a ∈ U i) (hj : a ∈ U j),
33     value i ⟨a, hi⟩ = value j ⟨a, hj⟩
34 
35 namespace GaugeMatching
36 variable {U : I → Set V}
37 
38 @[ext] theorem ext {m n : GaugeMatching (G := G) U}
39     (h : ∀ i a, m.value i a = n.value i a) : m = n := by
40   cases m with
41   | mk ml ma =>
42     cases n with
43     | mk nl na =>
44       have he : ml = nl := by
45         funext i a
46         exact h i a
47       cases he
48       rfl
49 
50 /-- Assemble a global gauge family from locally matching values. -/
51 noncomputable def assemble (h : ViewSystem.ObjectCover U) (m : GaugeMatching (G := G) U) :
52     ∀ a, G a :=
53   fun a => m.value (Classical.choose (h a))
54     ⟨a, Classical.choose_spec (h a)⟩
55 
56 theorem assemble_local (h : ViewSystem.ObjectCover U) (m : GaugeMatching (G := G) U)
57     (i : I) (a : V) (ha : a ∈ U i) :
58     m.assemble h a = m.value i ⟨a, ha⟩ := by
59   exact m.agree _ i a _ ha
60 
61 variable [Category.{v} V] [∀ a, Group (G a)]
62 
63 /-- Local gauge equations relating two global cocycles. -/
64 def Relates (F : GroupViewSystem V G) (m : GaugeMatching (G := G) U)
65     (c d : F.Cocycle) : Prop :=
66   ∀ (i : I) (a b : U i) (f : a.val ⟶ b.val),
67     m.value i a * c.edge f * (F.pull f (m.value i b))⁻¹ = d.edge f
68 
69 /-- A transition-covered matching of local gauges gives one global gauge equation. -/
70 theorem assemble_relates (F : GroupViewSystem V G) (m : GaugeMatching (G := G) U)
71     (c d : F.Cocycle) (hcover : ViewSystem.TransitionCover U)
72     (hrel : Relates F m c d) :
73     F.gauge (m.assemble (ViewSystem.TransitionCover.objectCover U hcover)) c = d := by
74   apply Cocycle.ext
75   intro a b f
76   obtain ⟨i, ha, hb⟩ := hcover a b f
77   change m.assemble (ViewSystem.TransitionCover.objectCover U hcover) a * c.edge f *
78       (F.pull f (m.assemble (ViewSystem.TransitionCover.objectCover U hcover) b))⁻¹ = d.edge f
79   rw [m.assemble_local (ViewSystem.TransitionCover.objectCover U hcover) i a ha,
80       m.assemble_local (ViewSystem.TransitionCover.objectCover U hcover) i b hb]
81   exact hrel i ⟨a, ha⟩ ⟨b, hb⟩ f
82 
83 /-- Local identity on a framing domain survives assembly. -/
84 def BasedOn (m : GaugeMatching (G := G) U) (B : Set V) : Prop :=
85   ∀ (i : I) (a : V) (ha : a ∈ U i), a ∈ B → m.value i ⟨a, ha⟩ = 1
86 
87 /-- The assembled family is a member of the existing based gauge subgroup. -/
88 noncomputable def assembleBased (F : GroupViewSystem V G)
89     (m : GaugeMatching (G := G) U) (B : Set V)
90     (hcover : ViewSystem.ObjectCover U) (hbased : BasedOn m B) : F.basedGauge B :=
91   ⟨m.assemble hcover, by
92     intro a
93     obtain ⟨i, ha⟩ := hcover a.val
94     rw [m.assemble_local hcover i a.val ha]
95     exact hbased i a.val ha a.property⟩
96 
97 @[simp] theorem assembleBased_val (F : GroupViewSystem V G)
98     (m : GaugeMatching (G := G) U) (B : Set V)
99     (hcover : ViewSystem.ObjectCover U) (hbased : BasedOn m B) (a : V) :
100     (assembleBased F m B hcover hbased).val a = m.assemble hcover a := rfl
101 
102 /-- Descent data for a framed gauge morphism between two already-global cocycles. -/
103 structure FramedDescent (F : GroupViewSystem V G) (U : I → Set V)
104     (B : Set V) (c d : F.GaugeObject B) where
105   matching : GaugeMatching (G := G) U
106   relates : Relates F matching c.labels d.labels
107   based : BasedOn matching B
108 
109 namespace FramedDescent
110 variable {F : GroupViewSystem V G} {U : I → Set V}
111 
112 /-- Glue compatible local framed gauges to an actual morphism of gauge objects. -/
113 noncomputable def glueHom {B : Set V} {c d : F.GaugeObject B}
114     (D : FramedDescent F U B c d) (hcover : ViewSystem.TransitionCover U) : c ⟶ d :=
115   ⟨assembleBased F D.matching B (ViewSystem.TransitionCover.objectCover U hcover) D.based,
116     assemble_relates F D.matching c.labels d.labels hcover D.relates⟩
117 
118 @[simp] theorem glueHom_change_value {B : Set V} {c d : F.GaugeObject B}
119     (D : FramedDescent F U B c d) (hcover : ViewSystem.TransitionCover U)
120     (a : V) :
121     (D.glueHom hcover).change.val a = D.matching.assemble (ViewSystem.TransitionCover.objectCover U hcover) a := rfl
122 
123 /-- The glued morphism restricts to every specified local gauge value. -/
124 theorem glueHom_local {B : Set V} {c d : F.GaugeObject B}
125     (D : FramedDescent F U B c d) (hcover : ViewSystem.TransitionCover U)
126     (i : I) (a : V) (ha : a ∈ U i) :
127     (D.glueHom hcover).change.val a = D.matching.value i ⟨a, ha⟩ := by
128   rw [glueHom_change_value]
129   exact D.matching.assemble_local (ViewSystem.TransitionCover.objectCover U hcover) i a ha
130 
131 /-- A global framed gauge morphism agreeing with all local gauges is unique. -/
132 theorem glueHom_unique {B : Set V} {c d : F.GaugeObject B}
133     (D : FramedDescent F U B c d) (hcover : ViewSystem.TransitionCover U)
134     (a : c ⟶ d)
135     (ha : ∀ i (x : U i), a.change.val x.val = D.matching.value i x) :
136     a = D.glueHom hcover := by
137   apply GaugeObject.Hom.ext
138   apply Subtype.ext
139   funext x
140   obtain ⟨i, hx⟩ := (ViewSystem.TransitionCover.objectCover U hcover) x
141   calc
142     a.change.val x = D.matching.value i ⟨x, hx⟩ := ha i ⟨x, hx⟩
143     _ = (D.glueHom hcover).change.val x := (D.glueHom_local hcover i x hx).symm
144 
145 /-- Existence and uniqueness of a global morphism realizing a fixed matching family. -/
146 theorem exists_unique_glued_hom {B : Set V} {c d : F.GaugeObject B}
147     (D : FramedDescent F U B c d) (hcover : ViewSystem.TransitionCover U) :
148     ∃! a : c ⟶ d, ∀ i (x : U i), a.change.val x.val = D.matching.value i x := by
149   refine ⟨D.glueHom hcover, ?_, ?_⟩
150   · intro i x
151     exact D.glueHom_local hcover i x.val x.property
152   · intro a ha
153     exact D.glueHom_unique hcover a ha
154 
155 end FramedDescent
156 end GaugeMatching
157 end GroupViewSystem
158 end KomorebiSpace

Back to source controls