Auxiliary data witnessing Lemma 24.4 at the level of a generic homomorphism $\varphi_{\mathrm{hom}} \colon E_1 \to E_2$: a function field and a smaller "pullback" field related by translation pullback maps, with separation and compatibility axioms.
- FunctionField : Type
- PullbackField : Type
- field_top : Field self.FunctionField
- field_bot : Field self.PullbackField
- algebra_inst : Algebra self.PullbackField self.FunctionField
- translationPullback : W₁.toAffine.Point → RingAut self.FunctionField
- eval : self.FunctionField → W₁.toAffine.Point → self.FunctionField
- eval_translationPullback (P : W₁.toAffine.Point) (f : self.FunctionField) (Q : W₁.toAffine.Point) : self.eval ((self.translationPullback P) f) Q = self.eval f (Q + P)
- eval_algebraMap_eq_of_image_eq (x : self.PullbackField) (Q R : W₁.toAffine.Point) : φ_hom Q = φ_hom R → self.eval ((algebraMap self.PullbackField self.FunctionField) x) Q = self.eval ((algebraMap self.PullbackField self.FunctionField) x) R
Instances For
If $P \in \ker \varphi_{\mathrm{hom}}$ then $\varphi_{\mathrm{hom}}$ is invariant under translation by $P$: $\varphi_{\mathrm{hom}}(R + P) = \varphi_{\mathrm{hom}}(R)$ for all $R$.
Compatibility of translationPullback with the algebra-map image of the pullback field:
elements coming from PullbackField are fixed by translationPullback P whenever
$P \in \ker \varphi_{\mathrm{hom}}$.
Translation-pullback is a homomorphism into the group of ring automorphisms: $\mathrm{translationPullback}(P + Q) = \mathrm{translationPullback}(P) \cdot \mathrm{translationPullback}(Q)$.
Faithfulness on points: if $P \ne 0$, then translation pullback by $P$ is a nontrivial ring automorphism.
Translation pullback by the zero element is the identity automorphism.
Translation pullback by $-P$ is the inverse of translation pullback by $P$.
Translation pullback by $P - Q$ equals $\mathrm{translationPullback}(P) \cdot \mathrm{translationPullback}(Q)^{-1}$.
Restated: for $P \in \ker\varphi_{\mathrm{hom}}$, translation pullback by $P$ fixes every
element in the image of the algebra map from PullbackField.
Translation pullback restricted to $\ker\varphi_{\mathrm{hom}}$, viewed as an additive
homomorphism into Additive (RingAut FunctionField).
Instances For
Translation pullback is injective: distinct points produce distinct ring automorphisms.
The translation-pullback homomorphism restricted to the kernel is injective.
Core of Lemma 24.4: $\ker\varphi$ embeds into $\mathrm{Aut}(\mathrm{FunctionField})$
via translation pullback, fixing the subfield PullbackField.
For an elliptic curve isogeny $\varphi \colon W_1 \to W_2$, a TranslationPullbackData
packages the function field extension data with the translation-pullback action on the function
field, together with separation and compatibility axioms.
- field_top : Field self.FunctionField
- field_bot : Field self.PullbackField
- algebra_inst : Algebra self.PullbackField self.FunctionField
- translationPullback : W₁.toAffine.Point → RingAut self.FunctionField
- eval : self.FunctionField → W₁.toAffine.Point → self.FunctionField
- eval_translationPullback (P : W₁.toAffine.Point) (f : self.FunctionField) (Q : W₁.toAffine.Point) : self.eval ((self.translationPullback P) f) Q = self.eval f (Q + P)
- eval_algebraMap_eq_of_image_eq (x : self.PullbackField) (Q R : W₁.toAffine.Point) : φ Q = φ R → self.eval ((algebraMap self.PullbackField self.FunctionField) x) Q = self.eval ((algebraMap self.PullbackField self.FunctionField) x) R
Instances For
Forget the isogeny-specific structure and view a TranslationPullbackData as the more
generic KernelAutData for the underlying homomorphism.
Instances For
Lemma 24.4: For an isogeny $\varphi$ of elliptic curves, $\ker\varphi$ embeds as a subgroup of automorphisms of the function field of $W_1$ fixing the pulled-back subfield.