Frobenius endomorphism, endomorphism pencils, kernel degrees

Definition: EllipticCurve_FrobeniusEndo (460a2eaf-43a0-5271-b6de-7d072eb2b020), by Claude, 2026-09-05.

For an additive commutative group $A$ and an additive endomorphism $\psi$ of $A$, FrobeniusEndo.linePencil ψ m n is, for integers $m,n$, the additive endomorphism $P \mapsto m\cdot P - n\cdot\psi(P)$ of $A$ (written as the difference $m\bullet\mathrm{id}_A - n\bullet\psi$ in the group of additive endomorphisms); linePencil_apply records its value on a point, and mem_ker_linePencil_iff says that $P$ lies in its kernel exactly when $m\cdot P = n\cdot\psi(P)$. The accompanying numerical invariant FrobeniusEndo.kerDeg ψ m n is defined as Nat.card of the kernel of this pencil, i.e. the number of elements of $\ker(m - n\psi)$, with the usual convention that it is $0$ when that kernel is infinite; kerDeg_def restates the definition.

The second group of definitions applies this to a Weierstrass curve. The standing context is a tower $R \to S \to k$ of commutative rings with $k$ a field, a Weierstrass curve $W$ over $R$, and an $S$-algebra automorphism $\sigma$ of $k$. Here $\sigma$ acts on the group of affine points (W⁄k).Point by applying $\sigma$ to coordinates, and FrobeniusEndo.frobEnd W σ is this action viewed as an additive endomorphism $P \mapsto \sigma\cdot P$ of (W⁄k).Point, with frobEnd_apply recording that value. For a natural number $p$, FrobeniusEndo.frobPencilEnd W σ p m n is the $\mathbb{Z}/p$-linear endomorphism $\bar m\cdot 1 - \bar n\cdot\rho(\sigma)$ of the $p$-torsion submodule $\{P : p\cdot P = 0\}$ of (W⁄k).Point, where $\rho(\sigma)$ is the endomorphism induced by $\sigma$ (the value at $\sigma$ of galoisRepModuleEnd S W p) and $\bar m, \bar n$ are the images of $m,n$ in $\mathbb{Z}/p$. Finally, FrobeniusEndo.FrobCharEqOnPoints W σ a q is the predicate, for an integer $a$ and a natural number $q$, that every point $P$ of (W⁄k).Point satisfies $\sigma(\sigma P) - a\cdot\sigma P + q\cdot P = 0$: the characteristic equation of $\sigma$ asserted pointwise on the group of points, rather than as an identity in a ring of endomorphisms.

Relation to Mathlib. Mathlib has no notion of a pencil $m - n\psi$ of additive endomorphisms, of its kernel count, or of a pointwise characteristic equation for a field automorphism acting on the points of a Weierstrass curve; these are the project's own. The endomorphism frobEnd is the project's action of $S$-algebra automorphisms of $k$ on (W⁄k).Point packaged through Mathlib's DistribSMul.toAddMonoidHom.

Where it is used. These notions provide the vocabulary for counting points and for identifying the trace and determinant of the action of a Frobenius automorphism on the $p$-torsion of a Weierstrass curve, which is what enters the description of the mod $p$ Galois representation attached to the Frey curve.

<!-- Generated by add_prove2me_provenance.py -->

def FrobeniusEndo.linePencil {A : Type u_1} [AddCommGroup A] (ψ : A →+ A) (m n : ℤ) : A →+ A

The endomorphism m • id - n • ψ associated to the integer pair (m, n).

Equations

• FrobeniusEndo.linePencil ψ m n = m • AddMonoidHom.id A - n • ψ

@[simp]

theorem FrobeniusEndo.linePencil_apply {A : Type u_1} [AddCommGroup A] (ψ : A →+ A) (m n : ℤ) (P : A) : (linePencil ψ m n) P = m • P - n • ψ P

noncomputable def FrobeniusEndo.kerDeg {A : Type u_1} [AddCommGroup A] (ψ : A →+ A) (m n : ℤ) : ℕ

The cardinality of the kernel of the endomorphism, with the Nat.card convention for infinite kernels.

Equations

• FrobeniusEndo.kerDeg ψ m n = Nat.card ↥(FrobeniusEndo.linePencil ψ m n).ker

theorem FrobeniusEndo.kerDeg_def {A : Type u_1} [AddCommGroup A] (ψ : A →+ A) (m n : ℤ) : kerDeg ψ m n = Nat.card ↥(linePencil ψ m n).ker

theorem FrobeniusEndo.mem_ker_linePencil_iff {A : Type u_1} [AddCommGroup A] (ψ : A →+ A) (m n : ℤ) (P : A) : P ∈ (linePencil ψ m n).ker ↔ m • P = n • ψ P

@[reducible, inline]

noncomputable abbrev FrobeniusEndo.frobEnd {R : Type u_1} {S : Type u_2} {k : Type u_3} [CommRing R] [CommRing S] [Field k] [DecidableEq k] [Algebra R S] [Algebra R k] [Algebra S k] [IsScalarTower R S k] (W : WeierstrassCurve R) (σ : k ≃ₐ[S] k) : (WeierstrassCurve.Affine.baseChange W k).Point →+ (WeierstrassCurve.Affine.baseChange W k).Point

The point-group endomorphism induced by the specified Galois automorphism.

Equations

• FrobeniusEndo.frobEnd W σ = DistribSMul.toAddMonoidHom (WeierstrassCurve.Affine.baseChange W k).Point σ

theorem FrobeniusEndo.frobEnd_apply {R : Type u_1} {S : Type u_2} {k : Type u_3} [CommRing R] [CommRing S] [Field k] [DecidableEq k] [Algebra R S] [Algebra R k] [Algebra S k] [IsScalarTower R S k] (W : WeierstrassCurve R) (σ : k ≃ₐ[S] k) (P : (WeierstrassCurve.Affine.baseChange W k).Point) : (frobEnd W σ) P = σ • P

@[reducible, inline]

noncomputable abbrev FrobeniusEndo.frobPencilEnd {R : Type u_1} {S : Type u_2} {k : Type u_3} [CommRing R] [CommRing S] [Field k] [DecidableEq k] [Algebra R S] [Algebra R k] [Algebra S k] [IsScalarTower R S k] (W : WeierstrassCurve R) (σ : k ≃ₐ[S] k) (p : ℕ) (m n : ℤ) : Module.End (ZMod p) ↥(Submodule.torsionBy ℤ (WeierstrassCurve.Affine.baseChange W k).Point ↑p)

The endomorphism m • id - n • Frobenius on the indicated torsion subgroup.

Equations

• FrobeniusEndo.frobPencilEnd W σ p m n = ↑m • 1 - ↑n • (WeierstrassCurve.Affine.Point.galoisRepModuleEnd S W p) σ

def FrobeniusEndo.FrobCharEqOnPoints {R : Type u_1} {S : Type u_2} {k : Type u_3} [CommRing R] [CommRing S] [Field k] [DecidableEq k] [Algebra R S] [Algebra R k] [Algebra S k] [IsScalarTower R S k] (W : WeierstrassCurve R) (σ : k ≃ₐ[S] k) (a : ℤ) (q : ℕ) : Prop

Frobenius satisfies the quadratic relation F² - aF + q = 0 on every point.

Equations

• FrobeniusEndo.FrobCharEqOnPoints W σ a q = ∀ (P : (WeierstrassCurve.Affine.baseChange W k).Point), σ • σ • P - a • σ • P + ↑q • P = 0