RelativeCocycleRealization.lean

1 import KomorebiSpace.MarkedTransport
2 import KomorebiSpace.PatchViewEquivalence
3 
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 
7 /-!
8 # Presentation-independent relative cocycle realizations
9 
10 The boundary object belongs to the existing unframed patch groupoid. A global
11 realization includes an isomorphism from its actual restricted cocycle to that
12 boundary. The proved square of patch pullbacks supplies a concrete comparison
13 of these groupoids under equivalent views and saturated domains.
14 -/
15 universe u₁ u₂ v₁ v₂ w
16 namespace KomorebiSpace
17 open CategoryTheory
18 namespace GroupViewSystem
19 variable {V : Type u₁} [Category.{v₁} V]
20 variable {W : Type u₂} [Category.{v₂} W]
21 variable {G : W → Type w} [∀ a, Group (G a)]
22 variable (F : GroupViewSystem W G)
23 
24 /-- Actual relative reconstruction fiber, retaining the chosen boundary identification. -/
25 abbrev RelativeRealization {U T : Set W} (h : U ⊆ T)
26     (b : (F.onPatch U).GaugeObject ∅) := MarkedRealization (F.patchRestrict h) b
27 
28 /-- Restriction and actual view pullback form the square used in fiber transport. -/
29 def relativeSquare (H : V ⥤ W) {U T : Set W} (h : U ⊆ T) :
30     F.patchRestrict h ⋙ F.patchPullback H U ≅
31       F.patchPullback H T ⋙ (F.reindex H).patchRestrict (Set.preimage_mono h) :=
32   Iso.refl _
33 
34 /-- The direct functor keeps the actual pulled-back cocycle and boundary arrow. -/
35 def relativePullback (H : V ⥤ W) {U T : Set W} (h : U ⊆ T)
36     (b : (F.onPatch U).GaugeObject ∅) :
37     F.RelativeRealization h b ⥤
38       (F.reindex H).RelativeRealization (Set.preimage_mono h)
39         ((F.patchPullback H U).obj b) :=
40   MarkedRealization.transport (F.patchPullback H T) (F.patchPullback H U)
41     (F.relativeSquare H h) b
42 
43 @[simp] theorem relativePullback_object (H : V ⥤ W) {U T : Set W} (h : U ⊆ T)
44     (b : (F.onPatch U).GaugeObject ∅) (x : F.RelativeRealization h b) :
45     ((F.relativePullback H h b).obj x).obj = (F.patchPullback H T).obj x.obj := rfl
46 
47 @[simp] theorem relativePullback_identification (H : V ⥤ W) {U T : Set W} (h : U ⊆ T)
48     (b : (F.onPatch U).GaugeObject ∅) (x : F.RelativeRealization h b) :
49     ((F.relativePullback H h b).obj x).identify =
50       (F.patchPullback H U).map x.identify := by
51   change 𝟙 _ ≫ (F.patchPullback H U).map x.identify = _
52   exact Category.id_comp _
53 
54 /-- Both presentations of the same relative reconstruction problem are equivalent. -/
55 noncomputable def relativeCocycleEquivalence (e : V ≌ W) {U T : Set W}
56     (h : U ⊆ T) (hU : CompositionSite.IsoClosed U) (hT : CompositionSite.IsoClosed T)
57     (b : (F.onPatch U).GaugeObject ∅) :
58     F.RelativeRealization h b ≌
59       (F.reindex e.functor).RelativeRealization (Set.preimage_mono h)
60         ((F.patchPullback e.functor U).obj b) := by
61   letI : (F.patchPullback e.functor T).IsEquivalence := by
62     change (F.saturatedPatchCocycleEquivalence e T hT).functor.IsEquivalence
63     infer_instance
64   letI : (F.patchPullback e.functor U).IsEquivalence := by
65     change (F.saturatedPatchCocycleEquivalence e U hU).functor.IsEquivalence
66     infer_instance
67   exact MarkedRealization.transportEquivalence
68     (F.patchPullback e.functor T) (F.patchPullback e.functor U)
69     (F.relativeSquare e.functor h) b
70 
71 @[simp] theorem relativeCocycleEquivalence_functor (e : V ≌ W) {U T : Set W}
72     (h : U ⊆ T) (hU : CompositionSite.IsoClosed U) (hT : CompositionSite.IsoClosed T)
73     (b : (F.onPatch U).GaugeObject ∅) :
74     (F.relativeCocycleEquivalence e h hU hT b).functor =
75       F.relativePullback e.functor h b := rfl
76 
77 /-- Empty and nonempty relative realization groupoids are distinguished invariantly. -/
78 theorem relative_cocycle_nonempty_iff (e : V ≌ W) {U T : Set W}
79     (h : U ⊆ T) (hU : CompositionSite.IsoClosed U) (hT : CompositionSite.IsoClosed T)
80     (b : (F.onPatch U).GaugeObject ∅) :
81     Nonempty (F.RelativeRealization h b) ↔
82       Nonempty ((F.reindex e.functor).RelativeRealization (Set.preimage_mono h)
83         ((F.patchPullback e.functor U).obj b)) := by
84   let q := F.relativeCocycleEquivalence e h hU hT b
85   exact ⟨fun ⟨x⟩ => ⟨q.functor.obj x⟩, fun ⟨x⟩ => ⟨q.inverse.obj x⟩⟩
86 
87 /-- Boundary-preserving comparisons and automorphisms are transported, not quotiented away. -/
88 noncomputable def relativeCocycleHomEquiv (e : V ≌ W) {U T : Set W}
89     (h : U ⊆ T) (hU : CompositionSite.IsoClosed U) (hT : CompositionSite.IsoClosed T)
90     (b : (F.onPatch U).GaugeObject ∅) (x y : F.RelativeRealization h b) :
91     (x ⟶ y) ≃
92       ((F.relativePullback e.functor h b).obj x ⟶
93         (F.relativePullback e.functor h b).obj y) :=
94   (F.relativeCocycleEquivalence e h hU hT b).fullyFaithfulFunctor.homEquiv
95 
96 end GroupViewSystem
97 end KomorebiSpace

Back to source controls