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 ❙
❚