HexECPPTheory.Hasse.Frobenius

source

noncomputable def Hex.ECPP.pointFrobenius (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

(W.baseChange K).Point →+ (W.baseChange K).Point

The p-power Frobenius endomorphism on the points of a curve over ZMod p.

Equations

Hex.ECPP.pointFrobenius p W = WeierstrassCurve.Affine.Point.map (FiniteField.frobeniusAlgHom (ZMod p) K)

Instances For

source

@[simp]

theorem Hex.ECPP.pointFrobenius_zero (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

(pointFrobenius p W) 0 = 0

Frobenius fixes the point at infinity.

source

theorem Hex.ECPP.pointFrobenius_baseChange (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) (P : (W.baseChange (ZMod p)).Point) :

(pointFrobenius p W) ((WeierstrassCurve.Affine.Point.baseChange (ZMod p) K) P) = (WeierstrassCurve.Affine.Point.baseChange (ZMod p) K) P

Every point defined over the prime field is fixed after base change.

source

theorem Hex.ECPP.pointFrobenius_fixed_coords (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) {x y : K} (h : (W.baseChange K).Nonsingular x y) (hfix : (pointFrobenius p W) (WeierstrassCurve.Affine.Point.some x y h) = WeierstrassCurve.Affine.Point.some x y h) :

x ^ p = x ∧ y ^ p = y

A fixed affine point has both coordinates fixed by p-power Frobenius.

source

theorem Hex.ECPP.pointFrobenius_fixed_iff (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) (P : (W.baseChange K).Point) :

(pointFrobenius p W) P = P ↔ ∃ (Q : (W.baseChange (ZMod p)).Point), (WeierstrassCurve.Affine.Point.baseChange (ZMod p) K) Q = P

Characterize fixed points as points obtained by base change from ZMod p.

source

noncomputable def Hex.ECPP.rationalPointsEquivFixed (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

(W.baseChange (ZMod p)).Point ≃ { P : (W.baseChange K).Point // (pointFrobenius p W) P = P }

The rational points are exactly the Frobenius fixed points.

Equations

Hex.ECPP.rationalPointsEquivFixed p W = Equiv.ofBijective (fun (Q : (W.baseChange (ZMod p)).Point) => ⟨(WeierstrassCurve.Affine.Point.baseChange (ZMod p) K) Q, ⋯⟩) ⋯

Instances For

source

@[instance_reducible]

noncomputable instance Hex.ECPP.instFintypeSubtypePointBaseChangeZModEqCoeAddMonoidHomPointFrobenius (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

Fintype { P : (W.baseChange K).Point // (pointFrobenius p W) P = P }

Equations

Hex.ECPP.instFintypeSubtypePointBaseChangeZModEqCoeAddMonoidHomPointFrobenius p W = Fintype.ofEquiv (W.baseChange (ZMod p)).Point (Hex.ECPP.rationalPointsEquivFixed p W)

source

theorem Hex.ECPP.card_fixedPoints (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

Fintype.card { P : (W.baseChange K).Point // (pointFrobenius p W) P = P } = Fintype.card (W.baseChange (ZMod p)).Point

Frobenius has as many fixed points as the curve has prime-field points.

source

noncomputable def Hex.ECPP.oneSubFrobenius (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

(W.baseChange K).Point →+ (W.baseChange K).Point

The endomorphism whose kernel is the set of rational points.

Equations

Hex.ECPP.oneSubFrobenius p W = AddMonoidHom.id (W.baseChange K).Point - Hex.ECPP.pointFrobenius p W

Instances For

source

@[simp]

theorem Hex.ECPP.oneSubFrobenius_eq_zero (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) (P : (W.baseChange K).Point) :

(oneSubFrobenius p W) P = 0 ↔ (pointFrobenius p W) P = P

1 - Frobenius vanishes exactly on Frobenius fixed points.

source

theorem Hex.ECPP.mem_ker_oneSubFrobenius (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) (P : (W.baseChange K).Point) :

P ∈ (oneSubFrobenius p W).ker ↔ (pointFrobenius p W) P = P

Membership in the kernel of 1 - Frobenius is the fixed-point condition.

source

noncomputable def Hex.ECPP.rationalPointsEquivKer (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

(W.baseChange (ZMod p)).Point ≃ ↥(oneSubFrobenius p W).ker

The kernel of 1 - Frobenius consists of the rational points.

Equations

Hex.ECPP.rationalPointsEquivKer p W = (Hex.ECPP.rationalPointsEquivFixed p W).trans (Equiv.subtypeEquivProp ⋯).symm

Instances For

source

@[instance_reducible]

noncomputable instance Hex.ECPP.instFintypeSubtypePointBaseChangeZModMemAddSubgroupKerOneSubFrobenius (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

Fintype ↥(oneSubFrobenius p W).ker

Equations

Hex.ECPP.instFintypeSubtypePointBaseChangeZModMemAddSubgroupKerOneSubFrobenius p W = Fintype.ofEquiv (W.baseChange (ZMod p)).Point (Hex.ECPP.rationalPointsEquivKer p W)

source

theorem Hex.ECPP.card_ker_oneSubFrobenius (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [DecidableEq K] [Algebra (ZMod p) K] (W : WeierstrassCurve.Affine (ZMod p)) :

Fintype.card ↥(oneSubFrobenius p W).ker = Fintype.card (W.baseChange (ZMod p)).Point

The kernel of 1 - Frobenius has the prime-field point count.