MarkedTransport.lean

1 import KomorebiSpace.MarkedRealization
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Transport of identified-boundary groupoids
7 
8 A square commuting by a specified natural isomorphism induces a functor on
9 identified-boundary realizations. Full faithfulness and essential surjectivity
10 are proved by explicitly lifting morphisms and objects; the fiber equivalence
11 is not an assumption. The square may be non-strict.
12 -/
13 universe u₁ u₂ u₃ u₄ v₁ v₂ 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 {C' : Type u₃} [Groupoid.{v₃} C']
20 variable {D' : Type u₄} [Groupoid.{v₄} D']
21 variable {F : C ⥤ D} {F' : C' ⥤ D'}
22 
23 /-- The comparison isomorphism transports the boundary along the square. -/
24 def transport (E : C ⥤ C') (K : D ⥤ D') (s : F ⋙ K ≅ E ⋙ F') (b : D) :
25     MarkedRealization F b ⥤ MarkedRealization F' (K.obj b) where
26   obj x := ⟨E.obj x.obj, s.inv.app x.obj ≫ K.map x.identify⟩
27   map := fun {x y} f =>
28     ⟨E.map f.val, by
29       change F'.map (E.map f.val) ≫ (s.inv.app y.obj ≫ K.map y.identify) =
30         s.inv.app x.obj ≫ K.map x.identify
31       have hs : F'.map (E.map f.val) ≫ s.inv.app y.obj =
32           s.inv.app x.obj ≫ K.map (F.map f.val) := s.inv.naturality f.val
33       rw [← Category.assoc, hs, Category.assoc, ← K.map_comp, f.comm]⟩
34   map_id := by intro x; apply Hom.ext; exact E.map_id x.obj
35   map_comp := by intro x y z f g; apply Hom.ext; exact E.map_comp f.val g.val
36 
37 @[simp] theorem transport_obj (E : C ⥤ C') (K : D ⥤ D')
38     (s : F ⋙ K ≅ E ⋙ F') (b : D) (x : MarkedRealization F b) :
39     ((transport E K s b).obj x).obj = E.obj x.obj := rfl
40 
41 @[simp] theorem transport_identify (E : C ⥤ C') (K : D ⥤ D')
42     (s : F ⋙ K ≅ E ⋙ F') (b : D) (x : MarkedRealization F b) :
43     ((transport E K s b).obj x).identify = s.inv.app x.obj ≫ K.map x.identify := rfl
44 
45 @[simp] theorem transport_map (E : C ⥤ C') (K : D ⥤ D')
46     (s : F ⋙ K ≅ E ⋙ F') (b : D) {x y : MarkedRealization F b} (f : x ⟶ y) :
47     ((transport E K s b).map f).val = E.map f.val := rfl
48 
49 /-- Lift an actual fiber morphism and reflect its boundary equation. -/
50 noncomputable def liftHom (E : C ⥤ C') (K : D ⥤ D')
51     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.Full] [E.Faithful] [K.Faithful]
52     {x y : MarkedRealization F b}
53     (a : (transport E K s b).obj x ⟶ (transport E K s b).obj y) : x ⟶ y where
54   val := E.preimage a.val
55   comm := by
56     apply K.map_injective
57     apply (cancel_epi (s.inv.app x.obj)).mp
58     have hs : F'.map (E.map (E.preimage a.val)) ≫ s.inv.app y.obj =
59         s.inv.app x.obj ≫ K.map (F.map (E.preimage a.val)) :=
60       s.inv.naturality (E.preimage a.val)
61     calc
62       s.inv.app x.obj ≫ K.map (F.map (E.preimage a.val) ≫ y.identify) =
63           F'.map (E.map (E.preimage a.val)) ≫ (s.inv.app y.obj ≫ K.map y.identify) := by
64             rw [K.map_comp, ← Category.assoc, ← hs, Category.assoc]
65       _ = s.inv.app x.obj ≫ K.map x.identify := by
66         rw [E.map_preimage a.val]
67         exact a.comm
68 
69 noncomputable def transportFullyFaithful (E : C ⥤ C') (K : D ⥤ D')
70     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.Full] [E.Faithful] [K.Faithful] :
71     (transport E K s b).FullyFaithful where
72   preimage := liftHom E K s b
73   map_preimage := by intro x y a; apply Hom.ext; exact E.map_preimage a.val
74   preimage_map := by intro x y a; apply Hom.ext; exact E.preimage_map a.val
75 
76 /-- Chosen global preimage and a lifted identification, not an assumed fiber preimage. -/
77 noncomputable def chosenPreimage (E : C ⥤ C') (K : D ⥤ D')
78     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.EssSurj] [K.Full]
79     (y : MarkedRealization F' (K.obj b)) : MarkedRealization F b where
80   obj := E.objPreimage y.obj
81   identify := K.preimage (s.hom.app (E.objPreimage y.obj) ≫
82     F'.map (E.objObjPreimageIso y.obj).hom ≫ y.identify)
83 
84 /-- Essential surjectivity includes compatibility of the chosen boundary mark. -/
85 noncomputable def chosenComparison (E : C ⥤ C') (K : D ⥤ D')
86     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.EssSurj] [K.Full]
87     (y : MarkedRealization F' (K.obj b)) :
88     (transport E K s b).obj (chosenPreimage E K s b y) ⟶ y where
89   val := (E.objObjPreimageIso y.obj).hom
90   comm := by
91     change F'.map (E.objObjPreimageIso y.obj).hom ≫ y.identify =
92       s.inv.app (E.objPreimage y.obj) ≫ K.map
93         (K.preimage (s.hom.app (E.objPreimage y.obj) ≫
94           F'.map (E.objObjPreimageIso y.obj).hom ≫ y.identify))
95     rw [K.map_preimage]
96     simp
97 
98 /-- Proved essential surjectivity on the identified-boundary groupoid. -/
99 theorem transport_essentially_surjective (E : C ⥤ C') (K : D ⥤ D')
100     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.EssSurj] [K.Full] :
101     (transport E K s b).EssSurj := by
102   constructor
103   intro y
104   exact ⟨chosenPreimage E K s b y,
105     ⟨(Groupoid.isoEquivHom _ _).symm (chosenComparison E K s b y)⟩⟩
106 
107 /-- Equivalence of presentations preserves the full identified-boundary groupoid. -/
108 theorem transport_isEquivalence (E : C ⥤ C') (K : D ⥤ D')
109     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.IsEquivalence] [K.IsEquivalence] :
110     (transport E K s b).IsEquivalence := by
111   let ff := transportFullyFaithful E K s b
112   let : (transport E K s b).Full := ff.full
113   let : (transport E K s b).Faithful := ff.faithful
114   let : (transport E K s b).EssSurj := transport_essentially_surjective E K s b
115   exact {}
116 
117 noncomputable def transportEquivalence (E : C ⥤ C') (K : D ⥤ D')
118     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.IsEquivalence] [K.IsEquivalence] :
119     MarkedRealization F b ≌ MarkedRealization F' (K.obj b) := by
120   letI := transport_isEquivalence E K s b
121   exact (transport E K s b).asEquivalence
122 
123 @[simp] theorem transportEquivalence_functor (E : C ⥤ C') (K : D ⥤ D')
124     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.IsEquivalence] [K.IsEquivalence] :
125     (transportEquivalence E K s b).functor = transport E K s b := rfl
126 
127 /-- Every boundary-preserving Hom, including automorphisms, is retained. -/
128 noncomputable def transportHomEquiv (E : C ⥤ C') (K : D ⥤ D')
129     (s : F ⋙ K ≅ E ⋙ F') (b : D) [E.Full] [E.Faithful] [K.Faithful]
130     (x y : MarkedRealization F b) :
131     (x ⟶ y) ≃ ((transport E K s b).obj x ⟶ (transport E K s b).obj y) :=
132   (transportFullyFaithful E K s b).homEquiv
133 
134 end MarkedRealization
135 end KomorebiSpace

Back to source controls