## Stream: Is there code for X?

### Topic: isomorphisms define category

#### 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?

#### Yury G. Kudryashov (Jun 29 2020 at 00:05):

category_theory/core

#### Alena Gusakov (Jun 29 2020 at 00:27):

Thanks!

Last updated: May 19 2021 at 02:10 UTC