The pullback of the invariant differential is additive in the morphism

A morphism f : W₁ → W₂ of elliptic curves pulls the invariant differential ω₂ of W₂ back to a differential f^*ω₂ on W₁: along the isogeny when f is nonzero, and to 0 when f = 0. This file proves that the assignment f ↦ f^*ω₂ is additive (Silverman III.5.2), (f + g)^*ω₂ = f^*ω₂ + g^*ω₂, together with (-f)^*ω₂ = -f^*ω₂.

The pullback is functorial in the morphism (pullbackDifferential_id and pullbackDifferential_comp), and additivity makes f ↦ f^*ω₂ compatible with the group structure of Hom W₁ W₂: the pullback of the invariant differential along a sum, a difference or a negative of morphisms is computed termwise. Its first use is the separability of 1 − π over a finite field, TauCeti.Isogeny.isSeparable_oneSubFrobeniusIsogeny: (1 − π)^*ω = ω − π^*ω = ω ≠ 0.

Main definitions

• TauCeti.Isogeny.Hom.pullbackDifferential: the pullback of differentials along a morphism.

Main results

• TauCeti.Isogeny.Hom.pullbackDifferential_add_invariantDifferential: (f + g)^*ω = f^*ω + g^*ω.
• TauCeti.Isogeny.Hom.pullbackDifferential_neg_invariantDifferential: (-f)^*ω = -f^*ω.
• TauCeti.Isogeny.Hom.pullbackDifferential_sub_invariantDifferential: (f - g)^*ω = f^*ω - g^*ω.
• TauCeti.Isogeny.Hom.pullbackDifferential_zsmul_invariantDifferential: (n • f)^*ω = n • f^*ω.
• TauCeti.Isogeny.Hom.pullbackDifferential_zsmul_id_invariantDifferential: [n]^*ω = n • ω.
• TauCeti.Isogeny.Hom.pullbackDifferential_id and pullbackDifferential_comp: the pullback is functorial in the morphism.
• pullbackDifferential_zsmul_sub_zsmul_id_invariantDifferential_of_pullbackDifferential_eq_zero: (r • f - s • id)^*ω = -s • ω when f^*ω = 0.
• TauCeti.Isogeny.Hom.zsmul_sub_zsmul_id_ne_zero_of_pullbackDifferential_eq_zero and Hom.isSeparable_toIsogeny_zsmul_sub_zsmul_id_iff_of_pullbackDifferential_eq_zero: the pencil is nonzero when s ≠ 0 in the field, and a nonzero pencil is separable exactly then.

Provenance

The AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit 513e83879e2f8cbc626eb9e04d660e92be16ccba) states the additivity only in the form (1 + α)^*ω = ω + α^*ω for an endomorphism α, as kaehlerD_addPullback_x_eq_one_add_smul_omega in RouteBGeneral.lean, and for a scalar coefficient omegaPullbackCoeff of the pulled-back d x rather than for the differential. Here the statement is for two arbitrary morphisms f, g : W₁ → W₂ and for the pulled-back differential itself; nothing is taken from the source.

The same revision proves Frobenius-pencil separability as genuineIsogSmulSub_isSeparable in GapSpines.lean, using the scalar identity genuineIsogSmulSub_omegaPullbackCoeff, and transports it across base change in WeilPairing/PencilSeparable.lean. The pencil lemmas here are independent proofs for any endomorphism f with f^*ω = 0, using the pulled-back differential and function-field separability; no finite-field or Frobenius hypothesis is needed.

References

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

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

The pullback of differentials along a morphism: the pullback along the isogeny for a nonzero morphism, and zero for the zero morphism.

Equations

• f.pullbackDifferential = if hf : f = 0 then 0 else (TauCeti.Isogeny.Hom.toIsogeny hf).pullbackDifferential

@[simp]

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

@[simp]

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

@[simp]

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

The identity morphism pulls differentials back trivially.

@[simp]

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

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

@[simp]

theorem TauCeti.Isogeny.Hom.pullbackDifferential_pow {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} (f : Hom W₁ W₁) (n : ℕ) : (f ^ n).pullbackDifferential = f.pullbackDifferential ^ n

Pullback along a power is the corresponding power of the pullback operator.

@[simp]

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

Negation negates the pullback of the invariant differential.

@[simp]

theorem TauCeti.Isogeny.Hom.pullbackDifferential_add_invariantDifferential {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f g : Hom W₁ W₂) : (f + g).pullbackDifferential W₂.invariantDifferential = f.pullbackDifferential W₂.invariantDifferential + g.pullbackDifferential W₂.invariantDifferential

The pullback of the invariant differential is additive in the morphism (Silverman III.5.2): (f + g)^*ω = f^*ω + g^*ω.

@[simp]

theorem TauCeti.Isogeny.Hom.pullbackDifferential_sub_invariantDifferential {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f g : Hom W₁ W₂) : (f - g).pullbackDifferential W₂.invariantDifferential = f.pullbackDifferential W₂.invariantDifferential - g.pullbackDifferential W₂.invariantDifferential

The pullback of the invariant differential respects subtraction.

@[simp]

theorem TauCeti.Isogeny.Hom.pullbackDifferential_zsmul_invariantDifferential {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (n : ℤ) : (n • f).pullbackDifferential W₂.invariantDifferential = n • f.pullbackDifferential W₂.invariantDifferential

The pullback of ω scales with an integer multiple of a morphism: (n • f)^*ω = n • f^*ω.

theorem TauCeti.Isogeny.Hom.pullbackDifferential_zsmul_id_invariantDifferential {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (n : ℤ) : (n • id W).pullbackDifferential W.invariantDifferential = n • W.invariantDifferential

[n]^*ω = n • ω (Silverman III.5.4): the invariant differential pulls back along multiplication by n with the factor n.

theorem TauCeti.Isogeny.Hom.pullbackDifferential_zsmul_sub_zsmul_id_invariantDifferential_of_pullbackDifferential_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {f : Hom W W} (hf : f.pullbackDifferential W.invariantDifferential = 0) (r s : ℤ) : (r • f - s • id W).pullbackDifferential W.invariantDifferential = -s • W.invariantDifferential

If f kills the invariant differential, the pencil r • f - s • id pulls it back to -s • ω.

theorem TauCeti.Isogeny.Hom.zsmul_sub_zsmul_id_ne_zero_of_pullbackDifferential_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {f : Hom W W} (hf : f.pullbackDifferential W.invariantDifferential = 0) (r s : ℤ) (hs : ↑s ≠ 0) : r • f - s • id W ≠ 0

If f kills the invariant differential and s is nonzero in the field, then r • f - s • id is nonzero.

theorem TauCeti.Isogeny.Hom.isSeparable_toIsogeny_zsmul_sub_zsmul_id_iff_of_pullbackDifferential_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {f : Hom W W} (hf : f.pullbackDifferential W.invariantDifferential = 0) (r s : ℤ) (h : r • f - s • id W ≠ 0) : Algebra.IsSeparable (↥(toIsogeny h).fieldPullback.fieldRange) W.FunctionField ↔ ↑s ≠ 0

If f kills the invariant differential, a nonzero pencil r • f - s • id is separable exactly when s is nonzero in the field.