Zulip Chat Archive

Stream: Is there code for X?

Topic: Monoid instance on End(X)


view this post on Zulip Adam Topaz (Sep 25 2020 at 16:24):

If C\mathscr{C} is any category, and XX is an object of C\mathscr{C}, then Hom(X,X)\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?

view this post on Zulip Bhavik Mehta (Sep 25 2020 at 16:25):

Look in ct.endomorphism

view this post on Zulip Adam Topaz (Sep 25 2020 at 16:26):

Thanks!


Last updated: May 07 2021 at 21:10 UTC