feat(combinatorics/quiver/*) Notation for prefunctors (#17576)

bottine · kim-em · bottine · commit c6dd521ebdce · 2022-11-18T07:46:14.000Z
Co-authored-by: Scott Morrison &lt;scott@tqft.net&gt;
diff --git a/src/category_theory/groupoid/free_groupoid.lean b/src/category_theory/groupoid/free_groupoid.lean
@@ -129,13 +129,12 @@ instance : groupoid (free_groupoid V) :=
   comp_inv' := λ X Y p, quot.induction_on p $ λ pp, congr_comp_reverse pp }
 
 /-- The inclusion of the quiver on `V` to the underlying quiver on `free_groupoid V`-/
-def of (V) [quiver V] : prefunctor V (free_groupoid V) :=
+def of (V) [quiver V] : V ⥤q (free_groupoid V) :=
 { obj := λ X, ⟨X⟩,
   map := λ X Y f, quot.mk _ f.to_pos_path }
 
 lemma of_eq : of V =
-  ((quiver.symmetrify.of).comp
-    paths.of).comp (quotient.functor $ @red_step V _).to_prefunctor :=
+  (quiver.symmetrify.of ⋙q paths.of).comp (quotient.functor $ @red_step V _).to_prefunctor :=
 begin
   apply prefunctor.ext, rotate,
   { rintro X, refl, },
@@ -144,10 +143,10 @@ end
 
 section universal_property
 
-variables {V' : Type u'} [groupoid V'] (φ : prefunctor V V')
+variables {V' : Type u'} [groupoid V'] (φ : V ⥤q V')
 
 /-- The lift of a prefunctor to a groupoid, to a functor from `free_groupoid V` -/
-def lift (φ : prefunctor V V') : free_groupoid V ⥤ V' :=
+def lift (φ : V ⥤q V') : free_groupoid V ⥤ V' :=
 quotient.lift _
   (paths.lift $ quiver.symmetrify.lift φ)
   (by
@@ -157,15 +156,15 @@ quotient.lift _
       symmetry,
       apply groupoid.comp_inv, })
 
-lemma lift_spec (φ : prefunctor V V') : (of V).comp (lift φ).to_prefunctor = φ :=
+lemma lift_spec (φ : V ⥤q V') : of V ⋙q (lift φ).to_prefunctor = φ :=
 begin
   rw [of_eq, prefunctor.comp_assoc, prefunctor.comp_assoc, functor.to_prefunctor_comp],
   dsimp [lift],
   rw [quotient.lift_spec, paths.lift_spec, quiver.symmetrify.lift_spec],
 end
 
-lemma lift_unique (φ : prefunctor V V') (Φ : free_groupoid V ⥤ V')
-  (hΦ : (of V).comp Φ.to_prefunctor = φ) : Φ = (lift φ) :=
+lemma lift_unique (φ : V ⥤q V') (Φ : free_groupoid V ⥤ V')
+  (hΦ : of V ⋙q Φ.to_prefunctor = φ) : Φ = lift φ :=
 begin
   apply quotient.lift_unique,
   apply paths.lift_unique,
@@ -186,8 +185,8 @@ section functoriality
 variables {V' : Type u'} [quiver.{v'+1} V'] {V'' : Type u''} [quiver.{v''+1} V'']
 
 /-- The functor of free groupoid induced by a prefunctor of quivers -/
-def _root_.category_theory.free_groupoid_functor (φ : prefunctor V V') :
-  free_groupoid V ⥤ free_groupoid V' := lift (φ.comp (of V'))
+def _root_.category_theory.free_groupoid_functor (φ : V ⥤q V') :
+  free_groupoid V ⥤ free_groupoid V' := lift (φ ⋙q of V')
 
 lemma free_groupoid_functor_id :
   free_groupoid_functor (prefunctor.id V) = functor.id (free_groupoid V) :=
@@ -197,8 +196,8 @@ begin
 end
 
 lemma free_groupoid_functor_comp
-  (φ : prefunctor V V') (φ' : prefunctor V' V'') :
-  free_groupoid_functor (φ.comp φ') = (free_groupoid_functor φ) ⋙ (free_groupoid_functor φ') :=
+  (φ : V ⥤q V') (φ' : V' ⥤q V'') :
+  free_groupoid_functor (φ ⋙q φ') = free_groupoid_functor φ ⋙ free_groupoid_functor φ' :=
 begin
   dsimp only [free_groupoid_functor], symmetry,
   apply lift_unique, refl,
diff --git a/src/category_theory/path_category.lean b/src/category_theory/path_category.lean
@@ -46,14 +46,14 @@ variables {V}
 The inclusion of a quiver `V` into its path category, as a prefunctor.
 -/
 @[simps]
-def of : prefunctor V (paths V) :=
+def of : V ⥤q (paths V) :=
 { obj := λ X, X,
   map := λ X Y f, f.to_path, }
 
 local attribute [ext] functor.ext
 
 /-- Any prefunctor from `V` lifts to a functor from `paths V` -/
-def lift {C} [category C] (φ : prefunctor V C) : (paths V) ⥤ C :=
+def lift {C} [category C] (φ : V ⥤q C) : paths V ⥤ C :=
 { obj := φ.obj,
   map := λ X Y f, @quiver.path.rec V _ X (λ Y f, φ.obj X ⟶ φ.obj Y) (𝟙 $ φ.obj X)
                   (λ Y Z p f ihp, ihp ≫ (φ.map f)) Y f,
@@ -64,18 +64,18 @@ def lift {C} [category C] (φ : prefunctor V C) : (paths V) ⥤ C :=
     { have : f ≫ g'.cons p = (f ≫ g').cons p, by apply quiver.path.comp_cons,
       rw this, simp only, rw [ih, category.assoc], } } }
 
-@[simp] lemma lift_nil {C} [category C] (φ : prefunctor V C) (X : V) :
+@[simp] lemma lift_nil {C} [category C] (φ : V ⥤q C) (X : V) :
   (lift φ).map (quiver.path.nil) = 𝟙 (φ.obj X) := rfl
 
-@[simp] lemma lift_cons {C} [category C] (φ : prefunctor V C) {X Y Z : V}
+@[simp] lemma lift_cons {C} [category C] (φ : V ⥤q C) {X Y Z : V}
   (p : quiver.path X Y) (f : Y ⟶ Z) :
   (lift φ).map (p.cons f) = (lift φ).map p ≫ (φ.map f) := rfl
 
-@[simp] lemma lift_to_path {C} [category C] (φ : prefunctor V C) {X Y : V} (f : X ⟶ Y) :
+@[simp] lemma lift_to_path {C} [category C] (φ : V ⥤q C) {X Y : V} (f : X ⟶ Y) :
   (lift φ).map f.to_path = φ.map f := by {dsimp [quiver.hom.to_path,lift], simp, }
 
-lemma lift_spec {C} [category C] (φ : prefunctor V C) :
-  of.comp (lift φ).to_prefunctor = φ :=
+lemma lift_spec {C} [category C] (φ : V ⥤q C) :
+  of ⋙q (lift φ).to_prefunctor = φ :=
 begin
   apply prefunctor.ext, rotate,
   { rintro X, refl, },
@@ -84,8 +84,8 @@ begin
     simp only [category.id_comp], },
 end
 
-lemma lift_unique {C} [category C] (φ : prefunctor V C) (Φ : paths V ⥤ C)
-  (hΦ : of.comp Φ.to_prefunctor = φ) : Φ = lift φ :=
+lemma lift_unique {C} [category C] (φ : V ⥤q C) (Φ : paths V ⥤ C)
+  (hΦ : of ⋙q Φ.to_prefunctor = φ) : Φ = lift φ :=
 begin
   subst_vars,
   apply functor.ext, rotate,
@@ -122,8 +122,7 @@ end paths
 variables (W : Type u₂) [quiver.{v₂+1} W]
 
 -- A restatement of `prefunctor.map_path_comp` using `f ≫ g` instead of `f.comp g`.
-@[simp] lemma prefunctor.map_path_comp' (F : prefunctor V W)
-  {X Y Z : paths V} (f : X ⟶ Y) (g : Y ⟶ Z) :
+@[simp] lemma prefunctor.map_path_comp' (F : V ⥤q W) {X Y Z : paths V} (f : X ⟶ Y) (g : Y ⟶ Z) :
   F.map_path (f ≫ g) = (F.map_path f).comp (F.map_path g) :=
 prefunctor.map_path_comp _ _ _
 
diff --git a/src/combinatorics/quiver/basic.lean b/src/combinatorics/quiver/basic.lean
@@ -90,12 +90,13 @@ def comp {U : Type*} [quiver U] {V : Type*} [quiver V] {W : Type*} [quiver W]
 lemma comp_assoc
   {U V W Z : Type*} [quiver U] [quiver V] [quiver W] [quiver Z]
   (F : prefunctor U V) (G : prefunctor V W) (H : prefunctor W Z) :
-  (F.comp G).comp H = F.comp (G.comp H) :=
-begin
-  apply prefunctor.ext, rotate,
-  { rintro X, refl, },
-  { rintro X Y Z, refl, }
-end
+  (F.comp G).comp H = F.comp (G.comp H) := rfl
+
+infix ` ⥤q `:50 := prefunctor
+
+infix ` ⋙q `:50 := prefunctor.comp
+
+notation `𝟭q` := id
 
 end prefunctor
 
diff --git a/src/combinatorics/quiver/path.lean b/src/combinatorics/quiver/path.lean
@@ -142,7 +142,7 @@ namespace prefunctor
 
 open quiver
 
-variables {V : Type u₁} [quiver.{v₁} V] {W : Type u₂} [quiver.{v₂} W] (F : prefunctor V W)
+variables {V : Type u₁} [quiver.{v₁} V] {W : Type u₂} [quiver.{v₂} W] (F : V ⥤q W)
 
 /-- The image of a path under a prefunctor. -/
 def map_path {a : V} :
