PatchViewEquivalence.lean

1 import KomorebiSpace.ViewSiteTransport
2 import KomorebiSpace.PatchViewSystem
3 
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 
7 /-!
8 # Equivalent presentations of isomorphism-closed view patches
9 
10 The equivalences use actual full subcategories and commute with restriction.
11 No equivalence of the posets of all raw subsets is asserted.
12 -/
13 universe u₁ u₂ v₁ v₂ w
14 namespace KomorebiSpace
15 open CategoryTheory
16 namespace ViewChange
17 variable {V : Type u₁} [Category.{v₁} V]
18 variable {W : Type u₂} [Category.{v₂} W]
19 
20 /-- Restrict a view functor to the inverse image of a full patch. -/
21 def patchFunctor (H : V ⥤ W) (S : Set W) :
22     PatchViews (H.obj ⁻¹' S) ⥤ PatchViews S where
23   obj x := ⟨H.obj x.val, x.property⟩
24   map f := InducedCategory.homMk (H.map f.hom)
25   map_id := by intro x; apply InducedCategory.hom_ext; exact H.map_id x.val
26   map_comp := by intro x y z f g; apply InducedCategory.hom_ext; exact H.map_comp f.hom g.hom
27 
28 /-- Isomorphism closure makes the inverse representative lie in the source patch. -/
29 def patchInverse (e : V ≌ W) (S : Set W) (hS : CompositionSite.IsoClosed S) :
30     PatchViews S ⥤ PatchViews (e.functor.obj ⁻¹' S) where
31   obj x := ⟨e.inverse.obj x.val, hS (e.counitIso.app x.val).symm x.property⟩
32   map f := InducedCategory.homMk (e.inverse.map f.hom)
33   map_id := by intro x; apply InducedCategory.hom_ext; exact e.inverse.map_id x.val
34   map_comp := by intro x y z f g; apply InducedCategory.hom_ext; exact e.inverse.map_comp f.hom g.hom
35 
36 /-- Unit on the actual full subcategory. -/
37 def patchUnit (e : V ≌ W) (S : Set W) (hS : CompositionSite.IsoClosed S) :
38     𝟭 (PatchViews (e.functor.obj ⁻¹' S)) ≅
39       patchFunctor e.functor S ⋙ patchInverse e S hS :=
40   NatIso.ofComponents (fun x =>
41     { hom := InducedCategory.homMk (e.unitIso.hom.app x.val)
42       inv := InducedCategory.homMk (e.unitIso.inv.app x.val)
43       hom_inv_id := by apply InducedCategory.hom_ext; exact (e.unitIso.app x.val).hom_inv_id
44       inv_hom_id := by apply InducedCategory.hom_ext; exact (e.unitIso.app x.val).inv_hom_id })
45     (by intro x y f; apply InducedCategory.hom_ext; exact e.unitIso.hom.naturality f.hom)
46 
47 /-- Counit on the actual full subcategory. -/
48 def patchCounit (e : V ≌ W) (S : Set W) (hS : CompositionSite.IsoClosed S) :
49     patchInverse e S hS ⋙ patchFunctor e.functor S ≅ 𝟭 (PatchViews S) :=
50   NatIso.ofComponents (fun x =>
51     { hom := InducedCategory.homMk (e.counitIso.hom.app x.val)
52       inv := InducedCategory.homMk (e.counitIso.inv.app x.val)
53       hom_inv_id := by apply InducedCategory.hom_ext; exact (e.counitIso.app x.val).hom_inv_id
54       inv_hom_id := by apply InducedCategory.hom_ext; exact (e.counitIso.app x.val).inv_hom_id })
55     (by intro x y f; apply InducedCategory.hom_ext; exact e.counitIso.hom.naturality f.hom)
56 
57 /-- Restriction of an equivalence to an isomorphism-closed patch. -/
58 def patchEquivalence (e : V ≌ W) (S : Set W) (hS : CompositionSite.IsoClosed S) :
59     PatchViews (e.functor.obj ⁻¹' S) ≌ PatchViews S :=
60   CategoryTheory.Equivalence.mk (patchFunctor e.functor S) (patchInverse e S hS)
61     (patchUnit e S hS) (patchCounit e S hS)
62 
63 @[simp] theorem patchEquivalence_functor (e : V ≌ W) (S : Set W)
64     (hS : CompositionSite.IsoClosed S) :
65     (patchEquivalence e S hS).functor = patchFunctor e.functor S := rfl
66 
67 end ViewChange
68 
69 namespace GroupViewSystem
70 variable {V : Type u₁} [Category.{v₁} V]
71 variable {W : Type u₂} [Category.{v₂} W]
72 variable {G : W → Type w} [∀ a, Group (G a)]
73 variable (F : GroupViewSystem W G)
74 
75 /-- The group coefficients in patch pullback are definitionally the actual restrictions. -/
76 def patchPullback (H : V ⥤ W) (S : Set W) :
77     (F.onPatch S).GaugeObject ∅ ⥤ ((F.reindex H).onPatch (H.obj ⁻¹' S)).GaugeObject ∅ :=
78   (F.onPatch S).reindexFunctor (ViewChange.patchFunctor H S)
79 
80 /-- The forward patch comparisons commute strictly with subpatch restriction. -/
81 @[simp] theorem patchPullback_restrict (H : V ⥤ W) {S T : Set W} (h : S ⊆ T) :
82     F.patchRestrict h ⋙ F.patchPullback H S =
83       F.patchPullback H T ⋙ (F.reindex H).patchRestrict (Set.preimage_mono h) := rfl
84 
85 /-- Existing stack values agree on corresponding isomorphism-closed patches. -/
86 def saturatedPatchCocycleEquivalence (e : V ≌ W) (S : Set W)
87     (hS : CompositionSite.IsoClosed S) :
88     (F.onPatch S).GaugeObject ∅ ≌
89       ((F.reindex e.functor).onPatch (e.functor.obj ⁻¹' S)).GaugeObject ∅ :=
90   (F.onPatch S).reindexEquivalence (ViewChange.patchEquivalence e S hS)
91 
92 @[simp] theorem saturatedPatchCocycleEquivalence_functor (e : V ≌ W) (S : Set W)
93     (hS : CompositionSite.IsoClosed S) :
94     (F.saturatedPatchCocycleEquivalence e S hS).functor = F.patchPullback e.functor S := rfl
95 
96 end GroupViewSystem
97 end KomorebiSpace

Back to source controls