Trebor-Huang

Basic Group Structure of Elliptic Curves

We quickly go over various concepts in the study of elliptic curve groups. This records everything notable during my couse of study.

0. Projective Plane

When studying algebraic curves, it is often necessary to introduce an extension of the plane $\mathbb F\times\mathbb F$, by introducing an auxiliary variable $z$, to make the equation homogeneous, e.g. $$y^2z=x^3+axz^2+bz^3.$$ Now we can consider the triplet $(x:y:z)$ as a ratio. This adds the case where $z=0$ to the curve, which eases the analysis in the future. We call this extended space the projective plane $\mathbb{PF}^2$.

When viewed in the 3-dimensional space, $\mathbb{PF}^2$ is equivalent to all straight lines passing through the origin of the space. By setting $z=1$, we are effectively obtaining a section of the lines. Those that are parallel to the plane $z=1$ are considered to be the points at infinity. However, there is nothing to stop us from using a different plane, say $x+y+z=1$. In this case

Trebor-Huang

Require Coq.Lists.List.

Module Type Sig.
  Parameter Atomic : Set.
  Parameter Atomic_dec : forall x y : Atomic, {x = y} + {x <> y}.
End Sig.

Module Propositional (UnderlyingAtomic : Sig).
Import UnderlyingAtomic.
Import Coq.Lists.List.

Trebor-Huang

{-# OPTIONS --prop --without-K --safe #-}

module Synthesis where

-- Utilities
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Nat using (zero; suc; _+_) renaming (Nat to ℕ)

infixl 8 _∧_ _×_

Trebor-Huang

{-# OPTIONS --prop #-}
module Logic where

id : ∀ {ℓ} {A : Set ℓ} -> A -> A
id x = x

data 𝕋 : Set where
    𝒩𝒶𝓉 : 𝕋
    𝒫𝓇ℴ𝓅 : 𝕋
    _⟶_ : 𝕋 -> 𝕋 -> 𝕋

Trebor-Huang

{-# OPTIONS --cubical --no-import-sorts --postfix-projections -W ignore #-}
module freeCCC where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Unit using (Unit; isPropUnit; isSetUnit)
open import Cubical.Data.Bool using (Bool; true; false; if_then_else_; isSetBool)
open import Cubical.Data.Sum using (_⊎_; inr; inl)
open import Cubical.Data.Sigma using (Σ; _×_; ΣPathP)

Trebor-Huang

module _ where
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Fin using (Fin) renaming (zero to 𝕫; suc to 𝕤_)
open import Data.Vec using (Vec; []; [_]; _∷_; tail; map; allFin) renaming (lookup to _!_)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
open import Data.Vec.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

variable
  n m n' : ℕ

Trebor-Huang

from functools import lru_cache

class Map:
    def __init__(self, f, iterable):
        self.data = (f, iterable)

    def __iter__(self):
        for i in self.data[1]:
            yield self.data[0](i)

Trebor-Huang

{-# OPTIONS --cubical -Wignore #-}
module lccc where
open import Cubical.Foundations.Prelude

data Obj : Type
data Hom : Obj → Obj → Type

variable
  A B C D X Y : Obj
  f g h u v e : Hom A B

Trebor-Huang

structure Pprop : Type where
  pos : Prop
  neg : Prop
  syn : pos → neg → False := by intros; assumption
namespace Pprop

instance : CoeSort Pprop Prop := ⟨Pprop.pos⟩
instance : Coe Bool Pprop where
  coe
  | true => {pos := True, neg := False}

Trebor-Huang

{-# OPTIONS --postfix-projections #-}
open import Agda.Primitive
open import Data.Product
module Polynomial where

variable
  X I O : Set

record Poly : Set₁ where
  -- A polynomial is an expression