# Zulip Chat Archive

## Stream: new members

### Topic: Additive group homeomorphisms on fields

#### Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:16):

Since fields extend additive groups , I thought that something `hom_int_to_field`

below should work:

import algebra.field import field_theory.subfield variables {K L : Type} [field K] [field L] (f : K → L) def nat_to_field : ℕ → K | 0 := 0 | (nat.succ n) := nat_to_field(n) + 1 def int_to_field : ℤ → K | (int.of_nat n) := nat_to_field n | (int.neg_succ_of_nat n) := -(1 + nat_to_field(n)) theorem hom_int_to_field : is_add_group_hom int_to_field := sorry

But it doesn't -- it tells me it can't synthesise the instance. Instead, I need to create a proof that `K`

is an additive group, give it a name:

instance AK : add_group K := { add := has_add.add, add_assoc := add_monoid.add_assoc, zero := 0, zero_add := add_monoid.zero_add, add_zero := add_monoid.add_zero, neg := add_group.neg, add_left_neg := add_group.add_left_neg }

And then use it:

theorem hom_int_to_field : @is_add_group_hom _ _ _ (AK : add_group K) int_to_field := sorry

Can't I use the fact that fields are -- by definition -- additive groups?

#### Johan Commelin (Jan 11 2019 at 10:18):

You know about `int.cast`

?

#### Johan Commelin (Jan 11 2019 at 10:19):

It is your `int_to_field`

, for arbitrary rings

#### Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:19):

Oh, I didn't know it casted to a general field. Yes, `int.cast.is_ring_hom`

#### Johan Commelin (Jan 11 2019 at 10:20):

And somewhere there must be a proof that it is a ring hom

#### Johan Commelin (Jan 11 2019 at 10:20):

But that doesn't answer why your instance can't be found.

#### Johan Commelin (Jan 11 2019 at 10:20):

I don't know what's wrong there.

#### Johan Commelin (Jan 11 2019 at 10:21):

(Also, mathematician's field is `discrete_field`

. For reasons that I don't get. Since I'm a mathematician :see_no_evil:)

#### Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:23):

Oh -- what about subfields? Is there a "discrete subfield"?

#### Johan Commelin (Jan 11 2019 at 10:23):

@Kenny Lau :up:

#### Kenny Lau (Jan 11 2019 at 10:23):

I think every subfield of a discrete field is discrete by default

#### Kenny Lau (Jan 11 2019 at 10:23):

but I don't think this is in mathlib yet

#### Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:25):

And discrete field homeomorphisms? Can I just use `is_field_hom`

?

#### Kenny Lau (Jan 11 2019 at 10:26):

yes

#### Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:35):

But that doesn't answer why your instance can't be found.

If I change `theorem`

to `instance`

, it works.

#### Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:35):

That's how they do it in mathlib.

Last updated: May 14 2021 at 12:18 UTC