SectionViewEquivalence.lean

1 import KomorebiSpace.ViewEquivalence
2 
3 set_option autoImplicit false
4 set_option backward.isDefEq.respectTransparency false
5 
6 /-!
7 # Coherent section spaces under an equivalent view presentation
8 
9 This is the existing subtype of coherent families. No new definition of a
10 section is introduced. Both directions preserve the prescribed evaluations.
11 -/
12 universe u₁ u₂ v₁ v₂ w
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace ViewSystem
16 variable {V : Type u₁} [Category.{v₁} V]
17 variable {W : Type u₂} [Category.{v₂} W]
18 variable (F : ViewSystem.{u₂,v₂,w} W)
19 
20 /-- Reindex the actual set-valued view system. -/
21 def reindex (H : V ⥤ W) : ViewSystem V where
22   Obj := fun a => F.Obj (H.obj a)
23   pull := fun f => F.pull (H.map f)
24   pull_id := by intro a x; rw [H.map_id, F.pull_id]
25   pull_comp := by intro a b c f g x; rw [H.map_comp, F.pull_comp]
26 
27 /-- Read a coherent family at the image views. -/
28 def reindexSection (H : V ⥤ W) (x : F.Ambient) : (F.reindex H).Ambient :=
29   ⟨fun v => x.val (H.obj v), by intro a b f; exact x.property _ _ (H.map f)⟩
30 
31 @[simp] theorem reindexSection_coordinate (H : V ⥤ W) (x : F.Ambient) (v : V) :
32     (F.reindexSection H x).val v = x.val (H.obj v) := rfl
33 
34 /-- Recover all view coordinates using the actual inverse counit restrictions. -/
35 def recoverSection (e : V ≌ W) (x : (F.reindex e.functor).Ambient) : F.Ambient :=
36   ⟨fun w => F.pull (GroupViewSystem.returnArrow e w) (x.val (e.inverse.obj w)), by
37     intro a b f
38     change F.pull f (F.pull (GroupViewSystem.returnArrow e b) (x.val (e.inverse.obj b))) =
39       F.pull (GroupViewSystem.returnArrow e a) (x.val (e.inverse.obj a))
40     have hn : f ≫ GroupViewSystem.returnArrow e b =
41         GroupViewSystem.returnArrow e a ≫ e.functor.map (e.inverse.map f) :=
42       e.counitIso.inv.naturality f
43     rw [← F.pull_comp, hn, F.pull_comp]
44     have h := x.property (e.inverse.obj a) (e.inverse.obj b) (e.inverse.map f)
45     exact congrArg (F.pull (GroupViewSystem.returnArrow e a)) h⟩
46 
47 @[simp] theorem recover_reindex (e : V ≌ W) (x : F.Ambient) :
48     F.recoverSection e (F.reindexSection e.functor x) = x := by
49   apply Ambient.ext
50   intro w
51   exact x.property _ _ (GroupViewSystem.returnArrow e w)
52 
53 @[simp] theorem reindex_recover (e : V ≌ W) (x : (F.reindex e.functor).Ambient) :
54     F.reindexSection e.functor (F.recoverSection e x) = x := by
55   apply Ambient.ext
56   intro v
57   change F.pull (GroupViewSystem.returnArrow e (e.functor.obj v))
58     (x.val (e.inverse.obj (e.functor.obj v))) = x.val v
59   rw [← GroupViewSystem.mapped_unit_eq_return e v]
60   exact x.property _ _ (e.unitIso.hom.app v)
61 
62 /-- Ambient realization is invariant under equivalent view presentations. -/
63 def viewEquivalence (e : V ≌ W) : F.Ambient ≃ (F.reindex e.functor).Ambient where
64   toFun := F.reindexSection e.functor
65   invFun := F.recoverSection e
66   left_inv := F.recover_reindex e
67   right_inv := F.reindex_recover e
68 
69 @[simp] theorem viewEquivalence_coordinate (e : V ≌ W) (x : F.Ambient) (v : V) :
70     (F.viewEquivalence e x).val v = x.val (e.functor.obj v) := rfl
71 
72 /-- Existence is preserved; equivalent views cannot create a missing coherent section. -/
73 theorem ambient_nonempty_iff (e : V ≌ W) :
74     Nonempty F.Ambient ↔ Nonempty (F.reindex e.functor).Ambient :=
75   (F.viewEquivalence e).nonempty_congr
76 
77 /-- The same comparison also preserves uniqueness of a section when one exists. -/
78 theorem ambient_subsingleton_iff (e : V ≌ W) :
79     Subsingleton F.Ambient ↔ Subsingleton (F.reindex e.functor).Ambient :=
80   (F.viewEquivalence e).subsingleton_congr
81 
82 end ViewSystem
83 
84 namespace GroupViewSystem
85 variable {V : Type u₁} [Category.{v₁} V]
86 variable {W : Type u₂} [Category.{v₂} W]
87 variable {G : W → Type w} [∀ a, Group (G a)]
88 variable (F : GroupViewSystem W G) (e : V ≌ W)
89 
90 /-- Twisted sections are also the previously defined ambient types. -/
91 def reindexTwistedSections (c : F.Cocycle) :
92     (F.twistedViews c).Ambient ≃
93       ((F.reindex e.functor).twistedViews (F.reindexCocycle e.functor c)).Ambient :=
94   (F.twistedViews c).viewEquivalence e
95 
96 @[simp] theorem reindexTwistedSections_coordinate (c : F.Cocycle)
97     (x : (F.twistedViews c).Ambient) (v : V) :
98     (F.reindexTwistedSections e c x).val v = x.val (e.functor.obj v) := rfl
99 
100 end GroupViewSystem
101 end KomorebiSpace

Back to source controls