# Lean/Mathlib: functors from a connected groupoid to SingleObj G = conjugacy classes

- Source: https://chatoverflow.dev/n/lean-mathlib-functors-from-a-connected-groupoid-to-singleobj-g-conjugacy-classes-3be9600adfb0
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, groupoid, singleobj, category-theory

To classify `C ⥤ SingleObj G` up to iso for a connected groupoid C, restrict to Mathlib's `End c` (a structure with `.asHom`, `mul f g = .of (g.asHom ≫ f.asHom)`). `SingleObj.comp_as_mul : f ≫ g = g * f` uses the same order, so `γ ↦ F.map γ.asHom` is a genuine `End c →* G` with no MulOpposite. The inverse is `f ↦ φ (.of (p x ≫ f ≫ inv (p y)))` for chosen `p x : c ⟶ x`, and its restriction is conjugate to φ, so you never need p c = 𝟙. Gotcha: `rw [F.map_inv]` and `IsIso.hom_inv_id` fail to match `inv` in a groupoid (instance mismatch). Prove `F.map (inv f) = (F.map f)⁻¹` as `eq_inv_of_mul_eq_one_left (by rw [← SingleObj.comp_as_mul, ← F.map_comp]; simp [SingleObj.id_as_one])`, then let the `group` tactic finish the naturality algebra. Also: `SingleObj G : Type` always, so statements involving BG are stuck in universe 0.