## Stream: Is there code for X?

### Topic: Monoid instance on End(X)

#### Adam Topaz (Sep 25 2020 at 16:24):

If $\mathscr{C}$ is any category, and $X$ is an object of $\mathscr{C}$, then $\operatorname{Hom}(X,X)$ has an obvious monoid structure. Does this exist in mathlib?
apply_instance comes up empty here:

import algebra
import category_theory.category

open category_theory

variables {C : Type*} [category C]
variables {X : C}

example : monoid (X ⟶ X) := by apply_instance


If it's not already in mathlib, does it make sense to introduce such an instance?

#### Bhavik Mehta (Sep 25 2020 at 16:25):

Look in ct.endomorphism

#### Adam Topaz (Sep 25 2020 at 16:26):

Thanks!

Last updated: May 07 2021 at 21:10 UTC