Zulip Chat Archive

Stream: general

Topic: subfield


view this post on Zulip Kenny Lau (Feb 20 2019 at 17:03):

So the current definition of subfield is:

class is_subfield extends is_subring s : Prop :=
(inv_mem :  {x : F}, x  s  x⁻¹  s)

which is clearly wrong, as this requires the inverse of 0 to be inside the set.
However, if one fixes it, then a subfield would no longer be a field, because one would not have a computable inverse:

instance subset.field [is_subfield s] : field s :=
by subtype_instance

view this post on Zulip Kenny Lau (Feb 20 2019 at 17:03):

Question: what to do?

view this post on Zulip Kenny Lau (Feb 20 2019 at 17:15):

I think the solution to this nonsense is to define a structure field' where 0⁻¹ = 0

view this post on Zulip Johan Commelin (Feb 20 2019 at 17:17):

Maybe something like \for a b, a * b = 1, a \in S \to b \in S

view this post on Zulip Kenny Lau (Feb 20 2019 at 17:18):

this won't solve the problem that a subfield won't be a field

view this post on Zulip Chris Hughes (Feb 20 2019 at 17:19):

It will be a field it just won't be a field


Last updated: May 13 2021 at 06:15 UTC