The kernel of a separable isogeny is the kernel of its point map #
An isogeny φ : W₁ → W₂ has two kernels. Isogeny.ker is read off the function field: the points
P whose translation τ_P^* fixes every function pulled back from W₂. The class-group point map
Isogeny.toPointHom has an ordinary kernel, the points sent to O₂. For a separable isogeny over
a separably closed field the two agree (Silverman III.4.10).
One inclusion is formal. If τ_P^* fixes the pulled-back field then restricting places along the
pullback cannot distinguish the place of P from the place of O₁, and by the point--place
dictionary that is φ(P) = O₂. The other inclusion is where separability and the closed base
field enter, through the compatibility τ_P^* ∘ φ^* = φ^* ∘ τ_{φ(P)}^* of translations with the
pullback. For every point Q off the fibres of O₂ under Q ↦ φ(Q) and Q ↦ φ(Q + P), the
functions τ_P^* φ^* x and φ^* τ_{φ(P)}^* x both take at Q the value of x at
φ(Q + P) = φ(Q) + φ(P); there are infinitely many such Q, and a nonzero function has only
finitely many zeros, so the two agree, likewise for y, and hence on the whole function field.
When φ(P) = O₂ the right-hand side is φ^*, so τ_P^* fixes the pulled-back field.
Since the point kernel has deg φ elements, so does Isogeny.ker, and the reduction of the
kernel count to Galois theory in Isogeny/Kernel.lean then closes: F(W₁) is Galois over the
pulled-back field, whose automorphisms are exactly the translations by kernel points, and which is
the fixed field of those translations.
Main results #
TauCeti.Isogeny.translation_fieldPullback:τ_P^* ∘ φ^* = φ^* ∘ τ_{φ(P)}^*for a separable isogeny over a separably closed field.TauCeti.Isogeny.mem_ker_iff_toPointHom_eq_zero: a point lies inIsogeny.kerexactly when the point map sends it toO₂.TauCeti.Isogeny.ker_eq_map_ker_toPointHom:Isogeny.keris the kernel oftoPointHom.TauCeti.Isogeny.card_ker_eq_degree:#ker φ = deg φfor a separable isogeny over a separably closed field.TauCeti.Isogeny.isGalois_fieldRange,TauCeti.Isogeny.exists_mem_ker_translation_eq_of_mem_fixingSubgroupandTauCeti.Isogeny.translationFixedField_ker:F(W₁)is Galois overφ^* F(W₂)with group the translations byker φ, andφ^* F(W₂)is the fixed field of those translations.
References #
Translation commutes with a separable isogeny: τ_P^* ∘ φ^* = φ^* ∘ τ_{φ(P)}^* on the
function field of W₂, over a separably closed field. This is the function-field form of
φ(Q + P) = φ(Q) + φ(P).
A point lies in the kernel of a separable isogeny exactly when its point map kills it, over
a separably closed field: τ_P^* fixes the pulled-back function field if and only if
φ(P) = O₂ (Silverman III.4.10).
The kernel of a separable isogeny is the kernel of its point map, over a separably closed
field, carried along the identification of the points of W₁ with those of its trivial base
change.
The kernel of a separable isogeny has deg φ points over a separably closed field
(Silverman III.4.10(c)).
The function field of W₁ is Galois over the field pulled back along a separable isogeny,
over a separably closed field (Silverman III.4.10(b)).
Every automorphism of F(W₁) over the pulled-back field is the translation by a kernel
point, over a separably closed field (Silverman III.4.10(b)).
The pulled-back field is the fixed field of the translations by the kernel, over a separably closed field (Silverman III.4.10(b)).