A genus-one curve points type over $k$: C_pts is nonempty after base change to the
algebraic closure, and is of arithmetic genus one.
- nonempty_over_closure : Nonempty C_pts
- genus_one : IsArithGenus1 k C_pts
Instances
Abstract predicate: the action of $E$ on $C$ defining a torsor is realised by a $k$-rational morphism of varieties.
Instances For
Class wrapping the IsKActionMorphism predicate as an instance argument; required for the
torsor structure to define an "elliptic curve torsor over $k$".
- action_is_k_morphism : IsKActionMorphism k W E_pts C_pts
Instances
The transported torsor obtained from addTorsorOfEquiv is automatically a $k$-action
morphism.
The torsor obtained from a bijection $\varphi \colon C \simeq E$ satisfies the
IsActionMorphismOverk axiom.
An $E$-torsor over $k$: the data of an AddTorsor structure of $E_{\mathrm{pts}}$ on
$C_{\mathrm{pts}}$, a witness that $C$ is a genus-one curve points type, and a witness that the
action is a $k$-rational morphism.
- toAddTorsor : AddTorsor E_pts C_pts
- genusOne : IsGenusOneCurvePoints k C_pts
- actionMorphism : IsActionMorphismOverk k W E_pts C_pts
Instances For
An $E$-torsor over $k$ is nonempty (since AddTorsor requires nonemptiness).
Choosing a base point $c_0 \in C$ in an $E$-torsor produces an equivalence $E \simeq C$ via $g \mapsto g +_v c_0$.
Instances For
An $E$-torsor (over $k$) is in particular a torsor in the abstract sense.
Instances For
A $k$-rational map between two curve point types, encoded as an inductive closure under identity, symmetry, and composition.
- refl_equiv {k : Type u} [Field k] (C_pts : Type u) : IsKRationalMap k C_pts C_pts (Equiv.refl C_pts)
- symm_equiv {k : Type u} [Field k] {C₁_pts C₂_pts : Type u} {e : C₁_pts ≃ C₂_pts} : IsKRationalMap k C₁_pts C₂_pts e → IsKRationalMap k C₂_pts C₁_pts e.symm
- trans_equiv {k : Type u} [Field k] {C₁_pts C₂_pts C₃_pts : Type u} {e₁₂ : C₁_pts ≃ C₂_pts} {e₂₃ : C₂_pts ≃ C₃_pts} : IsKRationalMap k C₁_pts C₂_pts e₁₂ → IsKRationalMap k C₂_pts C₃_pts e₂₃ → IsKRationalMap k C₁_pts C₃_pts (e₁₂.trans e₂₃)
Instances For
A $k$-isomorphism of curve points: a bijection $e$ that is $k$-rational as a map of algebraic varieties.
- is_k_rational : IsKRationalMap k C₁_pts C₂_pts e
Instances
The identity map is $k$-rational.
The inverse of a $k$-rational equivalence is $k$-rational.
The composition of two $k$-rational equivalences is $k$-rational.
If two torsor base points $q_1, q_2$ are cohomologous as cocycles, then the torsor translation map between the corresponding base-pointed presentations is $k$-rational.
The torsor-translation map associated to two cohomologous cocycles is a $k$-isomorphism.
Reflexivity of $k$-isomorphism.
The inverse of a $k$-isomorphism is a $k$-isomorphism.
The composition of two $k$-isomorphisms is a $k$-isomorphism.
A bundled $E$-torsor: a points type C_pts together with an IsETorsor proof.
- C_pts : Type u
Instances For
Two $E$-torsors $T_1, T_2$ are equivalent if there is a $k$-isomorphism $C_{T_1} \simeq C_{T_2}$ that intertwines the $E$-actions: $e(p +_v q) = p +_v e(q)$.
Instances For
Reflexivity: every torsor is equivalent to itself via the identity.
Symmetry of torsor equivalence.
Transitivity of torsor equivalence.
The setoid on ETorsor whose equivalence relation is torsor equivalence.
An $E$-action-preserving equivalence of torsors is automatically $-_v$-preserving: $e(P) -_v e(Q) = P -_v Q$.
Conversely, a $-_v$-preserving map of torsors is automatically $+_v$-compatible.
An equivalence of $E$-torsors is $+_v$-compatible iff it is $-_v$-preserving.
The Weil-Châtelet set of $E/k$: the set of $E$-torsors over $k$ up to $k$-isomorphism,
realised as the quotient of ETorsor by the equivalence relation.
Instances For
The scalar multiplication $n \mapsto n \cdot e$ packaged as an additive homomorphism $\mathbb{Z} \to E$.
Instances For
The Abel-Jacobi map at the level of free abelian groups: $\sum n_P [P] \mapsto \sum n_P (P -_v Q_0)$, viewed as an additive homomorphism $(C \to_0 \mathbb{Z}) \to E$.
Instances For
The degree map sends a single basis element $[P]_n$ to $n$.
The Abel-Jacobi map piMap Q₀ is surjective: every element of $E$ can be realised as the
image of a divisor of degree zero.
Comparison of two base points: $\mathrm{piMap}\,Q_0(D) - \mathrm{piMap}\,Q_1(D) = \deg(D) \cdot (Q_1 -_v Q_0)$.
On divisors of degree zero, the Abel-Jacobi map is independent of the chosen base point.
Auxiliary data for the Abel-Jacobi isomorphism $\mathrm{Pic}^0(C) \simeq E$: a factorisation
of the Abel-Jacobi map $\pi$ through an intermediate group DivZero_E, together with the
inclusion of principal divisors and a "function field" compatibility condition.
- PrincDiv_E : AddSubgroup DivZero_E
- func_field (D : DivZero) : self.τ D ∈ self.PrincDiv_E → D ∈ PrincDiv
Instances For
The kernel of the Abel-Jacobi map $\pi$ is contained in the principal divisors: $\ker(\pi) \subseteq \mathrm{Princ}$.
Conversely, principal divisors are contained in the kernel of $\pi$, provided the converse
versions of the EllipticCurveDivisorData axioms hold.
Combining the two inclusions: $\ker(\pi) = \mathrm{Princ}$.
The Abel-Jacobi isomorphism: assuming the abstract divisor data and surjectivity of $\pi$, one has $\mathrm{Pic}^0(C) = \mathrm{Div}^0/\mathrm{Princ} \cong E$.
Instances For
Compatibility: the Abel-Jacobi isomorphism sends the class $[D]$ of a divisor $D$ to its image $\pi(D)$ in $E$.
The Abel-Jacobi isomorphism is additive: $\Phi(x + y) = \Phi(x) + \Phi(y)$.
The Abel-Jacobi isomorphism sends $0$ to $0$.
Inverse formula: $\Phi^{-1}(P)$ is the class of any preimage of $P$ under $\pi$, chosen via the surjectivity hypothesis.
Theorem 26.17 (concrete form): the Abel-Jacobi isomorphism
$\mathrm{Pic}^0(C) \cong E$ obtained from the concrete piMap and a divisor data.
Instances For
Surjectivity statement from Theorem 26.17: piMap Q₀ is surjective.
Kernel-containment statement from Theorem 26.17: $\ker(\mathrm{piMap}\,Q_0) \subseteq \mathrm{Princ}$.
Reverse containment from Theorem 26.17: $\mathrm{Princ} \subseteq \ker(\mathrm{piMap}\,Q_0)$.
Base-point independence from Theorem 26.17: for divisors of degree zero, piMap does not
depend on the chosen base point.