Kähler differentials of a Weierstrass function field under base change

For a field homomorphism f : F →+* K, the embedding FunctionField.map W f : F(W) → K(W.map f) and f form a commuting square, so Mathlib's functorial map on Kähler differentials gives a semilinear map

  Ω[F(W)/F] ──▸ Ω[K(W.map f)/K].

It sends the invariant differential of W to that of W.map f. Since the invariant differential is a basis, this map reflects zero.

Main definitions

• WeierstrassCurve.Affine.FunctionField.mapDifferential: the semilinear map on differentials induced by base change of a Weierstrass function field.

Main results

• WeierstrassCurve.Affine.FunctionField.mapDifferential_D: it sends d z to d of the image of z.
• WeierstrassCurve.Affine.FunctionField.mapDifferential_invariantDifferential: base change carries the invariant differential to the invariant differential.
• WeierstrassCurve.Affine.FunctionField.mapDifferential_eq_zero_iff: for an elliptic curve, base change of differentials reflects zero.

No material is copied from an external formalisation.

noncomputable def WeierstrassCurve.Affine.FunctionField.mapDifferential {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) : Ω[W.FunctionField⁄F] →ₛₗ[map W f] Ω[(W.map f).FunctionField⁄K]

The map on Kähler differentials induced by field base change. For f : F →+* K, this is the semilinear map Ω[F(W)/F] → Ω[K(W.map f)/K] induced by the commuting square formed by f and FunctionField.map W f.

Equations

• WeierstrassCurve.Affine.FunctionField.mapDifferential W f = { toFun := ⇑(KaehlerDifferential.map F K W.FunctionField (W.map f).FunctionField), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.mapDifferential_D {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) (z : W.FunctionField) : (mapDifferential W f) ((KaehlerDifferential.D F W.FunctionField) z) = (KaehlerDifferential.D K (W.map f).FunctionField) ((map W f) z)

Base change of differentials sends d z to the differential of the image of z.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.map_invariantDifferentialDenom {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) : (map W f) W.invariantDifferentialDenom = (W.map f).invariantDifferentialDenom

Base change carries the denominator 2y + a₁x + a₃ of the invariant differential to the corresponding denominator on the base-changed curve.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.mapDifferential_invariantDifferential {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) : (mapDifferential W f) W.invariantDifferential = (W.map f).invariantDifferential

Base change carries the invariant differential to the invariant differential.

theorem WeierstrassCurve.Affine.FunctionField.mapDifferential_eq_zero_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) [WeierstrassCurve.IsElliptic W] (f : F →+* K) (η : Ω[W.FunctionField⁄F]) : (mapDifferential W f) η = 0 ↔ η = 0

Base change of differentials reflects zero for an elliptic function field. The invariant differential is a basis on both curves, and the coefficient embedding FunctionField.map W f is injective.