ViewCorrespondence.lean

1 import KomorebiSpace.SectionGluing
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Common ambient realizations as section-valued bridge fibers
7 
8 At the strict set-valued level, taking coherent sections commutes with the
9 specified fiber of a correspondence span. Existence is not assumed. Matching
10 local bridge sections give a global bridge under transition-covered gluing.
11 -/
12 universe u v w z t i
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace ViewSystem
16 variable {V : Type u} [Category.{v} V]
17 variable {M : ViewSystem.{u,v,w} V} {F : ViewSystem.{u,v,z} V}
18 variable {G : ViewSystem.{u,v,t} V}
19 
20 /-- A strict fiber of a specified span at two ambient sections. -/
21 def GlobalBridge (p : Morphism M F) (q : Morphism M G)
22     (a : F.Ambient) (b : G.Ambient) :=
23   {s : M.Ambient // p.onAmbient s = a ∧ q.onAmbient s = b}
24 
25 /-- Each view contains realizations of the prescribed pair in the span. -/
26 def bridgeSystem (p : Morphism M F) (q : Morphism M G)
27     (a : F.Ambient) (b : G.Ambient) : ViewSystem V where
28   Obj v := {x : M.Obj v // p.app v x = a.val v ∧ q.app v x = b.val v}
29   pull := fun {v w} f x => ⟨M.pull f x.val, by
30     constructor
31     · calc
32         p.app v (M.pull f x.val) = F.pull f (p.app w x.val) := (p.natural f x.val).symm
33         _ = F.pull f (a.val w) := congrArg (F.pull f) x.property.1
34         _ = a.val v := a.property v w f
35     · calc
36         q.app v (M.pull f x.val) = G.pull f (q.app w x.val) := (q.natural f x.val).symm
37         _ = G.pull f (b.val w) := congrArg (G.pull f) x.property.2
38         _ = b.val v := b.property v w f⟩
39   pull_id := by intro v x; apply Subtype.ext; exact M.pull_id v x.val
40   pull_comp := by intro v w z f g x; apply Subtype.ext; exact M.pull_comp f g x.val
41 
42 /-- This is the set-level fiber/section equivalence, not a homotopy-fiber theorem. -/
43 def bridgeEquiv (p : Morphism M F) (q : Morphism M G)
44     (a : F.Ambient) (b : G.Ambient) :
45     (bridgeSystem p q a b).Ambient ≃ GlobalBridge p q a b where
46   toFun := fun x =>
47     ⟨⟨fun v => (x.val v).val, by
48         intro v w f
49         exact congrArg Subtype.val (x.property v w f)⟩, by
50       constructor
51       · apply Ambient.ext; intro v; exact (x.val v).property.1
52       · apply Ambient.ext; intro v; exact (x.val v).property.2⟩
53   invFun := fun s =>
54     ⟨fun v => ⟨s.val.val v, by
55         constructor
56         · exact congrArg (fun x : F.Ambient => x.val v) s.property.1
57         · exact congrArg (fun x : G.Ambient => x.val v) s.property.2⟩, by
58       intro v w f
59       apply Subtype.ext
60       exact s.val.property v w f⟩
61   left_inv := by intro x; apply Ambient.ext; intro v; rfl
62   right_inv := by intro s; apply Subtype.ext; apply Ambient.ext; intro v; rfl
63 
64 @[simp] theorem bridgeEquiv_coordinate (p : Morphism M F) (q : Morphism M G)
65     (a : F.Ambient) (b : G.Ambient) (x : (bridgeSystem p q a b).Ambient) (v : V) :
66     (bridgeEquiv p q a b x).val.val v = (x.val v).val := rfl
67 
68 theorem bridge_nonempty_iff (p : Morphism M F) (q : Morphism M G)
69     (a : F.Ambient) (b : G.Ambient) :
70     Nonempty (GlobalBridge p q a b) ↔ Nonempty (bridgeSystem p q a b).Ambient := by
71   constructor
72   · rintro ⟨x⟩; exact ⟨(bridgeEquiv p q a b).symm x⟩
73   · rintro ⟨x⟩; exact ⟨bridgeEquiv p q a b x⟩
74 
75 /-- Glue the correspondence objects themselves, with both projected objects fixed. -/
76 noncomputable def glueBridge (p : Morphism M F) (q : Morphism M G)
77     (a : F.Ambient) (b : G.Ambient) {I : Type i} {U : I → Set V}
78     (h : TransitionCover U) (m : Matching (bridgeSystem p q a b) U) :
79     GlobalBridge p q a b := bridgeEquiv p q a b (m.glue h)
80 
81 @[simp] theorem glueBridge_left (p : Morphism M F) (q : Morphism M G)
82     (a : F.Ambient) (b : G.Ambient) {I : Type i} {U : I → Set V}
83     (h : TransitionCover U) (m : Matching (bridgeSystem p q a b) U) :
84     p.onAmbient (glueBridge p q a b h m).val = a :=
85   (glueBridge p q a b h m).property.1
86 
87 @[simp] theorem glueBridge_right (p : Morphism M F) (q : Morphism M G)
88     (a : F.Ambient) (b : G.Ambient) {I : Type i} {U : I → Set V}
89     (h : TransitionCover U) (m : Matching (bridgeSystem p q a b) U) :
90     q.onAmbient (glueBridge p q a b h m).val = b :=
91   (glueBridge p q a b h m).property.2
92 
93 /-- Local bridges must form a matching family, not merely exist individually. -/
94 theorem bridge_exists_iff_matching (p : Morphism M F) (q : Morphism M G)
95     (a : F.Ambient) (b : G.Ambient) {I : Type i} (U : I → Set V)
96     (h : TransitionCover U) :
97     Nonempty (GlobalBridge p q a b) ↔ Nonempty (Matching (bridgeSystem p q a b) U) := by
98   constructor
99   · rintro ⟨x⟩
100     exact ⟨(bridgeSystem p q a b).toMatching U ((bridgeEquiv p q a b).symm x)⟩
101   · rintro ⟨m⟩
102     exact ⟨glueBridge p q a b h m⟩
103 
104 /-- A fixed matching family determines its global bridge uniquely. -/
105 theorem bridge_glue_unique (p : Morphism M F) (q : Morphism M G)
106     (a : F.Ambient) (b : G.Ambient) {I : Type i} {U : I → Set V}
107     (h : TransitionCover U) (m : Matching (bridgeSystem p q a b) U)
108     (z : GlobalBridge p q a b)
109     (hz : ∀ j, (bridgeSystem p q a b).restrict (U j)
110       ((bridgeEquiv p q a b).symm z) = m.localSection j) :
111     z = glueBridge p q a b h m := by
112   have he := m.glue_unique h ((bridgeEquiv p q a b).symm z) hz
113   have he' := congrArg (bridgeEquiv p q a b) he
114   simpa only [Equiv.apply_symm_apply, glueBridge] using he'
115 
116 end ViewSystem
117 end KomorebiSpace

Back to source controls