Inductive type of elements defined by radicals

Stream: maths

[Thomas Browning]

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]

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]

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

[Alex J. Best]

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]

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

[Thomas Browning]

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]

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

[Reid Barton]

no, that's right

[Reid Barton]

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]

ah, and now you can do cases?

[Johan Commelin]

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

[Johan Commelin]

Why not

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

[Patrick Lutz]

Johan Commelin said:

Why not

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

because we didn't think of it?

[Johan Commelin]

Aah, that's a familiar experience (-;