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 ❙