ViewEquivalence.lean

1 import KomorebiSpace.ViewPullback
2 
3 set_option autoImplicit false
4 set_option backward.isDefEq.respectTransparency false
5 
6 /-!
7 # Invariance of the cocycle groupoid under equivalence of view categories
8 
9 The forward functor is actual pullback. The inverse transports coefficients
10 along the inverse counit; no coefficient groups are identified by fiat.
11 -/
12 universe u₁ u₂ v₁ v₂ w
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace GroupViewSystem
16 variable {V : Type u₁} [Category.{v₁} V]
17 variable {W : Type u₂} [Category.{v₂} W]
18 variable {G : W → Type w} [∀ a, Group (G a)]
19 variable (F : GroupViewSystem W G) (e : V ≌ W)
20 
21 /-- The inverse counit supplies the comparison arrow with explicit endpoints. -/
22 abbrev returnArrow (a : W) : a ⟶ e.functor.obj (e.inverse.obj a) :=
23   e.counitIso.inv.app a
24 
25 /-- Naturality, with coefficient transport written out. -/
26 theorem return_pull_natural {a b : W} (f : a ⟶ b)
27     (x : G (e.functor.obj (e.inverse.obj b))) :
28     F.pull (returnArrow e a) (F.pull (e.functor.map (e.inverse.map f)) x) =
29       F.pull f (F.pull (returnArrow e b) x) := by
30   rw [← F.pull_comp, ← F.pull_comp]
31   exact congrArg (fun k => F.pull k x) (e.counitIso.inv.naturality f).symm
32 
33 /-- Extend a pulled-back cocycle using the supplied categorical equivalence. -/
34 def returnCocycle (c : (F.reindex e.functor).Cocycle) : F.Cocycle where
35   edge := fun {a b} f => F.pull (returnArrow e a) (c.edge (e.inverse.map f))
36   edge_id := by intro a; rw [e.inverse.map_id, c.edge_id, map_one]
37   edge_comp := by
38     intro a b z f g
39     rw [e.inverse.map_comp, c.edge_comp, map_mul]
40     congr 1
41     exact F.return_pull_natural e f (c.edge (e.inverse.map g))
42 
43 @[simp] theorem returnCocycle_edge (c : (F.reindex e.functor).Cocycle)
44     {a b : W} (f : a ⟶ b) :
45     (F.returnCocycle e c).edge f =
46       F.pull (returnArrow e a) (c.edge (e.inverse.map f)) := rfl
47 
48 /-- The inverse also transports gauge witnesses, not just cocycle classes. -/
49 def returnFunctor : (F.reindex e.functor).GaugeObject ∅ ⥤ F.GaugeObject ∅ where
50   obj c := ⟨F.returnCocycle e c.labels⟩
51   map := fun {c d} a =>
52     { change := ⟨fun v => F.pull (returnArrow e v) (a.change.val (e.inverse.obj v)), by
53         intro v; exact False.elim v.property⟩
54       target := by
55         apply Cocycle.ext
56         intro v w f
57         have h := congrArg (fun c => c.edge (e.inverse.map f)) a.target
58         change a.change.val (e.inverse.obj v) * c.labels.edge (e.inverse.map f) *
59           (F.pull (e.functor.map (e.inverse.map f)) (a.change.val (e.inverse.obj w)))⁻¹ =
60             d.labels.edge (e.inverse.map f) at h
61         change F.pull (returnArrow e v) (a.change.val (e.inverse.obj v)) *
62           F.pull (returnArrow e v) (c.labels.edge (e.inverse.map f)) *
63           (F.pull f (F.pull (returnArrow e w) (a.change.val (e.inverse.obj w))))⁻¹ = _
64         rw [← F.return_pull_natural e f]
65         rw [← map_inv, ← map_mul, ← map_mul, h]
66         rfl }
67   map_id := by
68     intro c
69     apply GaugeObject.Hom.ext
70     apply Subtype.ext
71     funext v
72     exact map_one _
73   map_comp := by
74     intro c d k a b
75     apply GaugeObject.Hom.ext
76     apply Subtype.ext
77     funext v
78     exact map_mul _ _ _
79 
80 /-- Comparison of the global round trip to the original cocycle. -/
81 def globalComparison (c : F.GaugeObject ∅) :
82     ((F.reindexFunctor e.functor) ⋙ F.returnFunctor e).obj c ⟶ c where
83   change := ⟨fun v => c.labels.edge (returnArrow e v), by
84     intro v; exact False.elim v.property⟩
85   target := by
86     apply Cocycle.ext
87     intro a b f
88     exact F.natural_comparison (e.inverse ⋙ e.functor) (returnArrow e)
89       (fun g => (e.counitIso.inv.naturality g).symm) c.labels f
90 
91 /-- The global comparison is natural on all gauge arrows. -/
92 def globalComparisonIso :
93     (F.reindexFunctor e.functor) ⋙ F.returnFunctor e ≅ 𝟭 (F.GaugeObject ∅) :=
94   NatIso.ofComponents
95     (fun c => (Groupoid.isoEquivHom _ _).symm (F.globalComparison e c)) (by
96       intro c d a
97       apply GaugeObject.Hom.ext
98       apply Subtype.ext
99       funext v
100       exact F.gauge_comparison_naturality a (returnArrow e v))
101 
102 /-- The triangle law identifies the two actual arrows used in the other round trip. -/
103 theorem mapped_unit_eq_return (v : V) :
104     e.functor.map (e.unitIso.hom.app v) = returnArrow e (e.functor.obj v) := by
105   exact (e.counitInv_app_functor v).symm
106 
107 /-- Comparison of the pulled-back round trip to the starting pulled-back cocycle. -/
108 def localComparison (c : (F.reindex e.functor).GaugeObject ∅) :
109     (F.returnFunctor e ⋙ F.reindexFunctor e.functor).obj c ⟶ c where
110   change := ⟨fun v => c.labels.edge (a := v) (e.unitIso.hom.app v), by
111     intro v; exact False.elim v.property⟩
112   target := by
113     apply Cocycle.ext
114     intro a b f
115     change c.labels.edge (a := a) (e.unitIso.hom.app a) *
116       F.pull (returnArrow e (e.functor.obj a)) (c.labels.edge (e.inverse.map (e.functor.map f))) *
117       (F.pull (e.functor.map f) (c.labels.edge (a := b) (e.unitIso.hom.app b)))⁻¹ = c.labels.edge f
118     rw [← mapped_unit_eq_return e a]
119     exact (F.reindex e.functor).natural_comparison (e.functor ⋙ e.inverse)
120       (fun v => e.unitIso.hom.app v)
121       (fun g => (e.unitIso.hom.naturality g).symm) c.labels f
122 
123 /-- The local comparison is likewise natural on all arrows. -/
124 def localComparisonIso :
125     F.returnFunctor e ⋙ F.reindexFunctor e.functor ≅
126       𝟭 ((F.reindex e.functor).GaugeObject ∅) :=
127   NatIso.ofComponents
128     (fun c => (Groupoid.isoEquivHom _ _).symm (F.localComparison e c)) (by
129       intro c d a
130       apply GaugeObject.Hom.ext
131       apply Subtype.ext
132       funext v
133       change d.labels.edge (a := v) (e.unitIso.hom.app v) *
134         F.pull (returnArrow e (e.functor.obj v)) (a.change.val (e.inverse.obj (e.functor.obj v))) =
135         a.change.val v * c.labels.edge (a := v) (e.unitIso.hom.app v)
136       rw [← mapped_unit_eq_return e v]
137       exact (F.reindex e.functor).gauge_comparison_naturality a (e.unitIso.hom.app v))
138 
139 /-- Actual pullback is an equivalence of the existing cocycle gauge groupoids. -/
140 def reindexEquivalence :
141     F.GaugeObject ∅ ≌ (F.reindex e.functor).GaugeObject ∅ :=
142   CategoryTheory.Equivalence.mk (F.reindexFunctor e.functor) (F.returnFunctor e)
143     (F.globalComparisonIso e).symm (F.localComparisonIso e)
144 
145 @[simp] theorem reindexEquivalence_functor :
146     (F.reindexEquivalence e).functor = F.reindexFunctor e.functor := rfl
147 
148 /-- Standard equivalence predicate for the concrete pullback functor. -/
149 theorem reindex_isEquivalence : (F.reindexFunctor e.functor).IsEquivalence := by
150   change (F.reindexEquivalence e).functor.IsEquivalence
151   infer_instance
152 
153 /-- Every Hom set, in particular every automorphism set, is retained. -/
154 def reindexHomEquiv (c d : F.GaugeObject ∅) :
155     (c ⟶ d) ≃ ((F.reindexFunctor e.functor).obj c ⟶
156       (F.reindexFunctor e.functor).obj d) :=
157   (F.reindexEquivalence e).fullyFaithfulFunctor.homEquiv
158 
159 /-- The equivalence uses the actual pullback of gauge witnesses. -/
160 @[simp] theorem reindexHomEquiv_apply (c d : F.GaugeObject ∅) (a : c ⟶ d) :
161     F.reindexHomEquiv e c d a = (F.reindexFunctor e.functor).map a := rfl
162 
163 /-- Isomorphism-class equality is both preserved and reflected. -/
164 theorem reindex_class_eq_iff (c d : F.Cocycle) :
165     (F.reindex e.functor).orbitClass ∅ (F.reindexCocycle e.functor c) =
166       (F.reindex e.functor).orbitClass ∅ (F.reindexCocycle e.functor d) ↔
167     F.orbitClass ∅ c = F.orbitClass ∅ d := by
168   change (F.reindex e.functor).orbitClass ∅ ((F.reindexFunctor e.functor).obj ⟨c⟩).labels =
169       (F.reindex e.functor).orbitClass ∅ ((F.reindexFunctor e.functor).obj ⟨d⟩).labels ↔ _
170   rw [← (F.reindex e.functor).morphism_nonempty_iff_class,
171       ← F.morphism_nonempty_iff_class ∅ (⟨c⟩ : F.GaugeObject ∅) (⟨d⟩ : F.GaugeObject ∅)]
172   exact (F.reindexHomEquiv e ⟨c⟩ ⟨d⟩).nonempty_congr.symm
173 
174 /-- Changing to an equivalent view category does not erase an unframed obstruction. -/
175 theorem reindex_neutral_iff (c : F.Cocycle) :
176     (F.reindex e.functor).orbitClass ∅ (F.reindexCocycle e.functor c) =
177       (F.reindex e.functor).neutralClass ∅ ↔
178     F.orbitClass ∅ c = F.neutralClass ∅ :=
179   F.reindex_class_eq_iff e c F.trivial
180 
181 end GroupViewSystem
182 end KomorebiSpace

Back to source controls