Rational two-torsion bounds

This file bounds the two-torsion of a Weierstrass curve in characteristic different from two and excludes an elementary abelian subgroup of order eight. These are elementary structural inputs to the torsion classification in Mazur's theorem.

theorem MazurTorsion.finite_two_torsion {F : Type u_1} [Field F] [DecidableEq F] (E : WeierstrassCurve F) [NeZero 2] : Finite { P : (WeierstrassCurve.Affine.baseChange E F).Point // 2 • P = 0 }

The points killed by 2 form a finite type in characteristic different from two.

theorem MazurTorsion.ncard_two_torsion_le_four {F : Type u_1} [Field F] [DecidableEq F] (E : WeierstrassCurve F) [NeZero 2] : {P : (WeierstrassCurve.Affine.baseChange E F).Point | 2 • P = 0}.ncard ≤ 4

Over a field of characteristic different from two, an elliptic curve has at most four points killed by 2.

theorem MazurTorsion.ncard_four_torsion_le_sixteen {F : Type u_1} [Field F] [DecidableEq F] (E : WeierstrassCurve F) [NeZero 2] [E.IsElliptic] : {P : (WeierstrassCurve.Affine.baseChange E F).Point | 4 • P = 0}.ncard ≤ 16

For an elliptic curve in characteristic different from two, the points killed by 4 have cardinality at most sixteen.

theorem MazurTorsion.not_injective_zmod_two_cube {F : Type u_1} [Field F] [DecidableEq F] (E : WeierstrassCurve F) [NeZero 2] (φ : ZMod 2 × ZMod 2 × ZMod 2 →+ (WeierstrassCurve.Affine.baseChange E F).Point) : ¬Function.Injective ⇑φ

There is no embedding of an elementary abelian group of order eight into the rational points of a Weierstrass curve in characteristic different from two. This is the full-2-torsion obstruction used in Mazur's classification.