add_monoid_hom.comp_assoc is the wrong way around

Stream: maths

[Kevin Buzzard]

import algebra.group.hom_instances

open add_monoid_hom

instance {A : Type*} [add_comm_monoid A] :
  semiring (A →+ A) :=
{ mul := comp,
  mul_assoc := λ _ _ _, (comp_assoc _ _ _).symm, -- oops
  one := add_monoid_hom.id _,
  one_mul := id_comp,
  mul_one := comp_id,
  zero_mul := zero_comp,
  mul_zero := comp_zero,
  left_distrib := comp_add,
  right_distrib := add_comp,
  ..add_monoid_hom.add_comm_monoid }

Do we not have this instance? I couldn't find it. The proof is so beautiful, all the fields are there already in the add_monoid_hom namespace. But is this evidence that we got add_monoid_hom.comp_assoc backwards?

[Adam Topaz]

We have docs#linear_map.endomorphism_semiring

[Adam Topaz]

and of course any add_comm_monoid is a nat-semimodule in a unique way.

[Adam Topaz]

I expected this to work, but it doesn't

import algebra
import algebra.group.hom

instance {A : Type*} [add_comm_monoid A] :
  semiring (add_monoid.End A) := by apply_instance

[Adam Topaz]

it does have the monoid instance though, so that's a bit of a shortcut

[Eric Wieser]

docs#add_monoid.End.monoid, I assume?

[Adam Topaz]

Yeah, that's what I mean by "the monoid instance"

[Eric Wieser]

I guess there's a semiring (additive (monoid.End M)) instance to be declared too?

[Adam Topaz]

No, I don't think so. The addition on (additive (monoid.End M)) is almost never commutative

[Adam Topaz]

Maybe I'm misunserstanding what you want here...

[Eric Wieser]

Hmm, I mean the semiring where * is composition and + is multiplication in the codomain

[Eric Wieser]

Maybe that's a bad way to spell that

[Adam Topaz]

Ah I see... so you want the additive to decorate M.

[Adam Topaz]

semiring (monoid.End (additive M))

[Eric Wieser]

I guess that's probably add_monoid.End (additive M) anyway, which is the original instance

[Eric Wieser]

Kevin, I don't get your assoc claim; the instance that already proves it does not have the symm

[Eric Wieser]

Perhaps the proof is just rfl anyway so lean doesn't care if you get it backwards

[Kevin Buzzard]

Yes it's refl so I now agree that I could be wrong

[Eric Wieser]

docs#add_monoid_hom.comp_assoc for reference

[Eric Wieser]

I think you're wrong?

[Eric Wieser]

c.f. docs#mul_assoc

[Kevin Buzzard]

mul_assoc := λ _ _ _, comp_assoc _ _ _, does work, so there's a chance I'm wrong, (and indeed mul_assoc := λ _ _ _, rfl works too, unsurprisingly) but mul_assoc := comp_assoc does _not_ work, so if I'm wrong, then why doesn't it work?

[Kevin Buzzard]

Got it!

mul_assoc := λ a b c, comp_assoc c b a,

So my revised claim is that add_monoid_hom.comp_assoc has its inputs in the wrong order according to Lean's style.

[Adam Topaz]

Note that docs#function.comp.assoc is in the right order

[Kevin Buzzard]

@[to_additive] lemma monoid_hom.comp_assoc {Q : Type*}
  [mul_one_class M] [mul_one_class N] [mul_one_class P] [mul_one_class Q]
  (f : M →* N) (g : N →* P) (h : P →* Q) :
  (h.comp g).comp f = h.comp (g.comp f) := rfl

The counter-argument is that "we apply f first when composing these homs, so it must be the first input". Do we buy this?

[Adam Topaz]

So yes, I think this is an issue with add_monoid_hom.comp_assoc

[Adam Topaz]

docs#add_monoid_hom.comp_assoc must have been written by a category theorist

[Kevin Buzzard]

Is Eric a category theorist?

[Adam Topaz]

Kevin Buzzard said:

Is Eric a category theorist?

future category theorist ;)

[Adam Topaz]

Or maybe he's a future topologist who doesn't like monodromy.

[Eric Wieser]

I doubt I wrote that

[Eric Wieser]

I probably just touched it in a refactor

[Kevin Buzzard]

@Scott Morrison is this a situation where it's impossible to please all of the people all of the time?

[Eric Wieser]

I think the order of the arguments to monoid_hom.comp_assoc should be consistent with the order to monoid_hom.comp, so this is probably just an accident that can be fixed.