The kernel of an isogeny #
An isogeny is a map of function fields, so it has no point map to take a fibre of. Its kernel is
read off the translation action instead: a point P of W₁ lies in the kernel exactly when
translating by P moves no function pulled back from W₂. On the points where the two notions
can be compared this is the usual kernel, since φ(X + P) = φ(X) + φ(P), and it is stated here
for every isogeny over every field, with no separability or rationality hypothesis.
The degree bounds the kernel: a pulled-back field of degree d is fixed by at most d
translations. The bound is often strict, because these are the F-rational points only: a
separable isogeny whose geometric kernel is not rational has fewer of them than its degree.
Equality needs separability and rationality of the whole geometric kernel. For 1 − π_q over a
finite field both hold, its geometric kernel being the 𝔽_q-rational points, and the point count
deg (1 − π_q) = #E(𝔽_q) is what they then yield; neither that identity nor the general equality
is proved here.
Main definitions #
TauCeti.Isogeny.ker: the subgroup of points whose translation fixes the pulled-back field.
Main results #
TauCeti.Isogeny.mem_ker_iff_comp_pullback_eqandTauCeti.Isogeny.mem_ker_iff_map_tautologicalPoint_eq: membership is fixing the coordinate pullback, equivalently its tautological point.TauCeti.Isogeny.card_ker_le_degree: the kernel has at mostdeg φelements.TauCeti.Isogeny.ker_le_ker_comp: postcomposition can only enlarge the kernel.TauCeti.Isogeny.ker_eq_bot_of_separableDegree_eq_one: separable degree one forces this kernel to be trivial, as for Frobenius.TauCeti.Isogeny.card_ker_eq_degree_iff: the cardinality statement is equivalent to the reverse fixed-field inclusion.TauCeti.Isogeny.card_ker_eq_degree_of_forall_exists_translationandcard_ker_eq_degree_iff_isGalois_and_forall_exists_translation: it holds exactly when the function field is Galois over the pulled-back field and every automorphism over that field is a translation, so those two conditions are what remains of the identity.TauCeti.Isogeny.card_ker_dvd_separableDegreeandcard_ker_le_separableDegree: the kernel order divides, so is bounded by, the separable degree.
Provenance #
The AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit
513e83879e2f8cbc626eb9e04d660e92be16ccba) proves the corresponding cardinality statement in
EC/SeparableKernelTorsor.lean as card_kernel_eq_degree_of_separable_isogeny, parametric on two
witnesses. The second exists only because its isogeny carries a point map independent of the
function-field pullback, so separability and the kernel are a priori unrelated there. The kernel
here is defined from the pullback, so that witness has no counterpart.
References #
The kernel of an isogeny: the points whose translation fixes every pulled-back function.
Equations
Instances For
The defining equation of ker.
A point is in the kernel exactly when it translates every pulled-back function to itself.
Membership in the kernel is fixing the coordinate pullback: P ∈ ker φ exactly when
τ_P^* ∘ φ^* = φ^* on the coordinate ring of W₂. The function-field pullback is determined by
the coordinate pullback, so fixing the latter fixes every pulled-back function.
Membership in the kernel is fixing the tautological point. A translation fixes every pulled-back function exactly when it fixes the coordinate pullback, and a coordinate pullback is determined by its tautological point, so the kernel is read off that point alone.
The kernel is finite, the pulled-back field being of finite index.
Postcomposition can only enlarge the kernel: a function pulled back from W₃ arrives
through W₂, so a translation fixing everything from W₂ fixes it too.
The kernel order divides the separable degree, the kernel being the subgroup of translations fixing the pulled-back field and that field having finite degree.
The separable degree bounds the kernel, sharpening the bound by the degree.
The degree bounds the kernel, the separable degree being at most the degree. The bound is often strict, this being the rational kernel: equality needs the isogeny to be separable and its geometric kernel to be rational.
An isogeny of separable degree one has a trivial kernel here, the bound leaving no room. This is the right hypothesis: a purely inseparable isogeny such as Frobenius has separable degree one, so its kernel in this point-valued sense is trivial whatever its degree — its scheme-theoretic kernel, which this file does not model, is not.
The kernel counts the degree exactly when it cuts out the pulled-back field. This is a reduction, not the separable-locus theorem: one inclusion holds for free, so the cardinality statement and the reverse inclusion are two names for the same thing.
That inclusion is where separability enters, and over a base field that is not separably closed it can fail: the kernel here consists of the rational points, while the extension is cut out by the geometric ones. Deriving it from separability and rationality of the geometric kernel is not done here.
The kernel counts the degree as soon as K(W₁) is Galois over the pulled-back field and
every automorphism over that field is a translation. This is the shape the point count needs:
given the Galois hypothesis, what is left of deg φ = #ker φ is a statement about automorphisms,
not about fields — are there automorphisms of K(W₁) over φ^*K(W₂) beyond the translations by
kernel points?
The kernel counts the degree exactly when K(W₁) is Galois over the pulled-back field and
every automorphism over it is a translation. So the two hypotheses of
card_ker_eq_degree_of_forall_exists_translation are jointly necessary as well as sufficient: this
is what is left of deg φ = #ker φ.
The identity isogeny has trivial kernel.