EffectiveDescentExamples.lean

1 import KomorebiSpace.DescentEquivalence
2 import KomorebiSpace.CocycleExamples
3 import Mathlib.CategoryTheory.Category.Preorder
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Nontrivial overlap data and the necessity of the triple-overlap law
9 
10 Four proper patches of four ordered views give a composition cover. The local
11 cocycles are deliberately unequal on a common arrow, and their overlap gauges
12 use noncommuting permutations. A separate group-theoretic obstruction shows
13 that pairwise overlap arrows cannot replace the triple-overlap condition.
14 -/
15 universe u v w z
16 namespace KomorebiSpace
17 open CategoryTheory GroupViewSystem
18 namespace EffectiveDescentExamples
19 
20 section Frames
21 variable {V : Type u} [Category.{v} V]
22 variable {G : V → Type w} [∀ a, Group (G a)]
23 variable {I : Type z} {F : GroupViewSystem V G} {U : I → Set V}
24 
25 /-- Benchmark descent data made from arbitrary local changes of frame. -/
26 def fromFrames (c : F.Cocycle) (k : ∀ i, ∀ x : U i, G x.val) :
27     F.CocycleDescentData U where
28   patch := fun i => (F.restrictCocycle c (U i)).gauge (k i)
29   change := fun i j x hi hj => k j ⟨x,hj⟩ * (k i ⟨x,hi⟩)⁻¹
30   change_edge := by
31     intro i j x y hxi hyi hxj hyj f
32     simp only [PatchCocycle.gauge_edge, restrictCocycle, map_mul, map_inv]
33     group
34   change_comp := by intros; group
35 
36 /-- The benchmark's known global answer, independent of the gluing algorithm. -/
37 def framesEffectuation (c : F.Cocycle) (k : ∀ i, ∀ x : U i, G x.val) :
38     (fromFrames c k).Effectuation where
39   global := c
40   compare := k
41   local_eq := by intros; rfl
42   overlap := by intros; change _ = (_ * _⁻¹) * _; group
43 end Frames
44 
45 abbrev S3 := CocycleExamples.S3
46 abbrev t : S3 := CocycleExamples.transposition
47 abbrev uperm : S3 := CocycleExamples.otherTransposition
48 
49 def fourCoefficients : GroupViewSystem (Fin 4) (fun _ => S3) where
50   pull := fun _ => MonoidHom.id S3
51   pull_id := by intros; rfl
52   pull_comp := by intros; rfl
53 
54 def patches (i : Fin 4) : Set (Fin 4) := {x | x ≠ i}
55 
56 instance (i x : Fin 4) : Decidable (x ∈ patches i) :=
57   inferInstanceAs (Decidable (x ≠ i))
58 
59 theorem patches_proper (i : Fin 4) : ∃ x, x ∉ patches i := ⟨i, by simp [patches]⟩
60 
61 theorem patches_compositionCover : CompositionCover patches := by
62   have h : ∀ a b c : Fin 4, ∃ i : Fin 4, a ≠ i ∧ b ≠ i ∧ c ≠ i := by decide
63   intro a b c f g
64   exact h a b c
65 
66 /-- Patches zero and three deliberately use distinct permutations at view one. -/
67 def localFrames (i : Fin 4) (x : patches i) : S3 :=
68   if x.val = 1 then if i = 0 then t else if i = 3 then uperm else 1 else 1
69 
70 def data : fourCoefficients.CocycleDescentData patches :=
71   fromFrames fourCoefficients.trivial localFrames
72 
73 def edge12 : (1 : Fin 4) ⟶ (2 : Fin 4) := homOfLE (by decide)
74 
75 /-- Strict label agreement does not hold for this valid descent datum. -/
76 theorem local_labels_differ :
77     (data.patch 0).edge (a := ⟨1,by decide⟩) (b := ⟨2,by decide⟩) edge12 ≠
78       (data.patch 3).edge (a := ⟨1,by decide⟩) (b := ⟨2,by decide⟩) edge12 := by decide
79 
80 theorem overlap_nonidentity :
81     data.change 0 3 1 (by decide) (by decide) ≠ 1 := by decide
82 
83 /-- Reversing the required multiplication order produces the wrong overlap. -/
84 theorem overlap_order_matters :
85     data.change 0 3 1 (by decide) (by decide) ≠
86       data.change 0 2 1 (by decide) (by decide) *
87         data.change 2 3 1 (by decide) (by decide) := by decide
88 
89 noncomputable def reconstructed : data.Effectuation := data.effectuate patches_compositionCover
90 
91 theorem reconstructed_local (i : Fin 4) (x y : patches i) (f : x.val ⟶ y.val) :
92     reconstructed.compare i x * reconstructed.global.edge f *
93       (fourCoefficients.pull f (reconstructed.compare i y))⁻¹ = (data.patch i).edge f :=
94   reconstructed.local_eq i x y f
95 
96 /-- The independent benchmark and the constructed answer agree up to the required gauge. -/
97 noncomputable def reconstructedIso :
98     reconstructed.object ≅ (framesEffectuation fourCoefficients.trivial localFrames).object :=
99   reconstructed.comparisonIso (framesEffectuation fourCoefficients.trivial localFrames)
100     patches_compositionCover.transitionCover
101 
102 /-- Actual groupoid equivalence on a proper-patch cover with unequal local cocycles. -/
103 noncomputable def exampleEquivalence :
104     fourCoefficients.GaugeObject ∅ ≌ fourCoefficients.CocycleDescentData patches :=
105   CocycleDescentData.descentEquivalence fourCoefficients patches patches_compositionCover
106 
107 section Necessity
108 variable {H : Type u} [Group H]
109 
110 /-- Any effectuation's local identifications force the triple-overlap law. -/
111 theorem comparisons_force_triple (b0 b1 b2 a01 a12 a02 : H)
112     (h01 : b1 = a01 * b0) (h12 : b2 = a12 * b1) (h02 : b2 = a02 * b0) :
113     a02 = a12 * a01 := by
114   apply mul_right_cancel (b := b0)
115   calc
116     a02 * b0 = b2 := h02.symm
117     _ = a12 * b1 := h12
118     _ = (a12 * a01) * b0 := by rw [h01, mul_assoc]
119 end Necessity
120 
121 /-- Three individually invertible overlap gauges can still be incompatible. -/
122 theorem inconsistent_triple_no_frames :
123     ¬ ∃ b0 b1 b2 : S3, b1 = t * b0 ∧ b2 = t * b1 ∧ b2 = t * b0 := by
124   rintro ⟨b0,b1,b2,h01,h12,h02⟩
125   have he := comparisons_force_triple b0 b1 b2 t t t h01 h12 h02
126   exact CocycleExamples.transposition_nontrivial
127     (he.trans CocycleExamples.transposition_square)
128 
129 end EffectiveDescentExamples
130 end KomorebiSpace

Back to source controls