ViewSiteTransport.lean

1 import KomorebiSpace.CompositionSite
2 import KomorebiSpace.ViewEquivalence
3 
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 
7 /-!
8 # Composition covers under a change of view category
9 
10 Inverse image preserves composition covers for any functor. Reflection under
11 an equivalence requires patches closed under isomorphism. Raw subsets are not
12 silently treated as equivalence-invariant patches.
13 -/
14 universe u₁ u₂ v₁ v₂ z
15 namespace KomorebiSpace
16 open CategoryTheory
17 namespace CompositionSite
18 variable {V : Type u₁} [Category.{v₁} V]
19 variable {W : Type u₂} [Category.{v₂} W]
20 
21 /-- A patch closed under replacing a view by an isomorphic view. -/
22 def IsoClosed (S : Set V) : Prop :=
23   ∀ ⦃a b : V⦄, (a ≅ b) → a ∈ S → b ∈ S
24 
25 theorem mem_iff_of_iso {S : Set V} (h : IsoClosed S) {a b : V} (i : a ≅ b) :
26     a ∈ S ↔ b ∈ S := ⟨h i, h i.symm⟩
27 
28 /-- No fullness or equivalence is needed for preservation of covers. -/
29 theorem familyCovers_preimage (H : V ⥤ W) {I : Type z}
30     {S : Set W} {U : I → Set W} (h : FamilyCovers S U) :
31     FamilyCovers (H.obj ⁻¹' S) (fun i => H.obj ⁻¹' U i) := by
32   intro q hq
33   let t : Triangle W := ⟨H.obj q.a, H.obj q.b, H.obj q.c,
34     H.map q.first, H.map q.second⟩
35   have ht : t.support ⊆ S := (t.support_le_iff S).mpr
36     ⟨hq q.a_mem, hq q.b_mem, hq q.c_mem⟩
37   obtain ⟨i, hi⟩ := h t ht
38   exact ⟨i, (q.support_le_iff _).mpr ⟨hi t.a_mem, hi t.b_mem, hi t.c_mem⟩⟩
39 
40 /-- Reflection uses isomorphism closure of the original patch and cover members. -/
41 theorem familyCovers_reflect (e : V ≌ W) {I : Type z}
42     {S : Set W} {U : I → Set W} (hS : IsoClosed S) (hU : ∀ i, IsoClosed (U i))
43     (h : FamilyCovers (e.functor.obj ⁻¹' S) (fun i => e.functor.obj ⁻¹' U i)) :
44     FamilyCovers S U := by
45   intro q hq
46   let t : Triangle V := ⟨e.inverse.obj q.a, e.inverse.obj q.b, e.inverse.obj q.c,
47     e.inverse.map q.first, e.inverse.map q.second⟩
48   have ht : t.support ⊆ e.functor.obj ⁻¹' S := (t.support_le_iff _).mpr
49     ⟨hS (e.counitIso.app q.a).symm (hq q.a_mem),
50      hS (e.counitIso.app q.b).symm (hq q.b_mem),
51      hS (e.counitIso.app q.c).symm (hq q.c_mem)⟩
52   obtain ⟨i, hi⟩ := h t ht
53   exact ⟨i, (q.support_le_iff _).mpr
54     ⟨hU i (e.counitIso.app q.a) (hi t.a_mem),
55      hU i (e.counitIso.app q.b) (hi t.b_mem),
56      hU i (e.counitIso.app q.c) (hi t.c_mem)⟩⟩
57 
58 /-- The exact cover comparison, without an unsupported claim about all subsets. -/
59 theorem familyCovers_preimage_iff (e : V ≌ W) {I : Type z}
60     {S : Set W} {U : I → Set W} (hS : IsoClosed S) (hU : ∀ i, IsoClosed (U i)) :
61     FamilyCovers (e.functor.obj ⁻¹' S) (fun i => e.functor.obj ⁻¹' U i) ↔
62       FamilyCovers S U :=
63   ⟨familyCovers_reflect e hS hU, familyCovers_preimage e.functor⟩
64 
65 theorem isoClosed_preimage (H : V ⥤ W) {S : Set W} (h : IsoClosed S) :
66     IsoClosed (H.obj ⁻¹' S) := by
67   intro a b i hi
68   exact h (H.mapIso i) hi
69 
70 /-- An isomorphism-closed patch, with its inherited inclusion order. -/
71 def SaturatedPatch (V : Type u₁) [Category.{v₁} V] := {S : Set V // IsoClosed S}
72 
73 instance : PartialOrder (SaturatedPatch V) := inferInstanceAs (PartialOrder {S : Set V // IsoClosed S})
74 
75 /-- On isomorphism-closed patches, inverse image is an actual order isomorphism. -/
76 def saturatedPatchEquiv (e : V ≌ W) : SaturatedPatch W ≃o SaturatedPatch V where
77   toFun S := ⟨e.functor.obj ⁻¹' S.val, isoClosed_preimage e.functor S.property⟩
78   invFun S := ⟨e.inverse.obj ⁻¹' S.val, isoClosed_preimage e.inverse S.property⟩
79   left_inv S := by
80     apply Subtype.ext
81     ext w
82     exact mem_iff_of_iso S.property (e.counitIso.app w)
83   right_inv S := by
84     apply Subtype.ext
85     ext v
86     exact mem_iff_of_iso S.property (e.unitIso.app v).symm
87   map_rel_iff' := by
88     intro S T
89     constructor
90     · intro h w hw
91       exact T.property (e.counitIso.app w)
92         (h (S.property (e.counitIso.app w).symm hw))
93     · intro h v hv
94       exact h hv
95 
96 @[simp] theorem saturatedPatchEquiv_value (e : V ≌ W) (S : SaturatedPatch W) :
97     (saturatedPatchEquiv e S).val = e.functor.obj ⁻¹' S.val := rfl
98 
99 end CompositionSite
100 end KomorebiSpace

Back to source controls