Definitions/Def_ModularCurve_LevelNormalForm.lean

Over a commutative ring T, the predicate ModularCurve.IsNormalForm takes a natural number \ell, a Weierstrass curve W over T (with coefficients a_1,\dots,a_6) and a quadruple D = (x_P, y_P, x_Q, y_Q) of elements of T (the project's LevelPData, the coordinates of two affine points), and asserts a list of equations on these data, split according to whether \ell equals 3. For \ell = 3 it asserts a_2 = 0, a_4 = 0, a_6 = 0, x_P = 0, y_P = 0 and x_Q = y_Q. For every \ell \neq 3 it asserts a_4 = 0, a_6 = 0, a_2 = a_3, x_P = 0 and y_P = 0; thus in the second case the curve is y^2 + a_1xy + a_3y = x^3 + a_3x^2 with the first point at the affine origin, the shape of the Tate normal form, while in the case \ell = 3 the curve is y^2 + a_1xy + a_3y = x^3 with the first point at the origin and the second on the line x = y. It is a condition on a chosen Weierstrass presentation together with chosen coordinates, not on an isomorphism class, and it imposes nothing beyond these equations: neither invertibility of the discriminant nor the condition IsLevelPStructure on D is required. Two rewriting lemmas record the two branches of the definition explicitly, and ModularCurve.IsNormalForm.map states that the predicate is preserved by base change along a ring homomorphism f : T \to T', applied to the coefficients of W and to the four coordinates of D.