English
For polynomials p, q in R[X], the norm of the affine combination p·1 + q·Y in the coordinate ring is given by a explicit quadratic expression in p and q with Weierstrass coefficients a1, a2, a3, a4, a6, namely p^2 − p q (a1 X + a3) − q^2 (X^3 + a2 X^2 + a4 X + a6).
Русский
Для полиномов p, q ∈ R[X] нормa элемента p·1 + q·Y в координатном кольце задается явным квадратичным выражением в p и q с коэффициентами a1, a2, a3, a4, a6: p^2 − p q (a1 X + a3) − q^2 (X^3 + a2 X^2 + a4 X + a6).
LaTeX
$$$\\operatorname{norm}_{R[X]}\\big(p\\cdot 1 + q\\cdot Y\\big) = p^2 - p q\\,(a_1 X + a_3) - q^2\\,(X^3 + a_2 X^2 + a_4 X + a_6)$$$
Lean4
theorem norm_smul_basis (p q : R[X]) :
Algebra.norm R[X] (p • (1 : W'.CoordinateRing) + q • mk W' Y) =
p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) :=
by
simp_rw [Algebra.norm_eq_matrix_det <| CoordinateRing.basis W', Matrix.det_fin_two, Algebra.leftMulMatrix_eq_repr_mul,
basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add, Finsupp.add_apply, map_smul, Finsupp.smul_apply, ←
basis_zero, ← basis_one, Basis.repr_self_apply, if_pos, one_ne_zero, if_false, smul_eq_mul]
ring1
