@[reducible, inline]

noncomputable abbrev ArithmeticGeometry.specOf (R : Type u) [CommRing R] : AlgebraicGeometry.Scheme

The affine scheme $\mathrm{Spec}\, R$ for a commutative ring $R$.

noncomputable def ArithmeticGeometry.specAlgClosureToSpec (k : Type u) [Field k] : specOf (AlgebraicClosure k) ⟶ specOf k

The morphism of schemes $\mathrm{Spec}\, \overline{k} \to \mathrm{Spec}\, k$ induced by the algebraic closure inclusion $k \hookrightarrow \overline{k}$.

noncomputable def ArithmeticGeometry.baseChangeToAlgClosure (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (specOf k)] : AlgebraicGeometry.Scheme

Base change of a $k$-scheme $X$ along the algebraic closure, producing the $\overline{k}$-scheme $X_{\overline{k}} := X \times_{\mathrm{Spec}\, k} \mathrm{Spec}\, \overline{k}$.

@[implicit_reducible]

noncomputable instance ArithmeticGeometry.baseChangeToAlgClosure_over (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (specOf k)] : (baseChangeToAlgClosure k X).Over (specOf (AlgebraicClosure k))

The base change $X_{\overline{k}}$ is canonically a scheme over $\mathrm{Spec}\, \overline{k}$.

def ArithmeticGeometry.AreTwists (k : Type u) [Field k] (X Y : AlgebraicGeometry.Scheme) [X.Over (specOf k)] [Y.Over (specOf k)] : Prop

Definition 26.1. Two $k$-schemes $X$ and $Y$ are twists of each other if they become isomorphic over the algebraic closure: $X_{\overline{k}} \cong Y_{\overline{k}}$ as $\overline{k}$-schemes.

theorem ArithmeticGeometry.AreTwists.refl {k : Type u} [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (specOf k)] : AreTwists k X X

Reflexivity of the twist relation: every scheme is a twist of itself.

theorem ArithmeticGeometry.AreTwists.symm {k : Type u} [Field k] {X Y : AlgebraicGeometry.Scheme} [X.Over (specOf k)] [Y.Over (specOf k)] (h : AreTwists k X Y) : AreTwists k Y X

Symmetry of the twist relation: if $X$ and $Y$ are twists, then so are $Y$ and $X$.

theorem ArithmeticGeometry.AreTwists.trans {k : Type u} [Field k] {X Y Z : AlgebraicGeometry.Scheme} [X.Over (specOf k)] [Y.Over (specOf k)] [Z.Over (specOf k)] (hXY : AreTwists k X Y) (hYZ : AreTwists k Y Z) : AreTwists k X Z

Transitivity of the twist relation: if $X$ is a twist of $Y$ and $Y$ is a twist of $Z$, then $X$ is a twist of $Z$.

def GenusOneCurve.IsTwistOfEllipticCurve {k : Type v} [Field k] (C : GenusOneCurve k) (E : EllipticCurveOver k) : Prop

A genus-one curve $C$ is a twist of an elliptic curve $E$ if its Jacobian becomes isomorphic to $E$ over the algebraic closure $\overline{k}$, via a Weierstrass variable change.

theorem GenusOneCurve.exists_ellipticCurve_twist {k : Type v} [Field k] (C : GenusOneCurve k) : ∃ (E : EllipticCurveOver k), C.IsTwistOfEllipticCurve E

Theorem 26.3 (existence of an elliptic curve with prescribed $j$-invariant). Every genus-one curve $C$ over $k$ is a twist of some elliptic curve $E$ over $k$ sharing the same $j$-invariant.

def EllipticCurveOver.IsIsomorphicOverK {k : Type v} [Field k] (E₁ E₂ : EllipticCurveOver k) : Prop

Two elliptic curves over $k$ are isomorphic over $k$ if there exists a Weierstrass variable change defined over $k$ taking one to the other.

theorem Rat.no_fourth_root_of_four (q : ℚ) : q ^ 4 ≠ 4

No rational number satisfies $q^4 = 4$; equivalently, $\sqrt[4]{4}$ is irrational. Used to exhibit nontrivial twists over $\mathbb{Q}$.

theorem not_iso_y2x3mx_y2x3m4x : ¬∃ (σ : WeierstrassCurve.VariableChange ℚ), { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := -1, a₆ := 0 } = σ • { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := -4, a₆ := 0 }

The elliptic curves $y^2 = x^3 - x$ and $y^2 = x^3 - 4x$ over $\mathbb{Q}$ are not isomorphic over $\mathbb{Q}$, even though they have the same $j$-invariant. Concrete witness that nontrivial twists exist over $\mathbb{Q}$.

@[reducible, inline]

noncomputable abbrev uliftQToQ : ULift.{v, 0} ℚ →+* ℚ

The ring homomorphism $\mathrm{ULift}\, \mathbb{Q} \to \mathbb{Q}$ coming from the canonical equivalence. A universe-polymorphism utility.