MulHom dot notation

Stream: mathlib4

[Sky Wilshaw]

Is it possible to use dot notation with MulHoms and similar bundled morphisms?

import Mathlib.Algebra.Hom.Group

structure Foo

structure Bar

instance : MulOneClass Foo
    where
  one := ⟨⟩
  mul _ _ := ⟨⟩
  one_mul _ := rfl
  mul_one _ := rfl

instance : MulOneClass Bar
    where
  one := ⟨⟩
  mul _ _ := ⟨⟩
  one_mul _ := rfl
  mul_one _ := rfl

def Foo.hom : Foo →* Bar
    where
  toFun _ := ⟨⟩
  map_one' := rfl
  map_mul' _ _ := rfl

def apply (x : Foo) : Bar := x.hom -- invalid field notation, function 'Foo.hom' does not have argument with type (Foo ...) that can be used, it must be explicit or implicit with a unique name

or is it better to just define the map as a function with associated lemmas (map_mul etc.)?

[Kyle Miller]

It's not possible to get x.hom to work at the moment. I think there's general agreement that it's something we'd want, but it would take carefully specifying how it would work and then changing core Lean.

A workaround you'll find in mathlib is to define an additional function toBar : Foo -> Bar that can do the dot notation along with a lemma that Foo.hom x = x.toBar

[Eric Wieser]

If you make it an abbrev then you probably don't even need the lemma