Homomorphism induced by left composition

Stream: Is there code for X?

[Heather Macbeth]

I have written a construction below for monoids, but one can write this construction -- the homomorphism of function spaces induced by a homomorphism of the targets -- for any algebraic structure:

import algebra.group.pi

variables {A B ι : Type*} [monoid A] [monoid B]

def monoid_hom.comp_left_hom (f : A →* B) : (ι → A) →* (ι → B) :=
{ to_fun := λ h, f ∘ h,
  map_one' := by ext; simp,
  map_mul' := λ i j, by ext; simp }

Do any of these constructions exist in mathlib? If so, what is the naming convention? (I would like to PR analogous constructions for C(ι, A) →* C(ι, B).)

[Eric Wieser]

We have docs#monoid_hom.comp_hom for when the arguments are not functions but monoid_homs

[Eric Wieser]

I think for C(ι, A) →* C(ι, A) this would be continuous_map.comp_monoid_hom

[Eric Wieser]

I think for C(ι, A) →* C(ι, A) this would be continuous_map.comp_monoid_hom

[Eric Wieser]

Perhaps the one you suggest is pi.comp_monoid_hom?

[Eric Wieser]

To match pi.eval_monoid_hom?

[Heather Macbeth]

Indeed, the version when the arguments are morphisms exists in mathlib in a few cases: in addition to docs#monoid_hom.comp_hom there is docs#linear_map.llcomp. Someone should standardize the notation (though I am not volunteering!)

[Heather Macbeth]

Now PR'd as #7984.

[Eric Wieser]

Oops: docs#linear_map.fun_left vs docs#linear_map.comp_left

[Eric Wieser]

Oh, maybe those aren't duplicates after all

[Eric Wieser]

But the names are certainly using different conventions