Views.lean

1 import Mathlib.Data.Set.Lattice.Indexed
2 
3 namespace ProofPath
4 universe u
5 
6 /-- A declared graph of views. Edges induce restrictions in the opposite direction. -/
7 structure ViewDiagram (V E : Type*) where
8   fiber : V → Type u
9   source : E → V
10   target : E → V
11   restriction : (e : E) → fiber (target e) → fiber (source e)
12 
13 namespace ViewDiagram
14 variable {V E I : Type*} (F : ViewDiagram V E)
15 
16 def Coherent (x : (v : V) → F.fiber v) : Prop :=
17   ∀ e, F.restriction e (x (F.target e)) = x (F.source e)
18 
19 theorem arrow_cover_gluing (U : I → Set V)
20     (s : (i : I) → (v : V) → v ∈ U i → F.fiber v)
21     (cover : ∀ v, ∃ i, v ∈ U i)
22     (edgeCover : ∀ e, ∃ i, F.source e ∈ U i ∧ F.target e ∈ U i)
23     (matching : ∀ i j v (hi : v ∈ U i) (hj : v ∈ U j), s i v hi = s j v hj)
24     (localCoherence : ∀ i e (hs : F.source e ∈ U i) (ht : F.target e ∈ U i),
25       F.restriction e (s i (F.target e) ht) = s i (F.source e) hs) :
26     ∃! x : (v : V) → F.fiber v,
27       F.Coherent x ∧ ∀ i v (h : v ∈ U i), x v = s i v h := by
28   classical
29   let x : (v : V) → F.fiber v := fun v =>
30     s (Classical.choose (cover v)) v (Classical.choose_spec (cover v))
31   have agree : ∀ i v (h : v ∈ U i), x v = s i v h := by
32     intro i v h
33     exact matching _ i v _ h
34   refine ⟨x, ⟨?_, agree⟩, ?_⟩
35   · intro e
36     obtain ⟨i, hs, ht⟩ := edgeCover e
37     rw [agree i (F.target e) ht, agree i (F.source e) hs]
38     exact localCoherence i e hs ht
39   · intro y hy
40     funext v
41     obtain ⟨i, hi⟩ := cover v
42     exact (hy.2 i v hi).trans (agree i v hi).symm
43 
44 end ViewDiagram
45 end ProofPath

Back to source controls