Zulip Chat Archive

Stream: maths

Topic: Inherit field instance from carrier


view this post on Zulip Thomas Browning (Aug 28 2020 at 23:04):

We have a situation where there is a subalgebra whose carrier is known to be a subfield, and we would like to show that the subalgebra is a field. What is the best way to do this?

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] (E : Type*) [field E] [algebra F E] (K : subalgebra F E)

instance obvious (h : is_subfield (K : set E)) : field K := sorry

view this post on Zulip Thomas Browning (Aug 28 2020 at 23:28):

It is possible to do manually, but surely there's a better way

instance obvious (h : is_subfield (K : set E)) : field K := {
    add := λ x y, x+y,
    add_assoc := add_assoc,
    add_comm := add_comm,
    zero := 0,
    zero_add := zero_add,
    add_zero := add_zero,
    neg := λ x, -x,
    add_left_neg := add_left_neg,
    mul := λ x y, x*y,
    mul_assoc := mul_assoc,
    mul_comm := mul_comm,
    one := 1,
    one_mul := one_mul,
    mul_one := mul_one,
    left_distrib := left_distrib,
    right_distrib := right_distrib,
    inv := λ x, (x : E)⁻¹,begin
        apply h.inv_mem,
        cases x,
        assumption,
    end,
    mul_inv_cancel :=
    begin
        intros a ha,
        ext,
        simp only [subsemiring.coe_mul, submodule.coe_mk, subsemiring.coe_one],
        apply mul_inv_cancel,
        intro ha',
        apply ha,
        ext,
        exact ha',
    end,
    inv_zero :=
    begin
        ext,
        simp only [submodule.coe_mk, inv_zero, submodule.coe_zero],
    end,
    exists_pair_ne :=
    begin
        use 0,
        use 1,
        simp only [ne.def, not_false_iff, zero_ne_one],
    end,
}

view this post on Zulip Adam Topaz (Aug 28 2020 at 23:32):

Surely you can at least inherit the commutative ring structure, e.g. with ..show comm_ring K, by apply_instance

view this post on Zulip Thomas Browning (Aug 28 2020 at 23:34):

that's true, although I feel like the whole thing should be obvious

instance obvious (h : is_subfield (K : set E)) : field K := {
    inv := λ x, (x : E)⁻¹,begin
        apply h.inv_mem,
        cases x,
        assumption,
    end,
    mul_inv_cancel :=
    begin
        intros a ha,
        ext,
        simp only [subsemiring.coe_mul, submodule.coe_mk, subsemiring.coe_one],
        apply mul_inv_cancel,
        intro ha',
        apply ha,
        ext,
        exact ha',
    end,
    inv_zero :=
    begin
        ext,
        simp only [submodule.coe_mk, inv_zero, submodule.coe_zero],
    end,
    exists_pair_ne :=
    begin
        use 0,
        use 1,
        simp only [ne.def, not_false_iff, zero_ne_one],
    end,
    ..show comm_ring K, by apply_instance,
}

view this post on Zulip Adam Topaz (Aug 28 2020 at 23:41):

You could probably golf those proofs a bit, but I don't know if you can avoid those fields altogether.

view this post on Zulip Kyle Miller (Aug 29 2020 at 00:32):

instance obvious (h : is_subfield (K : set E)) : field K := @is_subfield.field E _ (K : set E) _

It turns out that is_subfield.field gives something that's defeq to the instance. It just takes some gentle prodding to get Lean to agree.

view this post on Zulip Thomas Browning (Aug 29 2020 at 00:33):

Thanks Kyle!

view this post on Zulip Adam Topaz (Aug 29 2020 at 00:55):

Ah nice! I missed the is_subfield in the first message. Actually, I didn't even know that was a thing!

view this post on Zulip Kyle Miller (Aug 29 2020 at 01:38):

I think I saw a message a while back that is_subfield will eventually be replaced by bundled objects, like how other subobjects are handled, which would be as terms of a type subfield E.

view this post on Zulip Adam Topaz (Aug 29 2020 at 01:54):

Yeah I think all the is_foo things are being deprecated.

view this post on Zulip Johan Commelin (Aug 29 2020 at 03:59):

About the bundled vs unbundled story... We should definitely continue with bundling things. But Reid pointed out (and I agree) that maybe we shouldn't throw away the is_subfoobars. What we should do, is make them mere structures instead of classes. Because they can be genuinely useful for certain inductive arguments.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 07:14):

I don't know if is_subfield should be bundled. It could just be a predicate on is_subring. Does the community have a clear view on this?

view this post on Zulip Reid Barton (Aug 29 2020 at 14:06):

Johan Commelin said:

About the bundled vs unbundled story... We should definitely continue with bundling things. But Reid pointed out (and I agree) that maybe we shouldn't throw away the is_subfoobars. What we should do, is make them mere structures instead of classes. Because they can be genuinely useful for certain inductive arguments.

And the same for is_foo_hom as well

view this post on Zulip Adam Topaz (Aug 29 2020 at 14:41):

Why can't we have both? E.g. why isn't subring defined as bundled is_subring (pseudo-code)?

view this post on Zulip Adam Topaz (Aug 29 2020 at 14:43):

Well, bundled wouldn't work here, since it assumes a typeclass as an input, not a structure on a set, but surely you get the idea.

view this post on Zulip Reid Barton (Aug 29 2020 at 14:49):

Why isn't monoid_hom defined as subtype is_monoid_hom?

view this post on Zulip Reid Barton (Aug 29 2020 at 14:52):

Of course the transition cost would be pretty high unless we could paper over the differences somehow

view this post on Zulip Adam Topaz (Aug 29 2020 at 15:06):

How bad would it be? E.g. for monoid hom it seems that the main thing would be to redefine monoid_hom.map_mul as subtype.prop.map_mul, and similarly for map_one.

view this post on Zulip Reid Barton (Aug 29 2020 at 15:11):

{} constructors would all need to be modified

view this post on Zulip Reid Barton (Aug 29 2020 at 15:12):

it's too bad we can't use extends somehow

view this post on Zulip Adam Topaz (Aug 29 2020 at 15:13):

Oh right :oh_no:

view this post on Zulip Patrick Massot (Aug 29 2020 at 15:15):

There two relevant things I hope will be much better in Lean 4: alternate constructors as first class citizens (already named arguments could make this mostly ok) and smarter dot notation.

view this post on Zulip Reid Barton (Aug 29 2020 at 15:57):

Well, in any case, actually being defined as a subtype or what have you isn't particularly important

view this post on Zulip Johan Commelin (Aug 29 2020 at 16:24):

Well... I just refactored fin because there I thought it was important :rofl: :oops:

view this post on Zulip Reid Barton (Aug 29 2020 at 16:29):

In the past I think we've also moved away from using subtype to custom structures

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:47):

My impression about these sorts of questions is that I naturally assume (or assumed) that "the computer scientists" would completely understand this kind of question, which presumably has been around for as long as people have been doing basic algebra in theorem provers, so why can't they just tell us the best way to do it? But what I now am beginning to realise is that the actual answer seems to be massively system-dependent, and even in Lean we are still kind of feeling our way around what the best answer is -- and there's even a possibility that in Lean 4 we might want to change our mind e.g. back to a formerly deprecated method.

view this post on Zulip Kyle Miller (Aug 29 2020 at 19:18):

Mathlib seems to use classes in some places because they let us pretend we have sub-type polymorphism, where the sub-type relationship is the relationship between a structure and a structure that extends it. If the Lean elaborator were able to automatically coerce sub-types using the to_FOO functions, then it would make certain designs easier, I think. For example, the is_subfield class extends is_subring, so right now you can use objects with an is_subfield instance with functions that except an object with an is_subringinstance. Switching these to structures would require manual coercions right now, but what if the elaborator could automatically insert the to_is_subring coercion? Is there some theoretical reason why this cannot be done? (I think there are some issues with type inference, specifically generalization in a Hindley-Milner setup, but this doesn't seem like something that affects Lean.)

A proposal that doesn't involve wide-sweeping changes to the language: for functions that are meant to be sub-type polymorphic, have an annotation that specifies which arguments are meant to accept subtypes. Given the annotation, replace the definition with one that instead accepts arguments that implement a coercion typeclass (probably not has_lift, but perhaps a new has_supertype_lift or something like that), and have every structure automatically implement this typeclass for every structure it transitively extends using the to_FOO functions. (Implementation detail: the original definition would still be available, but renamed.)

Implementing this would probably only involve some attributes that do metaprogramming, but I haven't looked into this corner of Lean -- it just seems this functionality must exist given that things like @[simps] exist.

More generally, this could apply to types that aren't strictly sub-types of a structure. It could give us a principled way of adding automatic coercions to the arguments of functions -- it seems mathlib relies a lot on has_coe_to_fun and has_coe_to_sort to make ergonomic interfaces, and this might help make some of them even more natural.


Last updated: May 14 2021 at 18:28 UTC