Category of groupoids

This file contains the definition of the category Grpd of all groupoids. In this category objects are groupoids and morphisms are functors between these groupoids.

We also provide two “forgetting” functors: objects : Grpd ⥤ Type and forgetToCat : Grpd ⥤ Cat.

Implementation notes

Though Grpd is not a concrete category, we use Bundled to define its carrier type.

def CategoryTheory.Grpd : Type (max (u + 1) u (v + 1))

Category of groupoids

@[implicit_reducible]

instance CategoryTheory.Grpd.instInhabited : Inhabited Grpd

@[implicit_reducible]

instance CategoryTheory.Grpd.str' (C : Grpd) : Groupoid ↑C

@[implicit_reducible]

instance CategoryTheory.Grpd.instCoeSortType : CoeSort Grpd (Type u_1)

def CategoryTheory.Grpd.of (C : Type u) [Groupoid C] : Grpd

Construct a bundled Grpd from the underlying type and the typeclass Groupoid.

@[simp]

theorem CategoryTheory.Grpd.coe_of (C : Type u) [Groupoid C] : ↑(of C) = C

@[implicit_reducible]

instance CategoryTheory.Grpd.category : LargeCategory Grpd

Category structure on Grpd

def CategoryTheory.Grpd.objects : Functor Grpd (Type u)

Functor that gets the set of objects of a groupoid. It is not called forget, because it is not a faithful functor.

def CategoryTheory.Grpd.forgetToCat : Functor Grpd Cat

Forgetting functor to Cat

@[implicit_reducible]

instance CategoryTheory.Grpd.instGroupoidαCategoryObjCatForgetToCat (X : Grpd) : Groupoid ↑(forgetToCat.obj X)

instance CategoryTheory.Grpd.forgetToCat_full : forgetToCat.Full

instance CategoryTheory.Grpd.forgetToCat_faithful : forgetToCat.Faithful

theorem CategoryTheory.Grpd.comp_eq_comp {C D E : Grpd} (f : C ⟶ D) (g : D ⟶ E) : CategoryStruct.comp f g = Functor.comp f g

Convert arrows in the category of groupoids to functors, which sometimes helps in applying simp lemmas

theorem CategoryTheory.Grpd.id_eq_id {C : Grpd} : CategoryStruct.id C = Functor.id ↑C

Converts identity in the category of groupoids to the functor identity

def CategoryTheory.Grpd.piLimitFan ⦃J : Type u⦄ (F : J → Grpd) : Limits.Fan F

Construct the product over an indexed family of groupoids, as a fan.

def CategoryTheory.Grpd.piLimitFanIsLimit ⦃J : Type u⦄ (F : J → Grpd) : Limits.IsLimit (piLimitFan F)

The product fan over an indexed family of groupoids, is a limit cone.

instance CategoryTheory.Grpd.has_pi : Limits.HasProducts Grpd

noncomputable def CategoryTheory.Grpd.piIsoPi (J : Type u) (f : J → Grpd) : of ((j : J) → ↑(f j)) ≅ ∏ᶜ f

The product of a family of groupoids is isomorphic to the product object in the category of Groupoids

@[simp]

theorem CategoryTheory.Grpd.piIsoPi_hom_π (J : Type u) (f : J → Grpd) (j : J) : CategoryStruct.comp (piIsoPi J f).hom (Limits.Pi.π f j) = Pi.eval (fun (i : J) => ↑(f i)) j