PatchViewSystem.lean

1 import KomorebiSpace.CocycleGaugeGroupoid
2 import Mathlib.CategoryTheory.InducedCategory
3 import Mathlib.CategoryTheory.Category.Cat
4 import Mathlib.CategoryTheory.Category.Preorder
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Restriction of the existing cocycle groupoids to full view patches
10 
11 The patch assignment is an actual contravariant functor to Cat. All fibers
12 are the previously defined unframed gauge groupoids, with unchanged
13 coefficient groups and maps. This is not an arbitrary category-valued system.
14 -/
15 universe u v w
16 namespace KomorebiSpace
17 open CategoryTheory Opposite
18 
19 /-- Full view patches retain every original arrow between their objects. -/
20 abbrev PatchViews {V : Type u} [Category.{v} V] (W : Set V) :=
21   InducedCategory V (fun x : W => x.val)
22 
23 namespace GroupViewSystem
24 variable {V : Type u} [Category.{v} V]
25 variable {G : V → Type w} [∀ a, Group (G a)]
26 variable (F : GroupViewSystem V G)
27 
28 /-- Restrict the actual coefficient system, without altering the groups or transports. -/
29 def onPatch (W : Set V) : GroupViewSystem (PatchViews W) (fun x => G x.val) where
30   pull := fun f => F.pull f.hom
31   pull_id := fun x g => F.pull_id x.val g
32   pull_comp := fun f g x => F.pull_comp f.hom g.hom x
33 
34 /-- Restriction of a coherent cocycle to a smaller full patch. -/
35 def patchCocycleRestrict {U W : Set V} (h : U ⊆ W)
36     (c : (F.onPatch W).Cocycle) : (F.onPatch U).Cocycle where
37   edge := fun {a b} f =>
38     c.edge (a := ⟨a.val, h a.property⟩) (b := ⟨b.val, h b.property⟩)
39       (InducedCategory.homMk f.hom)
40   edge_id := fun a => c.edge_id ⟨a.val, h a.property⟩
41   edge_comp := by
42     intro a b e f g
43     exact c.edge_comp (a := ⟨a.val, h a.property⟩)
44       (b := ⟨b.val, h b.property⟩) (c := ⟨e.val, h e.property⟩)
45       (InducedCategory.homMk f.hom) (InducedCategory.homMk g.hom)
46 
47 /-- The actual restriction functor on the existing unframed gauge groupoids. -/
48 def patchRestrict {U W : Set V} (h : U ⊆ W) :
49     (F.onPatch W).GaugeObject ∅ ⥤ (F.onPatch U).GaugeObject ∅ where
50   obj c := ⟨F.patchCocycleRestrict h c.labels⟩
51   map a :=
52     { change := ⟨fun x => a.change.val ⟨x.val, h x.property⟩, by
53         intro x; exact False.elim x.property⟩
54       target := by
55         apply Cocycle.ext
56         intro x y f
57         have he := congrArg (fun c => c.edge
58           (a := ⟨x.val, h x.property⟩) (b := ⟨y.val, h y.property⟩)
59           (InducedCategory.homMk f.hom)) a.target
60         exact he }
61   map_id := by intro c; rfl
62   map_comp := by intro c d e a b; rfl
63 
64 @[simp] theorem patchRestrict_identity (W : Set V) :
65     F.patchRestrict (Set.Subset.refl W) = 𝟭 ((F.onPatch W).GaugeObject ∅) := rfl
66 
67 @[simp] theorem patchRestrict_comp {U W Z : Set V} (h : U ⊆ W) (k : W ⊆ Z) :
68     F.patchRestrict k ⋙ F.patchRestrict h = F.patchRestrict (h.trans k) := rfl
69 
70 /-- A strict category-valued presheaf on the patch poset. Each value is a groupoid. -/
71 def patchDiagram : (Set V)ᵒᵖ ⥤ Cat where
72   obj W := Cat.of ((F.onPatch (unop W)).GaugeObject ∅)
73   map h := (F.patchRestrict (leOfHom h.unop)).toCatHom
74   map_id := by intro W; apply Cat.ext; rfl
75   map_comp := by intro U W Z f g; apply Cat.ext; rfl
76 
77 @[simp] theorem patchRestrict_edge {U W : Set V} (h : U ⊆ W)
78     (c : (F.onPatch W).GaugeObject ∅) {a b : PatchViews U} (f : a ⟶ b) :
79     ((F.patchRestrict h).obj c).labels.edge f =
80       c.labels.edge (a := ⟨a.val, h a.property⟩) (b := ⟨b.val, h b.property⟩)
81         (InducedCategory.homMk f.hom) := rfl
82 
83 @[simp] theorem patchRestrict_gauge {U W : Set V} (h : U ⊆ W)
84     {c d : (F.onPatch W).GaugeObject ∅} (a : c ⟶ d) (x : PatchViews U) :
85     ((F.patchRestrict h).map a).change.val x =
86       a.change.val ⟨x.val, h x.property⟩ := rfl
87 
88 @[simp] theorem gauge_identity_value (B : Set V) (c : F.GaugeObject B) (x : V) :
89     (𝟙 c : c ⟶ c).change.val x = 1 := rfl
90 
91 @[simp] theorem gauge_composition_value {B : Set V} {c d e : F.GaugeObject B}
92     (a : c ⟶ d) (b : d ⟶ e) (x : V) :
93     (a ≫ b).change.val x = b.change.val x * a.change.val x := rfl
94 
95 @[simp] theorem gauge_inverse_value {B : Set V} {c d : F.GaugeObject B}
96     (a : c ⟶ d) (x : V) :
97     (Groupoid.inv a).change.val x = (a.change.val x)⁻¹ := rfl
98 
99 end GroupViewSystem
100 end KomorebiSpace

Back to source controls