## Stream: maths

### Topic: Inductive type of elements defined by radicals

#### 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


#### 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

#### Thomas Browning (Dec 05 2020 at 00:24):

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

#### 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 α


#### 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

#### 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.

#### 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

no, that's right

#### 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 α


#### Thomas Browning (Dec 05 2020 at 00:37):

ah, and now you can do cases?

#### Johan Commelin (Dec 05 2020 at 05:23):

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

#### Johan Commelin (Dec 05 2020 at 05:26):

Why not

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


#### 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?

#### Johan Commelin (Dec 05 2020 at 05:32):

Aah, that's a familiar experience (-;

Last updated: May 11 2021 at 16:22 UTC