Inherit field instance from carrier

Stream: maths

[Thomas Browning]

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

[Thomas Browning]

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,
}

[Adam Topaz]

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

[Thomas Browning]

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,
}

[Adam Topaz]

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

[Kyle Miller]

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.

[Thomas Browning]

Thanks Kyle!

[Adam Topaz]

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

[Kyle Miller]

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.

[Adam Topaz]

Yeah I think all the is_foo things are being deprecated.

[Johan Commelin]

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.

[Kevin Buzzard]

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?

[Reid Barton]

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

[Adam Topaz]

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

[Adam Topaz]

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.

[Reid Barton]

Why isn't monoid_hom defined as subtype is_monoid_hom?

[Reid Barton]

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

[Adam Topaz]

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.

[Reid Barton]

{} constructors would all need to be modified

[Reid Barton]

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

[Adam Topaz]

Oh right :oh_no:

[Patrick Massot]

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.

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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

[Kevin Buzzard]

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.

[Kyle Miller]

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.