Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 11 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

11 results

Clear filters
Project-declaredLean 4.32.0

Quadratic Twist Point Equiv galois

WeierstrassCurve.quadraticTwistPointEquiv_galois

Plain-language statement

Twisting the Galois action. The Galois action on the points of the quadratic twist is the Galois action on the points of E, twisted by the quadratic character of L/K: for σ ∈ Aut(M/K), transporting the action of σ on Eᴸ(M) through Eᴸ(M) ≅ E(M) gives χ(σ) times the action of σ on E(M). Taking M to be a separable closure of K, this...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Quadratic Twist Point Equiv map

WeierstrassCurve.quadraticTwistPointEquiv_map

Plain-language statement

Naturality of quadraticTwistPointEquiv in M: the isomorphisms on M-points over varying M ⊇ L are all induced by a single isomorphism of curves over L, so they commute with the maps on points induced by any L-algebra homomorphism.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Quadratic Twist Point Equiv map of not fixed

WeierstrassCurve.quadraticTwistPointEquiv_map_of_not_fixed

Plain-language statement

The anti-equivariance underlying quadraticTwistPointEquiv_galois: if σ ∈ Aut(M/K) does not fix L pointwise (χ(σ) = -1), then transporting its action through Eᴸ(M) ≅ E(M) gives minus its action. This is the point-level shadow of quadraticTwistVarChange_baseChange_map.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Quadratic Twist Var Change base Change map

WeierstrassCurve.quadraticTwistVarChange_baseChange_map

Plain-language statement

The M-level form of the twist's defining cocycle: any σ ∈ Aut(M/K) not fixing L pointwise (i.e. with χ(σ) = -1) conjugates the base change to M of quadraticTwistVarChange by the automorphism [-1] of E. This is the base change of quadraticTwistVarChange_map.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Quadratic Twist Var Change map

WeierstrassCurve.quadraticTwistVarChange_map

Plain-language statement

The defining cocycle of the quadratic twist. The nontrivial σ ∈ Gal(L/K) conjugates the change of variables quadraticTwistVarChange (carrying E to Eᴸ) by the automorphism [-1] of E. This is the datum expressing that Eᴸ is the descent of E along the twisted Galois action σ ↦ (-1) ∘ σ, and it holds for every j.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record