Negation

The involution (x, y) ↦ (x, -y - a₁x - a₃) of a Weierstrass curve is negation for the group law. Its pullback on functions is CoordinateRing.conj, the conjugation of the coordinate ring over F[X], so negation is an isogeny of W with itself, an involution, and of degree one.

Postcomposing with it negates on the hom carrier, which is the Neg structure the carrier's additive group is built from. That this pullback really is negation, and not just some involution of degree one, is tautologicalPoint_negPullback: its tautological point is the negated generic point.

Main definitions

• TauCeti.Isogeny.negPullback: the coordinate pullback x ↦ conj x.
• TauCeti.Isogeny.negIsogeny: the same map packaged as an Isogeny W W.
• TauCeti.Isogeny.Hom.instNeg: negation on Hom W₁ W₂, by postcomposition.

Main results

• TauCeti.Isogeny.negIsogeny_comp_negIsogeny: negation is an involution.
• TauCeti.Isogeny.degree_negIsogeny: negation has degree one, so it is an automorphism of W fixing the point at infinity.
• TauCeti.Isogeny.Hom.neg_comp and TauCeti.Isogeny.Hom.degree_neg: negation passes through composition, and preserves degrees, on the carrier.
• TauCeti.Isogeny.tautologicalPoint_negPullback: read at the generic point, negation is the group law's inverse — which is what identifies this pullback as negation rather than merely some degree-one involution.

The MapsInfinity condition says each x of the coordinate ring is integral over the pulled-back copy. Conjugation is an equivalence, so every function is the pullback of its own conjugate — the algebraic form of "negation fixes the point at infinity".

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.2.

noncomputable def TauCeti.Isogeny.negPullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : CoordinatePullback W W

The negation coordinate pullback: an element of the coordinate ring is sent to its conjugate over F[X], viewed in the function field.

Equations

• TauCeti.Isogeny.negPullback W = (IsScalarTower.toAlgHom F W.CoordinateRing W.FunctionField).comp (AlgHom.restrictScalars F ↑(TauCeti.WeierstrassCurve.Affine.CoordinateRing.conj W))

@[simp]

theorem TauCeti.Isogeny.negPullback_apply {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (x : W.CoordinateRing) : (negPullback W) x = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.conj W) x)

The negation pullback is conjugation.

theorem TauCeti.Isogeny.mapsInfinity_negPullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (negPullback W).MapsInfinity

Negation maps the point at infinity to itself.

noncomputable def TauCeti.Isogeny.negIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : Isogeny W W

Negation, as an isogeny W ⟶ W.

Equations

• TauCeti.Isogeny.negIsogeny W = { pullback := TauCeti.Isogeny.negPullback W, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.negIsogeny_pullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (negIsogeny W).pullback = negPullback W

The negation isogeny's pullback is conjugation.

@[simp]

theorem TauCeti.Isogeny.negIsogeny_comp_negIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (negIsogeny W).comp (negIsogeny W) = id W

Negation is an involution.

@[simp]

theorem TauCeti.Isogeny.degree_negIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (negIsogeny W).degree = 1

Negation has degree one, so it is an automorphism of W fixing the point at infinity.

@[simp]

theorem TauCeti.Isogeny.tautologicalPoint_negPullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : (negPullback W).tautologicalPoint = -W.genericPoint

Negation's tautological point is the negated generic point. This is what identifies negIsogeny as negation: read at the generic point of W, it is the group law's inverse.

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.Hom.instNeg {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} : Neg (Hom W₁ W₂)

Negation on the hom carrier, by postcomposition with the negation isogeny. This is the Neg structure of the carrier's additive group; the addition is not built here.

Equations

• TauCeti.Isogeny.Hom.instNeg = { neg := fun (f : TauCeti.Isogeny.Hom W₁ W₂) => (TauCeti.Isogeny.Hom.ofIsogeny (TauCeti.Isogeny.negIsogeny W₂)).comp f }

theorem TauCeti.Isogeny.Hom.neg_def {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (f : Hom W₁ W₂) : -f = (ofIsogeny (negIsogeny W₂)).comp f

The equation lemma for negation: the definition's body is not exposed across the module boundary, so this is how downstream modules compute with it.

@[simp]

theorem TauCeti.Isogeny.Hom.neg_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} : -0 = 0

The zero map is its own negative.

@[simp]

theorem TauCeti.Isogeny.Hom.neg_ofIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : -ofIsogeny φ = ofIsogeny ((negIsogeny W₂).comp φ)

Negating a nonzero element postcomposes the underlying isogeny.

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.Hom.instInvolutiveNeg {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} : InvolutiveNeg (Hom W₁ W₂)

Negation on the carrier is an involution, because it is on the curve.

Equations

• TauCeti.Isogeny.Hom.instInvolutiveNeg = { toNeg := TauCeti.Isogeny.Hom.instNeg, neg_neg := ⋯ }

@[simp]

theorem TauCeti.Isogeny.Hom.neg_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (g : Hom W₂ W₃) (f : Hom W₁ W₂) : (-g).comp f = -g.comp f

Negation passes through composition on the left.

@[simp]

theorem TauCeti.Isogeny.Hom.degree_neg {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (f : Hom W₁ W₂) : (-f).degree = f.degree

Negation preserves degrees, negation itself having degree one.