Zulip Chat Archive

Stream: new members

Topic: Additive group homeomorphisms on fields


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jan 11 2019 at 10:18):

You know about int.cast?

view this post on Zulip Johan Commelin (Jan 11 2019 at 10:19):

It is your int_to_field, for arbitrary rings

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 11 2019 at 10:20):

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

view this post on Zulip Johan Commelin (Jan 11 2019 at 10:20):

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

view this post on Zulip Johan Commelin (Jan 11 2019 at 10:20):

I don't know what's wrong there.

view this post on Zulip 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:)

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:23):

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

view this post on Zulip Johan Commelin (Jan 11 2019 at 10:23):

@Kenny Lau :up:

view this post on Zulip Kenny Lau (Jan 11 2019 at 10:23):

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

view this post on Zulip Kenny Lau (Jan 11 2019 at 10:23):

but I don't think this is in mathlib yet

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 11 2019 at 10:25):

And discrete field homeomorphisms? Can I just use is_field_hom?

view this post on Zulip Kenny Lau (Jan 11 2019 at 10:26):

yes

view this post on Zulip 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.

view this post on Zulip 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