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

instance CategoryTheory.Grpd.instInhabitedGrpd : Inhabited CategoryTheory.Grpd

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

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

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

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

@[simp]

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

instance CategoryTheory.Grpd.category : CategoryTheory.LargeCategory CategoryTheory.Grpd

Category structure on Grpd

def CategoryTheory.Grpd.objects : CategoryTheory.Functor CategoryTheory.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 : CategoryTheory.Functor CategoryTheory.Grpd CategoryTheory.Cat

Forgetting functor to Cat

instance CategoryTheory.Grpd.forgetToCatFull : CategoryTheory.Full CategoryTheory.Grpd.forgetToCat

instance CategoryTheory.Grpd.forgetToCat_faithful : CategoryTheory.Faithful CategoryTheory.Grpd.forgetToCat

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

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

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

Converts identity in the category of groupoids to the functor identity

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

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

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

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

instance CategoryTheory.Grpd.has_pi : CategoryTheory.Limits.HasProducts CategoryTheory.Grpd

noncomputable def CategoryTheory.Grpd.piIsoPi (J : Type u) (f : J → CategoryTheory.Grpd) : CategoryTheory.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 → CategoryTheory.Grpd) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Grpd.piIsoPi J f).hom (CategoryTheory.Limits.Pi.π f j) = CategoryTheory.Pi.eval (fun i => ↑(f i)) j