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.

source

@[nolint]

def category_theory.Groupoid :

Type (max (u+1) u (v+1))

Category of groupoids

Equations

category_theory.Groupoid = category_theory.bundled category_theory.groupoid

source

@[protected, instance]

def category_theory.Groupoid.inhabited :

inhabited category_theory.Groupoid

Equations

category_theory.Groupoid.inhabited = {default := category_theory.bundled.of (category_theory.single_obj punit) (category_theory.single_obj.groupoid punit)}

source

@[protected, instance]

def category_theory.Groupoid.str (C : category_theory.Groupoid) :

category_theory.groupoid C.α

Equations

C.str = C.str

source

def category_theory.Groupoid.of (C : Type u) [category_theory.groupoid C] :

category_theory.Groupoid

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

Equations

category_theory.Groupoid.of C = category_theory.bundled.of C

source

@[protected, instance]

def category_theory.Groupoid.category :

category_theory.large_category category_theory.Groupoid

Category structure on Groupoid

Equations

category_theory.Groupoid.category = {to_category_struct := {to_quiver := {hom := λ (C D : category_theory.Groupoid), C.α ⥤ D.α}, id := λ (C : category_theory.Groupoid), 𝟭 C.α, comp := λ (C D E : category_theory.Groupoid) (F : C ⟶ D) (G : D ⟶ E), F ⋙ G}, id_comp' := category_theory.Groupoid.category._proof_1, comp_id' := category_theory.Groupoid.category._proof_2, assoc' := category_theory.Groupoid.category._proof_3}

source

def category_theory.Groupoid.objects :

category_theory.Groupoid ⥤ Type u

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

Equations

category_theory.Groupoid.objects = {obj := category_theory.bundled.α category_theory.groupoid, map := λ (C D : category_theory.Groupoid) (F : C ⟶ D), F.obj, map_id' := category_theory.Groupoid.objects._proof_1, map_comp' := category_theory.Groupoid.objects._proof_2}

source

def category_theory.Groupoid.forget_to_Cat :

category_theory.Groupoid ⥤ category_theory.Cat

Forgetting functor to Cat

Equations

category_theory.Groupoid.forget_to_Cat = {obj := λ (C : category_theory.Groupoid), category_theory.Cat.of C.α, map := λ (C D : category_theory.Groupoid), id, map_id' := category_theory.Groupoid.forget_to_Cat._proof_1, map_comp' := category_theory.Groupoid.forget_to_Cat._proof_2}

source

@[protected, instance]

def category_theory.Groupoid.forget_to_Cat_full :

category_theory.full category_theory.Groupoid.forget_to_Cat

Equations

category_theory.Groupoid.forget_to_Cat_full = {preimage := λ (C D : category_theory.Groupoid), id, witness' := category_theory.Groupoid.forget_to_Cat_full._proof_1}

source

@[protected, instance]

def category_theory.Groupoid.forget_to_Cat_faithful :

category_theory.faithful category_theory.Groupoid.forget_to_Cat

source

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

source

@[simp]

theorem category_theory.Groupoid.pi_limit_cone_is_limit_lift {J : Type u} (F : category_theory.discrete J ⥤ category_theory.Groupoid) (s : category_theory.limits.cone F) :

(category_theory.Groupoid.pi_limit_cone F).is_limit.lift s = category_theory.functor.pi' s.π.app

source

def category_theory.Groupoid.pi_limit_cone {J : Type u} (F : category_theory.discrete J ⥤ category_theory.Groupoid) :

category_theory.limits.limit_cone F

The cone for the product of a family of groupoids indexed by J is a limit cone

Equations

category_theory.Groupoid.pi_limit_cone F = {cone := {X := category_theory.Groupoid.of (Π (j : J), (F.obj j).α) category_theory.groupoid_pi, π := {app := λ (j : J), category_theory.pi.eval (λ (j : J), (F.obj j).α) j, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F), category_theory.functor.pi' s.π.app, fac' := _, uniq' := _}}

source

@[simp]

theorem category_theory.Groupoid.pi_limit_cone_cone_X {J : Type u} (F : category_theory.discrete J ⥤ category_theory.Groupoid) :

(category_theory.Groupoid.pi_limit_cone F).cone.X = category_theory.Groupoid.of (Π (j : J), (F.obj j).α)

source

@[simp]

theorem category_theory.Groupoid.pi_limit_cone_cone_π_app {J : Type u} (F : category_theory.discrete J ⥤ category_theory.Groupoid) (j : J) :

(category_theory.Groupoid.pi_limit_cone F).cone.π.app j = category_theory.pi.eval (λ (j : J), (F.obj j).α) j

source

def category_theory.Groupoid.pi_limit_fan {J : Type u} (F : J → category_theory.Groupoid) :

category_theory.limits.fan F

pi_limit_cone reinterpreted as a fan

source

@[protected, instance]

def category_theory.Groupoid.has_pi :

category_theory.limits.has_products category_theory.Groupoid

source

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

category_theory.Groupoid.pi_iso_pi J f = (category_theory.Groupoid.pi_limit_cone (category_theory.discrete.functor f)).is_limit.cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit (category_theory.discrete.functor f))

source

@[simp]

theorem category_theory.Groupoid.pi_iso_pi_hom_π (J : Type u) (f : J → category_theory.Groupoid) (j : J) :

(category_theory.Groupoid.pi_iso_pi J f).hom ≫ category_theory.limits.pi.π f j = category_theory.pi.eval (λ (j : J), (f j).α) j