Node Poly map root relations
WeierstrassCurve.nodePoly_map_root_relations
Plain-language statement
If the root of the reduced node polynomial P̄ (assumed irreducible) satisfies a monic quadratic relation X² - t·X + n over the residue field, then comparing with the defining relation of P̄ (aeval_root_nodePoly_map) and using the linear independence of 1 and the root (AdjoinRoot.eq_zero_of_mul_root_add_eq_zero) yields the relations `φc₄·t + φ(...
Exact Lean statement
theorem nodePoly_map_root_relations [E.HasMultiplicativeReduction R]
(hirr : Irreducible ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))))
{t n : ResidueField R}
(hρ : AdjoinRoot.root ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))) ^ 2
- algebraMap (ResidueField R)
(AdjoinRoot ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))) t
* AdjoinRoot.root ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))
+ algebraMap (ResidueField R)
(AdjoinRoot ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))) n
= 0) :
residue R (E.integralModel R).c₄ * t
+ residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0
∧ residue R (E.integralModel R).c₄ * n
+ residue R (54 * (E.integralModel R).b₆
- 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄
+ (E.integralModel R).a₂ * (E.integralModel R).c₄) = 0Formal artifact
Lean source
theorem nodePoly_map_root_relations [E.HasMultiplicativeReduction R] (hirr : Irreducible ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))) {t n : ResidueField R} (hρ : AdjoinRoot.root ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))) ^ 2 - algebraMap (ResidueField R) (AdjoinRoot ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))) t * AdjoinRoot.root ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))) + algebraMap (ResidueField R) (AdjoinRoot ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))) n = 0) : residue R (E.integralModel R).c₄ * t + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0 ∧ residue R (E.integralModel R).c₄ * n + residue R (54 * (E.integralModel R).b₆ - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄ + (E.integralModel R).a₂ * (E.integralModel R).c₄) = 0 := by set P := (E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)) with hP have : Fact (Irreducible P) := ⟨hirr⟩ have hPdeg2 : P.natDegree = 2 := natDegree_nodePoly_map E R have hρ2 : algebraMap (ResidueField R) (AdjoinRoot P) (algebraMap R (ResidueField R) (E.integralModel R).c₄) * (AdjoinRoot.root P) ^ 2 + algebraMap (ResidueField R) (AdjoinRoot P) (algebraMap R (ResidueField R) ((E.integralModel R).a₁ * (E.integralModel R).c₄)) * (AdjoinRoot.root P) - algebraMap (ResidueField R) (AdjoinRoot P) (algebraMap R (ResidueField R) (54 * (E.integralModel R).b₆ - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄ + (E.integralModel R).a₂ * (E.integralModel R).c₄)) = 0 := aeval_root_nodePoly_map (algebraMap R (ResidueField R)) (E.integralModel R) obtain ⟨hA, hB⟩ := AdjoinRoot.eq_zero_of_mul_root_add_eq_zero hPdeg2.ge (a := residue R (E.integralModel R).c₄ * t + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄)) (b := -(residue R (E.integralModel R).c₄ * n + residue R (54 * (E.integralModel R).b₆ - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄ + (E.integralModel R).a₂ * (E.integralModel R).c₄))) (by simp only [IsLocalRing.ResidueField.algebraMap_eq, map_add, map_mul, map_neg] at hρ2 ⊢ linear_combination hρ2 - algebraMap (ResidueField R) (AdjoinRoot P) (residue R (E.integralModel R).c₄) * hρ) rw [neg_eq_zero] at hB exact ⟨hA, hB⟩- Project
- Fermat's Last Theorem
- License
- Apache-2.0
- Commit
- 8dd808888295
- Source
- FLT/KnownIn1980s/EllipticCurves/QuadraticTwists/SplitMultiplicativeReduction.lean:191-230
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Eq finsum quotient out of bij On
AbstractHeckeOperator.eq_finsum_quotient_out_of_bijOn'
Plain-language statement
If a is fixed by V then ∑ᶠ g ∈ s, g • a is independent of the choice s of coset representatives in G for a subset of G ⧸ V
Source project: Fermat's Last Theorem
Person-level attribution pending.
Comm Group no compact automorphisms
CommGroup.no_compact_automorphisms
Plain-language statement
A connected compact Hausdorff abelian topological group does not admit a nontrivial compact group of automorphisms.
Source project: Fermat's Last Theorem
Person-level attribution pending.
Fermat Last Theorem of p ge 5
FermatLastTheorem.of_p_ge_5
Plain-language statement
If Fermat's Last Theorem is true for primes p ≥ 5, then FLT is true.
Source project: Fermat's Last Theorem
Person-level attribution pending.