ViewPullback.lean

1 import KomorebiSpace.CocycleGaugeGroupoid
2 import Mathlib.CategoryTheory.Equivalence
3 
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 
7 /-!
8 # Pullback along a functor of view categories
9 
10 The coefficient groups are pulled back, not silently identified. The induced
11 functor uses the original cocycles and unframed gauge groupoids.
12 -/
13 universe u₁ u₂ v₁ v₂ w
14 namespace KomorebiSpace
15 open CategoryTheory
16 namespace GroupViewSystem
17 variable {V : Type u₁} [Category.{v₁} V]
18 variable {W : Type u₂} [Category.{v₂} W]
19 variable {G : W → Type w} [∀ a, Group (G a)]
20 
21 /-- Pull back the specified group coefficients along an actual view functor. -/
22 def reindex (F : GroupViewSystem W G) (H : V ⥤ W) :
23     GroupViewSystem V (fun a => G (H.obj a)) where
24   pull := fun f => F.pull (H.map f)
25   pull_id := by intro a x; rw [H.map_id, F.pull_id]
26   pull_comp := by intro a b c f g x; rw [H.map_comp, F.pull_comp]
27 
28 /-- Pullback retains the labels on the image arrows. -/
29 def reindexCocycle (F : GroupViewSystem W G) (H : V ⥤ W) (c : F.Cocycle) :
30     (F.reindex H).Cocycle where
31   edge := fun f => c.edge (H.map f)
32   edge_id := by intro a; rw [H.map_id, c.edge_id]
33   edge_comp := by intro a b d f g; rw [H.map_comp, c.edge_comp]; rfl
34 
35 @[simp] theorem reindexCocycle_edge (F : GroupViewSystem W G) (H : V ⥤ W)
36     (c : F.Cocycle) {a b : V} (f : a ⟶ b) :
37     (F.reindexCocycle H c).edge f = c.edge (H.map f) := rfl
38 
39 /-- The pullback is a functor on the actual symmetry-retaining groupoids. -/
40 def reindexFunctor (F : GroupViewSystem W G) (H : V ⥤ W) :
41     F.GaugeObject ∅ ⥤ (F.reindex H).GaugeObject ∅ where
42   obj c := ⟨F.reindexCocycle H c.labels⟩
43   map a :=
44     { change := ⟨fun v => a.change.val (H.obj v), by
45         intro v; exact False.elim v.property⟩
46       target := by
47         apply Cocycle.ext
48         intro v w f
49         exact congrArg (fun c => c.edge (H.map f)) a.target }
50   map_id := by intro c; rfl
51   map_comp := by intro c d e a b; rfl
52 
53 @[simp] theorem reindexFunctor_gauge (F : GroupViewSystem W G) (H : V ⥤ W)
54     {c d : F.GaugeObject ∅} (a : c ⟶ d) (v : V) :
55     ((F.reindexFunctor H).map a).change.val v = a.change.val (H.obj v) := rfl
56 
57 @[simp] theorem reindex_trivial (F : GroupViewSystem W G) (H : V ⥤ W) :
58     F.reindexCocycle H F.trivial = (F.reindex H).trivial := rfl
59 
60 /-- Cocycle compatibility along a natural transformation supplies a gauge comparison.
61 No invertibility of the transformation's components is needed for this identity. -/
62 theorem natural_comparison (F : GroupViewSystem W G) (T : W ⥤ W)
63     (σ : ∀ a, a ⟶ T.obj a)
64     (hn : ∀ {a b} (f : a ⟶ b), σ a ≫ T.map f = f ≫ σ b)
65     (c : F.Cocycle) {a b : W} (f : a ⟶ b) :
66     c.edge (σ a) * F.pull (σ a) (c.edge (T.map f)) *
67       (F.pull f (c.edge (σ b)))⁻¹ = c.edge f := by
68   have h := congrArg (fun k => c.edge k) (hn f)
69   simp only [c.edge_comp] at h
70   rw [h]
71   group
72 
73 /-- A gauge equation on an arrow is the naturality equation for its comparison. -/
74 theorem gauge_comparison_naturality (F : GroupViewSystem W G)
75     {c d : F.GaugeObject ∅} (a : c ⟶ d) {v w : W} (f : v ⟶ w) :
76     d.labels.edge f * F.pull f (a.change.val w) =
77       a.change.val v * c.labels.edge f := by
78   have h := congrArg (fun k => k.edge f) a.target
79   change a.change.val v * c.labels.edge f * (F.pull f (a.change.val w))⁻¹ =
80     d.labels.edge f at h
81   rw [← h]
82   group
83 
84 end GroupViewSystem
85 end KomorebiSpace

Back to source controls