The factorisation of an isogeny

The pointedness criterion in Isogeny/InfinityPlace.lean discharges the pointedness of a factor. If two isogenies φ : W₁ → W₂ and ψ : W₁ → W₃ satisfy ψ^*F(W₃) ⊆ φ^*F(W₂) as subfields of F(W₁), then inverting φ^* on its image gives an embedding σ : F(W₃) → F(W₂) with φ^* ∘ σ = ψ^*. Restricting the place at infinity of W₁ along φ^* and ψ^* gives the places at infinity of W₂ and W₃, so restricting along σ carries the one to the other; the criterion then makes σ an isogeny λ : W₂ → W₃, and λ ∘ φ = ψ. Uniqueness is TauCeti.Isogeny.comp_right_injective, and the degree formula deg ψ = deg λ · deg φ is the tower formula TauCeti.Isogeny.degree_comp.

The criterion is stated on subfields, not on kernels: over ℚ a curve with no rational 2-torsion has ker [2](ℚ) = ker (id)(ℚ) = {O} while id does not factor through [2], and relative Frobenius has trivial geometric point kernel while id does not factor through it. Both are correctly excluded here, the subfield containment failing in each case.

When #ker φ = deg φ, however, ker φ cuts out φ^*F(W₂): the kernel test ker φ ≤ ker ψ is then equivalent to the subfield criterion. In this development Isogeny.ker consists of base-field points, and the cardinality condition is equivalent to the relevant fixed-field equality (TauCeti.Isogeny.card_ker_eq_degree_iff). Over a separably closed field it is the condition a separable isogeny is expected to satisfy.

Main results

• TauCeti.Isogeny.existsUnique_comp_eq_iff_fieldRange_le: the factorisation theorem, that ψ factors through φ by a unique isogeny exactly when ψ^*F(W₃) ⊆ φ^*F(W₂).
• TauCeti.Isogeny.existsUnique_comp_eq_iff_ker_le: when #ker φ = deg φ, the same criterion can equivalently be stated as ker φ ≤ ker ψ.
• TauCeti.Isogeny.exists_comp_eq_id_and_comp_eq_id_of_degree_eq_one: a degree-one isogeny is an isomorphism, the first consequence of the factorisation theorem.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 1, "The factorisation theorem — made a milestone in its own right, because it is what the dual is built from": for isogenies φ : W₁ → W₂ and ψ : W₁ → W₃, ψ factors as ψ = λ ∘ φ for a unique isogeny λ iff ψ^*K(W₃) ⊆ φ^*K(W₂) as subfields of K(W₁), with deg ψ = deg φ · deg λ. The same layer's dual-isogeny bullet asks for the route taken here — "an unpointed induced-place map for finite function-field embeddings, with the named criterion MapsInfinity λ ↔ λ_*(O₂) = O₃ (equivalently its valuation/integral-closure form), and functoriality of induced places along λ ∘ φ = ψ".

Provenance

Not ported. Silverman's III.4.11 is stated for separable isogenies and proved by Galois theory of the function-field extension; the subfield criterion here subsumes it and needs no separability, and the pointedness of the factor — which the classical account does not have to address, its morphisms being maps of projective curves — is discharged by the place criterion above. The kernel form uses the translation-action correspondence of Affine/FunctionField/Translation/FixedField.lean for the same Galois theory.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.4, III.4.11.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 1.1.13.

theorem TauCeti.Isogeny.existsUnique_comp_eq_iff_fieldRange_le {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (ψ : Isogeny W₁ W₃) : (∃! χ : Isogeny W₂ W₃, χ.comp φ = ψ) ↔ ψ.fieldPullback.fieldRange ≤ φ.fieldPullback.fieldRange

The factorisation theorem (Silverman, The Arithmetic of Elliptic Curves, III.4.11 in its separable form): an isogeny ψ : W₁ → W₃ factors through an isogeny φ : W₁ → W₂, by a unique isogeny λ : W₂ → W₃, exactly when the function field ψ pulls back sits inside the one φ pulls back.

The criterion is on subfields of F(W₁), not on kernels of point maps, and that is what makes it correct in general: over ℚ, a curve with no rational 2-torsion has ker [2](ℚ) = {O} without the identity factoring through [2], and relative Frobenius has trivial geometric point kernel without the identity factoring through it. In both cases the subfield containment fails, as it should.

theorem TauCeti.Isogeny.existsUnique_comp_eq_iff_ker_le {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [DecidableEq F] [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} (hφ : Nat.card ↥φ.ker = φ.degree) (ψ : Isogeny W₁ W₃) : (∃! χ : Isogeny W₂ W₃, χ.comp φ = ψ) ↔ φ.ker ≤ ψ.ker

The kernel form of the factorisation theorem (Silverman III.4.11). When the kernel of φ : W₁ → W₂ has deg φ points, an isogeny ψ : W₁ → W₃ factors through φ, by a unique isogeny, exactly when ker φ ≤ ker ψ.

Without the hypothesis only the forward implication holds (TauCeti.Isogeny.ker_le_ker_comp). The subfield criterion TauCeti.Isogeny.existsUnique_comp_eq_iff_fieldRange_le needs no hypothesis.

theorem TauCeti.Isogeny.exists_comp_eq_id_and_comp_eq_id_of_degree_eq_one {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (hφ : φ.degree = 1) : ∃ (χ : Isogeny W₂ W₁), χ.comp φ = id W₁ ∧ φ.comp χ = id W₂

An isogeny of degree one is an isomorphism (Silverman, The Arithmetic of Elliptic Curves, II.2.4.1): it has an isogeny which is both a left and a right inverse.