MarkedRealization.lean

1 import Mathlib.CategoryTheory.Equivalence
2 import Mathlib.CategoryTheory.Groupoid
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Realizations with an identified boundary
8 
9 For a functor between groupoids, a realization over b is an object together
10 with an actual arrow identifying its image with b. Every such arrow is an
11 isomorphism. Morphisms must commute with the chosen identification. This is
12 the explicit groupoid homotopy fiber, not the naive equality fiber.
13 -/
14 universe u₁ u₂ u₃ u₄ v₁ v₂ v₃ v₄
15 namespace KomorebiSpace
16 open CategoryTheory
17 
18 structure MarkedRealization {C : Type u₁} [Groupoid.{v₁} C]
19     {D : Type u₂} [Groupoid.{v₂} D] (F : C ⥤ D) (b : D) where
20   obj : C
21   identify : F.obj obj ⟶ b
22 
23 namespace MarkedRealization
24 variable {C : Type u₁} [Groupoid.{v₁} C]
25 variable {D : Type u₂} [Groupoid.{v₂} D]
26 variable {F : C ⥤ D} {b : D}
27 
28 structure Hom (x y : MarkedRealization F b) where
29   val : x.obj ⟶ y.obj
30   comm : F.map val ≫ y.identify = x.identify
31 
32 @[ext] theorem Hom.ext {x y : MarkedRealization F b} {f g : Hom x y}
33     (h : f.val = g.val) : f = g := by cases f; cases g; cases h; rfl
34 
35 def identity (x : MarkedRealization F b) : Hom x x :=
36   ⟨𝟙 x.obj, by simp⟩
37 
38 def compose {x y z : MarkedRealization F b} (f : Hom x y) (g : Hom y z) : Hom x z :=
39   ⟨f.val ≫ g.val, by rw [F.map_comp, Category.assoc, g.comm, f.comm]⟩
40 
41 def reverse {x y : MarkedRealization F b} (f : Hom x y) : Hom y x :=
42   ⟨Groupoid.inv f.val, by rw [← f.comm, ← Category.assoc, ← F.map_comp]; simp⟩
43 
44 instance : Groupoid (MarkedRealization F b) where
45   Hom := Hom
46   id := identity
47   comp := compose
48   id_comp := by intros; apply Hom.ext; exact Category.id_comp _
49   comp_id := by intros; apply Hom.ext; exact Category.comp_id _
50   assoc := by intros; apply Hom.ext; exact Category.assoc _ _ _
51   inv := reverse
52   inv_comp := by intros; apply Hom.ext; exact Groupoid.inv_comp _
53   comp_inv := by intros; apply Hom.ext; exact Groupoid.comp_inv _
54 
55 @[simp] theorem comp_val {x y z : MarkedRealization F b} (f : x ⟶ y) (g : y ⟶ z) :
56     (f ≫ g).val = f.val ≫ g.val := rfl
57 
58 /-- Forget the boundary identification, but retain the actual underlying morphism. -/
59 def forget (F : C ⥤ D) (b : D) : MarkedRealization F b ⥤ C where
60   obj x := x.obj
61   map f := f.val
62 
63 /-- Nonemptiness means actual membership in the essential image. -/
64 theorem nonempty_iff (F : C ⥤ D) (b : D) :
65     Nonempty (MarkedRealization F b) ↔ ∃ x : C, Nonempty (F.obj x ≅ b) := by
66   constructor
67   · rintro ⟨x⟩
68     exact ⟨x.obj, ⟨(Groupoid.isoEquivHom _ _).symm x.identify⟩⟩
69   · rintro ⟨x, ⟨i⟩⟩
70     exact ⟨⟨x,i.hom⟩⟩
71 
72 /-- The identification forces automorphisms to be invisible at the boundary. -/
73 theorem endomorphism_condition (x : MarkedRealization F b) (a : x.obj ⟶ x.obj) :
74     F.map a ≫ x.identify = x.identify ↔ F.map a = 𝟙 (F.obj x.obj) := by
75   constructor
76   · intro h
77     apply (cancel_mono x.identify).mp
78     simpa using h
79   · intro h
80     rw [h, Category.id_comp]
81 
82 /-- For fixed underlying objects, all allowable comparison witnesses are retained. -/
83 def homEquiv (x y : MarkedRealization F b) :
84     (x ⟶ y) ≃ {a : x.obj ⟶ y.obj // F.map a ≫ y.identify = x.identify} where
85   toFun a := ⟨a.val,a.comm⟩
86   invFun a := ⟨a.val,a.property⟩
87   left_inv _ := rfl
88   right_inv _ := rfl
89 
90 end MarkedRealization
91 end KomorebiSpace

Back to source controls