Theorems · Definition · algebraic geometry
WeierstrassCurve.Jacobian.NonsingularLift
{R : Type r} → [inst : CommRing R] → WeierstrassCurve.Jacobian R → WeierstrassCurve.Jacobian.PointClass R → PropThe proposition that a Jacobian point class on a Weierstrass curve W is nonsingular.
If P is a Jacobian point representative on W, then W.NonsingularLift ⟦P⟧ is definitionally
equivalent to W.Nonsingular P.
Note that this definition is only mathematically accurate for fields.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- WeierstrassCurve.Jacobianstatement and proof · cited by 232
- WeierstrassCurve.Jacobian.Nonsingularproof · cited by 40
- WeierstrassCurve.Jacobian.PointClassstatement and proof · cited by 21
Cited by26
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Jacobian.Point.casesOnstatement and proof · cited by 2
- WeierstrassCurve.Jacobian.nonsingularLift_somestatement · cited by 2
- WeierstrassCurve.Jacobian.Point.extproof · cited by 1
- WeierstrassCurve.Jacobian.Point.mk_ne_zerostatement and proof · cited by 1
- WeierstrassCurve.Jacobian.Point.mk.injstatement and proof · cited by 1
- WeierstrassCurve.Jacobian.Point.mk.noConfusionstatement and proof · cited by 1
- WeierstrassCurve.Jacobian.nonsingularLift_zerostatement · cited by 1
- WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_leftstatement and proof · cited by 0
- WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_rightstatement and proof · cited by 0
- WeierstrassCurve.Jacobian.Point.fromAffine_somestatement · cited by 0
- WeierstrassCurve.Jacobian.Point.mk_pointstatement and proof · cited by 0
- WeierstrassCurve.Jacobian.Point.noConfusionproof · cited by 0