The pullback of differentials along an isogeny, and separability

An isogeny φ : W₁ → W₂ pulls differentials back along its function-field pullback, φ^* : Ω[K(W₂)/F] → Ω[K(W₁)/F]. This file packages that map, records its basic properties, and proves the differential criterion for separability: φ is separable exactly when φ^*ω₂ ≠ 0, where ω₂ is the invariant differential of W₂ (Silverman II.4.2(c)).

Main definitions

• TauCeti.Isogeny.pullbackDifferential: the pullback of differentials along an isogeny, the map KaehlerDifferential.mapSemilinear along the function-field pullback packaged F-linearly.

Main results

• TauCeti.Isogeny.pullbackDifferential_D and pullbackDifferential_smul: the pullback of d f is d (φ^* f), and the pullback is semilinear over the function-field pullback.
• TauCeti.Isogeny.pullbackDifferential_id and pullbackDifferential_comp: the pullback is functorial.
• TauCeti.Isogeny.pullbackDifferential_invariantDifferential: φ^*ω₂ is dx / W_Y read at the tautological point of φ, and pullbackDifferential_negIsogeny_invariantDifferential: negation pulls ω back to -ω.
• TauCeti.Isogeny.evalEval_polynomialY_tautologicalPoint_ne_zero: the denominator W_Y does not vanish at the tautological point of an isogeny.
• TauCeti.Isogeny.isSeparable_iff_pullbackDifferential_ne_zero: the differential criterion for separability — the isogeny is separable if and only if it pulls the invariant differential back to a nonzero differential.

Provenance

The criterion is Silverman II.4.2(c). The AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit 513e83879e2f8cbc626eb9e04d660e92be16ccba) proves it for endomorphisms as isSeparable_iff_omegaPullbackCoeff_ne_zero_of_finiteDim, through isSeparable_iff_pullbackKaehler_injective and, in Curves/Differentials.lean, pullbackKaehler_injective_iff_omegaPullbackCoeff_ne_zero. Here it is stated for any isogeny, on the pulled-back differential itself.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.4.2, III.5.

noncomputable def TauCeti.Isogeny.pullbackDifferential {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Ω[W₂.FunctionField⁄F] →ₗ[F] Ω[W₁.FunctionField⁄F]

The pullback of differentials along an isogeny, φ^* : Ω[K(W₂)/F] → Ω[K(W₁)/F]: the map of Kähler differentials along the function-field pullback, KaehlerDifferential.mapSemilinear φ.fieldPullback, packaged as an F-linear map. The semilinear map's type depends on φ through φ.fieldPullback; the F-linear packaging is a type independent of φ.

Equations

• φ.pullbackDifferential = { toFun := ⇑(KaehlerDifferential.mapSemilinear φ.fieldPullback), map_add' := ⋯, map_smul' := ⋯ }

theorem TauCeti.Isogeny.pullbackDifferential_apply {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (η : Ω[W₂.FunctionField⁄F]) : φ.pullbackDifferential η = (KaehlerDifferential.mapSemilinear φ.fieldPullback) η

The pullback of differentials is KaehlerDifferential.mapSemilinear along the function-field pullback.

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_D {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : W₂.FunctionField) : φ.pullbackDifferential ((KaehlerDifferential.D F W₂.FunctionField) f) = (KaehlerDifferential.D F W₁.FunctionField) (φ.fieldPullback f)

The pullback commutes with the universal derivation: φ^*(d f) = d (φ^* f).

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_smul {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (c : W₂.FunctionField) (η : Ω[W₂.FunctionField⁄F]) : φ.pullbackDifferential (c • η) = φ.fieldPullback c • φ.pullbackDifferential η

The pullback of differentials is semilinear over the function-field pullback.

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (id W).pullbackDifferential = LinearMap.id

The identity isogeny pulls differentials back trivially.

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : (ψ.comp φ).pullbackDifferential = φ.pullbackDifferential ∘ₗ ψ.pullbackDifferential

The pullback of differentials is functorial: pulling back along a composite is composing the pullbacks, in the reverse order.

theorem TauCeti.Isogeny.fieldPullback_invariantDifferentialDenom {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : φ.fieldPullback W₂.invariantDifferentialDenom = Polynomial.evalEval φ.pullback.tautologicalPoint.xCoord φ.pullback.tautologicalPoint.yCoord (WeierstrassCurve.toAffine (W₂.baseChange W₁.FunctionField)).polynomialY

The function-field pullback of the denominator 2y + a₁x + a₃ of the invariant differential is W_Y at the tautological point of the isogeny. The target is elliptic so that the tautological point is a point of W₂⁄K(W₁).

theorem TauCeti.Isogeny.evalEval_polynomialY_tautologicalPoint_ne_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : Polynomial.evalEval φ.pullback.tautologicalPoint.xCoord φ.pullback.tautologicalPoint.yCoord (WeierstrassCurve.toAffine (W₂.baseChange W₁.FunctionField)).polynomialY ≠ 0

W_Y does not vanish at the tautological point of an isogeny: it is the pullback of the nonzero denominator of the invariant differential along an injective map.

theorem TauCeti.Isogeny.pullbackDifferential_invariantDifferential {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : φ.pullbackDifferential W₂.invariantDifferential = (Polynomial.evalEval φ.pullback.tautologicalPoint.xCoord φ.pullback.tautologicalPoint.yCoord (WeierstrassCurve.toAffine (W₂.baseChange W₁.FunctionField)).polynomialY)⁻¹ • (KaehlerDifferential.D F W₁.FunctionField) φ.pullback.tautologicalPoint.xCoord

The pullback of the invariant differential is dx / W_Y at the tautological point: the formula ω₂ = dx / (2y + a₁x + a₃) pulled back coordinate by coordinate. The target is elliptic so that the tautological point is a point of W₂⁄K(W₁).

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_negIsogeny_invariantDifferential {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (negIsogeny W).pullbackDifferential W.invariantDifferential = -W.invariantDifferential

Negation pulls the invariant differential back to its negative.

theorem TauCeti.Isogeny.isSeparable_iff_pullbackDifferential_ne_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField ↔ φ.pullbackDifferential W₂.invariantDifferential ≠ 0

An isogeny is separable exactly when it pulls the invariant differential back to a nonzero differential.