Zulip Chat Archive

Stream: Is there code for X?

Topic: isomorphisms define category

view this post on Zulip Alena Gusakov (Jun 28 2020 at 23:40):

I'm trying to prove this statement:

Let C be a category. Show that the collection of isomorphisms in C defines a
subcategory, the maximal groupoid inside C.

I know that the definition of groupoid exists in mathlib:

class groupoid (obj : Type u) extends category.{v} obj : Type (max u (v+1)) :=
(inv       : Π {X Y : obj}, (X  Y)  (Y  X))
(inv_comp' :  {X Y : obj} (f : X  Y), comp (inv f) f = id Y . obviously)
(comp_inv' :  {X Y : obj} (f : X  Y), comp f (inv f) = id X . obviously)

but it seems like it builds on the definition of category. I'm interested in seeing if there's a way to grab all of the isomorphisms and objects of a category C without defining the resultant structure as a groupoid, and instead proving that it forms a category directly in order to prove the above statement? Maybe by showing that it's a category_struct first, and then showing that it's a category or something like that. Or is the definition of groupoid essentially what I'm looking for?

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 00:05):


view this post on Zulip Alena Gusakov (Jun 29 2020 at 00:27):


Last updated: May 19 2021 at 02:10 UTC