monoid instance on self maps

Stream: Is there code for X?

[Oliver Nash]

I cannot seem to find this:

import algebra.default

instance function.monoid {α : Type*} : monoid (α → α) := infer_instance --fails

Is this really missing or am I missing the obvious?

[Eric Wieser]

We have docs#pi.monoid

[Eric Wieser]

I don't think it has the multiplication you want though

[Oliver Nash]

But that's different, right? I'm talking about composing functions.

[Eric Wieser]

That would have to be a type alias then

[Oliver Nash]

As in:

instance function.monoid {α : Type*} : monoid (α → α) :=
{ mul        := function.comp,
  mul_assoc  := function.comp.assoc,
  one        := id,
  one_mul    := λ f, by simp,
  mul_one    := λ f, by simp,

[Oliver Nash]

or even:

instance function.monoid {α : Type*} : monoid (α → α) :=
{ mul        := function.comp,
  mul_assoc  := function.comp.assoc,
  one        := id,
  one_mul    := λ f, by simp,
  mul_one    := λ f, by simp,
  npow       := λ n f, f^[n],
  npow_zero' := λ f, rfl,
  npow_succ' := λ n f, by simpa only [function.iterate_succ'], }

which leads me to my second question:

[Oliver Nash]

couldn't we use the above together with monoid.has_pow instead of nat.iterate?

[Oliver Nash]

Eric Wieser said:

That would have to be a type alias then

Sorry I was too busy pasting in code and I missed this. I don't follow your point here. What does this mean?

[Kevin Buzzard]

If alpha is something like a monoid then probably alpha -> alpha inherits a pointwise monoid structure which is not what you want.

[Oliver Nash]

Oh right I see. Thanks.

[Kevin Buzzard]

Yeah,

import algebra.direct_sum_graded

example (α : Type) [monoid α] : monoid (α → α) := infer_instance

and it's not what you want

[Kevin Buzzard]

PS do you have to fill in npow? Hopefully it happens by magic if you just leave it out.

[Eric Wieser]

Like docs#monoid.End.monoid

[Oliver Nash]

Kevin Buzzard said:

PS do you have to fill in npow? Hopefully it happens by magic if you just leave it out.

You don't have to fill it in. My second snippet (above the words "or even") omitted this.

[Kevin Buzzard]

I would check but my lightbulb is broken :-( :cry:

[Oliver Nash]

I saw that. No ideas I'm afraid.

[Eric Wieser]

Vs docs#monoid_hom.comm_monoid, which is elementwise

[Eric Wieser]

So I guess you need function.End to exist

[Oliver Nash]

Gotcha

[David Wärn]

import category_theory.types
import category_theory.single_obj

variable {α : Type*}
@[derive monoid]
def foo := category_theory.End α
#check (rfl : foo = (α → α))

[Eric Wieser]

docs#category_theory.End

[Thomas Browning]

Would it not be possible to have this instance at a lower instance priority? Would this allow you to define Nat.iterate and Function.Commute in terms of pow and Commute?

[Eric Wieser]

Note that docs#instMonoidEnd exists

[Eric Wieser]

Instance priorities are a bad tool for everything except performance optimization

[Thomas Browning]

Yes, it just feels a bit weird to have Function.Commute be a special case of Commute with duplicated API. But maybe there's no better way.

[Yury G. Kudryashov]

Note that docs#Function.Semiconj is not a docs#SemiconjBy for some M

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

Really the correct generalization is semiconjugacy in a monoid-oid, aka a category :grinning_face_with_smiling_eyes:

[Yury G. Kudryashov]

But semiconjugacy in a category is not universe polymorphic...