Theorems · Definition · number theory

WeierstrassCurve.reduction

(R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [inst_2 : IsDiscreteValuationRing R] →
        {K : Type u_2} →
          [inst_3 : Field K] →
            [inst_4 : Algebra R K] →
              [inst_5 : IsFractionRing R K] →
                (W : WeierstrassCurve K) →
                  [WeierstrassCurve.IsMinimal R W] → WeierstrassCurve (IsLocalRing.ResidueField R)

The reduction of a Weierstrass curve over K given by a minimal Weierstrass equation, which is a Weierstrass curve over the residue field of R.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Cited by

2 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainIsDiscreteValuationRingFieldAlgebraIsFractionRingWeierstrassCurve.IsMinimal