Explicit definitions of specific multiplicative homomorphism

Stream: new members

[Alex Griffin]

Given two instances of has_mul, one can then define the type of multiplicative homomorphisms from one to the other by using →* analogously to how one uses → for defining the type of more general functions from one type to another. This is all well and good, but how does one go about describing a specific instance of this type? For example, if you were to try and define a semidirect product of two groups N and G, you would need a map from G to mul_aut N. Importantly, this map needs to be of type G →* (mul_aut N), as opposed to merely being of type G → (mul_aut N). The thing is, it's a bit unclear as to how to explicitly define a specific term of this type. If one were to try and define it via some anonymous λ definition, the resulting term would be of type G → (mul_aut N), but not of type G →* (mul_aut N). Is there some analogous way to explicitly define multiplicative homomorphisms?

[Kevin Buzzard]

Are you just asking about constructors of →*? It's defined as a structure, and the usual structure constructor requires that you give a map and then proofs that it commutes with 1 and *. Or have I misunderstood the question?

[Mario Carneiro]

That is, you write:

def foo : A ->* B :=
{ to_fun := \lam a, ...,
  map_one := ...,
  map_mul := ... }

[Alex Griffin]

Thank you for the direction.