Zulip Chat Archive

Stream: new members

Topic: Explicit definitions of specific multiplicative homomorphism

Alex Griffin (Feb 02 2021 at 16:38):

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 (Feb 02 2021 at 16:40):

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 (Feb 02 2021 at 16:43):

That is, you write:

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

Alex Griffin (Feb 02 2021 at 16:45):

Thank you for the direction.

Last updated: Dec 20 2023 at 11:08 UTC