Fibres of the class-group point map

Over a separably closed field, every fibre of a separable isogeny's point map has exactly the degree of the isogeny many points. In particular, the point map is surjective, and its kernel is finite with cardinality equal to the degree.

The map here is Isogeny.toPointHom, defined by extension and norm on ideal classes. The point--place dictionary intertwines it with restriction of places. Complete splitting then identifies its fibres with the finite fibres of restriction, including over infinity. Separably closed constants suffice: the residue extensions are separable because the isogeny is unramified, so every place above a rational place is again rational.

Main results

• TauCeti.Isogeny.ncard_fiber_toPointHom_eq_degree: every point fibre has size deg φ.
• TauCeti.Isogeny.finite_setOf_toPointHom_eq: every point fibre is finite.
• TauCeti.Isogeny.toPointHom_surjective: a separable isogeny is surjective on points over a separably closed field.
• TauCeti.Isogeny.card_ker_toPointHom_eq_degree: the point kernel has cardinality deg φ.
• TauCeti.Isogeny.finite_ker_toPointHom: the point kernel is finite.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.10.

theorem TauCeti.Isogeny.instIsIntegrallyClosedCoordinateRing_4 {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] : IsIntegrallyClosed W₁.CoordinateRing

theorem TauCeti.Isogeny.instIsIntegrallyClosedCoordinateRing_5 {F : Type u_1} [Field F] {W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] : IsIntegrallyClosed W₂.CoordinateRing

theorem TauCeti.Isogeny.instIsDedekindDomainCoordinateRing_4 {F : Type u_1} [Field F] {W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] : IsDedekindDomain W₂.CoordinateRing

@[simp]

theorem TauCeti.Isogeny.ncard_fiber_toPointHom_eq_degree {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] (Q : W₂.Point) : {P : W₁.Point | φ.toPointHom P = Q}.ncard = φ.degree

Every fibre of a separable isogeny's class-group point map has cardinality equal to its degree over a separably closed field.

theorem TauCeti.Isogeny.finite_setOf_toPointHom_eq {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] (Q : W₂.Point) : {P : W₁.Point | φ.toPointHom P = Q}.Finite

Every fibre of a separable isogeny's point map is finite over a separably closed field.

theorem TauCeti.Isogeny.toPointHom_surjective {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] : Function.Surjective ⇑φ.toPointHom

A separable isogeny is surjective on points over a separably closed field.

@[simp]

theorem TauCeti.Isogeny.card_ker_toPointHom_eq_degree {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] : Nat.card ↥φ.toPointHom.ker = φ.degree

The kernel of a separable isogeny's class-group point map has cardinality equal to the degree over a separably closed field.

instance TauCeti.Isogeny.finite_ker_toPointHom {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] : Finite ↥φ.toPointHom.ker

The point kernel of a separable isogeny over a separably closed field is finite.