feat: free groupoid on a category, free-forgetful adjunction (#29279)

- define `CategoryTheory.FreeGroupoid`
- show the universal property of this construction, as the initial category localizing all maps in the category. These are the defs `of`, `lift`, and their related theorems
- Show that this construction is functorial `CategoryTheory.FreeGroupoid.map`
- Convert this to a functor `CategoryTheory.Grpd.free` from `Cat` to `Grpd`, and show that it is left adjoint to the forgetful functor
- `CategoryTheory.Grpd.freeForgetAdjunction`

Co-authored-by: jlh18 <josephhua73@yahoo.com>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: Jlh18

Mathlib.lean

@@ -2398,6 +2398,7 @@ import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Groupoid.Basic
 import Mathlib.CategoryTheory.Groupoid.Discrete
 import Mathlib.CategoryTheory.Groupoid.FreeGroupoid
+import Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
 import Mathlib.CategoryTheory.Groupoid.Subgroupoid
 import Mathlib.CategoryTheory.Groupoid.VertexGroup
 import Mathlib.CategoryTheory.GuitartExact.Basic

Mathlib/CategoryTheory/Category/Grpd.lean

@@ -74,6 +74,8 @@ def forgetToCat : Grpd.{v, u} ⥤ Cat.{v, u} where
   obj C := Cat.of C
   map := id
 
+instance (X : Grpd) : Groupoid (Grpd.forgetToCat.obj X) := inferInstanceAs (Groupoid X)
+
 instance forgetToCat_full : forgetToCat.Full where map_surjective f := ⟨f, rfl⟩
 
 instance forgetToCat_faithful : forgetToCat.Faithful where

Mathlib/CategoryTheory/Functor/Basic.lean

@@ -137,6 +137,14 @@ theorem map_dite (F : C ⥤ D) {X Y : C} {P : Prop} [Decidable P]
 theorem toPrefunctor_comp (F : C ⥤ D) (G : D ⥤ E) :
     F.toPrefunctor.comp G.toPrefunctor = (F ⋙ G).toPrefunctor := rfl
 
+lemma toPrefunctor_injective {F G : C ⥤ D} (h : F.toPrefunctor = G.toPrefunctor) :
+    F = G := by
+  obtain ⟨obj, map, _, _⟩ := F
+  obtain ⟨obj', map', _, _⟩ := G
+  obtain rfl : obj = obj' := congr_arg Prefunctor.obj h
+  obtain rfl : @map = @map' := by simpa [Functor.toPrefunctor] using h
+  rfl
+
 end
 
 end Functor

Mathlib/CategoryTheory/Groupoid.lean

@@ -9,6 +9,7 @@ import Mathlib.CategoryTheory.Pi.Basic
 import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.Combinatorics.Quiver.Symmetric
 import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
+import Mathlib.CategoryTheory.MorphismProperty.Basic
 
 /-!
 # Groupoids
@@ -186,4 +187,15 @@ instance isGroupoidProd {α : Type u} {β : Type u₂} [Category.{v} α] [Catego
 
 end
 
+open MorphismProperty in
+lemma isGroupoid_iff_isomorphisms_eq_top (C : Type*) [Category C] :
+    IsGroupoid C ↔ isomorphisms C = ⊤ := by
+  constructor
+  · rw [eq_top_iff]
+    intro _ _
+    simp only [isomorphisms.iff, top_apply]
+    infer_instance
+  · intro h
+    exact ⟨of_eq_top h⟩
+
 end CategoryTheory

Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

@@ -16,10 +16,10 @@ extension as a functor from the free groupoid, and proves uniqueness of this ext
 
 Given the type `V` and a quiver instance on `V`:
 
-- `FreeGroupoid V`: a type synonym for `V`.
-- `FreeGroupoid.instGroupoid`: the `Groupoid` instance on `FreeGroupoid V`.
+- `Quiver.FreeGroupoid V`: a type synonym for `V`.
+- `Quiver.FreeGroupoid.instGroupoid`: the `Groupoid` instance on `Quiver.FreeGroupoid V`.
 - `lift`: the lifting of a prefunctor from `V` to `V'` where `V'` is a groupoid, to a functor.
-  `FreeGroupoid V ⥤ V'`.
+  `Quiver.FreeGroupoid V ⥤ V'`.
 - `lift_spec` and `lift_unique`: the proofs that, respectively, `lift` indeed is a lifting
   and is the unique one.
 
@@ -56,16 +56,14 @@ inductive FreeGroupoid.redStep : HomRel (Paths (Quiver.Symmetrify V))
     redStep (𝟙 ((Paths.of (Quiver.Symmetrify V)).obj X)) (f.toPath ≫ (Quiver.reverse f).toPath)
 
 /-- The underlying vertices of the free groupoid -/
-def FreeGroupoid (V) [Q : Quiver V] :=
+protected def FreeGroupoid (V) [Q : Quiver V] :=
   CategoryTheory.Quotient (@FreeGroupoid.redStep V Q)
 
-@[deprecated (since := "2025-10-02")] alias _root_.CategoryTheory.FreeGroupoid := FreeGroupoid
-
 namespace FreeGroupoid
 
 open Quiver
 
-instance {V} [Quiver V] [Nonempty V] : Nonempty (FreeGroupoid V) := by
+instance {V} [Quiver V] [Nonempty V] : Nonempty (Quiver.FreeGroupoid V) := by
   inhabit V; exact ⟨⟨@default V _⟩⟩
 
 theorem congr_reverse {X Y : Paths <| Quiver.Symmetrify V} (p q : X ⟶ Y) :
@@ -113,21 +111,21 @@ theorem congr_reverse_comp {X Y : Paths <| Quiver.Symmetrify V} (p : X ⟶ Y) :
   nth_rw 2 [← Quiver.Path.reverse_reverse p]
   apply congr_comp_reverse
 
-instance : Category (FreeGroupoid V) :=
+instance : Category (Quiver.FreeGroupoid V) :=
   Quotient.category redStep
 
 /-- The inverse of an arrow in the free groupoid -/
-def quotInv {X Y : FreeGroupoid V} (f : X ⟶ Y) : Y ⟶ X :=
+def quotInv {X Y : Quiver.FreeGroupoid V} (f : X ⟶ Y) : Y ⟶ X :=
   Quot.liftOn f (fun pp => Quot.mk _ <| pp.reverse) fun pp qq con =>
     Quot.sound <| congr_reverse pp qq con
 
-instance instGroupoid : Groupoid (FreeGroupoid V) where
+instance instGroupoid : Groupoid (Quiver.FreeGroupoid V) where
   inv := quotInv
   inv_comp p := Quot.inductionOn p fun pp => congr_reverse_comp pp
   comp_inv p := Quot.inductionOn p fun pp => congr_comp_reverse pp
 
 /-- The inclusion of the quiver on `V` to the underlying quiver on `FreeGroupoid V` -/
-def of (V) [Quiver V] : V ⥤q FreeGroupoid V where
+def of (V) [Quiver V] : V ⥤q Quiver.FreeGroupoid V where
   obj X := ⟨X⟩
   map f := Quot.mk _ f.toPosPath
 
@@ -140,7 +138,7 @@ section UniversalProperty
 variable {V' : Type u'} [Groupoid V']
 
 /-- The lift of a prefunctor to a groupoid, to a functor from `FreeGroupoid V` -/
-def lift (φ : V ⥤q V') : FreeGroupoid V ⥤ V' :=
+def lift (φ : V ⥤q V') : Quiver.FreeGroupoid V ⥤ V' :=
   CategoryTheory.Quotient.lift _ (Paths.lift <| Quiver.Symmetrify.lift φ) <| by
     rintro _ _ _ _ ⟨X, Y, f⟩
     -- Porting note: `simp` does not work, so manually `rewrite`
@@ -154,8 +152,8 @@ theorem lift_spec (φ : V ⥤q V') : of V ⋙q (lift φ).toPrefunctor = φ := by
   dsimp [lift]
   rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]
 
-theorem lift_unique (φ : V ⥤q V') (Φ : FreeGroupoid V ⥤ V') (hΦ : of V ⋙q Φ.toPrefunctor = φ) :
-    Φ = lift φ := by
+theorem lift_unique (φ : V ⥤q V') (Φ : Quiver.FreeGroupoid V ⥤ V')
+    (hΦ : of V ⋙q Φ.toPrefunctor = φ) : Φ = lift φ := by
   apply Quotient.lift_unique
   apply Paths.lift_unique
   fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _
@@ -179,11 +177,11 @@ open FreeGroupoid
 variable {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 freeGroupoidFunctor (φ : V ⥤q V') : FreeGroupoid V ⥤ FreeGroupoid V' :=
+def freeGroupoidFunctor (φ : V ⥤q V') : Quiver.FreeGroupoid V ⥤ Quiver.FreeGroupoid V' :=
   lift (φ ⋙q of V')
 
 theorem freeGroupoidFunctor_id :
-    freeGroupoidFunctor (Prefunctor.id V) = Functor.id (FreeGroupoid V) := by
+    freeGroupoidFunctor (Prefunctor.id V) = Functor.id (Quiver.FreeGroupoid V) := by
   dsimp only [freeGroupoidFunctor]; symm
   apply lift_unique; rfl