Realization.lean

1 import ProofPath.Field
2 import ProofPath.Views
3 
4 namespace ProofPath
5 
6 structure PatchInclusion (ι : Type*) where
7   small : Set ι
8   large : Set ι
9   le : small ⊆ large
10 
11 namespace Field
12 variable {ι J : Type*} (F : Field ι J)
13 
14 def patchDiagram : ViewDiagram (Set ι) (PatchInclusion ι) where
15   fiber U := F.Local U
16   source e := e.small
17   target e := e.large
18   restriction e := F.restrict e.le
19 
20 def modelSection (x : ι → Prop) (hx : F.Model x) : (U : Set ι) → F.Local U :=
21   F.localize x hx
22 
23 theorem modelSection_coherent (x : ι → Prop) (hx : F.Model x) :
24     F.patchDiagram.Coherent (F.modelSection x hx) := by
25   intro e
26   apply Local.ext
27   intro v
28   exact ⟨fun h => ⟨h.1, h.2.2⟩, fun h => ⟨h.1, e.le h.1, h.2⟩⟩
29 
30 theorem section_at_full_model (s : (U : Set ι) → F.Local U) :
31     F.Model (s Set.univ).val := by
32   constructor
33   · intro v hv
34     exact (s Set.univ).leaves v hv (Set.mem_univ v)
35   · intro j hj hp
36     exact (s Set.univ).rules j hj (Set.subset_univ _) hp
37 
38 /-- The full-patch equivalence identifies the ambient construction. It is not
39     an existence theorem for prescribed proper-patch data. -/
40 def modelEquivSections : {x : ι → Prop // F.Model x} ≃
41     {s : (U : Set ι) → F.Local U // F.patchDiagram.Coherent s} where
42   toFun x := ⟨F.modelSection x.val x.property, F.modelSection_coherent x.val x.property⟩
43   invFun s := ⟨(s.val Set.univ).val, F.section_at_full_model s.val⟩
44   left_inv x := by
45     apply Subtype.ext
46     funext v
47     exact propext (and_iff_right (Set.mem_univ v))
48   right_inv s := by
49     apply Subtype.ext
50     funext U
51     have hc := s.property (PatchInclusion.mk U Set.univ (Set.subset_univ U))
52     change F.restrict (Set.subset_univ U) (s.val Set.univ) = s.val U at hc
53     apply Local.ext
54     intro v
55     have he := congrArg (fun t : F.Local U => t.val v) hc
56     exact Iff.of_eq he
57 
58 end Field
59 end ProofPath

Back to source controls