Additive group homeomorphisms on fields

Stream: new members

[Abhimanyu Pallavi Sudhir]

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]

You know about int.cast?

[Johan Commelin]

It is your int_to_field, for arbitrary rings

[Abhimanyu Pallavi Sudhir]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I don't know what's wrong there.

[Johan Commelin]

(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]

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

[Johan Commelin]

@Kenny Lau :up:

[Kenny Lau]

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

[Kenny Lau]

but I don't think this is in mathlib yet

[Abhimanyu Pallavi Sudhir]

And discrete field homeomorphisms? Can I just use is_field_hom?

[Kenny Lau]

yes

[Abhimanyu Pallavi Sudhir]

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

If I change theorem to instance, it works.

[Abhimanyu Pallavi Sudhir]

That's how they do it in mathlib.