complex.I is algebraic !

Stream: new members

[Nicolás Ojeda Bär]

Hurrah! I installed Lean yesterday evening, and after "just" a day and a half, I managed to prove my first result, namely that i is algebraic. Surely experts should be able to condense my proof to just a few words; please share any advice you may have (tactics, style, etc.). Thanks!

import ring_theory.algebra

open polynomial

universes u v
variables (k : Type u) (R : Type v)
variables [field k] [comm_ring R] [algebra k R]

def is_algebraic (x : R) := ∃ p, monic p ∧ aeval k R x p = 0

lemma degree_one_le_1 : degree (1 : polynomial k) ≤ 1 :=
begin
norm_num,
exact (with_bot.coe_le_coe.2 (by simp))
end

example : is_algebraic ℝ ℂ complex.I :=
begin
unfold is_algebraic,
use (X^2 + 1),
split,
{ -- prove monic (X^2 + 1)
exact (monic_X_pow_add (degree_one_le_1 _))
},
{ -- prove that I^2 + 1 = 0
rewrite aeval_def,
rewrite (pow_two X),
simp
}
end

[Reid Barton]

My expert tip: rw is shorter than rewrite

[Alex J. Best]

I'm not an expert, but here's where I'd take it too if I found the same proof,

import ring_theory.algebra
import tactic.library_search -- how I "remembered" the name of degree_one just ask library_search

open polynomial complex -- so I can write I instead of complex.I

universes u v
variables (k : Type u) {R : Type v} -- I changed R to be implicit as we want it to be in is_algebraic, there is no need to specify R twice, as its already just whatever ring x is a term of and x is in the definition
variables [field k] [comm_ring R] [algebra k R]

def is_algebraic (x : R) := ∃ p, monic p ∧ aeval k R x p = 0

example : is_algebraic ℝ I := -- making R implicit above lets me remove \C here, opening complex lets me just write I
begin
-- removed the unfold as it's not needed (except to find the proof in the first place)
use (X^2 + 1),
split,
{ -- prove monic (X^2 + 1)
exact (monic_X_pow_add (by rw degree_one; exact dec_trivial)) -- there is a lemma saying degree of 1 is 0 already, so use it and then 0 \le \u 1 is boring so hit it with dec_trivial, probably there is a lemma for this but dec_trivial is good.
},
{ -- prove that I^2 + 1 = 0
simp [aeval_def, pow_two], -- bit of golfing, personal preference and not necessary, but is more like the human "simplify everything using the definition and that x^2=x"
}
end

[Alex J. Best]

And yeah probably someone here can get a one-line proof of this ;) but this seems a good balance to me

[Alex J. Best]

oops, confused myself and forgot the earlier conversation, integral = algebraic over a field!

[Floris van Doorn]

Here is my try. I didn't change Alex's proof, but I did change the statement. If we want to prove that i is algebraic, we really want to prove that it's algebraic over Q. I had to add some instances for Lean to recognize that C is an algebra over Q. These should be added to mathlib. Also, Alex's proof was robust enough to work without changes!

import ring_theory.algebra

open polynomial complex

instance rat.cast.is_ring_hom {α} [division_ring α] [char_zero α] :
  is_ring_hom (rat.cast : ℚ → α) :=
⟨rat.cast_one, rat.cast_mul, rat.cast_add⟩

instance algebra_rat {α} [field α] [char_zero α] : algebra ℚ α :=
algebra.of_ring_hom rat.cast (by apply_instance)

universes u v
variables (k : Type u) {R : Type v}
variables [field k] [comm_ring R] [algebra k R]

def is_algebraic (x : R) := ∃ p, monic p ∧ aeval k R x p = 0

example : is_algebraic ℚ I :=
begin
  use (X^2 + 1), split,
  { exact (monic_X_pow_add (by rw degree_one; exact dec_trivial)) },
  { simp [aeval_def, pow_two] }
end

[Alex J. Best]

Nice, definitely these should end up in mathlib. I also worked on getting exactly the same cast going to prove that X^2 + 1 was monic actually, I was hoping that dec_trivial would prove that monic polynomials over Q were in fact monic, and then the proof for R could involve convert (monic_map (rat.cast : ℚ → ℝ)) (dec_trivial : (monic : polynomial ℚ → Prop)(X^2 + 1)), I was hoping that this would be even more robust, and you could show that every polynomial which is "obviously" monic over Q was monic without work this way, rather than worrying about special lemmas on the form of the polynomial. But I couldn't make a decidable instance for polynomial.monic that was computable. I guess this is due to some lines in the polynomial files like noncomputable theory and prop_decidable instances, but I think it would be nice if this could work, is there a reason not to allow this sort of thing? Or am I missing an existing way to do this?

[Keeley Hoek]

There is an instance for decidability of monic-ness, monic.decidable, but it doesn't work at the moment in this case

instance dinst : decidable (@monic ℚ _ (X^2 + 1)) := by apply_instance

because of picking up classical stuff in the polynomial development

[Nicolás Ojeda Bär]

1) Just to confirm my understanding, what is the difference between rw aeval_def and simp [aeval_def] ?
2) How does it work in simp [pow_two] where the argument (X) is not passed (not even with a wildcard _)?

[Patrick Massot]

Did you read https://leanprover.github.io/theorem_proving_in_lean/tactics.html#rewriting and the next section?

[Nicolás Ojeda Bär]

No, not yet, I will do it now. Thanks for the hint!

[Kevin Buzzard]

rw h means "find the left hand side of h in the goal and replace it with the right hand side. simp [h] means "you can use h and also every single lemma tagged [simp] in core Lean and also every module you've imported, all applied according to some clever heuristics which you don't need to know about"