## 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 :=
zero := 0,


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):

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"?

@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?

yes

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

If I change theorem to instance, it works.