namespace http://mathhub.info/MitM/core/elliptic_curves ❚
import base http://mathhub.info/MitM/Foundation ❚
theory Weierstrass_model : ?Base =
include ☞http://mathhub.info/MitM/core/typedsets?Injective ❙
include ☞base:?Vectors ❙
weierstrass_model : type ❙
polynomial_equation : weierstrass_model ⟶ (polynomial rationalField) ❙
polynomial_equation_injectivity : {A, B} ⊦ polynomial_equation A ≐ polynomial_equation B ⟶ ⊦ A ≐ B ❙
// As the Weierstrass model is really defined by the polynomial_equation, this is really what defines equality. (1) ❙
discriminant : weierstrass_model ⟶ ℤ❙
// missing that this discriminant is really the discriminant of the polynomial equation
// and thus that this factors through the discriminant defined (elsewhere) for multivariate polynomials ❙
// Dennis: is it okay to just define the discriminant of a weierstrass model as above (i.e. as the discriminant of the associated polynomial?) ❙
a_invariants : weierstrass_model ⟶ (vector ℤ 5) ❙
a_invariants_factors_injectivity : ⊦ is_injective a_invariants ❙
// if formulation of (1) changes, this should change too
// really, this should go through the polynomial_equation, as it is more core to defn of a_invariants ❙
❚