SectionGluing.lean

1 import KomorebiSpace.ViewSections
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Gluing sections over a cover which includes transitions
7 
8 A cover of view objects alone is insufficient. The sufficient cover hypothesis
9 below requires every arrow's endpoints to occur together in some patch.
10 Under this combinatorial condition, matching local sections glue uniquely.
11 This is a strict set-valued gluing theorem, not a general higher-stack assertion.
12 -/
13 universe u v w z
14 namespace KomorebiSpace
15 open CategoryTheory
16 namespace ViewSystem
17 variable {V : Type u} [Category.{v} V]
18 variable (F : ViewSystem.{u,v,w} V) {I : Type z} (U : I → Set V)
19 
20 /-- Every view is seen somewhere. This alone need not suffice for gluing. -/
21 def ObjectCover : Prop := ∀ a : V, ∃ i, a ∈ U i
22 
23 /-- Every transition is seen with both endpoints in one patch. -/
24 def TransitionCover : Prop :=
25   ∀ (a b : V) (_ : a ⟶ b), ∃ i, a ∈ U i ∧ b ∈ U i
26 
27 theorem TransitionCover.objectCover (h : TransitionCover U) : ObjectCover U := by
28   intro a
29   obtain ⟨i, ha, _⟩ := h a a (𝟙 a)
30   exact ⟨i, ha⟩
31 
32 /-- Values agree on every common view, not only up to an unspecified relation. -/
33 structure Matching where
34   localSection : ∀ i, F.Partial (U i)
35   agree : ∀ i j a (hi : a ∈ U i) (hj : a ∈ U j),
36     (localSection i).val ⟨a, hi⟩ = (localSection j).val ⟨a, hj⟩
37 
38 namespace Matching
39 variable {F U}
40 
41 @[ext] theorem ext {m n : Matching F U}
42     (h : ∀ i, m.localSection i = n.localSection i) : m = n := by
43   cases m with
44   | mk ml ma =>
45     cases n with
46     | mk nl na =>
47       have he : ml = nl := funext h
48       cases he
49       rfl
50 
51 noncomputable def assemble (h : ObjectCover U) (m : Matching F U) : ∀ a, F.Obj a :=
52   fun a => (m.localSection (Classical.choose (h a))).val
53     ⟨a, Classical.choose_spec (h a)⟩
54 
55 theorem assemble_local (h : ObjectCover U) (m : Matching F U)
56     (i : I) (a : V) (ha : a ∈ U i) :
57     m.assemble h a = (m.localSection i).val ⟨a, ha⟩ := by
58   exact m.agree _ i a _ ha
59 
60 /-- Assembly becomes coherent because the cover also sees every transition. -/
61 theorem assemble_coherent (h : TransitionCover U) (m : Matching F U)
62     (a b : V) (f : a ⟶ b) :
63     F.pull f (m.assemble (TransitionCover.objectCover U h) b) = m.assemble (TransitionCover.objectCover U h) a := by
64   obtain ⟨i, ha, hb⟩ := h a b f
65   rw [m.assemble_local (TransitionCover.objectCover U h) i b hb, m.assemble_local (TransitionCover.objectCover U h) i a ha]
66   exact (m.localSection i).property ⟨a, ha⟩ ⟨b, hb⟩ f
67 
68 noncomputable def glue (h : TransitionCover U) (m : Matching F U) : F.Ambient :=
69   ⟨m.assemble (TransitionCover.objectCover U h), m.assemble_coherent h⟩
70 
71 @[simp] theorem glue_restrict (h : TransitionCover U) (m : Matching F U) (i : I) :
72     F.restrict (U i) (m.glue h) = m.localSection i := by
73   apply Partial.ext
74   intro a
75   exact m.assemble_local (TransitionCover.objectCover U h) i a.val a.property
76 
77 theorem glue_unique (h : TransitionCover U) (m : Matching F U) (s : F.Ambient)
78     (hs : ∀ i, F.restrict (U i) s = m.localSection i) : s = m.glue h := by
79   apply Ambient.ext
80   intro a
81   obtain ⟨i, ha⟩ := (TransitionCover.objectCover U h) a
82   have hv := congrArg (fun x : F.Partial (U i) => x.val ⟨a, ha⟩) (hs i)
83   exact hv.trans (m.assemble_local (TransitionCover.objectCover U h) i a ha).symm
84 
85 theorem exists_unique_glue (h : TransitionCover U) (m : Matching F U) :
86     ∃! s : F.Ambient, ∀ i, F.restrict (U i) s = m.localSection i := by
87   refine ⟨m.glue h, fun i => m.glue_restrict h i, ?_⟩
88   intro s hs
89   exact m.glue_unique h s hs
90 end Matching
91 
92 /-- Restriction gives a matching family without any cover hypothesis. -/
93 def toMatching (s : F.Ambient) : Matching F U where
94   localSection := fun i => F.restrict (U i) s
95   agree := by intros; rfl
96 
97 /-- A proved local/global equivalence for the specified transition-covered patches. -/
98 noncomputable def gluingEquiv (h : TransitionCover U) :
99     F.Ambient ≃ Matching F U where
100   toFun := F.toMatching U
101   invFun := fun m => m.glue h
102   left_inv := by
103     intro s
104     exact ((F.toMatching U s).glue_unique h s (fun _ => rfl)).symm
105   right_inv := by
106     intro m
107     apply Matching.ext
108     intro i
109     exact m.glue_restrict h i
110 
111 /-- Global equality needs only coverage of views; global existence needs more. -/
112 theorem restrict_jointly_injective (h : ObjectCover U) {s t : F.Ambient}
113     (hst : ∀ i, F.restrict (U i) s = F.restrict (U i) t) : s = t := by
114   apply Ambient.ext
115   intro a
116   obtain ⟨i, ha⟩ := h a
117   exact congrArg (fun x : F.Partial (U i) => x.val ⟨a, ha⟩) (hst i)
118 
119 end ViewSystem
120 end KomorebiSpace

Back to source controls