RelativeSections.lean

1 import KomorebiSpace.SectionViewEquivalence
2 import KomorebiSpace.ViewSiteTransport
3 import KomorebiSpace.NonabelianExtension
4 
5 set_option autoImplicit false
6 set_option backward.isDefEq.respectTransparency false
7 
8 /-!
9 # Prescribed section problems under equivalent views
10 
11 The source and target are the existing section and extension types. Prescribed
12 values are pulled back along the actual view functor. Isomorphism closure of
13 the prescribed domain allows the inverse counit to recover every prescribed
14 coordinate. No equivalence of all based-gauge orbit sets is asserted.
15 -/
16 universe u₁ u₂ v₁ v₂ w
17 namespace KomorebiSpace
18 open CategoryTheory
19 namespace ViewSystem
20 variable {V : Type u₁} [Category.{v₁} V]
21 variable {W : Type u₂} [Category.{v₂} W]
22 variable (F : ViewSystem.{u₂,v₂,w} W)
23 
24 /-- Prescribed data at image views, with the original coherence equations. -/
25 def reindexPartial (H : V ⥤ W) (U : Set W) (s : F.Partial U) :
26     (F.reindex H).Partial (H.obj ⁻¹' U) :=
27   ⟨fun v => s.val ⟨H.obj v.val, v.property⟩, by
28     intro a b f
29     exact s.property ⟨H.obj a.val,a.property⟩ ⟨H.obj b.val,b.property⟩ (H.map f)⟩
30 
31 @[simp] theorem reindexPartial_coordinate (H : V ⥤ W) (U : Set W)
32     (s : F.Partial U) (v : H.obj ⁻¹' U) :
33     (F.reindexPartial H U s).val v = s.val ⟨H.obj v.val,v.property⟩ := rfl
34 
35 @[simp] theorem reindex_restrict (H : V ⥤ W) (U : Set W) (x : F.Ambient) :
36     (F.reindex H).restrict (H.obj ⁻¹' U) (F.reindexSection H x) =
37       F.reindexPartial H U (F.restrict U x) := rfl
38 
39 /-- Forward transport of an actual extension with its prescribed values. -/
40 def reindexExtension (H : V ⥤ W) (U : Set W) (s : F.Partial U)
41     (x : F.Extensions U s) :
42     (F.reindex H).Extensions (H.obj ⁻¹' U) (F.reindexPartial H U s) :=
43   ⟨F.reindexSection H x.val, by rw [F.reindex_restrict, x.property]⟩
44 
45 /-- The recovered global section retains every prescribed target view. -/
46 def recoverExtension (e : V ≌ W) (U : Set W) (hU : CompositionSite.IsoClosed U)
47     (s : F.Partial U)
48     (x : (F.reindex e.functor).Extensions (e.functor.obj ⁻¹' U)
49       (F.reindexPartial e.functor U s)) : F.Extensions U s := by
50   refine ⟨F.recoverSection e x.val, ?_⟩
51   apply Partial.ext
52   intro w
53   have hm : e.functor.obj (e.inverse.obj w.val) ∈ U :=
54     hU (e.counitIso.app w.val).symm w.property
55   have hx := congrArg (fun t : (F.reindex e.functor).Partial (e.functor.obj ⁻¹' U) =>
56     t.val ⟨e.inverse.obj w.val,hm⟩) x.property
57   change x.val.val (e.inverse.obj w.val) =
58     s.val ⟨e.functor.obj (e.inverse.obj w.val),hm⟩ at hx
59   change F.pull (GroupViewSystem.returnArrow e w.val)
60     (x.val.val (e.inverse.obj w.val)) = s.val w
61   rw [hx]
62   exact s.property w ⟨e.functor.obj (e.inverse.obj w.val),hm⟩
63     (GroupViewSystem.returnArrow e w.val)
64 
65 /-- All global completions, not only their existence, are preserved. -/
66 def relativeViewEquivalence (e : V ≌ W) (U : Set W)
67     (hU : CompositionSite.IsoClosed U) (s : F.Partial U) :
68     F.Extensions U s ≃
69       (F.reindex e.functor).Extensions (e.functor.obj ⁻¹' U)
70         (F.reindexPartial e.functor U s) where
71   toFun := F.reindexExtension e.functor U s
72   invFun := F.recoverExtension e U hU s
73   left_inv x := Subtype.ext (F.recover_reindex e x.val)
74   right_inv x := Subtype.ext (F.reindex_recover e x.val)
75 
76 @[simp] theorem relativeViewEquivalence_coordinate (e : V ≌ W) (U : Set W)
77     (hU : CompositionSite.IsoClosed U) (s : F.Partial U) (x : F.Extensions U s) (v : V) :
78     (F.relativeViewEquivalence e U hU s x).val.val v = x.val.val (e.functor.obj v) := rfl
79 
80 theorem relative_nonempty_iff (e : V ≌ W) (U : Set W)
81     (hU : CompositionSite.IsoClosed U) (s : F.Partial U) :
82     Nonempty (F.Extensions U s) ↔
83       Nonempty ((F.reindex e.functor).Extensions (e.functor.obj ⁻¹' U)
84         (F.reindexPartial e.functor U s)) :=
85   (F.relativeViewEquivalence e U hU s).nonempty_congr
86 
87 theorem relative_subsingleton_iff (e : V ≌ W) (U : Set W)
88     (hU : CompositionSite.IsoClosed U) (s : F.Partial U) :
89     Subsingleton (F.Extensions U s) ↔
90       Subsingleton ((F.reindex e.functor).Extensions (e.functor.obj ⁻¹' U)
91         (F.reindexPartial e.functor U s)) :=
92   (F.relativeViewEquivalence e U hU s).subsingleton_congr
93 
94 end ViewSystem
95 
96 namespace GroupViewSystem
97 variable {V : Type u₁} [Category.{v₁} V]
98 variable {W : Type u₂} [Category.{v₂} W]
99 variable {G : W → Type w} [∀ a, Group (G a)]
100 variable (F : GroupViewSystem W G)
101 
102 /-- The same theorem on the existing twisted section types. -/
103 def relativeTwistedEquivalence (e : V ≌ W) (U : Set W)
104     (hU : CompositionSite.IsoClosed U) (c : F.Cocycle)
105     (s : (F.twistedViews c).Partial U) :
106     (F.twistedViews c).Extensions U s ≃
107       ((F.reindex e.functor).twistedViews (F.reindexCocycle e.functor c)).Extensions
108         (e.functor.obj ⁻¹' U) ((F.twistedViews c).reindexPartial e.functor U s) :=
109   (F.twistedViews c).relativeViewEquivalence e U hU s
110 
111 /-- Relative feasibility is invariant even though entire based-gauge orbit sets need not be. -/
112 theorem relative_neutral_iff (e : V ≌ W) (U : Set W)
113     (hU : CompositionSite.IsoClosed U) (c : F.Cocycle)
114     (s : (F.twistedViews c).Partial U) :
115     F.extensionOrbit c U s = F.neutralClass U ↔
116       (F.reindex e.functor).extensionOrbit (F.reindexCocycle e.functor c)
117         (e.functor.obj ⁻¹' U) ((F.twistedViews c).reindexPartial e.functor U s) =
118       (F.reindex e.functor).neutralClass (e.functor.obj ⁻¹' U) := by
119   rw [F.extensionOrbit_neutral_iff, (F.reindex e.functor).extensionOrbit_neutral_iff]
120   exact (F.relativeTwistedEquivalence e U hU c s).nonempty_congr
121 
122 end GroupViewSystem
123 end KomorebiSpace

Back to source controls