namespace http://mathhub.info/MitM/core/elliptic_curves ❚

theory Minimal_Weierstrass_model : ?Base =
  include ?Elliptic_curve ❙

 minimal : weierstrass_model ⟶ weierstrass_model ❙
 is_minimal : weierstrass_model ⟶ prop ❘ = [A] (minimal A) ≐ A ❙           
    // need separators ❙
    
 // minimality_condition : {A : tm Weierstrass_model,B : tm Weierstrass_model} ⊦ (minimal A) ≐ B → ⊦ absolute_value (discriminant B) ≤ absolute_value (discriminant A) ❙
 // Dennis: For some reason this doesn't typecheck. I have an idea why, but no idea how to solve it yet. ❙
 minimality_idempotence : {A} ⊦ minimal (minimal A) ≐ minimal A ❙
    
    // the whole thing with minimal stinks of redundancy. it should be reusing partial orders and minimality over N ❙

  minimality_of_minimal_Weierstrass_model : {A} ⊦ is_minimal (minimal_Weierstrass_model A) ❙
  injective_minimal_Weierstrass_model : {A,B} ⊦ minimal_Weierstrass_model A ≐ minimal_Weierstrass_model B ⟶ ⊦ A ≐ B ❙

  // roundtrip_Weierstrass_model_construction : {A} ⊦ A ≐ Weierstrass_model_construction (minimal_Weierstrass_model A) ❙
  // Dennis: now subsumed by elliptic_curve?construction_surjective ❙
❚