Weierstrass polynomial is always irreducible.

weierstrass_irreducible.lean

import data.polynomial.ring_division

structure EllipticCurve (K : Type*) := (a₁ a₂ a₃ a₄ a₆ : K)

variables {K : Type*} (E : EllipticCurve K)

namespace polynomial
open_locale polynomial

noncomputable def weierstrass_polynomial [ring K] : K[X][X] :=
X ^ 2 + C (C E.a₁ * X + C E.a₃) * X - C (X ^ 3 + C E.a₂ * X ^ 2 + C E.a₄ * X + C E.a₆)

lemma nat_degree_weierstrass_polynomial [ring K] [nontrivial K] :
  (weierstrass_polynomial E).nat_degree = 2 :=
begin
  rw [weierstrass_polynomial, sub_eq_add_neg, ← C_neg],
  convert nat_degree_quadratic (@one_ne_zero K[X] _ _ _),
  rw [C_1, one_mul],
end

lemma monic_weierstrass_polynomial [ring K] : (weierstrass_polynomial E).monic :=
begin
  nontriviality K,
  rw [weierstrass_polynomial, sub_eq_add_neg, ← C_neg],
  convert leading_coeff_quadratic (@one_ne_zero K[X] _ _ _),
  rw [C_1, one_mul],
end

lemma weierstrass_polynomial_coeff [ring K] :
  (weierstrass_polynomial E).coeff 0 = - (X ^ 3 + C E.a₂ * X ^ 2 + C E.a₄ * X + C E.a₆) ∧
  (weierstrass_polynomial E).coeff 1 = C E.a₁ * X + C E.a₃ :=
begin
  simp_rw [weierstrass_polynomial,
    coeff_sub, coeff_add, coeff_X_pow, coeff_C_mul, coeff_X, coeff_C],
  rw [if_neg, if_neg, if_pos rfl, if_neg, if_pos rfl, if_neg],
  { simp_rw [mul_zero, zero_add, zero_sub, mul_one, sub_zero], exact ⟨rfl, rfl⟩ },
  all_goals { dec_trivial },
end

lemma irreducible_weierstrass [comm_ring K] [is_domain K] :
  irreducible (weierstrass_polynomial E) :=
begin
  by_contra,
  obtain ⟨p, q, hmul, hadd⟩ := (not_irreducible_iff_exists_add_mul_eq_coeff
    (monic_weierstrass_polynomial E) (nat_degree_weierstrass_polynomial E)).1 h,
  obtain ⟨h0, h1⟩ := weierstrass_polynomial_coeff E,
  
  rw h0 at hmul, rw h1 at hadd, have hmul' := hmul,
  apply_fun nat_degree at hmul hadd,
  replace hadd := hadd.symm.trans_le nat_degree_linear_le,
  have hdc := nat_degree_cubic (@one_ne_zero K _ _ _),
  nth_rewrite 0 C_1 at hdc, rw one_mul at hdc,
  rw [nat_degree_neg, hdc, nat_degree_mul'] at hmul, swap,
  { rw [← leading_coeff_mul, ← hmul', leading_coeff_neg, neg_ne_zero],
    convert @one_ne_zero K _ _ _, convert leading_coeff_cubic (@one_ne_zero K _ _ _),
    rw [C_1, one_mul] },
  
  apply_fun (λ n, n - q.nat_degree) at hmul,
  rw nat.add_sub_cancel at hmul,
  obtain hq|hq := le_or_lt q.nat_degree 1,
  { have := (nat.sub_le_sub_left 3 hq).trans_eq hmul,
    rw nat_degree_add_eq_left_of_nat_degree_lt (hq.trans_lt this) at hadd,
    exact hadd.not_lt this },
  { have := hmul.symm.trans_le (nat.sub_le_sub_left 3 hq),
    rw nat_degree_add_eq_right_of_nat_degree_lt (this.trans_lt hq) at hadd,
    exact hq.not_le hadd },
end