Atlas.ArithmeticGeometry.code.EllipticCurves

theorem aut_P1_fixing_three_points_is_identity {K : Type u_1} [Field K] [DecidableEq K] (g : GL (Fin 2) K) (p₁ p₂ p₃ : OnePoint K) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) (hf₁ : g • p₁ = p₁) (hf₂ : g • p₂ = p₂) (hf₃ : g • p₃ = p₃) (p : OnePoint K) :

g • p = p

source

def MazurCyclicOrders :

Finset ℕ

Instances For

source

def MazurProductOrders :

Finset ℕ

Instances For

source

theorem WeierstrassCurve.Affine.Point.mazur_torsion (W : WeierstrassCurve ℚ) [W.IsElliptic] :

(∃ n ∈ MazurCyclicOrders, Nonempty (↥(AddCommGroup.torsion W.toAffine.Point) ≃+ ZMod n)) ∨ ∃ m ∈ MazurProductOrders, Nonempty (↥(AddCommGroup.torsion W.toAffine.Point) ≃+ ZMod 2 × ZMod (2 * m))

source

def WeierstrassCurve.Affine.Point.lineThirdIntersection {F : Type u_1} [Field F] {W : Affine F} [DecidableEq F] :

W.Point → W.Point → W.Point

Instances For

source

theorem WeierstrassCurve.Affine.Point.geometric_group_law {F : Type u_1} [Field F] {W : Affine F} [DecidableEq F] (P Q : W.Point) :

P + Q = -P.lineThirdIntersection Q

source

@[reducible, inline]

abbrev multiplicationByN {G : Type u_1} [AddCommGroup G] (n : ℕ) :

G →+ G

Instances For

source

def nTorsionSubgroup {G : Type u_1} [AddCommGroup G] (n : ℕ) :

AddSubgroup G

Instances For

source

@[simp]

theorem mem_nTorsionSubgroup {G : Type u_1} [AddCommGroup G] (n : ℕ) (P : G) :

P ∈ nTorsionSubgroup n ↔ n • P = 0

source

@[reducible, inline]

abbrev WeierstrassCurve.Affine.Point.nTorsion {F : Type u_1} [Field F] [DecidableEq F] {W : Affine F} (n : ℕ) :

AddSubgroup W.Point

Instances For

source

noncomputable def WeierstrassCurve.autGroup (R : Type u_1) [CommRing R] (W : WeierstrassCurve R) :

Subgroup (VariableChange R)

Instances For

source

theorem WeierstrassCurve.VariableChange.u_inv_ne_zero {F : Type u_1} [Field F] (C : VariableChange F) :

↑C.u⁻¹ ≠ 0

source

theorem WeierstrassCurve.aut_s_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) :

C.s = 0

source

theorem WeierstrassCurve.aut_r_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

C.r = 0

source

theorem WeierstrassCurve.aut_t_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

C.t = 0

source

theorem WeierstrassCurve.aut_u_inv_pow4_mul_a₄ {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

↑C.u⁻¹ ^ 4 * W.a₄ = W.a₄

source

theorem WeierstrassCurve.aut_u_inv_pow6_mul_a₆ {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

↑C.u⁻¹ ^ 6 * W.a₆ = W.a₆

source

theorem WeierstrassCurve.aut_u_inv_pow4_eq_one {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha4 : W.a₄ ≠ 0) :

↑C.u⁻¹ ^ 4 = 1

source

theorem WeierstrassCurve.aut_u_inv_pow6_eq_one {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha6 : W.a₆ ≠ 0) :

↑C.u⁻¹ ^ 6 = 1

source

theorem WeierstrassCurve.aut_u_inv_pow2_eq_one {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {C : VariableChange F} (hC : C • W = W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha4 : W.a₄ ≠ 0) (ha6 : W.a₆ ≠ 0) :

↑C.u⁻¹ ^ 2 = 1

source

theorem WeierstrassCurve.a₄_ne_zero_or_a₆_ne_zero {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] [W.IsElliptic] :

W.a₄ ≠ 0 ∨ W.a₆ ≠ 0

source

theorem WeierstrassCurve.u_pow_eq_one_of_inv_val_pow_eq_one {F : Type u_1} [Field F] {C : VariableChange F} {n : ℕ} (h : ↑C.u⁻¹ ^ n = 1) :

C.u ^ n = 1

source

theorem WeierstrassCurve.autGroup_u_pow_twelve {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] [W.IsElliptic] {C : VariableChange F} (hC : C ∈ autGroup F W) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

C.u ^ 12 = 1

source

instance WeierstrassCurve.autGroup_finite {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] [W.IsElliptic] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

Finite ↥(autGroup F W)

source

noncomputable def WeierstrassCurve.autGroupToFHom {F : Type u_1} [Field F] {W : WeierstrassCurve F} (_h2 : 2 ≠ 0) (_h3 : 3 ≠ 0) :

↥(autGroup F W) →* F

Instances For

source

theorem WeierstrassCurve.autGroupToFHom_injective {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

Function.Injective ⇑(autGroupToFHom h2 h3)

source

theorem WeierstrassCurve.autGroup_isCyclic {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] [W.IsElliptic] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) :

IsCyclic ↥(autGroup F W)

source

theorem WeierstrassCurve.autGroup_u_sq_eq_one_of_generic_j {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha4 : W.a₄ ≠ 0) (ha6 : W.a₆ ≠ 0) {C : VariableChange F} (hC : C ∈ autGroup F W) :

C.u ^ 2 = 1 ∧ C.r = 0 ∧ C.s = 0 ∧ C.t = 0

source

theorem WeierstrassCurve.autGroup_u_pow4_eq_one_of_j_1728 {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha4 : W.a₄ ≠ 0) {C : VariableChange F} (hC : C ∈ autGroup F W) :

C.u ^ 4 = 1 ∧ C.r = 0 ∧ C.s = 0 ∧ C.t = 0

source

theorem WeierstrassCurve.autGroup_u_pow6_eq_one_of_j_0 {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha6 : W.a₆ ≠ 0) {C : VariableChange F} (hC : C ∈ autGroup F W) :

C.u ^ 6 = 1 ∧ C.r = 0 ∧ C.s = 0 ∧ C.t = 0

source

theorem WeierstrassCurve.neg_one_mem_autGroup {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] :

{ u := -1, r := 0, s := 0, t := 0 } ∈ autGroup F W

source

theorem WeierstrassCurve.u_inv_val_pow_eq_one {F : Type u_1} [Field F] {n : ℕ} {u : Fˣ} (h : u ^ n = 1) :

↑u⁻¹ ^ n = 1

source

theorem WeierstrassCurve.fourth_root_mem_autGroup {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {u : Fˣ} (hu : u ^ 4 = 1) (ha₆ : W.a₆ = 0) :

{ u := u, r := 0, s := 0, t := 0 } ∈ autGroup F W

source

theorem WeierstrassCurve.sixth_root_mem_autGroup {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] {u : Fˣ} (hu : u ^ 6 = 1) (ha₄ : W.a₄ = 0) :

{ u := u, r := 0, s := 0, t := 0 } ∈ autGroup F W

source

theorem WeierstrassCurve.neg_one_ne_one_variableChange {F : Type u_1} [Field F] (h2 : 2 ≠ 0) :

{ u := -1, r := 0, s := 0, t := 0 } ≠ 1

source

theorem WeierstrassCurve.vc_eq_one_or_neg_one {F : Type u_1} [Field F] {C : VariableChange F} (hu : C.u ^ 2 = 1) (hr : C.r = 0) (hs : C.s = 0) (ht : C.t = 0) :

C = 1 ∨ C = { u := -1, r := 0, s := 0, t := 0 }

source

theorem WeierstrassCurve.autGroup_card_eq_two_of_generic_j {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha4 : W.a₄ ≠ 0) (ha6 : W.a₆ ≠ 0) :

Nat.card ↥(autGroup F W) = 2

source

noncomputable def WeierstrassCurve.autGroupEquivRootsOfUnity4 {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha4 : W.a₄ ≠ 0) (ha6 : W.a₆ = 0) :

↥(autGroup F W) ≃ ↥(rootsOfUnity 4 F)

Instances For

source

theorem WeierstrassCurve.autGroup_card_eq_four_of_j_1728 {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha4 : W.a₄ ≠ 0) (ha6 : W.a₆ = 0) {ζ : F} (hζ : IsPrimitiveRoot ζ 4) :

Nat.card ↥(autGroup F W) = 4

source

noncomputable def WeierstrassCurve.autGroupEquivRootsOfUnity6 {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha6 : W.a₆ ≠ 0) (ha4 : W.a₄ = 0) :

↥(autGroup F W) ≃ ↥(rootsOfUnity 6 F)

Instances For

source

theorem WeierstrassCurve.autGroup_card_eq_six_of_j_0 {F : Type u_1} [Field F] {W : WeierstrassCurve F} [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (ha6 : W.a₆ ≠ 0) (ha4 : W.a₄ = 0) {ζ : F} (hζ : IsPrimitiveRoot ζ 6) :

Nat.card ↥(autGroup F W) = 6

source

theorem WeierstrassCurve.Affine.shortNF_addX {F : Type u_1} [Field F] {W' : WeierstrassCurve F} [W'.IsShortNF] (x₁ x₂ ℓ : F) :

W'.toAffine.addX x₁ x₂ ℓ = ℓ ^ 2 - x₁ - x₂

source

theorem WeierstrassCurve.Affine.shortNF_addY {F : Type u_1} [Field F] {W' : WeierstrassCurve F} [W'.IsShortNF] (x₁ x₂ y₁ ℓ : F) :

W'.toAffine.addY x₁ x₂ y₁ ℓ = ℓ * (x₁ - W'.toAffine.addX x₁ x₂ ℓ) - y₁

source

theorem WeierstrassCurve.Affine.shortNF_slope_of_X_ne {F : Type u_1} [Field F] {W' : WeierstrassCurve F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (hx : x₁ ≠ x₂) :

W'.toAffine.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

source

theorem WeierstrassCurve.Affine.shortNF_slope_of_tangent {F : Type u_1} [Field F] {W' : WeierstrassCurve F} [W'.IsShortNF] [DecidableEq F] {x₁ y₁ y₂ : F} (hy : y₁ ≠ W'.toAffine.negY x₁ y₂) :

W'.toAffine.slope x₁ x₁ y₁ y₂ = (3 * x₁ ^ 2 + W'.a₄) / (2 * y₁)

source

theorem WeierstrassCurve.Affine.Point.explicit_chord_formula {F : Type u_1} [Field F] [DecidableEq F] {W' : WeierstrassCurve F} [W'.IsShortNF] {x₁ x₂ y₁ y₂ : F} (h₁ : W'.toAffine.Nonsingular x₁ y₁) (h₂ : W'.toAffine.Nonsingular x₂ y₂) (hx : x₁ ≠ x₂) :

have ℓ := W'.toAffine.slope x₁ x₂ y₁ y₂; have x₃ := W'.toAffine.addX x₁ x₂ ℓ; ∃ (h₃ : W'.toAffine.Nonsingular x₃ (W'.toAffine.addY x₁ x₂ y₁ ℓ)), some x₁ y₁ h₁ + some x₂ y₂ h₂ = some x₃ (W'.toAffine.addY x₁ x₂ y₁ ℓ) h₃ ∧ ℓ = (y₁ - y₂) / (x₁ - x₂) ∧ x₃ = ℓ ^ 2 - x₁ - x₂ ∧ W'.toAffine.addY x₁ x₂ y₁ ℓ = ℓ * (x₁ - x₃) - y₁

source

def ArithmeticGeometry.SmoothProjectiveCurve.genus {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) :

ℕ

Instances For

source

def ArithmeticGeometry.SmoothProjectiveCurve.HasRationalPoint {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) :

Prop

Instances For

source

theorem genus_zero_of_isomorphic_P1 {k : Type u_1} [Field k] (C : ArithmeticGeometry.SmoothProjectiveCurve k) (hiso : C.IsIsomorphicToP1) :

C.genus = 0

source

theorem exists_simple_pole_function_of_genus_zero {k : Type u_1} [Field k] (C : ArithmeticGeometry.SmoothProjectiveCurve k) (P : C.RatPoint) (hg : C.genus = 0) :

∃ (Q : C.RatPoint) (f : C.FunField), Q ≠ P ∧ f ≠ 0 ∧ C.principalDiv f = C.pointToDivisor Q + -C.pointToDivisor P

source

theorem isomorphic_P1_of_genus_zero_and_rational_point {k : Type u_1} [Field k] (C : ArithmeticGeometry.SmoothProjectiveCurve k) (hP : C.HasRationalPoint) (hg : C.genus = 0) :

C.IsIsomorphicToP1