Faithful additive base change of morphisms of elliptic curves

Base change of isogenies extends to Isogeny.Hom, sending the zero morphism to zero. It preserves identity and composition and is injective along every homomorphism of fields. For an elliptic target it also preserves addition: the tautological point of a transported morphism is the transported tautological point, and field embeddings preserve the point-group law. Thus identities between sums and composites can be checked after extending the ground field, for example to a separable closure. Base change also commutes with the action on points, the place of a transported point restricting to the place of the point; so statements about the action on points, too, can be checked after extending the ground field.

The construction reuses Isogeny.map, Mathlib's additive map on points Affine.Point.map, and the identification of morphisms with their tautological points in Isogeny.Hom.Add.

Main definitions and results

• TauCeti.Isogeny.Hom.map: transport along a homomorphism of fields.
• TauCeti.Isogeny.Hom.map_injective: transport reflects equality.
• TauCeti.Isogeny.Hom.tautologicalPoint_map: compatibility with tautological points.
• TauCeti.Isogeny.Hom.mapAddHom: additive base change.
• TauCeti.Isogeny.Hom.comp_map and TauCeti.Isogeny.Hom.map_add: preservation of composition and addition.
• TauCeti.Isogeny.Hom.pointMap_map: compatibility with the action on points.

References

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

noncomputable def TauCeti.Isogeny.Hom.map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) (f : F →+* K) : Hom (W₁.map f) (W₂.map f)

Transport a morphism along a homomorphism of its ground field, with zero sent to zero.

Equations

• h.map f = if hh : h = 0 then 0 else TauCeti.Isogeny.Hom.ofIsogeny ((TauCeti.Isogeny.Hom.toIsogeny hh).map f)

@[simp]

theorem TauCeti.Isogeny.Hom.zero_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (f : F →+* K) : map 0 f = 0

Base change sends the zero morphism to zero.

@[simp]

theorem TauCeti.Isogeny.Hom.ofIsogeny_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) : (ofIsogeny φ).map f = ofIsogeny (φ.map f)

Base change on nonzero morphisms is the existing base change of isogenies.

@[simp]

theorem TauCeti.Isogeny.Hom.map_coordinateRingMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) (f : F →+* K) (z : W₂.CoordinateRing) : (h.map f).toNonUnitalAlgHom ((WeierstrassCurve.Affine.CoordinateRing.map W₂ f) z) = (WeierstrassCurve.Affine.FunctionField.map W₁ f) (h.toNonUnitalAlgHom z)

The coordinate-ring square for the underlying multiplicative maps commutes, including at the zero morphism.

theorem TauCeti.Isogeny.Hom.map_injective {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (f : F →+* K) : Function.Injective fun (h : Hom W₁ W₂) => h.map f

Extending the ground field reflects equality of morphisms.

@[simp]

theorem TauCeti.Isogeny.Hom.map_inj {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (f : F →+* K) {h h' : Hom W₁ W₂} : h.map f = h'.map f ↔ h = h'

@[simp]

theorem TauCeti.Isogeny.Hom.map_eq_zero_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) (f : F →+* K) : h.map f = 0 ↔ h = 0

@[simp]

theorem TauCeti.Isogeny.Hom.comp_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (g : Hom W₂ W₃) (h : Hom W₁ W₂) (f : F →+* K) : (g.comp h).map f = (g.map f).comp (h.map f)

Base change preserves composition, including composites with zero.

@[simp]

theorem TauCeti.Isogeny.Hom.id_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) : (id W).map f = id (W.map f)

Base change preserves identity morphisms.

@[simp]

theorem TauCeti.Isogeny.Hom.map_id {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) : h.map (RingHom.id F) = h

Transport along the identity homomorphism fixes every morphism.

@[simp]

theorem TauCeti.Isogeny.Hom.map_map {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) (f : F →+* K) (g : K →+* L) : (h.map f).map g = h.map (g.comp f)

Transport is functorial in the ground-field homomorphism.

@[simp]

theorem TauCeti.Isogeny.Hom.tautologicalPoint_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (h : Hom W₁ W₂) (f : F →+* K) : (h.map f).tautologicalPoint = (AddEquiv.cast ⋯) (WeierstrassCurve.Affine.Point.mapAlong (WeierstrassCurve.Affine.FunctionField.map W₁ f) ⋯ h.tautologicalPoint)

The tautological point of a transported morphism is its transported tautological point. The cast identifies the two coefficient maps using the function-field commuting square.

@[simp]

theorem TauCeti.Isogeny.Hom.map_add {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (h h' : Hom W₁ W₂) (f : F →+* K) : (h + h').map f = h.map f + h'.map f

Base change preserves the group-law sum of morphisms.

noncomputable def TauCeti.Isogeny.Hom.mapAddHom {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f : F →+* K) : Hom W₁ W₂ →+ Hom (W₁.map f) (W₂.map f)

Additive base change of morphisms along a homomorphism of ground fields.

Equations

• TauCeti.Isogeny.Hom.mapAddHom f = { toFun := fun (h : TauCeti.Isogeny.Hom W₁ W₂) => h.map f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.Isogeny.Hom.mapAddHom_apply {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f : F →+* K) (h : Hom W₁ W₂) : (mapAddHom f) h = h.map f

@[simp]

theorem TauCeti.Isogeny.Hom.map_neg {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (h : Hom W₁ W₂) (f : F →+* K) : (-h).map f = -h.map f

Base change preserves negatives of morphisms.

@[simp]

theorem TauCeti.Isogeny.Hom.map_sub {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (h h' : Hom W₁ W₂) (f : F →+* K) : (h - h').map f = h.map f - h'.map f

Base change preserves differences of morphisms.

@[simp]

theorem TauCeti.Isogeny.Hom.map_zsmul {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (n : ℤ) (h : Hom W₁ W₂) (f : F →+* K) : (n • h).map f = n • h.map f

Base change commutes with integer multiples of morphisms.

@[simp]

theorem TauCeti.Isogeny.Hom.map_nsmul {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (n : ℕ) (h : Hom W₁ W₂) (f : F →+* K) : (n • h).map f = n • h.map f

Base change commutes with natural multiples of morphisms.

@[simp]

theorem TauCeti.Isogeny.Hom.pointMap_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} [DecidableEq F] [DecidableEq K] [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (h : Hom W₁ W₂) (f : F →+* K) (P : W₁.Point) : (h.map f).pointMap (WeierstrassCurve.Affine.Point.mapAlong f ⋯ P) = WeierstrassCurve.Affine.Point.mapAlong f ⋯ (h.pointMap P)

Base change commutes with the action on points: the transported morphism sends the transported point P to the transport of the image of P.