import Mathlib

open MvPolynomial

namespace ProjWeierstrassCubicPrime

section CommRing

variable {F : Type*} [CommRing F]

noncomputable def wCubic (V : WeierstrassCurve.Projective F) : Cubic (MvPolynomial (Fin 2) F) :=
  ⟨1, C V.a₂ * X 1, C V.a₄ * X 1 ^ 2 - C V.a₁ * X 0 * X 1,
    C V.a₆ * X 1 ^ 3 - X 0 ^ 2 * X 1 - C V.a₃ * X 0 * X 1 ^ 2⟩

theorem wCubic_toPoly_coeff_zero (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.coeff 0
      = C V.a₆ * X 1 ^ 3 - X 0 ^ 2 * X 1 - C V.a₃ * X 0 * X 1 ^ 2 := by
  rw [Cubic.coeff_eq_d]
  rfl

theorem wCubic_toPoly_coeff_one (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.coeff 1 = C V.a₄ * X 1 ^ 2 - C V.a₁ * X 0 * X 1 := by
  rw [Cubic.coeff_eq_c]
  rfl

theorem wCubic_toPoly_coeff_two (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.coeff 2 = C V.a₂ * X 1 := by
  rw [Cubic.coeff_eq_b]
  rfl

theorem finSuccEquiv_polynomial (V : WeierstrassCurve.Projective F) :
    finSuccEquiv F 2 V.polynomial = -(wCubic V).toPoly := by
  have h1 : (1 : Fin 3) = (0 : Fin 2).succ := rfl
  have h2 : (2 : Fin 3) = (1 : Fin 2).succ := rfl
  have hC : ∀ a : F, finSuccEquiv F 2 (C a) = Polynomial.C (C a) := fun a => by
    simp [finSuccEquiv_apply]
  rw [WeierstrassCurve.Projective.polynomial, wCubic, Cubic.toPoly]
  simp only [map_add, map_sub, map_mul, map_pow, map_one, finSuccEquiv_X_zero, h1, h2,
    finSuccEquiv_X_succ, hC]
  ring

theorem wCubic_toPoly_monic (V : WeierstrassCurve.Projective F) : (wCubic V).toPoly.Monic :=
  Cubic.monic_of_a_eq_one rfl

end CommRing

section IsDomain

variable {F : Type*} [CommRing F] [IsDomain F]

theorem wCubic_toPoly_natDegree (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.natDegree = 3 :=
  Cubic.natDegree_of_a_ne_zero one_ne_zero

theorem wCubic_isEisensteinAt (V : WeierstrassCurve.Projective F) :
    (wCubic V).toPoly.IsEisensteinAt (Ideal.span {(X 1 : MvPolynomial (Fin 2) F)}) := by
  refine ⟨?_, ?_, ?_⟩
  ·
    rw [(wCubic_toPoly_monic V).leadingCoeff]
    intro h
    rw [Ideal.mem_span_singleton] at h
    exact MvPolynomial.X_prime.not_unit (isUnit_of_dvd_one h)
  ·
    intro n hn
    rw [wCubic_toPoly_natDegree V] at hn
    interval_cases n
    · rw [wCubic_toPoly_coeff_zero, Ideal.mem_span_singleton]
      exact ⟨C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1, by ring⟩
    · rw [wCubic_toPoly_coeff_one, Ideal.mem_span_singleton]
      exact ⟨C V.a₄ * X 1 - C V.a₁ * X 0, by ring⟩
    · rw [wCubic_toPoly_coeff_two, Ideal.mem_span_singleton]
      exact ⟨C V.a₂, by ring⟩
  ·
    rw [wCubic_toPoly_coeff_zero, Ideal.span_singleton_pow, Ideal.mem_span_singleton]
    intro hdvd
    have he : (X 1 : MvPolynomial (Fin 2) F)
        * (C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1)
        = C V.a₆ * X 1 ^ 3 - X 0 ^ 2 * X 1 - C V.a₃ * X 0 * X 1 ^ 2 := by ring
    have h2 : (X 1 : MvPolynomial (Fin 2) F)
        ∣ C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1 := by
      refine (mul_dvd_mul_iff_left (MvPolynomial.X_ne_zero (1 : Fin 2))).mp ?_
      rw [show (X 1 : MvPolynomial (Fin 2) F) * X 1 = X 1 ^ 2 from (pow_two _).symm, he]
      exact hdvd
    have h3 : (X 1 : MvPolynomial (Fin 2) F) ∣ X 0 ^ 2 := by
      have h4 := dvd_sub (dvd_sub
        (dvd_mul_right (X 1 : MvPolynomial (Fin 2) F) (C V.a₆ * X 1))
        (dvd_mul_right (X 1 : MvPolynomial (Fin 2) F) (C V.a₃ * X 0))) h2
      have h5 : X 1 * (C V.a₆ * X 1) - X 1 * (C V.a₃ * X 0)
          - (C V.a₆ * X 1 ^ 2 - X 0 ^ 2 - C V.a₃ * X 0 * X 1)
          = (X 0 ^ 2 : MvPolynomial (Fin 2) F) := by ring
      rwa [h5] at h4
    have h6 : (X 1 : MvPolynomial (Fin 2) F) ∣ X 0 :=
      MvPolynomial.X_prime.dvd_of_dvd_pow h3
    rw [MvPolynomial.X_dvd_X] at h6
    exact absurd h6 (by decide)

theorem irreducible_wCubic_toPoly (V : WeierstrassCurve.Projective F) :
    Irreducible (wCubic V).toPoly :=
  (wCubic_isEisensteinAt V).irreducible
    ((Ideal.span_singleton_prime (MvPolynomial.X_ne_zero _)).mpr MvPolynomial.X_prime)
    (wCubic_toPoly_monic V).isPrimitive
    (by rw [wCubic_toPoly_natDegree V]; norm_num)

theorem irreducible_polynomial (V : WeierstrassCurve.Projective F) :
    Irreducible V.polynomial := by
  have hneg : Irreducible (-(wCubic V).toPoly) :=
    (Associated.irreducible ⟨-1, by simp⟩ (irreducible_wCubic_toPoly V))
  have himg : Irreducible (finSuccEquiv F 2 V.polynomial) := by
    rw [finSuccEquiv_polynomial V]
    exact hneg
  exact (MulEquiv.irreducible_iff (finSuccEquiv F 2)).mp himg

theorem polynomial_ne_zero (V : WeierstrassCurve.Projective F) : V.polynomial ≠ 0 :=
  (irreducible_polynomial V).ne_zero

theorem not_isUnit_polynomial (V : WeierstrassCurve.Projective F) : ¬IsUnit V.polynomial :=
  (irreducible_polynomial V).not_isUnit

end IsDomain

section UFD

variable {F : Type*} [CommRing F] [IsDomain F] [UniqueFactorizationMonoid F]

theorem prime_polynomial (V : WeierstrassCurve.Projective F) : Prime V.polynomial :=
  UniqueFactorizationMonoid.irreducible_iff_prime.mp (irreducible_polynomial V)

theorem span_polynomial_isPrime (V : WeierstrassCurve.Projective F) :
    (Ideal.span {V.polynomial}).IsPrime :=
  (Ideal.span_singleton_prime (polynomial_ne_zero V)).mpr (prime_polynomial V)

theorem isDomain_quotient_span_polynomial (V : WeierstrassCurve.Projective F) :
    IsDomain (MvPolynomial (Fin 3) F ⧸ Ideal.span {V.polynomial}) := by
  have h : (Ideal.span {V.polynomial}).IsPrime := span_polynomial_isPrime V
  exact Ideal.Quotient.isDomain _

end UFD

section Homogeneous

variable {F : Type*} [CommRing F]

theorem isHomogeneous_polynomial (V : WeierstrassCurve.Projective F) :
    V.polynomial.IsHomogeneous 3 := by
  have hA : (X 1 ^ 2 * X 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_X_pow (R := F) (1 : Fin 3) 2).mul (isHomogeneous_X F (2 : Fin 3))
    norm_num at h
    exact h
  have hB : (C V.a₁ * X 0 * X 1 * X 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := ((isHomogeneous_C_mul_X V.a₁ (0 : Fin 3)).mul
      (isHomogeneous_X F (1 : Fin 3))).mul (isHomogeneous_X F (2 : Fin 3))
    norm_num at h
    exact h
  have hC : (C V.a₃ * X 1 * X 2 ^ 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_C_mul_X V.a₃ (1 : Fin 3)).mul (isHomogeneous_X_pow (2 : Fin 3) 2)
    norm_num at h
    exact h
  have hD : (X 0 ^ 3 : MvPolynomial (Fin 3) F).IsHomogeneous 3 :=
    isHomogeneous_X_pow (0 : Fin 3) 3
  have hE : (C V.a₂ * X 0 ^ 2 * X 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_C_mul_X_pow V.a₂ (0 : Fin 3) 2).mul (isHomogeneous_X F (2 : Fin 3))
    norm_num at h
    exact h
  have hF : (C V.a₄ * X 0 * X 2 ^ 2 : MvPolynomial (Fin 3) F).IsHomogeneous 3 := by
    have h := (isHomogeneous_C_mul_X V.a₄ (0 : Fin 3)).mul (isHomogeneous_X_pow (2 : Fin 3) 2)
    norm_num at h
    exact h
  have hG : (C V.a₆ * X 2 ^ 3 : MvPolynomial (Fin 3) F).IsHomogeneous 3 :=
    isHomogeneous_C_mul_X_pow V.a₆ (2 : Fin 3) 3
  rw [WeierstrassCurve.Projective.polynomial]
  exact ((hA.add hB).add hC).sub (((hD.add hE).add hF).add hG)

theorem totalDegree_polynomial {F : Type*} [CommRing F] [IsDomain F]
    (V : WeierstrassCurve.Projective F) : V.polynomial.totalDegree = 3 :=
  (isHomogeneous_polynomial V).totalDegree (polynomial_ne_zero V)

end Homogeneous

section Gates

def gateCurveA : WeierstrassCurve ℚ := ⟨0, 0, 1, 0, 0⟩

def gateCurveB : WeierstrassCurve ℚ := ⟨0, 0, 0, 1, 0⟩

theorem gate_prime_A : Prime gateCurveA.toProjective.polynomial :=
  prime_polynomial _

theorem gate_prime_B : Prime gateCurveB.toProjective.polynomial :=
  prime_polynomial _

theorem gate_span_isPrime_A : (Ideal.span {gateCurveA.toProjective.polynomial}).IsPrime :=
  span_polynomial_isPrime _

theorem gate_isDomain_quotient_A :
    IsDomain (MvPolynomial (Fin 3) ℚ ⧸ Ideal.span {gateCurveA.toProjective.polynomial}) :=
  isDomain_quotient_span_polynomial _

theorem gate_quotient_nontrivial_A :
    Nontrivial (MvPolynomial (Fin 3) ℚ ⧸ Ideal.span {gateCurveA.toProjective.polynomial}) :=
  gate_isDomain_quotient_A.toNontrivial

theorem gate_span_ne_top_A : Ideal.span {gateCurveA.toProjective.polynomial} ≠ ⊤ :=
  gate_span_isPrime_A.ne_top

theorem gate_span_ne_bot_A : Ideal.span {gateCurveA.toProjective.polynomial} ≠ ⊥ := by
  rw [Ne, Ideal.span_singleton_eq_bot]
  exact polynomial_ne_zero _

theorem gate_eval_A :
    eval ![(0 : ℚ), 1, 1] gateCurveA.toProjective.polynomial = 2 := by
  rw [WeierstrassCurve.Projective.eval_polynomial]
  norm_num [gateCurveA, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons]

theorem gate_eval_B :
    eval ![(0 : ℚ), 1, 1] gateCurveB.toProjective.polynomial = 1 := by
  rw [WeierstrassCurve.Projective.eval_polynomial]
  norm_num [gateCurveB, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons]

theorem gate_polynomial_A_ne_B :
    gateCurveA.toProjective.polynomial ≠ gateCurveB.toProjective.polynomial := by
  intro h
  have hA := gate_eval_A
  rw [h, gate_eval_B] at hA
  norm_num at hA

theorem gate_isHomogeneous_A : gateCurveA.toProjective.polynomial.IsHomogeneous 3 :=
  isHomogeneous_polynomial _

theorem gate_totalDegree_A : gateCurveA.toProjective.polynomial.totalDegree = 3 :=
  totalDegree_polynomial _

end Gates

end ProjWeierstrassCubicPrime

/--
info: 'ProjWeierstrassCubicPrime.wCubic' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_zero
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_one' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_one
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_two' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_coeff_two
/--
info: 'ProjWeierstrassCubicPrime.finSuccEquiv_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.finSuccEquiv_polynomial
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_monic' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_monic
/--
info: 'ProjWeierstrassCubicPrime.wCubic_toPoly_natDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_toPoly_natDegree
/--
info: 'ProjWeierstrassCubicPrime.wCubic_isEisensteinAt' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.wCubic_isEisensteinAt
/--
info: 'ProjWeierstrassCubicPrime.irreducible_wCubic_toPoly' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.irreducible_wCubic_toPoly
/--
info: 'ProjWeierstrassCubicPrime.irreducible_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.irreducible_polynomial
/--
info: 'ProjWeierstrassCubicPrime.polynomial_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.polynomial_ne_zero
/--
info: 'ProjWeierstrassCubicPrime.not_isUnit_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.not_isUnit_polynomial
/--
info: 'ProjWeierstrassCubicPrime.prime_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.prime_polynomial
/--
info: 'ProjWeierstrassCubicPrime.span_polynomial_isPrime' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.span_polynomial_isPrime
/--
info: 'ProjWeierstrassCubicPrime.isDomain_quotient_span_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.isDomain_quotient_span_polynomial
/--
info: 'ProjWeierstrassCubicPrime.isHomogeneous_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.isHomogeneous_polynomial
/--
info: 'ProjWeierstrassCubicPrime.totalDegree_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.totalDegree_polynomial
/--
info: 'ProjWeierstrassCubicPrime.gateCurveA' depends on axioms: [propext, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gateCurveA
/--
info: 'ProjWeierstrassCubicPrime.gateCurveB' depends on axioms: [propext, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gateCurveB
/--
info: 'ProjWeierstrassCubicPrime.gate_prime_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_prime_A
/--
info: 'ProjWeierstrassCubicPrime.gate_prime_B' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_prime_B
/--
info: 'ProjWeierstrassCubicPrime.gate_span_isPrime_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_span_isPrime_A
/--
info: 'ProjWeierstrassCubicPrime.gate_isDomain_quotient_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_isDomain_quotient_A
/--
info: 'ProjWeierstrassCubicPrime.gate_quotient_nontrivial_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_quotient_nontrivial_A
/--
info: 'ProjWeierstrassCubicPrime.gate_span_ne_top_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_span_ne_top_A
/--
info: 'ProjWeierstrassCubicPrime.gate_span_ne_bot_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_span_ne_bot_A
/--
info: 'ProjWeierstrassCubicPrime.gate_eval_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_eval_A
/--
info: 'ProjWeierstrassCubicPrime.gate_eval_B' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_eval_B
/--
info: 'ProjWeierstrassCubicPrime.gate_polynomial_A_ne_B' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_polynomial_A_ne_B
/--
info: 'ProjWeierstrassCubicPrime.gate_isHomogeneous_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_isHomogeneous_A
/--
info: 'ProjWeierstrassCubicPrime.gate_totalDegree_A' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms ProjWeierstrassCubicPrime.gate_totalDegree_A