Subfields generated by a set

[tirix]

As discussed with @savask in #4246, this introduces the definition of the subfield generated by a set. This can be later used to build such fields as $ℚ[\sqrt{2}]$.

A few "deduction mode" algebra theorems moved to main.

[savask]

Ah, that's nice, I was actually going to reply to your message in #4246 .

You define fldGen in such a way, that the result is a field (i.e. a structure). I've noticed that in set.mm the practice seems to be that, for example, a subgroup is a subset of the group which is a group when equipped with the original operation, see SubGrp, similarly, a subring is a subset (see SubRing). A ring, spanned by a subset is also a subset, see RingSpan, and a submonoid generated by some subset also seems to be defined in terms of subsets (see gsumwspan and a related notion of a Moore closure). Maybe fields should also follow suit?

[tirix]

Yes, maybe that's better.
I'll revise this proposal in that sense. The theorem fldgenfld will then be:

   fldgenfld $p |- ( ph -> ( F |`s ( F fldGen S ) ) e. Field ) $=

It's a bit more verbose, but I guess maybe other theorems will be simpler.

[savask]

The theorem fldgenfld will then be:

Now, since we have SubGrp and SubRing, maybe we should have a SubField? Then fldgenfld could be restated like

|- ( ph -> ( F fldGen S ) e. ( SubField ` F ) )

Also if you like, we could continue fleshing out the plan in #4246 and maybe we'll see which definitions are more comfortable for proving the metamath 100 theorem.

[tirix]

Now, since we have SubGrp and SubRing, maybe we should have a SubField? Then fldgenfld could be restated like

Actually, we already have df-sdrg, which is already sufficient to express subfields. Since a field is commutative, any sub-division-ring is also commutative, and the sub-division-rings of fields are themselves fields, so they are subfields. Surprisingly, I did not see this statement in set.mm, I should also add it (if it's actually correct!)

I should use this in the definition of subfields generated by a set, this will be even more compact.
Maybe we can continue to discuss here the definition of the subfield generated by a set, and continue the discussion about which theorems from the Galois Theory are needed for trisecting the angle in #4246 ? As you prefer!

[savask]

SubDRing is a great find, I think it dispels my last doubts and the subfield generated by a set should itself be a set (like a subgroup, a subring and a sub-division-ring). I've noticed that there are some results about the prime field, like primefldcl, so if everything works out correctly, one could show that the prime field is a subfield generated by 1.

And sure, we can discuss this definition here - I'll reserve some other thoughts to the original issue though :-)

[tirix]

@savask This is the updated version. I'm quite happy with this. I suppose many theorems using this concept will also be valid in division rings, so the first few theorems are proved with division rings.

[savask]

Looks good to me as well!

[benjub]

f e. Ring (see above why not "DivRing") rather than f e. _V

[tirix]

That's an interesting point (specifying the domain : let's keep the discussion about DivRing vs. Ring elsewhere).

The list of definitions using _V where a stricter structure was available is very long (gsum, oppc, lub, glb, +f, freeMnd, -g, invg, .g, Cntz, cntr, LSSum...) This also includes LSpan, which is the model for this definition.

There are also examples where the domain is defined, of course, but my feeling is that they are in minority.

I believe I saw at one point in time a comment from Norm or Mario explaining that we prefer the most general case (_V), but I can't find it anymore. That was probably useful e.g. when we introduced Magma, I believe less definitions/theorems needed to be reviewed thanks to the use of _V as a domain for several functions listed above.

That's why I chose _V here. Of course this is open to discussion.

[benjub]

I understand that remark and I know that that style of common in set.mm. I still disagree with it. But this can be deferred to later discussions. Non-blocking for this PR.

[avekens]

I believe I saw at one point in time a comment from Norm or Mario explaining that we prefer the most general case (_V), but I can't find it anymore. That was probably useful e.g. when we introduced Magma, I believe less definitions/theorems needed to be reviewed thanks to the use of _V as a domain for several functions listed above.

Yes, I also remember the advice (by Mario, I think) to use _V instead of a concrete class. In Graph Theory, for example, we have UnivVtx = ( g e. _V |-> ... instead of UnivVtx = ( g e. UHGraph |-> .... Maybe @digama0 can give a hint where this discussion took place, or where this pattern is documented. If it is not documented, we should add it to our conventions.

[benjub]

Suggested change

	` _V ` or at least ` Ring ` and not only ` DivRing ` . $)
	` Ring ` and not only ` DivRing ` . $)

I understand your remark, and I know that we do a lot of things like that in set.mm, but I still think that it makes no sense to allow nonsensical things like "the set of sub-division-rings of { 2 } ".

[benjub]

(As you want for the present PR. Non-blocking.)

[tirix]

Yes, but you could imagine defining a sub-division-ring of something that's not even a ring. For example, QQ is a division ring which is a subset of the extended real numbers RR*s which is not even a group, but has the necessary structures and operations.
Isn't this similar to searching sub-division-rings starting with rings which are not themselves division rings?

Anyway, again, in practice, I don't think this will be used on anything else than fields. If you prefer to restrict the domain to something, Ring is a good choice because it the most generic structure with two operations (but then again why not e.g. semi-rings SRing?).

[benjub]

Isn't this similar to searching sub-division-rings starting with rings which are not themselves division rings?

The reason I gave above to use rings instead of division rings as the ambient structure is added simplicity rather than added generality. Of course, one can always find a more general setting, by doing what is called "centipede mathematics", but if it comes at the cost of simplicity, this may not be worth it.

[tirix]

@benjub I don't think there is any blocking point left for this PR, thanks for all the comments!

I plan rework the definition of SubDRing in a subsequent PR to use Ring instead of DivRing, and use this Ring restriction in the definition of "subfield generated by a set".

A more general discussion about whether we should restrict at all the domain for such functions can be launched separately.