The carrier of Hom(W₁, W₂)

An Isogeny is nonzero by construction: its pullback is injective, so there is no isogeny representing the zero morphism. The zero morphism has no pullback of functions at all — it sends every point to the target's point at infinity, which is not a point of the affine coordinate ring's spectrum — so it cannot be added to the isogenies as another pullback.

This file carves the hom carrier out of a slightly larger mapping type instead, adjoining nothing: the F-linear multiplicative maps R(W₂) → K(W₁), which include the zero map because multiplicativity does not force 1 ↦ 1. Into a field there is nothing else new — p 1 is idempotent, so MulHomClass.forall_apply_eq_zero_or_map_one splits the type as the zero map together with the unital maps, and a unital map with the pointedness condition is exactly an Isogeny. So the carrier is {0} ⊔ Isogeny W₁ W₂ as a set, obtained by weakening unitality rather than by a WithZero adjunction.

The zero element is a formal tag: the pullback identity a nonzero morphism satisfies is vacuous at zero, every point landing at infinity. Composition is therefore defined by cases, with the zero map absorbing, rather than derived from a pullback identity that does not hold there.

Addition is not defined here, so Hom W W is a monoid with zero rather than a ring. A sum of multiplicative maps is not multiplicative, so the carrier is not an additive subgroup of the linear maps; an additive structure on it has to be built from the elliptic-curve group law, which needs the rational addition formulas rather than anything in this file.

Main definitions

• NonUnitalAlgHom.MapsInfinityOfMapOne: the condition carving the carrier out — a map that is unital is pointed. It is vacuous at the zero map, which is how that map enters.
• TauCeti.Isogeny.Hom: the carrier of Hom(W₁, W₂), with 0 its zero map and TauCeti.Isogeny.Hom.ofIsogeny its nonzero elements.
• TauCeti.Isogeny.Hom.degree: the degree, extended by the stipulation degree 0 = 0.
• TauCeti.Isogeny.Hom.comp and TauCeti.Isogeny.Hom.id: composition and the identity, making Hom W W a MonoidWithZero.

Main results

• TauCeti.Isogeny.Hom.eq_zero_or_exists_ofIsogeny: every element is the zero map or comes from an isogeny.
• TauCeti.Isogeny.Hom.degree_eq_zero_iff: the degree vanishes exactly at the zero map.
• TauCeti.Isogeny.Hom.degree_comp: deg (g ∘ f) = deg g · deg f on the whole carrier, the zero map included — which is what the value degree 0 = 0 is chosen for.
• TauCeti.Isogeny.Hom.comp_eq_zero_iff: a composite vanishes exactly when a factor does, so the endomorphism monoid has no zero divisors.
• TauCeti.Isogeny.Hom.instNontrivialEnd: the endomorphism carrier has more than one element, which is what lets Mathlib's theory of nontrivial monoids with zero apply to it.

Implementation notes

degree 0 = 0 is a stipulation, not a theorem: the zero map's image generates no field, so there is no extension whose dimension could be measured. 0 is the value that makes degree vanish exactly at the zero map, which is what degree_eq_zero_iff records.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2 and III.6.

def NonUnitalAlgHom.MapsInfinityOfMapOne {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (p : W₂.CoordinateRing →ₙₐ[F] W₁.FunctionField) : Prop

The condition carving the hom carrier out of the non-unital pullbacks: if the map is unital, it is pointed. At the zero map the hypothesis is unsatisfiable, so the condition is vacuous there — which is what lets the zero map into the carrier without a pointedness claim about it.

Equations

• p.MapsInfinityOfMapOne = ∀ (h : p 1 = 1), TauCeti.CoordinatePullback.MapsInfinity (AlgHom.ofLinearMap { toFun := ⇑p, map_add' := ⋯, map_smul' := ⋯ } h ⋯)

@[simp]

theorem NonUnitalAlgHom.mapsInfinityOfMapOne_iff {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} {p : W₂.CoordinateRing →ₙₐ[F] W₁.FunctionField} : p.MapsInfinityOfMapOne ↔ ∀ (h : p 1 = 1), TauCeti.CoordinatePullback.MapsInfinity (AlgHom.ofLinearMap { toFun := ⇑p, map_add' := ⋯, map_smul' := ⋯ } h ⋯)

The condition unfolded, so a consumer can introduce and eliminate it without the definition's body: MapsInfinityOfMapOne p is exactly the implication it is defined to be.

structure TauCeti.Isogeny.Hom {F : Type u_1} [Field F] (W₁ W₂ : WeierstrassCurve.Affine F) : Type u_1

The carrier of Hom(W₁, W₂): an F-linear multiplicative map out of the target coordinate ring, pointed wherever it is unital. Its zero map is the zero morphism's formal representative and its unital elements are the isogenies.

• toNonUnitalAlgHom : W₂.CoordinateRing →ₙₐ[F] W₁.FunctionField

  The underlying multiplicative map. Not an AlgHom: unitality is what the zero map fails.

• mapsInfinity_of_map_one : self.toNonUnitalAlgHom.MapsInfinityOfMapOne

  Pointedness, required only of the unital maps.

theorem TauCeti.Isogeny.Hom.ext {F : Type u_1} {inst✝ : Field F} {W₁ W₂ : WeierstrassCurve.Affine F} {x y : Hom W₁ W₂} (toNonUnitalAlgHom : x.toNonUnitalAlgHom = y.toNonUnitalAlgHom) : x = y

theorem TauCeti.Isogeny.Hom.ext_iff {F : Type u_1} {inst✝ : Field F} {W₁ W₂ : WeierstrassCurve.Affine F} {x y : Hom W₁ W₂} : x = y ↔ x.toNonUnitalAlgHom = y.toNonUnitalAlgHom

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.Hom.instZero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} : Zero (Hom W₁ W₂)

Equations

• TauCeti.Isogeny.Hom.instZero = { zero := { toNonUnitalAlgHom := 0, mapsInfinity_of_map_one := ⋯ } }

@[simp]

theorem TauCeti.Isogeny.Hom.toNonUnitalAlgHom_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} : toNonUnitalAlgHom 0 = 0

noncomputable def TauCeti.Isogeny.Hom.ofIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Hom W₁ W₂

An isogeny, as an element of the carrier.

Equations

• TauCeti.Isogeny.Hom.ofIsogeny φ = { toNonUnitalAlgHom := NonUnitalAlgHomClass.toNonUnitalAlgHom φ.pullback, mapsInfinity_of_map_one := ⋯ }

@[simp]

theorem TauCeti.Isogeny.Hom.ofIsogeny_apply {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (x : W₂.CoordinateRing) : (ofIsogeny φ).toNonUnitalAlgHom x = φ.pullback x

theorem TauCeti.Isogeny.Hom.toNonUnitalAlgHom_ofIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : (ofIsogeny φ).toNonUnitalAlgHom = NonUnitalAlgHomClass.toNonUnitalAlgHom φ.pullback

The underlying map of an embedded isogeny is its pullback.

theorem TauCeti.Isogeny.Hom.ofIsogeny_injective {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} : Function.Injective ofIsogeny

The isogenies sit in the carrier as distinct elements.

@[simp]

theorem TauCeti.Isogeny.Hom.ofIsogeny_ne_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : ofIsogeny φ ≠ 0

No isogeny is the zero map, since a pullback sends 1 to 1.

noncomputable def TauCeti.Isogeny.Hom.toIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} {h : Hom W₁ W₂} (hz : h ≠ 0) : Isogeny W₁ W₂

The isogeny a nonzero element of the carrier comes from: it is unital, so its underlying map promotes to a pullback, and pointedness is the carrier's own condition.

Equations

• TauCeti.Isogeny.Hom.toIsogeny hz = { pullback := AlgHom.ofLinearMap { toFun := ⇑h.toNonUnitalAlgHom, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.Hom.toIsogeny_pullback_apply {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} {h : Hom W₁ W₂} (hz : h ≠ 0) (x : W₂.CoordinateRing) : (toIsogeny hz).pullback x = h.toNonUnitalAlgHom x

The pullback of the isogeny read off a nonzero element is that element's own map.

@[simp]

theorem TauCeti.Isogeny.Hom.ofIsogeny_toIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} {h : Hom W₁ W₂} (hz : h ≠ 0) : ofIsogeny (toIsogeny hz) = h

toIsogeny is a section of ofIsogeny: a nonzero element read as an isogeny and put back is unchanged.

@[simp]

theorem TauCeti.Isogeny.Hom.toIsogeny_ofIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : toIsogeny ⋯ = φ

toIsogeny is a retraction of ofIsogeny: an embedded isogeny read back is unchanged.

theorem TauCeti.Isogeny.Hom.eq_zero_or_exists_ofIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) : h = 0 ∨ ∃ (φ : Isogeny W₁ W₂), h = ofIsogeny φ

Every element of the carrier is the zero map or an isogeny. This is the dichotomy the carrier is built for: weakening unitality admits the zero map and nothing else.

noncomputable def TauCeti.Isogeny.Hom.degree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) : ℕ

The degree, extended to the carrier by stipulating degree 0 = 0: the zero map's image generates no field, so there is no extension for a dimension to measure.

Equations

• h.degree = if hz : h = 0 then 0 else (TauCeti.Isogeny.Hom.toIsogeny hz).degree

@[simp]

theorem TauCeti.Isogeny.Hom.degree_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} : degree 0 = 0

@[simp]

theorem TauCeti.Isogeny.Hom.degree_ofIsogeny {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : (ofIsogeny φ).degree = φ.degree

@[simp]

theorem TauCeti.Isogeny.Hom.degree_eq_zero_iff {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (h : Hom W₁ W₂) : h.degree = 0 ↔ h = 0

The degree vanishes exactly at the zero map: every isogeny has positive degree, so the stipulated value at zero is the only one.

noncomputable def TauCeti.Isogeny.Hom.comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (g : Hom W₂ W₃) (f : Hom W₁ W₂) : Hom W₁ W₃

Composition on the carrier. At a zero argument the composite is the zero map: the zero morphism composed either way is the zero morphism, and it has no pullback of functions to compose with the other side's, so the value there is stipulated rather than derived.

Equations

• g.comp f = if hg : g = 0 then 0 else if hf : f = 0 then 0 else TauCeti.Isogeny.Hom.ofIsogeny ((TauCeti.Isogeny.Hom.toIsogeny hg).comp (TauCeti.Isogeny.Hom.toIsogeny hf))

@[simp]

theorem TauCeti.Isogeny.Hom.zero_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (f : Hom W₁ W₂) : comp 0 f = 0

The zero map absorbs on the left.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_zero {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (g : Hom W₂ W₃) : g.comp 0 = 0

The zero map absorbs on the right.

@[simp]

theorem TauCeti.Isogeny.Hom.ofIsogeny_comp_ofIsogeny {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : (ofIsogeny ψ).comp (ofIsogeny φ) = ofIsogeny (ψ.comp φ)

The embedding carries Isogeny.comp to carrier composition.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_eq_zero_iff {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} {g : Hom W₂ W₃} {f : Hom W₁ W₂} : g.comp f = 0 ↔ g = 0 ∨ f = 0

A composite vanishes exactly when one of its factors does.

@[simp]

theorem TauCeti.Isogeny.Hom.degree_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (g : Hom W₂ W₃) (f : Hom W₁ W₂) : (g.comp f).degree = g.degree * f.degree

deg (g ∘ f) = deg g · deg f, on the whole carrier. The tower formula holds at the zero map too, and that is what the stipulation degree 0 = 0 buys: both sides are 0 there.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_assoc {F : Type u_1} [Field F] {W₁ W₂ W₃ W₄ : WeierstrassCurve.Affine F} (h : Hom W₃ W₄) (g : Hom W₂ W₃) (f : Hom W₁ W₂) : (h.comp g).comp f = h.comp (g.comp f)

Carrier composition is associative, the zero map included.

noncomputable def TauCeti.Isogeny.Hom.id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : Hom W W

The identity, as an element of the carrier.

Equations

• TauCeti.Isogeny.Hom.id W = TauCeti.Isogeny.Hom.ofIsogeny (TauCeti.Isogeny.id W)

theorem TauCeti.Isogeny.Hom.id_def {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : id W = ofIsogeny (Isogeny.id W)

The defining equation of id.

@[simp]

theorem TauCeti.Isogeny.Hom.id_comp {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (f : Hom W₁ W₂) : (id W₂).comp f = f

The identity is a left unit for composition.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_id {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (f : Hom W₁ W₂) : f.comp (id W₁) = f

The identity is a right unit for composition.

@[simp]

theorem TauCeti.Isogeny.Hom.degree_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (id W).degree = 1

The identity has degree one, its pullback being onto.

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.Hom.instMonoidWithZero {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} : MonoidWithZero (Hom W₁ W₁)

The endomorphisms of W form a monoid with zero under composition: the identity is its unit and the zero map is absorbing. The additive structure that would make it a ring is not built here.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.Isogeny.Hom.instNoZeroDivisors {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} : NoZeroDivisors (Hom W₁ W₁)

The endomorphism monoid has no zero divisors: a composite of nonzero endomorphisms is nonzero, since a composite of isogenies is an isogeny.

@[simp]

theorem TauCeti.Isogeny.Hom.mul_def {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} (g f : Hom W₁ W₁) : g * f = g.comp f

The monoid's multiplication is composition.

@[simp]

theorem TauCeti.Isogeny.Hom.one_def {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} : 1 = id W₁

The monoid's unit is the identity endomorphism.

instance TauCeti.Isogeny.Hom.instNontrivialEnd {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} : Nontrivial (Hom W₁ W₁)

The carrier has more than one element: the zero map has degree 0 and the identity degree 1. Supplying this makes Mathlib's generic theory of nontrivial monoids with zero apply, not_isUnit_zero among it.