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

Equations

• CategoryTheory.Grpd = CategoryTheory.Bundled CategoryTheory.Groupoid

instance CategoryTheory.Grpd.instInhabited : Inhabited CategoryTheory.Grpd

Equations

• CategoryTheory.Grpd.instInhabited = { default := CategoryTheory.Bundled.of (CategoryTheory.SingleObj PUnit.{?u.5 + 1}) }

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

Equations

• C.str' = C.str

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

Equations

• CategoryTheory.Grpd.instCoeSortType = CategoryTheory.Bundled.coeSort

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

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

Equations

• CategoryTheory.Grpd.of C = CategoryTheory.Bundled.of C

@[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

Equations

• CategoryTheory.Grpd.category = CategoryTheory.Category.mk @CategoryTheory.Grpd.category.proof_1 @CategoryTheory.Grpd.category.proof_2 @CategoryTheory.Grpd.category.proof_3

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.

Equations

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

def CategoryTheory.Grpd.forgetToCat : CategoryTheory.Functor CategoryTheory.Grpd CategoryTheory.Cat

Forgetting functor to Cat

Equations

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

instance CategoryTheory.Grpd.forgetToCat_full : CategoryTheory.Grpd.forgetToCat.Full

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

theorem CategoryTheory.Grpd.hom_to_functor {C D 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.

Equations

• CategoryTheory.Grpd.piLimitFan F = CategoryTheory.Limits.Fan.mk (CategoryTheory.Grpd.of ((j : J) → ↑(F j))) fun (j : J) => CategoryTheory.Pi.eval (fun (j : J) => ↑(F j)) j

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.

Equations

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

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

Equations

• CategoryTheory.Grpd.piIsoPi J f = (CategoryTheory.Grpd.piLimitFanIsLimit f).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor f))

@[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 : J) => ↑(f i)) j