English
The constant term of the univariate polynomial Ψ₂Sq in the coordinate ring equals ψ₂^2 minus four times the affine coordinate polynomial.
Русский
Постоянный член многочлена Ψ₂Sq равен ψ₂^2 минус четыре умноженное на аффинный координатный многочлен.
LaTeX
$$$$C(\Psi_2^{2}) = \psi_2^{2} - 4 \cdot \text{polynomial}^{\text{affine}}.$$$$
Lean4
theorem XYIdeal_eq₂ [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
XYIdeal W x₂ (C y₂) = XYIdeal W x₂ (linePolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
by
have hy₂ : y₂ = (linePolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂).eval x₂ :=
by
by_cases hx : x₁ = x₂
· have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
simp [linePolynomial]
· simp [field, linePolynomial, slope_of_X_ne hx, sub_ne_zero_of_ne hx]
ring1
nth_rw 1 [hy₂]
simp only [XYIdeal, XClass, YClass, linePolynomial]
rw [← span_pair_add_mul_right <| mk W <| C <| C <| -W.slope x₁ x₂ y₁ y₂, ← map_mul, ← map_add]
apply congr_arg (_ ∘ _ ∘ _ ∘ _)
simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul]
C_simp
ring1
