ViewDuplication.lean

1 import KomorebiSpace.PatchViewEquivalence
2 import KomorebiSpace.SectionViewEquivalence
3 
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 
7 /-!
8 # Redundant views and the failure of raw-patch invariance
9 
10 Duplicating every view is a categorical equivalence, not an object bijection.
11 Its skeleton can miss a nonempty, nonsaturated patch. For nontrivial group
12 coefficients the resulting patch pullback is not even faithful on gauges.
13 -/
14 universe u v w
15 namespace KomorebiSpace
16 open CategoryTheory
17 namespace ViewDuplication
18 variable (V : Type u) [Category.{v} V]
19 
20 /-- Two labelled, isomorphic copies of each view. -/
21 abbrev Duplicated := InducedCategory V (fun x : V × Bool => x.1)
22 
23 /-- Keep only copy false when choosing a representative. -/
24 def embed : V ⥤ Duplicated V where
25   obj x := (x, false)
26   map f := InducedCategory.homMk f
27   map_id := by intros; rfl
28   map_comp := by intros; rfl
29 
30 /-- Forget the redundant copy label, retaining all original arrows. -/
31 def forget : Duplicated V ⥤ V where
32   obj x := x.1
33   map f := f.hom
34   map_id := by intros; rfl
35   map_comp := by intros; rfl
36 
37 /-- The two copies are related by the original identity morphism. -/
38 def copyIso (x : V) (a b : Bool) : Iso (C := Duplicated V) (x,a) (x,b) where
39   hom := InducedCategory.homMk (𝟙 x)
40   inv := InducedCategory.homMk (𝟙 x)
41   hom_inv_id := by apply InducedCategory.hom_ext; simp
42   inv_hom_id := by apply InducedCategory.hom_ext; simp
43 
44 def counit : forget V ⋙ embed V ≅ 𝟭 (Duplicated V) :=
45   NatIso.ofComponents (fun x => copyIso V x.1 false x.2) (by
46     intro x y f
47     apply InducedCategory.hom_ext
48     change f.hom ≫ 𝟙 y.1 = 𝟙 x.1 ≫ f.hom
49     simp)
50 
51 /-- A genuine equivalence although the forward map is not onto on objects. -/
52 def equivalence : V ≌ Duplicated V :=
53   CategoryTheory.Equivalence.mk (embed V) (forget V) (Iso.refl (𝟭 V)) (counit V)
54 
55 theorem embed_not_surjective (x : V) : ¬ Function.Surjective (embed V).obj := by
56   intro h
57   obtain ⟨y,hy⟩ := h (x,true)
58   have hb := congrArg (fun p : Duplicated V => p.2) hy
59   change false = true at hb
60   cases hb
61 
62 /-- A raw patch can select only representatives omitted by the equivalence functor. -/
63 def missedPatch : Set (Duplicated V) := {x | x.2 = true}
64 
65 @[simp] theorem missedPatch_preimage : (embed V).obj ⁻¹' missedPatch V = ∅ := by
66   ext x
67   change (false = true) ↔ False
68   simp
69 
70 omit [Category.{v} V] in
71 theorem missedPatch_nonempty (x : V) : (missedPatch V).Nonempty :=
72   ⟨(x,true), rfl⟩
73 
74 theorem missedPatch_not_isoClosed (x : V) :
75     ¬ CompositionSite.IsoClosed (missedPatch V) := by
76   intro h
77   have hb := h (copyIso V x true false) (show (x,true) ∈ missedPatch V from rfl)
78   change false = true at hb
79   cases hb
80 
81 /-- Constant coefficients for the gauge-level failure witness. -/
82 def constantGroups (H : Type w) [Group H] :
83     GroupViewSystem (Duplicated V) (fun _ => H) where
84   pull := fun _ => MonoidHom.id H
85   pull_id := by intros; rfl
86   pull_comp := by intros; rfl
87 
88 def localObject (H : Type w) [Group H] :
89     ((constantGroups V H).onPatch (missedPatch V)).GaugeObject ∅ :=
90   ⟨((constantGroups V H).onPatch (missedPatch V)).trivial⟩
91 
92 /-- Constant group elements are genuine automorphisms of the trivial local cocycle. -/
93 def localGauge {H : Type w} [Group H] (a : H) :
94     localObject V H ⟶ localObject V H where
95   change := ⟨fun _ => a, by intro x; exact False.elim x.property⟩
96   target := by
97     apply GroupViewSystem.Cocycle.ext
98     intro x y f
99     change a * 1 * a⁻¹ = 1
100     group
101 
102 /-- Restricting to the missed inverse-image patch erases all these automorphisms. -/
103 theorem localGauge_images {H : Type w} [Group H] (a b : H) :
104     ((constantGroups V H).patchPullback (embed V) (missedPatch V)).map (localGauge V a) =
105       ((constantGroups V H).patchPullback (embed V) (missedPatch V)).map (localGauge V b) := by
106   apply GroupViewSystem.GaugeObject.Hom.ext
107   apply Subtype.ext
108   funext x
109   have hb := x.property
110   change false = true at hb
111   cases hb
112 
113 /-- On the original nonempty patch, different group elements are different gauge arrows. -/
114 theorem localGauge_ne {H : Type w} [Group H] (x : V) {a b : H} (hab : a ≠ b) :
115     localGauge V a ≠ localGauge V b := by
116   intro h
117   have he := congrArg (fun k : localObject V H ⟶ localObject V H =>
118     k.change.val ⟨(x,true),rfl⟩) h
119   exact hab he
120 
121 /-- Even an equivalence of view categories does not preserve arbitrary raw patch gauges. -/
122 theorem raw_patch_pullback_not_faithful {H : Type w} [Group H]
123     (x : V) (a : H) (ha : a ≠ 1) :
124     ¬ ((constantGroups V H).patchPullback (embed V) (missedPatch V)).Faithful := by
125   intro hf
126   let : ((constantGroups V H).patchPullback (embed V) (missedPatch V)).Faithful := hf
127   have h := ((constantGroups V H).patchPullback (embed V) (missedPatch V)).map_injective
128     (localGauge_images V a 1)
129   exact localGauge_ne V x ha h
130 
131 /-- Nevertheless, the entire cocycle groupoid is invariant under this duplication. -/
132 def cocycleEquivalence {G : V → Type w} [∀ a, Group (G a)] (F : GroupViewSystem V G) :
133     (F.reindex (forget V)).GaugeObject ∅ ≌ F.GaugeObject ∅ :=
134   (F.reindex (forget V)).reindexEquivalence (equivalence V)
135 
136 /-- The original coherent section space is also recovered from duplicated appearances. -/
137 def sectionEquivalence (F : ViewSystem.{u,v,w} V) :
138     (F.reindex (forget V)).Ambient ≃ F.Ambient :=
139   (F.reindex (forget V)).viewEquivalence (equivalence V)
140 
141 end ViewDuplication
142 end KomorebiSpace

Back to source controls