A connected groupoid is equivalent to its vertex group

Let C be a groupoid and x₀ : C a weakly initial object, that is, one which admits a morphism to every object. This file proves that the one-object category SingleObj (End x₀) of the vertex group at x₀ is equivalent to C, through the functor sending the unique object to x₀ and an endomorphism to itself.

Both halves are immediate once the functor is written down. It is fully faithful in any category, because its action on the single hom-set is the identity of End x₀, and it is essentially surjective because in a groupoid a morphism x₀ ⟶ x is already an isomorphism. What the equivalence buys is a dictionary: functors out of C become functors out of SingleObj (End x₀), that is, objects with an action of the vertex group, and the dictionary is natural in the target category; TauCeti.Groupoid.natIsoOfEnd in TauCeti.CategoryTheory.Groupoid.ConnectedFunctor is that dictionary applied to isomorphisms.

The weak initiality hypothesis is stated as the family of nonemptiness assertions ∀ x, Nonempty (x₀ ⟶ x) rather than through CategoryTheory.IsConnected: the intended source of that data is a path-connected topological space, whose fundamental groupoid comes with paths out of a chosen basepoint.

For a monoid M, a functor from such a groupoid to SingleObj M is determined by its values on the morphisms out of x₀ (TauCeti.Groupoid.functor_singleObj_ext_of_map_eq).

Main declarations

• TauCeti.Groupoid.singleObjFunctor: the functor SingleObj (End x₀) ⥤ C picking out x₀.
• TauCeti.Groupoid.fullyFaithfulSingleObjFunctor: it is fully faithful, without hypotheses.
• TauCeti.Groupoid.essSurj_singleObjFunctor and TauCeti.Groupoid.isEquivalence_singleObjFunctor: it is essentially surjective, hence an equivalence, when x₀ admits a morphism to every object.
• TauCeti.Groupoid.singleObjEquivalence: a connected groupoid is equivalent to the one-object category of its vertex group.
• TauCeti.Groupoid.functorOfEndHom: the functor to SingleObj G induced by a homomorphism End x₀ →* G and a choice of morphisms out of x₀.
• TauCeti.Groupoid.functor_singleObj_ext_of_map_eq: functors from a connected groupoid to SingleObj M are determined by their values on the morphisms out of one object.

def TauCeti.Groupoid.singleObjFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (x₀ : C) : CategoryTheory.Functor (CategoryTheory.SingleObj (CategoryTheory.End x₀)) C

The functor from the one-object category of the vertex group at x₀ that sends the unique object to x₀ and an endomorphism to itself.

It is @[expose]d so that the object and morphism equations hold by rfl downstream.

Equations

• TauCeti.Groupoid.singleObjFunctor x₀ = CategoryTheory.SingleObj.functor (MonoidHom.id (CategoryTheory.End x₀))

@[simp]

theorem TauCeti.Groupoid.singleObjFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (x₀ : C) (a : CategoryTheory.SingleObj (CategoryTheory.End x₀)) : (singleObjFunctor x₀).obj a = x₀

@[simp]

theorem TauCeti.Groupoid.singleObjFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] (x₀ : C) (g : CategoryTheory.End x₀) : (singleObjFunctor x₀).map g = g

def TauCeti.Groupoid.fullyFaithfulSingleObjFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (x₀ : C) : (singleObjFunctor x₀).FullyFaithful

The functor out of the one-object category of the vertex group is fully faithful: on the single hom-set it is the identity of End x₀.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.Groupoid.singleObjFunctor_full {C : Type u} [CategoryTheory.Category.{v, u} C] (x₀ : C) : (singleObjFunctor x₀).Full

instance TauCeti.Groupoid.singleObjFunctor_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] (x₀ : C) : (singleObjFunctor x₀).Faithful

theorem TauCeti.Groupoid.essSurj_singleObjFunctor {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) : (singleObjFunctor x₀).EssSurj

If x₀ admits a morphism to every object of the groupoid, then every object is isomorphic to x₀, so the functor out of the one-object category is essentially surjective.

theorem TauCeti.Groupoid.isEquivalence_singleObjFunctor {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) : (singleObjFunctor x₀).IsEquivalence

If x₀ admits a morphism to every object of the groupoid, the functor out of the one-object category of the vertex group is an equivalence.

noncomputable def TauCeti.Groupoid.singleObjEquivalence {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) : CategoryTheory.SingleObj (CategoryTheory.End x₀) ≌ C

A connected groupoid is equivalent to the one-object category of its vertex group.

The equivalence is induced by TauCeti.Groupoid.singleObjFunctor, so it sends the unique object to x₀ and an endomorphism to itself.

Equations

• TauCeti.Groupoid.singleObjEquivalence x₀ hconn = (TauCeti.Groupoid.singleObjFunctor x₀).asEquivalence

@[simp]

theorem TauCeti.Groupoid.singleObjEquivalence_functor {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) : (singleObjEquivalence x₀ hconn).functor = singleObjFunctor x₀

noncomputable def TauCeti.Groupoid.functorOfEndHom {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (τ : (y : C) → x₀ ⟶ y) {G : Type u_1} [Monoid G] (f : CategoryTheory.End x₀ →* G) : CategoryTheory.Functor C (CategoryTheory.SingleObj G)

A monoid homomorphism f out of the vertex group at x₀, together with a choice of morphisms τ y : x₀ ⟶ y for every object y, induces a functor from the whole groupoid to SingleObj G: a morphism g : y ⟶ z is sent to the image under f of the loop τ y ≫ g ≫ inv (τ z) at x₀.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Groupoid.functorOfEndHom_obj {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (τ : (y : C) → x₀ ⟶ y) {G : Type u_1} [Monoid G] (f : CategoryTheory.End x₀ →* G) (y : C) : (functorOfEndHom x₀ τ f).obj y = CategoryTheory.SingleObj.star G

@[simp]

theorem TauCeti.Groupoid.functorOfEndHom_map {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (τ : (y : C) → x₀ ⟶ y) {G : Type u_1} [Monoid G] (f : CategoryTheory.End x₀ →* G) {y z : C} (g : y ⟶ z) : (functorOfEndHom x₀ τ f).map g = f (CategoryTheory.CategoryStruct.comp (τ y) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv (τ z))))

theorem TauCeti.Groupoid.functor_singleObj_ext_of_map_eq {M : Type u_1} [Monoid M] {C : Type u} [CategoryTheory.Groupoid C] (x₀ : C) (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) {F F' : CategoryTheory.Functor C (CategoryTheory.SingleObj M)} (h : ∀ (x : C) (f : x₀ ⟶ x), F.map f = F'.map f) : F = F'

In a groupoid, two functors to the one-object category of a monoid are equal once they agree on every morphism out of an object x₀ which admits a morphism to every object.