The canonical nonsingular-reduction domain of a local Weierstrass equation #
For a singular special Weierstrass cubic, coordinatewise reduction is not defined on every local point with values in the group of nonsingular points: some local points reduce to the singular point. It is, however, defined on a canonical predicate. A point in the formal kernel reduces to infinity; a point outside the formal kernel has integral coordinates, and belongs to the predicate exactly when their residues form a nonsingular point of the special cubic.
This file constructs that predicate and the actual coordinatewise reduction function. Its kernel
is proved to be the exact-pinned formal filtration without any good-reduction hypothesis. The
interface NonsingularReductionIsAdditive says precisely that this canonical predicate is closed
under addition and that coordinatewise reduction respects the group law. From this statement we
construct the canonical identity subgroup and its reduction homomorphism; the downstream module
NonsingularReductionAdditive proves the interface unconditionally.
At five and eleven, an additive-special-fibre classification
(adicRedCurve W₀).Point ≃+ ResidueField 𝒪 and the genuine component bound then produce
TameAdditiveReductionDataAtFive or TameAdditiveReductionDataAtEleven. Thus downstream code no
longer accepts an arbitrary identity subgroup or an arbitrary map to the additive residue group.
The three remaining inputs name the actual group law, special-fibre classification, and component
geometry rather than hiding them. After importing NonsingularReductionAdditive, additivity is
checked and only the latter two inputs remain.
The pointwise reduction, kernel, and negation arguments are a singular-fibre
adaptation of Michael Stoll's good-reduction construction in
EllipticCurves.WeierstrassFormalGroup.Reduction, pinned at commit
3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f under Apache-2.0. Unlike that
source, this file does not assume the reduced cubic is elliptic and restricts
the map to the canonical nonsingular-reduction domain.
A local point has nonsingular reduction when it lies in the formal kernel, or, outside that kernel, its integral coordinates reduce to a nonsingular point of the special Weierstrass cubic.
The universal quantifier over hx makes the formal-kernel case propositionally automatic and
keeps this definition independent of a chosen decision procedure.
Equations
- One or more equations did not get rendered due to their size.
- WeierstrassCurve.Affine.HasNonsingularReduction hW WeierstrassCurve.Affine.Point.zero = True
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every point of the exact-pinned formal kernel belongs to the nonsingular-reduction domain.
Coordinatewise reduction on the canonical nonsingular-reduction domain. Formal-kernel
points reduce to infinity; all other points reduce using the integral coordinates supplied by
integral_of_not_mem.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The actual coordinatewise nonsingular reduction has exactly the formal filtration as its zero fibre. This statement does not assume good reduction or any Néron-model result.
The one group-law compatibility still needed to turn canonical coordinatewise reduction into the identity-component reduction homomorphism. It asserts both closure of the canonical domain and additivity of the already-defined reduction function; no subgroup or map is supplied by the hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical nonsingular-reduction predicate is stable under negation.
The canonical subgroup of local points reducing to the nonsingular locus of the special
Weierstrass cubic. Closure under addition is the sole content imported from
NonsingularReductionIsAdditive; zero, inverses, and containment of the formal kernel are
checked directly.
Equations
- WeierstrassCurve.Affine.nonsingularReductionSubgroup hW hadd = { carrier := {P : W.Point | WeierstrassCurve.Affine.HasNonsingularReduction hW P}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Coordinatewise reduction as a homomorphism on its canonical nonsingular-reduction subgroup.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel of canonical nonsingular reduction is exactly the formal filtration, viewed in the canonical identity subgroup.
Additive reduction forces the discriminant of Mathlib's actual reduced minimal equation to vanish. This is the first checked invariant needed to identify its singular cubic.
Additive reduction also forces c₄ of the actual reduced minimal equation to vanish. In
residue characteristic different from two and three, this distinguishes the cuspidal additive
cubic from the nodal multiplicative cubic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Build the five-adic tame-additive reduction handoff from the canonical nonsingular-reduction domain, actual coordinatewise reduction, an additive classification of the group of nonsingular points of the singular special cubic, and the genuine component bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identical canonical construction at eleven, used by the order-35 route.
Equations
- One or more equations did not get rendered due to their size.