MarkedBoundaryChange.lean

1 import KomorebiSpace.MarkedTransport
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Replacing the boundary by an isomorphic object
7 
8 The boundary is fixed as an object with specified identification, rather than
9 an independently frozen frame at every view. Changing its representative by
10 an isomorphism preserves the realization groupoid. For the identity restriction,
11 the identified-boundary fiber has a unique morphism between every pair of objects.
12 -/
13 universe u₁ u₂ v₁ v₂
14 namespace KomorebiSpace
15 open CategoryTheory
16 namespace MarkedRealization
17 variable {C : Type u₁} [Groupoid.{v₁} C]
18 variable {D : Type u₂} [Groupoid.{v₂} D]
19 variable {F : C ⥤ D} {b b' : D}
20 
21 def changeBoundary (F : C ⥤ D) (i : b ≅ b') :
22     MarkedRealization F b ⥤ MarkedRealization F b' where
23   obj x := ⟨x.obj,x.identify ≫ i.hom⟩
24   map f := ⟨f.val, by rw [← Category.assoc, f.comm]⟩
25   map_id := by intro x; rfl
26   map_comp := by intro x y z f g; rfl
27 
28 @[simp] theorem changeBoundary_identify (i : b ≅ b') (x : MarkedRealization F b) :
29     ((changeBoundary F i).obj x).identify = x.identify ≫ i.hom := rfl
30 
31 /-- The round trip is identified by the identity of the original global object. -/
32 def boundaryRoundTrip (F : C ⥤ D) (i : b ≅ b') :
33     changeBoundary F i ⋙ changeBoundary F i.symm ≅ 𝟭 (MarkedRealization F b) :=
34   NatIso.ofComponents (fun x => (Groupoid.isoEquivHom _ _).symm
35     (⟨𝟙 x.obj, by
36       change F.map (𝟙 x.obj) ≫ x.identify = (x.identify ≫ i.hom) ≫ i.inv
37       simp⟩ : (changeBoundary F i ⋙ changeBoundary F i.symm).obj x ⟶ x))
38     (by
39       intro x y a
40       apply Hom.ext
41       change a.val ≫ 𝟙 y.obj = 𝟙 x.obj ≫ a.val
42       simp)
43 
44 def boundaryEquivalence (F : C ⥤ D) (i : b ≅ b') :
45     MarkedRealization F b ≌ MarkedRealization F b' :=
46   CategoryTheory.Equivalence.mk (changeBoundary F i) (changeBoundary F i.symm)
47     (boundaryRoundTrip F i).symm (boundaryRoundTrip F i.symm)
48 
49 @[simp] theorem boundaryEquivalence_functor (i : b ≅ b') :
50     (boundaryEquivalence F i).functor = changeBoundary F i := rfl
51 
52 /-- A full boundary still allows different representatives, but fixes their identification. -/
53 def identityCenter (b : D) : MarkedRealization (𝟭 D) b := ⟨b,𝟙 b⟩
54 
55 def identityFiberArrow (x y : MarkedRealization (𝟭 D) b) : x ⟶ y :=
56   ⟨x.identify ≫ Groupoid.inv y.identify, by
57     change (x.identify ≫ Groupoid.inv y.identify) ≫ y.identify = x.identify
58     simp⟩
59 
60 /-- There is no spurious ambiguity from different representatives of an entirely fixed boundary. -/
61 theorem identityFiberArrow_unique (x y : MarkedRealization (𝟭 D) b) (a : x ⟶ y) :
62     a = identityFiberArrow x y := by
63   apply Hom.ext
64   apply (cancel_mono y.identify).mp
65   change a.val ≫ y.identify = (x.identify ≫ Groupoid.inv y.identify) ≫ y.identify
66   simpa using a.comm
67 
68 /-- Nonempty identity fibers are contractible as groupoids, not singletons as object types. -/
69 theorem identityFiber_unique_hom (x y : MarkedRealization (𝟭 D) b) :
70     ∃! _a : x ⟶ y, True := by
71   refine ⟨identityFiberArrow x y, trivial, ?_⟩
72   intro a ha
73   exact identityFiberArrow_unique x y a
74 
75 end MarkedRealization
76 end KomorebiSpace

Back to source controls