Elliptic curves: semistability (predicate)

[CBirkbeck]

Goal

Define the predicate IsSemistable E: E has good or multiplicative reduction at every prime (no additive reduction), equivalently its conductor is squarefree.

What already exists

• mathlib AlgebraicGeometry/EllipticCurve/Reduction.lean: HasGoodReduction, HasMultiplicativeReduction, HasAdditiveReduction (with partition/exclusivity theorems), minimal model.

What's missing

• IsSemistable E : Prop and the equivalence IsSemistable E ↔ ∀ p, ¬ HasAdditiveReduction E p (and ↔ good-or-multiplicative everywhere).

Test cases

• A semistable curve (e.g. conductor 11, 37) is IsSemistable; a curve with additive reduction is not.

References

• LMFDB: https://beta.lmfdb.org/knowledge/show/ec.semistable ; Blueprint: Elliptic curves

Blueprint & LMFDB targets

• ec.semistable — blueprint · LMFDB

Rendered blueprint: https://cbirkbeck.github.io/LeanBridge/ — the definitions / LMFDB knowls this issue feeds.

[Multramate]

I believe Jane Shi has already done this in #71