Zulip Chat Archive

Stream: maths

Topic: Inductive type of elements defined by radicals


view this post on Zulip Thomas Browning (Dec 05 2020 at 00:12):

We're trying to define a notion of an element that is solvable by radicals. We would like it to have constructors like base, add, neg, mul, inv, and also a constructor for taking radicals. See the code below.

Is there a way to define SBR and val simultaneously, so that the rad constructor for SBR requires a proof that β^n = α.val?

section abel_ruffini

inductive SBR (F : Type*) [field F] (E : Type*) [field E] [algebra F E]
| base (α : F) : SBR
| add (α β : SBR) : SBR
| neg (α : SBR) : SBR
| mul (α β : SBR) : SBR
| inv (α : SBR) : SBR
| rad (α : SBR) (n : ) (β : E) : SBR

namespace SBR

def val {F : Type*} [field F] {E : Type*} [field E] [algebra F E] : SBR F E  E
| (base α) := algebra_map F E α
| (add α β) := α.val + β.val
| (neg α) := - α.val
| (mul α β) := α.val * β.val
| (inv α) := (α.val)⁻¹
| (rad α n β) := β

def good {F : Type*} [field F] {E : Type*} [field E] [algebra F E] : SBR F E  Prop
| (base α) := true
| (add α β) := true
| (neg α) := true
| (mul α β) := true
| (inv α) := true
| (rad α n β) := (β^n = α.val)

end SBR

structure good_SBR (F : Type*) [field F] (E : Type*) [field E] [algebra F E]
(α : SBR F E) (h : SBR.good α)

end abel_ruffini

view this post on Zulip Reid Barton (Dec 05 2020 at 00:19):

This is an inductive-recursive definition, which Lean doesn't support directly, but often can be translated into something that it does--in this case the easiest way is to add the value being represented as an index of the inductive type SBR

view this post on Zulip Thomas Browning (Dec 05 2020 at 00:24):

what do you mean "an index of the inductive type"?

view this post on Zulip Alex J. Best (Dec 05 2020 at 00:29):

I think this does what you want?

inductive SBR (F : Type*) [field F] (E : Type*) [field E] [algebra F E] : E  Prop
| base (a : F) : SBR (algebra_map F E a)
| add (a b : E) : SBR a  SBR b  SBR (a + b)
| neg (α : E) : SBR α  SBR (-α)
| mul (α β : E) : SBR α  SBR β  SBR (α * β)
| inv (α : E) : SBR α  SBR (α⁻¹)
| rad (α β : E) (n : ) (h : α ^n = β): SBR β  SBR α

view this post on Zulip Reid Barton (Dec 05 2020 at 00:32):

You can also make it not a Prop if you like, but it might require some more explicit universe variables

view this post on Zulip Thomas Browning (Dec 05 2020 at 00:33):

the reason why I'm hesitate to go with a function E to Prop, is that I want to know what the solvable by radicals process was. In particular, I want to take an SBR element and produce a corresponding field from the SBR construction.

view this post on Zulip Thomas Browning (Dec 05 2020 at 00:34):

My impression is if SBR is a function E to Prop, then knowing SBR x doesn't let me do cases on how x arose. But I could be wrong

view this post on Zulip Reid Barton (Dec 05 2020 at 00:34):

no, that's right

view this post on Zulip Reid Barton (Dec 05 2020 at 00:36):

I'm not sure why Lean needs a bit more hand-holding, but

universes u v

inductive SBR (F : Type u) [field F] (E : Type v) [field E] [algebra F E] : E  Type (max u v)
| base (a : F) : SBR (algebra_map F E a)
| add (a b : E) : SBR a  SBR b  SBR (a + b)
| neg (α : E) : SBR α  SBR (-α)
| mul (α β : E) : SBR α  SBR β  SBR (α * β)
| inv (α : E) : SBR α  SBR (α⁻¹)
| rad (α β : E) (n : ) (h : α ^n = β): SBR β  SBR α

view this post on Zulip Thomas Browning (Dec 05 2020 at 00:37):

ah, and now you can do cases?

view this post on Zulip Johan Commelin (Dec 05 2020 at 05:23):

/me note to self: SBR = solvable by radicals :bulb:

view this post on Zulip Johan Commelin (Dec 05 2020 at 05:26):

Why not

| rad (α : E) (n : ) : SBR (α^n)  SBR α

view this post on Zulip Patrick Lutz (Dec 05 2020 at 05:28):

Johan Commelin said:

Why not

| rad (α : E) (n : ) : SBR (α^n)  SBR α

because we didn't think of it?

view this post on Zulip Johan Commelin (Dec 05 2020 at 05:32):

Aah, that's a familiar experience (-;


Last updated: May 11 2021 at 16:22 UTC