Define homomorphisms into a special group

Stream: new members

[Raphael Appenzeller]

I would like to define a class of homomorphisms from a group G into the fixed group \Z. Here is what I tried:

import algebra.group.defs
instance special_group : group ℤ :=
{
mul := λ x y , x+y,
one := 0,
mul_assoc := int.add_assoc,
mul_one := int.add_zero,
one_mul := int.zero_add,
inv := int.neg,
mul_left_inv := int.add_left_neg,
}

class my_auto (G:Type*) [group G] extends mul_hom G G

class hom_to_triv (G:Type*) [group G] extends mul_hom G special_group

However I get an error that the type does not match. I agree that the Types don't match, but don't know how to deal with it.

type mismatch at application
  G →ₙ* special_group
term
  special_group
has type
  group ℤ : Type
but is expected to have type
  Type ? : Type (?+1)

[Yaël Dillies]

special_group is the paint applied on the object ℤ. mul_hom is asking you about the object, but you're giving it the paint.

[Yaël Dillies]

Probably what you want here is mul_hom G (multiplicative ℤ), where docs#multiplicative turns addition into multiplication, subtraction into division, etc...

[Raphael Appenzeller]

I see. What do I do, when I defined my group using instance, for example:

instance special_group : group {a : ℤ | a = 0 } := ...

[Yaël Dillies]

Use {a : ℤ | a = 0} instead of writing special_group.

[Raphael Appenzeller]

In my case {a : ℤ | a = 0} is a long definition that I don't want to write everytime. I was trying to use instance in order to give it a name. Another idea is to use notation instead, but that also does not work since empty notation is not allowed?

[Yaël Dillies]

Using def is the canonical way of giving names to things. The error with notation is strange, you will have to give me more context.

[Raphael Appenzeller]

If I replace instance by def in the original program I posted, I get the same error as before:

import algebra.group.defs
def special_group : group ℤ :=
{
mul := λ x y , x+y,
one := 0,
mul_assoc := int.add_assoc,
mul_one := int.add_zero,
one_mul := int.zero_add,
inv := int.neg,
mul_left_inv := int.add_left_neg,
}

class my_auto (G:Type*) [group G] extends mul_hom G G

class hom_to_integers (G:Type*) [group G] extends mul_hom G special_group

[Yaël Dillies]

I was talking about "a long definition that I don't want to write everytime", not about the group instance.

[Raphael Appenzeller]

I forgot the ticks ` in notation. This now works and does what I want it to do. Do you think it is better to instead use def?

notation `naturals` := ℤ
class hom_to_triv (G:Type*) [group G] extends mul_hom G naturals

[Raphael Appenzeller]

Aha, I did the def all wrong. Thanks! I now figured it out. It should work something like this:

def special_group := \Z  -- actually a long definition that I don't want to write everytime
instance : group special_group := -- here i prove that special_group has a group structure
class hom_to_integers (G:Type*) [group G] extends mul_hom G special_group

Thanks a lot for your help!