Separability of isogenies under base change

An isogeny of elliptic curves is separable if and only if any base change of it is separable. This file proves that compatibility without first comparing the degrees of the original and base-changed function-field extensions. Instead it uses the differential criterion: an isogeny is separable exactly when the pullback of the invariant differential is nonzero.

For a field homomorphism f : F →+* K, the semilinear map on Kähler differentials WeierstrassCurve.Affine.FunctionField.mapDifferential : Ω[F(W)/F] → Ω[K(W.map f)/K] sends the invariant differential to the invariant differential and reflects zero. The commuting square Isogeny.map_fieldPullback_map then shows that it intertwines pullback by an isogeny with pullback by its base change.

Main results

• TauCeti.Isogeny.mapDifferential_pullback_invariantDifferential: base change commutes with the pullback of the invariant differential.
• TauCeti.Isogeny.isSeparable_map_iff: an isogeny is separable if and only if its base change is.

No material is copied from an external formalisation.

theorem TauCeti.Isogeny.mapDifferential_pullback_invariantDifferential {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) : (WeierstrassCurve.Affine.FunctionField.mapDifferential W₁ f) (φ.pullbackDifferential W₂.invariantDifferential) = (φ.map f).pullbackDifferential (W₂.map f).invariantDifferential

Pulling back the invariant differential commutes with field base change. This is the differential counterpart of map_fieldPullback_map.

theorem TauCeti.Isogeny.isSeparable_map_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (f : F →+* K) : Algebra.IsSeparable (↥(φ.map f).fieldPullback.fieldRange) (W₁.map f).FunctionField ↔ Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField

Separability is invariant under arbitrary field base change. An isogeny is separable if and only if the isogeny obtained by carrying its coefficients along f : F →+* K is separable.

theorem TauCeti.Isogeny.isSeparable_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (f : F →+* K) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] : Algebra.IsSeparable (↥(φ.map f).fieldPullback.fieldRange) (W₁.map f).FunctionField

A separable isogeny stays separable after field base change.

theorem TauCeti.Isogeny.isSeparable_of_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (f : F →+* K) [Algebra.IsSeparable (↥(φ.map f).fieldPullback.fieldRange) (W₁.map f).FunctionField] : Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField

Separability descends from any field base change.