Divisibility of Weierstrass invariants in Tate normal forms

The coefficient bounds in the late branches of Tate's algorithm imply these bounds on the Weierstrass invariants. They are polynomial identities over any commutative ring. The bounds on b₄, b₆, and b₈ carry an exponent shift n, so that one statement covers both the Step 8 normal form and the stronger Step 10 normal form. The Step 8–10 discriminant bounds in TateAlgorithm.LateDiscriminant use them.

Reference

J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, IV.9, Steps 8–10 of Tate's algorithm.

theorem WeierstrassCurve.pow_two_dvd_b₂ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) (h₁ : ϖ ∣ W.a₁) (h₂ : ϖ ^ 2 ∣ W.a₂) : ϖ ^ 2 ∣ W.b₂

If ϖ ∣ a₁ and ϖ² ∣ a₂, then ϖ² ∣ b₂.

theorem WeierstrassCurve.pow_add_one_dvd_b₄ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) {n : ℕ} (h₁ : ϖ ∣ W.a₁) (h₃ : ϖ ^ n ∣ W.a₃) (h₄ : ϖ ^ (n + 1) ∣ W.a₄) : ϖ ^ (n + 1) ∣ W.b₄

If ϖ ∣ a₁, ϖⁿ ∣ a₃, and ϖⁿ⁺¹ ∣ a₄, then ϖⁿ⁺¹ ∣ b₄.

theorem WeierstrassCurve.pow_add_four_dvd_b₆ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) {n : ℕ} (h₃ : ϖ ^ (n + 2) ∣ W.a₃) (h₆ : ϖ ^ (n + 4) ∣ W.a₆) : ϖ ^ (n + 4) ∣ W.b₆

If ϖⁿ⁺² ∣ a₃ and ϖⁿ⁺⁴ ∣ a₆, then ϖⁿ⁺⁴ ∣ b₆.

theorem WeierstrassCurve.pow_add_six_dvd_b₈ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) {n : ℕ} (h₁ : ϖ ∣ W.a₁) (h₂ : ϖ ^ 2 ∣ W.a₂) (h₃ : ϖ ^ (n + 2) ∣ W.a₃) (h₄ : ϖ ^ (n + 3) ∣ W.a₄) (h₆ : ϖ ^ (n + 4) ∣ W.a₆) : ϖ ^ (n + 6) ∣ W.b₈

If ϖ ∣ a₁, ϖ² ∣ a₂, ϖⁿ⁺² ∣ a₃, ϖⁿ⁺³ ∣ a₄, and ϖⁿ⁺⁴ ∣ a₆, then ϖⁿ⁺⁶ ∣ b₈. The case n = 0 is the Step 8 normal form, and n = 1 is the Step 10 normal form.