# mathlibdocumentation

category_theory.category.Groupoid

# Category of groupoids #

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

We also provide two “forgetting” functors: objects : Groupoid ⥤ Type and forget_to_Cat : Groupoid ⥤ Cat.

## Implementation notes #

Though Groupoid is not a concrete category, we use bundled to define its carrier type.

@[nolint]
def category_theory.Groupoid  :
Type (max (u+1) u (v+1))

Category of groupoids

Equations
Instances for category_theory.Groupoid
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations
@[simp]
theorem category_theory.Groupoid.coe_of (C : Type u)  :
@[protected, instance]

Category structure on Groupoid

Equations

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

Equations

Forgetting functor to Cat

Equations
Instances for category_theory.Groupoid.forget_to_Cat
@[protected, instance]
Equations
@[protected, instance]
theorem category_theory.Groupoid.hom_to_functor {C D E : category_theory.Groupoid} (f : C D) (g : D E) :
f g = f g

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

Converts identity in the category of groupoids to the functor identity

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

Equations

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

Equations
@[protected, instance]
noncomputable def category_theory.Groupoid.pi_iso_pi (J : Type u) (f : J → category_theory.Groupoid) :
category_theory.Groupoid.of (Π (j : J), (f j)) f

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

Equations
@[simp]
theorem category_theory.Groupoid.pi_iso_pi_hom_π (J : Type u) (f : J → category_theory.Groupoid) (j : J) :
= category_theory.pi.eval (λ (j : J), (f j)) j