FramingBoundaryExamples.lean

1 import KomorebiSpace.ViewDuplication
2 
3 set_option autoImplicit false
4 set_option backward.isDefEq.respectTransparency false
5 
6 /-!
7 # Literal full framing is not invariant under duplicated views
8 
9 This is a counterexample using the actual old based-gauge groupoid. Both
10 framing domains are the whole view category, hence saturated. Duplicating
11 isomorphic representatives introduces separate frozen trivializations. The
12 resulting pullback functor need not be full. Identified-boundary fibers do
13 not freeze these redundant choices independently.
14 -/
15 universe u₁ u₂ v₁ v₂ w
16 namespace KomorebiSpace
17 open CategoryTheory
18 namespace GroupViewSystem
19 variable {V : Type u₁} [Category.{v₁} V]
20 variable {W : Type u₂} [Category.{v₂} W]
21 variable {G : W → Type w} [∀ a, Group (G a)]
22 variable (F : GroupViewSystem W G)
23 
24 /-- Pullback exists for all framing domains, but is not always an equivalence. -/
25 def reindexFramedFunctor (H : V ⥤ W) (U : Set W) :
26     F.GaugeObject U ⥤ (F.reindex H).GaugeObject (H.obj ⁻¹' U) where
27   obj c := ⟨F.reindexCocycle H c.labels⟩
28   map a :=
29     { change := ⟨fun v => a.change.val (H.obj v),
30         fun v => a.change.property ⟨H.obj v.val,v.property⟩⟩
31       target := by
32         apply Cocycle.ext
33         intro v w f
34         exact congrArg (fun c => c.edge (H.map f)) a.target }
35   map_id := by intro c; rfl
36   map_comp := by intro c d k a b; rfl
37 
38 /-- Freezing every view forces every allowed gauge to be pointwise identity. -/
39 theorem fully_framed_gauge (a : F.basedGauge Set.univ) : a.val = 1 := by
40   funext v
41   exact a.property ⟨v,Set.mem_univ v⟩
42 
43 theorem fully_framed_equivalent_iff (c d : F.Cocycle) :
44     F.GaugeEquivalent Set.univ c d ↔ c = d := by
45   constructor
46   · rintro ⟨a,ha⟩
47     rw [F.fully_framed_gauge a, F.gauge_one] at ha
48     exact ha
49   · intro h
50     exact ⟨1, (F.gauge_one c).trans h⟩
51 
52 end GroupViewSystem
53 
54 namespace FramingBoundaryExamples
55 variable (V : Type u₁) [Category.{v₁} V]
56 variable {H : Type w} [Group H]
57 
58 /-- Give the redundant copy a different trivialization. -/
59 def copyFrame (g : H) : ViewDuplication.Duplicated V → H :=
60   fun x => if x.2 then g else 1
61 
62 def copyCocycle (g : H) : (ViewDuplication.constantGroups V H).Cocycle :=
63   (ViewDuplication.constantGroups V H).gauge (copyFrame V g)
64     (ViewDuplication.constantGroups V H).trivial
65 
66 /-- This is not a change in the gauge orbit, but it is a change of strict cocycle labels. -/
67 theorem copyCocycle_ne_trivial (v : V) (g : H) (hg : g ≠ 1) :
68     copyCocycle V g ≠ (ViewDuplication.constantGroups V H).trivial := by
69   intro h
70   have he := congrArg (fun c => c.edge (ViewDuplication.copyIso V v true false).hom) h
71   change g * 1 * (1 : H)⁻¹ = 1 at he
72   exact hg (by simpa using he)
73 
74 /-- Choosing the representative copy forgets those extra trivializations. -/
75 @[simp] theorem copyCocycle_pullback (g : H) :
76     (ViewDuplication.constantGroups V H).reindexCocycle (ViewDuplication.embed V)
77       (copyCocycle V g) =
78     ((ViewDuplication.constantGroups V H).reindex (ViewDuplication.embed V)).trivial := by
79   apply GroupViewSystem.Cocycle.ext
80   intro v w f
81   change (1 : H) * 1 * 1⁻¹ = 1
82   simp
83 
84 /-- Both framing domains in the counterexample are saturated. -/
85 theorem full_domain_isoClosed : CompositionSite.IsoClosed (Set.univ : Set (ViewDuplication.Duplicated V)) := by
86   intro a b i ha
87   exact Set.mem_univ b
88 
89 /-- Distinct fully framed cocycles acquire an arrow after pullback along an equivalence. -/
90 theorem full_framing_not_full (v : V) (g : H) (hg : g ≠ 1) :
91     ¬ ((ViewDuplication.constantGroups V H).reindexFramedFunctor
92       (ViewDuplication.embed V) Set.univ).Full := by
93   let F := ViewDuplication.constantGroups V H
94   let P := F.reindexFramedFunctor (ViewDuplication.embed V) Set.univ
95   let c : F.GaugeObject Set.univ := ⟨copyCocycle V g⟩
96   let d : F.GaugeObject Set.univ := ⟨F.trivial⟩
97   have he : F.reindexCocycle (ViewDuplication.embed V) c.labels =
98       F.reindexCocycle (ViewDuplication.embed V) d.labels := by
99     exact copyCocycle_pullback V g
100   let a : P.obj c ⟶ P.obj d :=
101     ⟨1, by
102       change (F.reindex (ViewDuplication.embed V)).gauge 1
103         (F.reindexCocycle (ViewDuplication.embed V) c.labels) =
104         F.reindexCocycle (ViewDuplication.embed V) d.labels
105       rw [(F.reindex (ViewDuplication.embed V)).gauge_one]
106       exact he⟩
107   intro hf
108   let : P.Full := hf
109   let k : c ⟶ d := P.preimage a
110   have hk : F.GaugeEquivalent Set.univ c.labels d.labels := ⟨k.change,k.target⟩
111   have eqc := (F.fully_framed_equivalent_iff c.labels d.labels).mp hk
112   exact copyCocycle_ne_trivial V v g hg eqc
113 
114 /-- In particular the actual fully framed pullback is not an equivalence. -/
115 theorem full_framing_not_equivalence (v : V) (g : H) (hg : g ≠ 1) :
116     ¬ ((ViewDuplication.constantGroups V H).reindexFramedFunctor
117       (ViewDuplication.embed V) Set.univ).IsEquivalence := by
118   intro h
119   let := h
120   exact full_framing_not_full V v g hg inferInstance
121 
122 end FramingBoundaryExamples
123 end KomorebiSpace

Back to source controls