SectionExtensionStages.lean

1 import KomorebiSpace.ViewSections
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Extension through an intermediate domain of views
7 
8 The total extension set is the dependent sum of extension fibers over every
9 compatible intermediate choice. This does not say every intermediate choice
10 can be extended, nor does it assert an infinite dependent-choice theorem.
11 -/
12 universe u v w
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace ViewSystem
16 variable {V : Type u} [Category.{v} V]
17 variable (F : ViewSystem.{u,v,w} V)
18 
19 /-- Compatible choices of an intermediate partial section. -/
20 def Intermediate {U W : Set V} (h : U ⊆ W) (s : F.Partial U) :=
21   {t : F.Partial W // F.restrictPartial h t = s}
22 
23 @[simp] theorem restrict_restrictPartial {U W : Set V} (h : U ⊆ W)
24     (x : F.Ambient) :
25     F.restrictPartial h (F.restrict W x) = F.restrict U x := rfl
26 
27 /-- An actual equivalence, retaining all possible intermediate choices. -/
28 def extensionStages {U W : Set V} (h : U ⊆ W) (s : F.Partial U) :
29     F.Extensions U s ≃ Σ t : F.Intermediate h s, F.Extensions W t.val where
30   toFun x := ⟨⟨F.restrict W x.val,x.property⟩,⟨x.val,rfl⟩⟩
31   invFun z := ⟨z.2.val,by
32     have he := congrArg (F.restrictPartial h) z.2.property
33     exact he.trans z.1.property⟩
34   left_inv x := rfl
35   right_inv z := by
36     rcases z with ⟨⟨t,ht⟩,x,hx⟩
37     dsimp at hx
38     subst t
39     rfl
40 
41 @[simp] theorem extensionStages_global {U W : Set V} (h : U ⊆ W)
42     (s : F.Partial U) (x : F.Extensions U s) :
43     (F.extensionStages h s x).2.val = x.val := rfl
44 
45 @[simp] theorem extensionStages_intermediate {U W : Set V} (h : U ⊆ W)
46     (s : F.Partial U) (x : F.Extensions U s) :
47     (F.extensionStages h s x).1.val = F.restrict W x.val := rfl
48 
49 /-- At least one intermediate choice must remain extendable. -/
50 theorem extension_nonempty_iff_intermediate {U W : Set V} (h : U ⊆ W)
51     (s : F.Partial U) :
52     Nonempty (F.Extensions U s) ↔
53       ∃ t : F.Intermediate h s, Nonempty (F.Extensions W t.val) := by
54   constructor
55   · rintro ⟨x⟩
56     exact ⟨(F.extensionStages h s x).1,⟨(F.extensionStages h s x).2⟩⟩
57   · rintro ⟨t,⟨x⟩⟩
58     exact ⟨(F.extensionStages h s).symm ⟨t,x⟩⟩
59 
60 /-- Restriction of an existing global extension gives an intermediate choice. -/
61 def intermediateOfExtension {U W : Set V} (h : U ⊆ W)
62     (s : F.Partial U) (x : F.Extensions U s) : F.Intermediate h s :=
63   (F.extensionStages h s x).1
64 
65 end ViewSystem
66 end KomorebiSpace

Back to source controls