structure FrobeniusEndomorphism.FixesCoeffs {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ : F →+* F) : Prop

A ring homomorphism $\varphi : F \to F$ fixes the coefficients of a Weierstrass curve $W$ if it acts as the identity on the five defining coefficients $a_1, a_2, a_3, a_4, a_6$. This is the condition needed for $\varphi$ to descend to a map of curves.

• fix_a₁ : φ W.a₁ = W.a₁
• fix_a₂ : φ W.a₂ = W.a₂
• fix_a₃ : φ W.a₃ = W.a₃
• fix_a₄ : φ W.a₄ = W.a₄
• fix_a₆ : φ W.a₆ = W.a₆

theorem FrobeniusEndomorphism.evalEval_polynomial_map {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) (x y : F) : Polynomial.evalEval (φ x) (φ y) W.polynomial = φ (Polynomial.evalEval x y W.polynomial)

A coefficient-fixing ring homomorphism commutes with two-variable evaluation of the defining polynomial of $W$: $f_W(\varphi x, \varphi y) = \varphi(f_W(x, y))$.

theorem FrobeniusEndomorphism.equation_preserved {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) {x y : F} (h : W.Equation x y) : W.Equation (φ x) (φ y)

A coefficient-fixing endomorphism sends solutions of the Weierstrass equation to solutions: if $W(x, y) = 0$ then $W(\varphi x, \varphi y) = 0$.

theorem FrobeniusEndomorphism.evalEval_polynomialX_map {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) (x y : F) : Polynomial.evalEval (φ x) (φ y) W.polynomialX = φ (Polynomial.evalEval x y W.polynomialX)

A coefficient-fixing endomorphism commutes with two-variable evaluation of the $x$-partial derivative $\partial_x W$ of the defining polynomial.

theorem FrobeniusEndomorphism.evalEval_polynomialY_map {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) (x y : F) : Polynomial.evalEval (φ x) (φ y) W.polynomialY = φ (Polynomial.evalEval x y W.polynomialY)

A coefficient-fixing endomorphism commutes with two-variable evaluation of the $y$-partial derivative $\partial_y W$ of the defining polynomial.

theorem FrobeniusEndomorphism.nonsingular_preserved {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) (hφ_inj : Function.Injective ⇑φ) {x y : F} (h : W.Nonsingular x y) : W.Nonsingular (φ x) (φ y)

An injective coefficient-fixing endomorphism preserves nonsingularity: if $(x, y)$ is a nonsingular point on $W$, so is $(\varphi x, \varphi y)$.

noncomputable def FrobeniusEndomorphism.pointMap {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) (hφ_inj : Function.Injective ⇑φ) : W.Point → W.Point

The induced self-map on the affine points $W(\overline{F})$ of a Weierstrass curve given by an injective coefficient-fixing endomorphism: it fixes the point at infinity and applies $\varphi$ coordinatewise to affine points.

@[simp]

theorem FrobeniusEndomorphism.pointMap_zero {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) (hφ_inj : Function.Injective ⇑φ) : pointMap hφ hφ_inj WeierstrassCurve.Affine.Point.zero = WeierstrassCurve.Affine.Point.zero

The induced map sends the point at infinity to itself.

@[simp]

theorem FrobeniusEndomorphism.pointMap_some {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ : F →+* F} (hφ : FixesCoeffs W φ) (hφ_inj : Function.Injective ⇑φ) {x y : F} (h : W.Nonsingular x y) : pointMap hφ hφ_inj (WeierstrassCurve.Affine.Point.some x y h) = WeierstrassCurve.Affine.Point.some (φ x) (φ y) ⋯

The induced map sends an affine point $(x, y)$ to $(\varphi x, \varphi y)$.

theorem FrobeniusEndomorphism.iterateFrobenius_algebraMap {F : Type u} [Field F] {p n : ℕ} [Fintype F] [Fact (Nat.Prime p)] {L : Type u} [Field L] [Algebra F L] [CharP L p] (hcard : Fintype.card F = p ^ n) (a : F) : (iterateFrobenius L p n) ((algebraMap F L) a) = (algebraMap F L) a

The $n$-th iterate of Frobenius on an $F$-algebra $L$ fixes the image of any element of $F = \mathbb{F}_{p^n}$, because by Fermat's little theorem $a^{p^n} = a$ for $a \in F$.

@[reducible, inline]

noncomputable abbrev FrobeniusEndomorphism.baseChange {F : Type u} [Field F] {L : Type u} [Field L] [Algebra F L] (W : WeierstrassCurve.Affine F) : WeierstrassCurve.Affine L

The base change of a Weierstrass curve $W/F$ along an algebra inclusion $F \hookrightarrow L$: the same equation viewed over the larger field $L$.

theorem FrobeniusEndomorphism.fixesCoeffs_iterateFrobenius {F : Type u} [Field F] {p n : ℕ} [Fintype F] [Fact (Nat.Prime p)] {L : Type u} [Field L] [Algebra F L] [CharP L p] (hcard : Fintype.card F = p ^ n) (W : WeierstrassCurve.Affine F) : FixesCoeffs (baseChange W) (iterateFrobenius L p n)

The $n$-th Frobenius iterate $x \mapsto x^{p^n}$ on $L$ fixes the coefficients of the base change to $L$ of any curve defined over $\mathbb{F}_{p^n}$, since those coefficients lie in the prime-field-fixed subfield.

noncomputable def FrobeniusEndomorphism.frobeniusPointMap {F : Type u} [Field F] {p n : ℕ} [Fintype F] [Fact (Nat.Prime p)] {L : Type u} [Field L] [Algebra F L] [CharP L p] (hcard : Fintype.card F = p ^ n) (W : WeierstrassCurve.Affine F) : (baseChange W).Point → (baseChange W).Point

The Frobenius endomorphism on points of $W_L$ for $W/\mathbb{F}_{p^n}$ (Definition 4.24): the self-map of points sending $(x, y) \mapsto (x^{p^n}, y^{p^n})$. This is the geometric Frobenius whose fixed points are the $\mathbb{F}_{p^n}$-rational points.

@[simp]

theorem FrobeniusEndomorphism.frobeniusPointMap_zero {F : Type u} [Field F] {p n : ℕ} [Fintype F] [Fact (Nat.Prime p)] {L : Type u} [Field L] [Algebra F L] [CharP L p] (hcard : Fintype.card F = p ^ n) (W : WeierstrassCurve.Affine F) : frobeniusPointMap hcard W WeierstrassCurve.Affine.Point.zero = WeierstrassCurve.Affine.Point.zero

Frobenius fixes the point at infinity.

@[simp]

theorem FrobeniusEndomorphism.frobeniusPointMap_some {F : Type u} [Field F] {p n : ℕ} [Fintype F] [Fact (Nat.Prime p)] {L : Type u} [Field L] [Algebra F L] [CharP L p] (hcard : Fintype.card F = p ^ n) (W : WeierstrassCurve.Affine F) {x y : L} (h : (baseChange W).Nonsingular x y) : frobeniusPointMap hcard W (WeierstrassCurve.Affine.Point.some x y h) = WeierstrassCurve.Affine.Point.some (x ^ p ^ n) (y ^ p ^ n) ⋯

Frobenius sends an affine point $(x, y)$ on the base change of $W$ to $(x^{p^n}, y^{p^n})$.