← all areas

Namespace WeierstrassCurve 1,003 theorems

Landmarks here: Modularity of semistable integral Weierstrass models · Mod-5 transport of residual modularity across the 3–5 switch · Residual modularity mod 3 at a cube-free level, with inertia condition · Mazur's Step 3 at one multiplicative prime ℓ · One of ρ̄_{W,3}, ρ̄_{W,5} is irreducible · Modularity lifting at p=3 from a prescribed residual level · Modularity lifting at p∈{3,5} for p²∤ M₀ · The 3–5 switch for semistable integral models · Four possible c₄³/Δ for rational 15-isogenies · Descent to the conductor level when p² ∤ N · From a patching datum to modularity at an explicit level · Level lowering at an unramified prime exactly dividing the level · Representability of the ordinary deformation problem for a semistable curve · Auxiliary curve for the 3–5 switch · Specialisations with rootless 3-division polynomial in a weighted family · Mod-3 irreducibility from Ψ₃ with no rational root

— 685 · Affine 135 · DrinfeldGlobal 164 · Generic 1 · IsCyclicGenKernel 4 · IsIntegralModelOf 3 · IsModularModelOfExactConductorLevel 1 · IsTwoKernel 4 · VariableChange 6

directly in WeierstrassCurve 685

• landmark Modularity of semistable integral Weierstrass models WeierstrassCurve.modularity_of_semistableModel 27,796 below · cited by 1 · depth 5
• Determinant of the mod-n torsion action as cyclotomic character WeierstrassCurve.apply_eq_pow_det_galoisRep_of_pow_eq_one 43 below · cited by 14 · depth 6
• The n-torsion of an elliptic curve has n² points WeierstrassCurve.card_torsion_of_isAlgClosed 0 below · cited by 115 · depth 6
• Determinant of the mod p representation is onto inertia at p WeierstrassCurve.det_galoisRep_surjOn_inertia 45 below · cited by 10 · depth 6
• Reduction-kernel filtration at a good ordinary prime p≠ 2 WeierstrassCurve.exists_atP_filtration_of_goodReduction 48 below · cited by 1 · depth 6
• Inertial filtration on p^m-torsion at multiplicative reduction WeierstrassCurve.exists_atP_filtration_of_multiplicativeReduction 65 below · cited by 2 · depth 6
• Inertia-fixed critical centre at a multiplicative prime WeierstrassCurve.exists_criticalCentre_of_multiplicativeReduction 1 below · cited by 13 · depth 6
• Integral quotient datum for a Galois-stable subgroup of order p WeierstrassCurve.exists_quotientDatum_of_galois_stable_primeCard 97 below · cited by 1 · depth 6
• Quotient data for cyclic p^m-subgroups from the prime-level case WeierstrassCurve.exists_quotientDatum_of_galois_stable_primePowCard 0 below · cited by 1 · depth 6
• Nonzero ℓ-torsion in the zero component at multiplicative reduction, ℓ≠ q WeierstrassCurve.exists_torsion_ne_zero_inZeroComponentAt_of_ne_residueChar 18 below · cited by 2 · depth 6
• Some ℓ-torsion point outside the zero component at a nodal prime WeierstrassCurve.exists_torsion_not_inZeroComponentAt_of_ne_residueChar 6 below · cited by 2 · depth 6
• ℓ-torsion in the zero component at a multiplicative prime WeierstrassCurve.exists_torsion_zeroComponent_submodule_of_multiplicativeReduction 0 below · cited by 7 · depth 6
• Frobenius satisfies its characteristic equation on prime-to-ℓ torsion WeierstrassCurve.frobenius_cayleyHamilton_on_torsion 24 below · cited by 3 · depth 6
• Equal level, opposite branches: the sum reduces smoothly WeierstrassCurve.inZeroComponentAt_add_of_level_eq_of_branch_ne 0 below · cited by 10 · depth 6
• Stability of the zero component under the decomposition group WeierstrassCurve.inZeroComponentAt_smul 0 below · cited by 6 · depth 6
• Inertia displacements lie in the zero component at q WeierstrassCurve.inZeroComponentAt_smul_sub_of_mem_inertiaSubgroupIn 12 below · cited by 8 · depth 6
• The zero component at A is closed under subtraction WeierstrassCurve.inZeroComponentAt_sub 0 below · cited by 11 · depth 6
• Equal level and same branch: the difference lies in the zero component WeierstrassCurve.inZeroComponentAt_sub_of_level_eq_of_branch_eq 0 below · cited by 7 · depth 6
• Modularity of a curve from a modular integral model WeierstrassCurve.isModular_map_of_isModularModel 0 below · cited by 1 · depth 6
• Openness of the pointwise stabiliser of n-torsion WeierstrassCurve.isOpen_torsionBy_fixingSubgroup 1 below · cited by 3 · depth 6
• landmark Mod-5 transport of residual modularity across the 3–5 switch WeierstrassCurve.isResiduallyModularOfLevel_of_switch 0 below · cited by 2 · depth 6
• landmark Residual modularity mod 3 at a cube-free level, with inertia condition WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel 7,306 below · cited by 2 · depth 6
• landmark Mazur's Step 3 at one multiplicative prime ℓ WeierstrassCurve.mazurStepThree_not_inZeroComponentAt 5,253 below · cited by 1 · depth 6
• landmark One of ρ̄_{W,3}, ρ̄_{W,5} is irreducible WeierstrassCurve.modThreeOrFiveIrreducible 25 below · cited by 2 · depth 6
• landmark Modularity lifting at p=3 from a prescribed residual level WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd 23,032 below · cited by 2 · depth 6
• landmark Modularity lifting at p∈{3,5} for p²∤ M₀ WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd 22,708 below · cited by 2 · depth 6
• Off the zero component iff the abscissa meets the node WeierstrassCurve.not_inZeroComponentAt_some_iff_of_criticalCentre 0 below · cited by 12 · depth 6
• Cofixed p-torsion forces p ∣ #W(𝔽_ℓ) WeierstrassCurve.prime_dvd_card_point_of_cofixed_addSubgroup_of_goodReduction 25 below · cited by 1 · depth 6
• Integrality of the branch slope at a shallow node-reducing point WeierstrassCurve.slope_mem_of_shallow 0 below · cited by 5 · depth 6
• Galois acts on a proper cofixed submodule of E[p] by the determinant WeierstrassCurve.smul_eq_det_smul_of_cofixed 1 below · cited by 1 · depth 6
• landmark The 3–5 switch for semistable integral models WeierstrassCurve.threeFiveSwitchCurve 124 below · cited by 2 · depth 6
• Discriminant valuation at a nodal critical centre WeierstrassCurve.valuation_discriminant_eq_of_criticalCentre 0 below · cited by 12 · depth 6
• Level of odd-order torsion reducing to a node WeierstrassCurve.valuation_pow_eq_of_torsion_odd_of_not_inZeroComponentAt 10 below · cited by 1 · depth 6
• Congruent p-torsion gives congruent Frobenius traces WeierstrassCurve.apOfModel_congr_of_torsionGaloisCongruent 47 below · cited by 1 · depth 7
• The n-torsion of an elliptic curve has n² points WeierstrassCurve.card_torsion_of_isAlgClosed_light 1 below · cited by 17 · depth 7
• Multiplicative primes q≠ p persist for the rescaled Vélu quotient WeierstrassCurve.dvd_discriminant_not_dvd_c4_integral_veluQuotient_rescale 29 below · cited by 1 · depth 7
• Hecke–Galois datum and patching datum at p=3, cube-free level WeierstrassCurve.exists_finite_extension_heckeGaloisRepDatum_patchingDatum_of_isResiduallyModular_of_level_of_inertia_moves_torsion_of_eq_three_capped_of_not_cube_dvd 22,990 below · cited by 1 · depth 7
• Hecke–Galois datum and patching datum over a finite extension WeierstrassCurve.exists_finite_extension_heckeGaloisRepDatum_patchingDatum_of_isResiduallyModular_of_level_of_not_sq_dvd_capped_of_not_cube_dvd 22,666 below · cited by 1 · depth 7
• Integral rescaling of the Vélu quotient by a Galois-stable subgroup WeierstrassCurve.exists_integral_veluQuotient_rescale_of_galois_stable 16 below · cited by 1 · depth 7
• Existence of the Weil pairing on n-torsion WeierstrassCurve.exists_pairing_torsionBy 42 below · cited by 4 · depth 7
• Kernel of reduction absorbs the inertia action WeierstrassCurve.exists_reductionKernel_absorbing_inertia 0 below · cited by 4 · depth 7
• Reduction map to the special fibre at a place of ℚ̄ WeierstrassCurve.exists_reduction_inZeroComponentAt 0 below · cited by 7 · depth 7
• Some q-torsion point escapes the zero component at q WeierstrassCurve.exists_torsionBy_residueChar_not_inZeroComponentAt 8 below · cited by 5 · depth 7
• Some ℓ-torsion escapes the zero component at a multiplicative prime WeierstrassCurve.exists_torsion_not_inZeroComponentAt_of_multiplicativeReduction 16 below · cited by 3 · depth 7
• Vélu isogeny with kernel ⟨ Q⟩ over ℚ̄ WeierstrassCurve.exists_veluPointHom_oddOrderSummingSet_algebraicClosure 55 below · cited by 1 · depth 7
• landmark Four possible c₄³/Δ for rational 15-isogenies WeierstrassCurve.fifteenIsogenyClassification 24 below · cited by 1 · depth 7
• Finiteness of the p-division field over ℚ WeierstrassCurve.galoisRepModuleEnd_factorsThroughFiniteLevel 1 below · cited by 25 · depth 7
• Good reduction at q gives ℓ-torsion unramified at q WeierstrassCurve.galoisRepUnramifiedAt_of_goodReduction 13 below · cited by 2 · depth 7
• Multiplicative reduction with ℓ ∣ v_q(Δ): ℓ-torsion unramified at q WeierstrassCurve.galoisRepUnramifiedAt_of_multiplicativeReduction 28 below · cited by 1 · depth 7
• Everywhere unramified action on W[n]/N is trivial WeierstrassCurve.galois_action_trivial_on_quotient_of_inertia_trivial 4 below · cited by 1 · depth 7
• Everywhere unramified torsion submodule is pointwise Galois-fixed WeierstrassCurve.galois_action_trivial_on_submodule_of_inertia_trivial 4 below · cited by 1 · depth 7
• Sum of two antipodal points at a node lies in E⁰ WeierstrassCurve.inZeroComponentAt_add_of_antipodal 2 below · cited by 6 · depth 7
• Zero-component transport along the Vélu coordinate map WeierstrassCurve.inZeroComponentAt_veluCoord_iff_of_multiplicative 28 below · cited by 1 · depth 7
• Level rad|Δ| modularity gives exact-conductor-level modularity WeierstrassCurve.isModularModelOfExactConductorLevel_of_level_conductorLevel 0 below · cited by 2 · depth 7
• landmark Descent to the conductor level when p² ∤ N WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd 11,044 below · cited by 2 · depth 7
• landmark From a patching datum to modularity at an explicit level WeierstrassCurve.isModularModelOfLevel_of_patchingDatum 64 below · cited by 2 · depth 7
• landmark Level lowering at an unramified prime exactly dividing the level WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf 12,481 below · cited by 3 · depth 7
• Antipodal plus shallow point at a node: level and branch WeierstrassCurve.level_add_of_antipodal_of_shallow 0 below · cited by 4 · depth 7
• Level of the sum of two same-branch shallow points WeierstrassCurve.level_add_of_branch_eq 0 below · cited by 4 · depth 7
• Level of a sum: opposite branches, distinct levels WeierstrassCurve.level_add_of_branch_ne_of_level_lt 0 below · cited by 4 · depth 7
• Translation by a point of E⁰ preserves level and branch at a node WeierstrassCurve.level_add_of_inZeroComponentAt 5 below · cited by 4 · depth 7
• Prime-to-q torsion has integral abscissa at a place over q WeierstrassCurve.mem_valuationSubring_of_nsmul_eq_zero_of_liesOverPrime 0 below · cited by 2 · depth 7
• Representability of the flat deformation problem for ρ̄_{E,p} WeierstrassCurve.nonempty_deformationRingData_flatCondition_of_isSemistableModel 182 below · cited by 2 · depth 7
• landmark Representability of the ordinary deformation problem for a semistable curve WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel 169 below · cited by 2 · depth 7
• Irreducibility of the packaged mod p representation of E WeierstrassCurve.residualGaloisRepOf_isIrreducible_iff 0 below · cited by 17 · depth 7
• Oddness of the mod-p representation of an elliptic curve WeierstrassCurve.residualGaloisRepOf_isOdd 46 below · cited by 18 · depth 7
• Unramifiedness of packaged mod-p representation as pointwise inertia-triviality WeierstrassCurve.residualGaloisRepOf_isUnramifiedAt_iff 0 below · cited by 3 · depth 7
• Ordinary/flat condition and Frobenius charpoly for odd p WeierstrassCurve.tateModuleRep_baseChangeAlong_condition_and_charpoly_flat_odd 182 below · cited by 2 · depth 7
• Residual representation of the Tate module is W[p] WeierstrassCurve.tateModuleRep_baseChangeAlong_residual_isEquiv 0 below · cited by 3 · depth 7
• landmark Auxiliary curve for the 3–5 switch WeierstrassCurve.threeFiveAuxiliaryCurveExists 77 below · cited by 1 · depth 7
• Levels of ℓ-torsion points at a node WeierstrassCurve.valuation_pow_eq_of_torsion_of_not_inZeroComponentAt 10 below · cited by 4 · depth 7
• Inertia preserves level and branch of shallow node-reducing points WeierstrassCurve.valuation_slope_smul_sub_slope_lt_one 1 below · cited by 1 · depth 7
• Node-reducing 2-torsion lies at half the node depth WeierstrassCurve.valuation_sq_eq_of_two_torsion_of_not_inZeroComponentAt 0 below · cited by 3 · depth 7
• Exact doubling identity at a critical centre WeierstrassCurve.addX_self_sub_mul_sq_of_criticalCentre 0 below · cited by 3 · depth 8
• Sum–difference abscissa identity at a critical centre WeierstrassCurve.addX_sub_mul_addX_neg_sub_mul_sq_of_criticalCentre 0 below · cited by 2 · depth 8
• Semistable integral models have c₄ ≠ 0 and c₆ ≠ 0 WeierstrassCurve.c4_ne_zero_and_c6_ne_zero_of_isSemistableModel 1 below · cited by 1 · depth 8
• Involutions act on p-torsion with determinant -1 WeierstrassCurve.det_galoisRep_eq_neg_one_of_mul_self_eq_one 45 below · cited by 2 · depth 8
• Determinant of Frobenius on p-torsion equals ℓ WeierstrassCurve.det_galoisRep_frobenius_eq_prime 43 below · cited by 14 · depth 8
• Division polynomials ψₙ² vanish at a singular point WeierstrassCurve.eval_psiSq_eq_zero_of_singular 0 below · cited by 1 · depth 8
• Finite flat Hopf model of pⁿ-torsion at odd good primes WeierstrassCurve.exists_finiteFlat_hopf_model_torsion_pow_of_isGoodPrimeFor 43 below · cited by 3 · depth 8
• landmark Specialisations with rootless 3-division polynomial in a weighted family WeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization 5 below · cited by 1 · depth 8
• Level-5 hauptmodul relation for mod-5 reducible curves WeierstrassCurve.exists_hauptmodulFive_of_not_modRepIsIrreducible 6 below · cited by 1 · depth 8
• Rational level-3 Hauptmodul value for mod-3 reducible curves WeierstrassCurve.exists_hauptmodulThree_of_not_modRepIsIrreducible 3 below · cited by 1 · depth 8
• Hecke–Galois datum at cube-free level, p=3 WeierstrassCurve.exists_heckeGaloisRepDatum_of_isResiduallyModular_of_inertia_moves_torsion_of_eq_three_capped_of_not_cube_dvd 6,886 below · cited by 1 · depth 8
• Hecke–Galois datum from a cube-free residual modularity witness WeierstrassCurve.exists_heckeGaloisRepDatum_of_isResiduallyModular_of_level_of_not_sq_dvd_capped_of_not_cube_dvd 6,072 below · cited by 1 · depth 8
• Integral models of short Weierstrass curves congruent mod n WeierstrassCurve.exists_isIntegralModelOf_of_dvd 0 below · cited by 1 · depth 8
• Deuring's criterion in division-polynomial form at odd good primes WeierstrassCurve.exists_prePsi_coeff_not_dvd_of_not_dvd_apOfModel 14 below · cited by 5 · depth 8
• Characteristic-zero Weierstrass curves admit the model y²=x³-27c₄x-54c₆ WeierstrassCurve.exists_variableChange_eq_shortModel 0 below · cited by 1 · depth 8
• Vélu quotient isogeny via places, odd order case WeierstrassCurve.exists_veluFunctionFieldHom_restrictAlong_placeOfPoint_eq 50 below · cited by 4 · depth 8
• Galois-stable Vélu quotient descends to ℚ WeierstrassCurve.exists_veluQuotient_descent_of_smul_mem_zmultiples 0 below · cited by 1 · depth 8
• Mod-p torsion of an elliptic curve has 𝔽ₚ-dimension 2 WeierstrassCurve.finrank_torsionBy_of_isAlgClosed 1 below · cited by 9 · depth 8
• Invariance of mod-n irreducibility under change of Weierstrass model WeierstrassCurve.galoisRepIsIrreducible_iff_of_variableChange_eq 4 below · cited by 1 · depth 8
• landmark Mod-3 irreducibility from Ψ₃ with no rational root WeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero 3 below · cited by 1 · depth 8
• Néron–Ogg–Shafarevich: good reduction gives E[n] unramified at q WeierstrassCurve.galoisRepUnramifiedAt_of_hasGoodReduction 12 below · cited by 2 · depth 8
• Frobenius trace on E[p] equals a_ℓ mod p WeierstrassCurve.galoisTrace_frobenius_eq_apOfModel 43 below · cited by 19 · depth 8
• Unit distance from the critical centre forces the zero component WeierstrassCurve.inZeroComponentAt_of_valuation_sub_eq_one 0 below · cited by 2 · depth 8
• Descent to the conductor level for a semistable model WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_factorization_eq 10,966 below · cited by 1 · depth 8
• Level lowering at a good prime exactly dividing N WeierstrassCurve.isModularModelOfLevel_div_of_isGoodPrimeFor_of_dvd_of_not_sq_dvd 3,973 below · cited by 1 · depth 8
• Level lowering at a prime q≡ 1mod p dividing M exactly WeierstrassCurve.isResiduallyModularOfLevel_div_of_cast_eq_one_of_isUnramifiedAt_sqf 12,473 below · cited by 1 · depth 8
• Residual modularity from a mod p Hecke eigenvector in J₀(N₀) WeierstrassCurve.isResiduallyModularOfLevel_of_heckeEigenvector_jZero 862 below · cited by 3 · depth 8
• Semistability transfers to a congruent integral model WeierstrassCurve.isSemistableModel_of_modEq 0 below · cited by 1 · depth 8
• Inertia image of the mod-3 representation has order prime to q WeierstrassCurve.natCard_inertia_map_coprime_of_isSemistableModel 151 below · cited by 2 · depth 8
• Inertia at 3 has image of order two under ρ WeierstrassCurve.natCard_inertia_map_modThreeRep_eq_two_of_inertia_fixed_torsion 160 below · cited by 1 · depth 8
• Chord trichotomy at a node of a Weierstrass cubic WeierstrassCurve.node_chord_trichotomy 0 below · cited by 1 · depth 8
• Flat condition for mod p torsion at odd good primes WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_flatCondition_of_ne_two 113 below · cited by 4 · depth 8
• Mod p representation of a semistable model is ordinary WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_ordinaryCondition 92 below · cited by 5 · depth 8
• Nonvanishing of Ψ^{sq}ₚ for a nodal cubic in characteristic p WeierstrassCurve.psiSq_ne_zero_of_nodal 2 below · cited by 2 · depth 8
• Inertia fixes ℓ-torsion off the zero component when ℓ∣ v_q(Δ) WeierstrassCurve.smul_eq_self_of_torsion_of_not_inZeroComponentAt_of_dvd 26 below · cited by 1 · depth 8
• Frobenius characteristic polynomial on the p-adic Tate module WeierstrassCurve.tateModuleRep_charpoly_frobenius 70 below · cited by 4 · depth 8
• Determinant of the Tate module representation is cyclotomic WeierstrassCurve.tateModuleRep_detIsCyclotomic 43 below · cited by 3 · depth 8
• Flatness at p of the Tate module representation from finite flat models WeierstrassCurve.tateModuleRep_isFlatAt 0 below · cited by 2 · depth 8
• Ordinarity of the Tate module at multiplicative and good ordinary p WeierstrassCurve.tateModuleRep_isOrdinaryAt 101 below · cited by 2 · depth 8
• Tate module unramified at good primes q ≠ p WeierstrassCurve.tateModuleRep_isUnramifiedAt_of_isGoodPrimeFor 13 below · cited by 3 · depth 8
• Integrality of prime-to-q torsion coordinates over ℚ̄ WeierstrassCurve.torsion_integral_of_not_dvd 3 below · cited by 6 · depth 8
• Vélu c₄ is a non-unit for formal-group p-torsion WeierstrassCurve.valuation_c4_add_veluTSum_lt_one_of_formal_kernel 9 below · cited by 1 · depth 8
• Levels of odd ℓ-torsion reducing to a node WeierstrassCurve.valuation_pow_eq_of_prime_torsion_of_not_inZeroComponentAt 10 below · cited by 3 · depth 8
• Valuation of the Vélu u-product over ⟨ Q⟩ at a multiplicative place WeierstrassCurve.valuation_prod_veluU_oddOrderSummingSet_of_multiplicative 19 below · cited by 2 · depth 8
• Vélu quotient has unit c₄ at a multiplicative prime WeierstrassCurve.valuation_veluQuotient_oddOrderSummingSet_c4_of_multiplicative 10 below · cited by 2 · depth 8
• j-invariant of a Vélu quotient lies in a subfield WeierstrassCurve.veluQuotient_j_mem_of_mem 1 below · cited by 3 · depth 8
• Vélu quotient by an odd cyclic kernel has nonzero discriminant WeierstrassCurve.veluQuotient_oddOrderSummingSet_discriminant_ne_zero 3 below · cited by 9 · depth 8
• Vélu discriminant identity for odd-order kernels WeierstrassCurve.veluQuotient_oddOrderSummingSet_discriminant_prod_veluU_pow 0 below · cited by 6 · depth 8
• No integral Weierstrass equation has discriminant ± 1 WeierstrassCurve.Delta_ne_one_and_Delta_ne_neg_one 0 below · cited by 1 · depth 9
• n-torsion of an elliptic curve over an algebraically closed field WeierstrassCurve.card_torsionBy_eq_sq_of_isAlgClosed 2 below · cited by 22 · depth 9
• Determinant of ρ̄_{E,p} at a Frobenius is ℓ WeierstrassCurve.det_galoisRepModuleEnd_frobenius_eq 45 below · cited by 4 · depth 9
• Reduction is injective on n-torsion, n invertible in the residue field WeierstrassCurve.eq_zero_of_smul_eq_zero_of_reducePoint_eq_zero 4 below · cited by 4 · depth 9
• Vélu quotient preserves roots of Ψ₂² for odd cyclic kernels WeierstrassCurve.eval_psi2Sq_veluQuotient_veluX_eq_zero_of_eval_psi2Sq_eq_zero 1 below · cited by 1 · depth 9
• Inertial filtration of E[p^m] at a good ordinary prime WeierstrassCurve.exists_atP_filtration_of_goodReduction_all_primes 48 below · cited by 1 · depth 9
• Inertial filtration of p^m-torsion at a multiplicative prime WeierstrassCurve.exists_atP_filtration_of_multiplicativeReduction_all_primes 84 below · cited by 1 · depth 9
• Deligne ordinary shape at p for mod p elliptic curve representations WeierstrassCurve.exists_deligneOrdinaryShape_residualGaloisRepOf_of_ordinary_or_multiplicative 69 below · cited by 2 · depth 9
• Interchange step of Ribet level lowering on J₀(Nq') WeierstrassCurve.exists_hasLowerLevelTorsion_jZero_of_twoNewEigenformCongruence_sqf_five 12,239 below · cited by 1 · depth 9
• Hecke–Galois datum at a level cube-free away from p WeierstrassCurve.exists_heckeGaloisRepDatum_of_isResiduallyModularOfLevel_capped 1,478 below · cited by 2 · depth 9
• Hecke maximal ideal from a curve-congruent eigenform WeierstrassCurve.exists_ideal_heckeAlgebra_of_isNormalizedEigenform 16 below · cited by 1 · depth 9
• Inertia eigenvector for a tame character, supersingular case WeierstrassCurve.exists_inertia_eigenvector_tameCharacter_residualGaloisRepOf_of_supersingular 13 below · cited by 2 · depth 9
• Variable change induces Galois-equivariant isomorphism on n-torsion WeierstrassCurve.exists_linearEquiv_torsionBy_of_variableChange_eq 2 below · cited by 3 · depth 9
• Level raising at q' for a congruent eigenform WeierstrassCurve.exists_newAt_congruentEigenform_of_levelRaisingCongruence 829 below · cited by 1 · depth 9
• Auxiliary primes with p ∣ a_{q'} and p ∣ q'+1 WeierstrassCurve.exists_prime_isGoodPrimeFor_dvd_apOfModel_dvd_add_one 116 below · cited by 1 · depth 9
• Specialisation homomorphism for a family over ℚ[X] WeierstrassCurve.exists_specializationHom 9 below · cited by 1 · depth 9
• A p-torsion point with A-integral x-coordinate when p ∤ aₚ WeierstrassCurve.exists_torsionBy_integral_of_not_dvd_apOfModel_all_primes 16 below · cited by 1 · depth 9
• Frobenius-equivariant isomorphism of p-torsion under reduction at ℓ WeierstrassCurve.exists_torsionBy_linearEquiv_residueField_of_isFrobeniusAt 13 below · cited by 2 · depth 9
• Residual absolute irreducibility and oddness from a mod-λ congruence WeierstrassCurve.forall_galoisRepAdic_residual_isAbsolutelyIrreducible_and_isOdd_of_modRepIsIrreducible_of_congruent 134 below · cited by 2 · depth 9
• Inertia at q ≠ p acts unipotently on p-torsion WeierstrassCurve.galoisRep_inertia_unipotent_of_isSemistableModel 34 below · cited by 4 · depth 9
• Frobenius on p-torsion: trace a_ℓ, determinant ℓ WeierstrassCurve.galoisTrace_frobenius_eq_apOfModel_of_card_torsionBy 30 below · cited by 2 · depth 9
• Frobenius trace on E[p] equals a_ℓ mod p WeierstrassCurve.galoisTrace_frobenius_eq_apOfModel_of_isIntegralModelOf 46 below · cited by 3 · depth 9
• Good reduction persists under finite base change WeierstrassCurve.hasGoodReduction_baseChange_of_valuation_lt_one 0 below · cited by 1 · depth 9
• Modularity of an integral model ascends divisible levels WeierstrassCurve.isModularModelOfLevel_of_dvd 5 below · cited by 2 · depth 9
• Level lowering at p, good supersingular case WeierstrassCurve.isResiduallyModularOfLevel_div_of_isGoodPrimeFor_of_dvd_apOfModel 5,995 below · cited by 2 · depth 9
• Level-p residual modularity from any level, p=3 WeierstrassCurve.isResiduallyModularOfLevel_mul_ordCompl_of_inertia_moves_torsion_of_two_dvd_of_eq_three 5,844 below · cited by 2 · depth 9
• Residual modularity of level M gives level N when M ∣ N WeierstrassCurve.isResiduallyModularOfLevel_of_dvd 5 below · cited by 8 · depth 9
• Residual modularity from a proper exit ideal WeierstrassCurve.isResiduallyModularOfLevel_of_exitIdeal_ne_top 641 below · cited by 2 · depth 9
• The j-invariant lies in any subfield containing the aᵢ WeierstrassCurve.j_mem_of_a_mem 0 below · cited by 1 · depth 9
• Vélu's quotient commutes with base change along a ring homomorphism WeierstrassCurve.map_veluQuotient_image 0 below · cited by 8 · depth 9
• Boston–Lenstra–Ribet decomposition of the Hecke 𝔪-torsion WeierstrassCurve.modRep_blrDecomposition_heckeTorsion_of_frobeniusQuadratic 124 below · cited by 2 · depth 9
• Elementary bound |aₚ|≤ p for an integral Weierstrass model WeierstrassCurve.natAbs_apOfModel_le 0 below · cited by 1 · depth 9
• Mod p Galois representation of an elliptic curve has cyclotomic determinant WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_detIsCyclotomic 44 below · cited by 5 · depth 9
• Flatness at odd p of the mod p representation of a good model WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_isFlatAt_of_ne_two 46 below · cited by 1 · depth 9
• Ordinarity at p of the mod p representation of a semistable model WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_isOrdinaryAt 67 below · cited by 3 · depth 9
• Mod p representation unramified at good primes q ≠ p WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_isUnramifiedAt 20 below · cited by 2 · depth 9
• Primes dividing M divide Δ, with M squarefree there WeierstrassCurve.prime_dvd_discr_and_not_sq_dvd_of_localType 5 below · cited by 1 · depth 9
• Reduction of points is additive under good reduction WeierstrassCurve.reducePoint_add 6 below · cited by 4 · depth 9
• Reduction of an integral affine point has residue coordinates WeierstrassCurve.reducePoint_some 0 below · cited by 7 · depth 9
• Affine point reduces to O iff x is non-integral WeierstrassCurve.reducePoint_some_eq_zero_iff 2 below · cited by 5 · depth 9
• Good reduction at q ≠ p: ρ̄_{E,p} is unramified at q WeierstrassCurve.residualGaloisRepOf_isUnramifiedAt_of_isGoodPrimeFor 19 below · cited by 5 · depth 9
• Separability of Ψ₃ for a nonsingular Weierstrass curve WeierstrassCurve.separable_Psi3 0 below · cited by 1 · depth 9
• Local conditions at p and Frobenius charpolys for Tate modules WeierstrassCurve.tateModuleRep_baseChangeAlong_condition_and_charpoly_flat_odd_finiteAt 182 below · cited by 1 · depth 9
• Determinant of Frobenius at ℓ ≠ p on the Tate module WeierstrassCurve.tateModuleRep_det_frobenius 45 below · cited by 1 · depth 9
• Unipotent inertia at a prime of multiplicative reduction WeierstrassCurve.tateModuleRep_isUnipotentOnInertiaAt_of_multiplicativeReduction 17 below · cited by 1 · depth 9
• Negation flips the branch slope at a shallow node reduction WeierstrassCurve.valuation_slope_sub_slope_neg_of_shallow 0 below · cited by 1 · depth 9
• Vélu quotient of a nodal cubic by an odd-order point WeierstrassCurve.veluQuotient_oddOrderSummingSet_c4_c6_discriminant_of_nodal 1 below · cited by 1 · depth 9
• Injectivity of Vélu's abscissa map on ψ₂²-roots WeierstrassCurve.veluX_oddOrderSummingSet_injOn_psi2Sq_roots 0 below · cited by 1 · depth 9
• Vélu's formulas land on the quotient curve (odd order) WeierstrassCurve.velu_map_equation_of_oddOrderSummingSet 0 below · cited by 2 · depth 9
• Nonvanishing of Ψ₂² for an elliptic curve in any characteristic WeierstrassCurve.Psi2Sq_ne_zero_of_isElliptic 0 below · cited by 20 · depth 10
• a_q of an integral Weierstrass model is never ±(q+1) WeierstrassCurve.apOfModel_ne_succ_and_ne_neg_succ 0 below · cited by 1 · depth 10
• Reduction bounds prime-to-p torsion of E(ℚ) WeierstrassCurve.card_dvd_card_reduction_of_nsmul_eq_zero 9 below · cited by 1 · depth 10
• Trivial bound #W(F)≤ 2#F+1 for Weierstrass curves WeierstrassCurve.card_le_two_mul_add_one 0 below · cited by 1 · depth 10
• Positivity of the point count of a Weierstrass curve WeierstrassCurve.card_pos 0 below · cited by 1 · depth 10
• Galois-equivariant isomorphism of points under a variable change WeierstrassCurve.exists_addEquiv_point_baseChange_variableChange_smul_algEquiv 1 below · cited by 2 · depth 10
• Variable change over F gives Galois-equivariant isomorphism of K-points WeierstrassCurve.exists_addEquiv_point_of_variableChange_eq 0 below · cited by 2 · depth 10
• Variable change induces an isomorphism of point groups WeierstrassCurve.exists_addEquiv_point_variableChange 0 below · cited by 19 · depth 10
• Capped admissible auxiliary level dividing a given modulus WeierstrassCurve.exists_dvd_roadAdmissible_level_capped 0 below · cited by 1 · depth 10
• Irreducible mod-p torsion gives a non-Eisenstein good prime WeierstrassCurve.exists_isGoodPrimeFor_not_dvd_apOfModel_sub_of_galoisRepIsIrreducible 112 below · cited by 3 · depth 10
• Residual Hecke eigensystem from residual modularity WeierstrassCurve.exists_residual_eigensystem_of_isResiduallyModularOfLevel 56 below · cited by 4 · depth 10
• Très ramifié p-torsion is not unit-Kummer at p ≥ 5 WeierstrassCurve.exists_torsion_forall_unitKummer_exists_inertia_smul_ne_of_not_dvd_padicValInt_of_five_le 53 below · cited by 3 · depth 10
• Inertia at a très ramifié multiplicative prime 3 moves the 3-torsion WeierstrassCurve.exists_torsion_forall_unitKummer_exists_inertia_smul_ne_of_not_dvd_padicValInt_three 51 below · cited by 3 · depth 10
• Nonzero ℓ-torsion in the zero component at a multiplicative prime WeierstrassCurve.exists_torsion_ne_zero_inZeroComponentAt_of_multiplicativeReduction 23 below · cited by 1 · depth 10
• Vélu function-field embedding with point map of kernel ⟨ Q⟩ WeierstrassCurve.exists_veluFunctionFieldHom_pointMapOfPushforward_ker_eq_zmultiples 51 below · cited by 5 · depth 10
• E(K)[p] has dimension two over mathbf Fₚ WeierstrassCurve.finrank_zmod_torsionBy_point_eq_two 1 below · cited by 3 · depth 10
• Inertia acts trivially modulo a proper subspace of E[p] WeierstrassCurve.galoisRep_ordinaryLineAt 22 below · cited by 2 · depth 10
• Complex conjugation on E[p] has trace 0, determinant -1 WeierstrassCurve.galoisTrace_complexConjugation_eq_zero_and_det_eq_neg_one 47 below · cited by 3 · depth 10
• Good reduction: all ℚ̄-points lie in the zero component WeierstrassCurve.inZeroComponentAt_of_isGoodPrimeFor 5 below · cited by 1 · depth 10
• q-torsion of the zero component at a multiplicative prime WeierstrassCurve.inZeroComponentAt_torsionBy_residueChar 3 below · cited by 1 · depth 10
• Coprimality of the division polynomials Φₙ and Ψₙ² WeierstrassCurve.isCoprime_Phi_PsiSq 0 below · cited by 28 · depth 10
• Level lowering at a prime of good reduction WeierstrassCurve.isResiduallyModularOfLevel_div_of_isGoodPrimeFor 5,994 below · cited by 5 · depth 10
• Level descent at p=3 from a newform of level divisible by 9 WeierstrassCurve.isResiduallyModularOfLevel_div_of_isNewform_of_inertia_moves_torsion_of_two_dvd_of_eq_three 5,842 below · cited by 1 · depth 10
• Level lowering at the residue characteristic p WeierstrassCurve.isResiduallyModularOfLevel_div_of_isPeuRamifieeAt 5,993 below · cited by 3 · depth 10
• Level lowering at p for primes p ≥ 5 WeierstrassCurve.isResiduallyModularOfLevel_div_of_isPeuRamifieeAt_of_five_le 5,994 below · cited by 1 · depth 10
• Residual modularity via maximal ideals of the Hecke algebra WeierstrassCurve.isResiduallyModularOfLevel_iff_exists_ideal_heckeAlgebra 55 below · cited by 2 · depth 10
• Minimal squarefree level for residual modularity at p=3 WeierstrassCurve.isResiduallyModularOfLevel_minimalLevel_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd 19,036 below · cited by 1 · depth 10
• Lowering a bounded residual-modularity witness to the minimal level WeierstrassCurve.isResiduallyModularOfLevel_minimalLevel_of_level_of_not_sq_dvd_of_not_cube_dvd 18,475 below · cited by 1 · depth 10
• Good reduction at ℓ: discriminant nonzero in the residue field WeierstrassCurve.map_residueField_discr_ne_zero_of_isGoodPrimeFor 2 below · cited by 3 · depth 10
• Degree of Φₙ - c Ψₙ² is n² WeierstrassCurve.natDegree_Phi_sub_C_mul_PsiSq 0 below · cited by 3 · depth 10
• Good reduction: integral solutions reduce to nonsingular points WeierstrassCurve.nonsingular_residue_of_isGoodPrimeFor 3 below · cited by 2 · depth 10
• Inertia at q ≠ p acts unipotently on E[p] WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_isUnipotentOnInertiaAt 35 below · cited by 5 · depth 10
• Très ramifié curves: mod p representation not flat at p WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_not_isFlatAt_of_not_isPeuRamifieeAt 128 below · cited by 2 · depth 10
• Strict ordinary condition at multiplicative p for semistable curves WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_strictOrdinaryCondition_of_dvd_discriminant 107 below · cited by 2 · depth 10
• Additivity of reduction for points with integral x-coordinate WeierstrassCurve.reducePoint_some_add_some_of_le_one 3 below · cited by 1 · depth 10
• Reduction is unchanged by adding a point of non-integral x WeierstrassCurve.reducePoint_some_add_some_of_not_le_one 3 below · cited by 1 · depth 10
• Absolute irreducibility on index-two subgroups of ρ̄_{W,p} WeierstrassCurve.residualGaloisRepOf_restrict_index_two 105 below · cited by 4 · depth 10
• Inertia at multiplicative reduction acts unipotently on torsion WeierstrassCurve.smul_smul_sub_eq_of_mem_inertiaSubgroupIn_of_multiplicativeReduction 15 below · cited by 1 · depth 10
• The n-torsion points of an elliptic curve sum to O WeierstrassCurve.sum_eq_zero_of_forall_mem_iff_smul_eq_zero 1 below · cited by 1 · depth 10
• Levelwise unipotent inertia gives unipotent inertia on the Tate module WeierstrassCurve.tateModuleRep_isUnipotentOnInertiaAt 0 below · cited by 1 · depth 10
• Integral x forces integral y on an integral Weierstrass model WeierstrassCurve.valuation_le_one_of_equation 0 below · cited by 4 · depth 10
• Valuations of p-torsion under supersingular coefficient condition WeierstrassCurve.valuation_torsion_of_coeff_prePsi_dvd 8 below · cited by 2 · depth 10
• Mod 3 image of order at most two WeierstrassCurve.card_range_galoisRep_three_le_two 45 below · cited by 1 · depth 11
• Tate dictionary for W[3] at a multiplicative prime 3 WeierstrassCurve.exists_addEquiv_torsionBy_localGaloisToGlobal_smul_eq_of_dvd_discr_of_eq_three 25 below · cited by 2 · depth 11
• Tate dictionary for W[p] at a multiplicative prime p≥ 5 WeierstrassCurve.exists_addEquiv_torsionBy_localGaloisToGlobal_smul_eq_of_dvd_discr_of_five_le 27 below · cited by 2 · depth 11
• Finite flat Hopf model of E[p] from flatness at p WeierstrassCurve.exists_finiteFlat_model_torsionBy_of_isFlatAt_residualGaloisRepOf 0 below · cited by 1 · depth 11
• Weight 2 or p+1 at level N' traded for weight 2 at level N'p WeierstrassCurve.exists_ideal_heckeAlgebra_mul_two_of_ideal_heckeAlgebra_two_or_succ 661 below · cited by 1 · depth 11
• Stripping the p-power part of a newform's level WeierstrassCurve.exists_ideal_heckeAlgebra_ordCompl_of_isNewform_sq_dvd 85 below · cited by 1 · depth 11
• Weight 2 or p+1 eigensystem placement at p=3 WeierstrassCurve.exists_ideal_heckeAlgebra_two_or_succ_of_ideal_heckeAlgebra_pow_mul_apOfModel_of_inertia_moves_torsion_of_katz_of_eq_three 5,557 below · cited by 1 · depth 11
• Weight at most p+1 for a curve's mod p eigensystem WeierstrassCurve.exists_ideal_heckeAlgebra_weight_le_succ_pow_mul_apOfModel_of_exists_prime_dvd_mod_three_eq_two 1,529 below · cited by 1 · depth 11
• Eigenform realising a Hecke maximal ideal congruent to a_ℓ(W) WeierstrassCurve.exists_isNormalizedEigenform_and_qCoeff_sub_apOfModel_mem_of_ideal_heckeAlgebra 29 below · cited by 3 · depth 11
• Descent to a minimal squarefree level, given one-prime steps WeierstrassCurve.exists_minimalLevel_of_steps_of_level_of_not_sq_dvd_of_not_cube_dvd_of_squarefree_step 0 below · cited by 2 · depth 11
• Stable line and quadratic character at a multiplicative prime WeierstrassCurve.exists_stableLine_character_of_not_isGoodPrimeFor 77 below · cited by 1 · depth 11
• Nonzero q-torsion in the zero component at residue characteristic q WeierstrassCurve.exists_torsionBy_residueChar_ne_zero_inZeroComponentAt 3 below · cited by 1 · depth 11
• Poles of order 2s and 3s on an integral Weierstrass model WeierstrassCurve.exists_valuation_eq_exp_of_not_le_one 0 below · cited by 1 · depth 11
• Inertia at a good supersingular prime on E[p] WeierstrassCurve.galoisRep_supersingularShapeAt 9 below · cited by 1 · depth 11
• Residual modularity at level M/p from an eigenform of divisor level WeierstrassCurve.isResiduallyModularOfLevel_div_of_isNormalizedEigenform_dvd_div 5 below · cited by 1 · depth 11
• Level lowering at q when q² ∣ M, q³ ∤ M WeierstrassCurve.isResiduallyModularOfLevel_div_of_prime_sq_dvd_of_not_cube_dvd 11,083 below · cited by 2 · depth 11
• Integral x-coordinate forces integral y-coordinate WeierstrassCurve.mem_valuationSubring_of_equation 0 below · cited by 1 · depth 11
• Cyclic subgroups of order n number ψ(n) WeierstrassCurve.natCard_addSubgroup_isAddCyclic_card_eq_dedekindPsi_of_isAlgClosed 8 below · cited by 10 · depth 11
• Variable changes induce isomorphic Weierstrass function fields WeierstrassCurve.nonempty_functionField_algEquiv_of_variableChange 2 below · cited by 5 · depth 11
• Flatness at p of ρ̄_{W,p}⊗ k for semistable peu ramifiée W WeierstrassCurve.ofResidualGaloisRep_residualGaloisRepOf_isFlatAt_of_semistable_of_isPeuRamifieeAt 281 below · cited by 1 · depth 11
• Residual modularity of level M forces unramifiedness outside Mp WeierstrassCurve.residualGaloisRepOf_isUnramifiedAt_of_isResiduallyModularOfLevel 1,422 below · cited by 2 · depth 11
• Inertia displacements of p-torsion lie on the cyclotomic line WeierstrassCurve.smul_inertia_displacement_eq_nsmul_of_torsion_of_dvd_discr_of_five_le 31 below · cited by 1 · depth 11
• Inertia acts on 3-torsion displacements through ω at 3 WeierstrassCurve.smul_inertia_displacement_eq_nsmul_of_torsion_of_dvd_discr_three 29 below · cited by 1 · depth 11
• Equal j of Vélu quotients forces equal cyclic subgroups WeierstrassCurve.zmultiples_eq_of_veluQuotient_j_eq_of_forall_pointEnd_eq_zsmul 70 below · cited by 1 · depth 11
• Trivial action on E[p] fixes the p-th roots of unity WeierstrassCurve.apply_eq_self_of_galoisRep_eq_one_of_pow_eq_one 44 below · cited by 1 · depth 12
• #E[2] = 1 + #{Ψ₂² = 0} in characteristic ≠ 2 WeierstrassCurve.card_torsionBy_two_eq_card_option_Psi2Sq_roots 2 below · cited by 1 · depth 12
• Equal j of Vélu 2-quotients forces equal abscissa WeierstrassCurve.eq_of_veluQuotient2_j_eq_of_not_isIntegral_j 8 below · cited by 1 · depth 12
• Tate curve p-torsion up to a quadratic sign twist WeierstrassCurve.exists_addEquiv_torsion_tateCurve_signTwist_of_tateParameter 12 below · cited by 3 · depth 12
• Galois-equivariant injection of n-torsion into p-adic points WeierstrassCurve.exists_addMonoidHom_torsionBy_injective_map_localGaloisToGlobal_smul 0 below · cited by 2 · depth 12
• Finite flat prolongation of E[p] over a DVR with unit discriminant WeierstrassCurve.exists_finiteFlat_prolongation_torsion_of_integralModel_isUnit_discr 224 below · cited by 3 · depth 12
• Finite flat prolongation of E[p] at a multiplicative peu-ramifiée prime WeierstrassCurve.exists_finiteFlat_prolongation_torsion_of_multiplicativeReduction_of_peuRamifiee 175 below · cited by 3 · depth 12
• Finite flat prolongation of E[p] when semistable and peu ramifiée at p WeierstrassCurve.exists_finiteFlat_prolongation_torsion_of_semistable_of_isPeuRamifieeAt 278 below · cited by 3 · depth 12
• Transfer of a mod p Hecke eigensystem from level N' to N'p WeierstrassCurve.exists_ideal_heckeAlgebra_mul_two_of_ideal_heckeAlgebra_two 0 below · cited by 1 · depth 12
• Weight at most p+1 for a twisted mod-p Hecke eigensystem WeierstrassCurve.exists_ideal_heckeAlgebra_weight_le_succ_pow_mul_of_pow_mul_of_exists_prime_dvd_mod_three_eq_two 1,528 below · cited by 1 · depth 12
• Base change of a Vélu quotient and its j-invariant WeierstrassCurve.exists_isElliptic_map_veluQuotient_j 1 below · cited by 2 · depth 12
• Lowering the q-exponent from two to one in the level WeierstrassCurve.exists_isNormalizedEigenform_level_div_of_isNewform_of_factorization_eq_two 11,080 below · cited by 1 · depth 12
• Good-reduction Weierstrass model over K[[t]] with j = a + t WeierstrassCurve.exists_isUnit_discriminant_and_c4_cube_eq_mul_C_add_X_powerSeries 0 below · cited by 1 · depth 12
• Good-reduction Weierstrass model over K[[t]] with j=t³ WeierstrassCurve.exists_isUnit_discriminant_and_c4_cube_eq_mul_X_cube_powerSeries 0 below · cited by 2 · depth 12
• Good-reduction Weierstrass model over K[[t]] with j-1728=t² WeierstrassCurve.exists_isUnit_discriminant_and_c6_sq_eq_mul_X_sq_powerSeries 0 below · cited by 2 · depth 12
• Unramified sign character on p-torsion modulo the zero component WeierstrassCurve.exists_sign_smul_sub_inZeroComponentAt_of_not_isGoodPrimeFor 23 below · cited by 1 · depth 12
• Tate parameter at a prime of multiplicative reduction WeierstrassCurve.exists_tateParameter_of_prime_dvd_discr 0 below · cited by 3 · depth 12
• Finiteness of n-torsion when n ≠ 0 in k WeierstrassCurve.finite_torsionBy_of_natCast_ne_zero 1 below · cited by 2 · depth 12
• Torsion coordinates of a good-reduction model are Laurent WeierstrassCurve.hasRamBound_one_of_nsmul_eq_zero_of_isUnit_discriminant_powerSeries 2 below · cited by 5 · depth 12
• Supersingular j-invariants satisfy j^{q^2}=j WeierstrassCurve.j_pow_q_sq_eq_j_of_forall_q_zsmul_eq_zero 5 below · cited by 7 · depth 12
• Stabiliser of y²=x³+a₆ under admissible changes of variables WeierstrassCurve.mem_stabilizer_variableChange_iff_of_isShortNF_of_a4_eq_zero 0 below · cited by 8 · depth 12
• Stabiliser of y²=x³+a₄x in the change-of-variables group WeierstrassCurve.mem_stabilizer_variableChange_iff_of_isShortNF_of_a6_eq_zero 0 below · cited by 8 · depth 12
• Cyclic N-subgroups of y²=x³+B stable under [ω] WeierstrassCurve.natCard_isAddCyclic_addSubgroup_card_eq_fixed_vcInvFun_eq_nuThree 14 below · cited by 1 · depth 12
• Cyclic N-subgroups of y²=x³+Ax stable under [i] WeierstrassCurve.natCard_isAddCyclic_addSubgroup_card_eq_fixed_vcInvFun_eq_nuTwo 12 below · cited by 1 · depth 12
• E[n](K)≅(ℤ/n)² over an algebraically closed field WeierstrassCurve.nonempty_torsionBy_addEquiv_zmod_prod_of_isAlgClosed 2 below · cited by 71 · depth 12
• Scaling by a cube root of unity fixes y² = x³ + B WeierstrassCurve.variableChange_mk_smul_eq_self_of_pow_three_eq_one 0 below · cited by 6 · depth 12
• Scaling by u with u²=-1 fixes y²=x³+Ax WeierstrassCurve.variableChange_mk_smul_eq_self_of_sq_eq_neg_one 0 below · cited by 6 · depth 12
• Nonvanishing discriminant of the order-two Vélu quotient WeierstrassCurve.veluQuotient2_Delta_ne_zero 4 below · cited by 6 · depth 12
• Odd cyclic subgroups determined by the Vélu quotient's j WeierstrassCurve.zmultiples_eq_of_veluQuotient_j_eq_of_transcendental 185 below · cited by 3 · depth 12
• x-coordinates of 2-torsion points are roots of Ψ₂² WeierstrassCurve.eval_Psi2Sq_of_two_nsmul_eq_zero 0 below · cited by 2 · depth 13
• Sign-twisted p-torsion isomorphism onto a Tate curve WeierstrassCurve.exists_addEquiv_torsion_tateCurve_signTwist_of_variableChange_galois_signBehavior 2 below · cited by 1 · depth 13
• [ω] acts non-scalarly on p-torsion of y²=x³+B WeierstrassCurve.exists_addOrderOf_eq_and_vcInvFun_ne_nsmul_of_pow_three_eq_one 8 below · cited by 1 · depth 13
• Non-scalar action of [i] on p-torsion of y²=x³+Ax WeierstrassCurve.exists_addOrderOf_eq_and_vcInvFun_ne_nsmul_of_sq_eq_neg_one 8 below · cited by 1 · depth 13
• Descent of a finite flat prolongation of E[p] to a DVR inside ℚ WeierstrassCurve.exists_finiteFlat_prolongation_torsion_of_padicInt_along 134 below · cited by 1 · depth 13
• Finite flat prolongation of E[p] from a Tate parameter WeierstrassCurve.exists_finiteFlat_prolongation_torsion_of_tateParameter_of_peuRamifiee 173 below · cited by 1 · depth 13
• Finite flat ℤₚ-prolongation of p-torsion in good reduction WeierstrassCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_isUnit_discr 175 below · cited by 1 · depth 13
• Mod-3 weight window: weight at most four up to twist WeierstrassCurve.exists_ideal_heckeAlgebra_three_weight_le_four_pow_mul_apOfModel_of_exists_prime_dvd_mod_three_eq_two 884 below · cited by 1 · depth 13
• Descent of an elliptic curve with a function-field endomorphism to a countable subfield WeierstrassCurve.exists_intermediateField_countable_map_eq_and_finrankAlong_eq 2 below · cited by 1 · depth 13
• Level lowering at q with q² ∥ L, q≡-1, supercuspidal case WeierstrassCurve.exists_isNormalizedEigenform_level_div_of_forall_linearMap_psCarrier_eq_zero_of_cast_eq_neg_one 10,757 below · cited by 1 · depth 13
• Level reduction to L/q for a twisted newform with q² ‖ L WeierstrassCurve.exists_isNormalizedEigenform_level_div_of_mem_fixedSubmodule_fnTwist_of_isNewform_of_factorization_eq_two 798 below · cited by 1 · depth 13
• Cuspidal representative of an irreducible mod p eigensystem WeierstrassCurve.exists_mem_modPCusp_isModPEigen_of_mem_modPMod_of_modRepIsIrreducible 77 below · cited by 1 · depth 13
• Mod p eigenform from a maximal Hecke ideal WeierstrassCurve.exists_mem_modPCusp_isModPEigen_pow_mul_apOfModel_of_ideal_heckeAlgebra 20 below · cited by 2 · depth 13
• Galois sign behaviour of the Tate curve variable change WeierstrassCurve.exists_variableChange_tateCurve_algebraicClosure_galois_signBehavior 8 below · cited by 1 · depth 13
• The order-two Vélu quotient of an elliptic curve is elliptic WeierstrassCurve.isElliptic_veluQuotient2_of_isElliptic 5 below · cited by 15 · depth 13
• Nonvanishing of `velu2QuadDisc` at a 2-torsion point WeierstrassCurve.velu2QuadDisc_ne_zero_of_two_torsion 1 below · cited by 1 · depth 13
• Nonvanishing of gₓ at a 2-torsion point WeierstrassCurve.veluGx_ne_zero_of_two_torsion 1 below · cited by 3 · depth 13
• Discriminant of the order-two Vélu quotient WeierstrassCurve.veluQuotient2_Delta_eq 0 below · cited by 3 · depth 13
• j-invariant of the order-two Vélu quotient WeierstrassCurve.veluQuotient2_j 7 below · cited by 2 · depth 13
• Equal j of Vélu quotients forces equal cyclic subgroups WeierstrassCurve.zmultiples_eq_of_veluQuotient_j_eq_of_forall_isogenyEndDatum_exists_int 70 below · cited by 1 · depth 13
• Δ = gₓ(Q)² d(x₀) at a 2-torsion point WeierstrassCurve.Delta_eq_veluGx_sq_mul_velu2QuadDisc 0 below · cited by 2 · depth 14
• Integral mod-p parabolic eigenclass at level L/q WeierstrassCurve.exists_H1_parabolic_not_dvd_diamondRaw_heckeT_congr_apOfModel_level_div_of_forall_linearMap_psCarrier_eq_zero 10,743 below · cited by 1 · depth 14
• Sign-twisted point isomorphism W(ℚ̄ₚ)≅ E_{q_T}(ℚ̄ₚ) WeierstrassCurve.exists_addEquiv_point_tateCurve_signTwist_of_variableChange_galois_signBehavior 1 below · cited by 1 · depth 14
• Finite flat ℤₚ-Hopf order of the p-torsion Hopf algebra WeierstrassCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_isUnit_discr_of_hopfAlgebra_padic 122 below · cited by 1 · depth 14
• Finite flat ℤₚ-prolongation of E[p] at peu-ramifiée Tate primes WeierstrassCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_tateParameter_of_peuRamifiee 52 below · cited by 1 · depth 14
• Descent of a finite flat prolongation of E[p] to ℤ₍ₚ₎ WeierstrassCurve.exists_finiteFlat_prolongation_torsion_ratLocalizedAt_of_padicInt 124 below · cited by 1 · depth 14
• A finite cocommutative ℚₚ-Hopf algebra for V[p] WeierstrassCurve.exists_hopfAlgebra_padic_torsionBy_withConv_equiv_algClosure 82 below · cited by 1 · depth 14
• Étale Hopf algebra for E[p] with global and p-adic point identifications WeierstrassCurve.exists_hopfAlgebra_rat_torsionBy_withConv_equiv_along 104 below · cited by 1 · depth 14
• Cuspidal representative of a curve's mod p eigensystem WeierstrassCurve.exists_mem_modPCusp_isModPEigen_of_mem_modPMod_of_modRepIsIrreducible_of_ne_two 76 below · cited by 2 · depth 14
• Mod-p representation of a semistable model: irreducibility and Frobenius traces WeierstrassCurve.exists_residualGaloisRep_isAbsolutelyIrreducible_trace_eq_apOfModel 147 below · cited by 2 · depth 14
• Galois sign behaviour of the Tate-curve variable change WeierstrassCurve.exists_variableChange_tateCurve_galois_signBehavior_of_stabilizer 5 below · cited by 1 · depth 14
• Vélu's 2-isogeny: function-field embedding matching places WeierstrassCurve.exists_velu2FunctionFieldHom_restrictAlong_placeOfPoint_veluPointMap2 11 below · cited by 2 · depth 14
• Mod-p eigenforms with elliptic curve eigenvalues are cuspidal WeierstrassCurve.mem_modPCusp_of_mem_modPMod_of_isModPEigen_pow_mul_apOfModel_of_modRepIsIrreducible 76 below · cited by 1 · depth 14
• Fibres of an orbit map on cyclic N-subgroups divide the j-width WeierstrassCurve.natCard_fibre_dvd_jWidth_of_variableChange_orbitMap 8 below · cited by 5 · depth 14
• Stabiliser of a Weierstrass model with c₄,c₆≠ 0 WeierstrassCurve.variableChange_smul_eq_self_iff_of_c4_ne_zero_of_c6_ne_zero 0 below · cited by 3 · depth 14
• Variable changes fixing a Tate normal form curve with c₄,c₆≠ 0 WeierstrassCurve.variableChange_smul_eq_self_iff_of_tateNormalForm 0 below · cited by 1 · depth 14
• c₄ of the order-two Vélu quotient WeierstrassCurve.veluQuotient2_cFour 0 below · cited by 1 · depth 14
• Reduction is bijective on N-torsion over a Henselian valuation subring WeierstrassCurve.bijective_reduceHom_restrict_torsion 4 below · cited by 3 · depth 15
• Bound #E[p] ≤ p² over an arbitrary field WeierstrassCurve.card_p_torsion_le_of_natCast_ne_zero 3 below · cited by 1 · depth 15
• Order of the automorphism group of an elliptic curve WeierstrassCurve.card_stabilizer_variableChange_eq_two_mul_jWidth 5 below · cited by 7 · depth 15
• A non-zero parabolic diamond-fixed eigenclass with curve eigenvalues WeierstrassCurve.exists_H1_bot_ne_zero_parabolic_of_diamondRaw_eq_of_heckeT_eq_smul 76 below · cited by 1 · depth 15
• Integral parabolic mod-p eigenclass attached to W at level N WeierstrassCurve.exists_H1_parabolic_not_dvd_heckeT_congr_apOfModel_of_isEigensystemH1_one 96 below · cited by 1 · depth 15
• Vélu's order-2 quotient map is additive WeierstrassCurve.exists_addMonoidHom_coe_eq_veluPointMap2 4 below · cited by 16 · depth 15
• Automorphisms of y² = x³ - x in characteristic 3 WeierstrassCurve.exists_addMonoidHom_i_tau_vcInvFun_of_char_three 1 below · cited by 4 · depth 15
• Mod p eigensystem of W on H¹ with Steinberg-quotient coefficients WeierstrassCurve.exists_charP_rep_steinberg_quotient_isEigensystemH1_apOfModel_of_isSemistableModel_of_qCoeff_congr 10,659 below · cited by 1 · depth 15
• Sign twist preserves finite flat prolongation of p-torsion WeierstrassCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_signTwist_addEquiv 15 below · cited by 1 · depth 15
• Free ℤₚ-Hopf order of rank p² inside A WeierstrassCurve.exists_finiteFree_hopfOrder_padicInt_rank_psq_of_isUnit_discr_of_hopfAlgebra_padic 120 below · cited by 1 · depth 15
• Full-kernel Vélu quotient: pushforward point map has kernel ℤQ WeierstrassCurve.exists_functionFieldHom_fullKernelQuotient_pointMapOfPushforward_ker_eq_zmultiples 81 below · cited by 2 · depth 15
• n-torsion of a non-elliptic Weierstrass curve via a finite Hopf algebra WeierstrassCurve.exists_hopfAlgebra_field_torsionBy_of_not_isElliptic_of_charZero 36 below · cited by 2 · depth 15
• Torsion Hopf algebra of W[n] over a field WeierstrassCurve.exists_hopfAlgebra_field_torsionBy_of_relativeGroupLaw_isPointsEval 20 below · cited by 2 · depth 15
• E[p] as points of a finite ℚ-Hopf algebra, over ℚ̄ and ℚ̄ₚ WeierstrassCurve.exists_hopfAlgebra_rat_torsionBy_withConv_equiv 99 below · cited by 2 · depth 15
• Every rational Weierstrass curve has an integral model WeierstrassCurve.exists_isIntegralModelOf_rat 0 below · cited by 1 · depth 15
• Two ℚₚ-models of E agree up to variable change WeierstrassCurve.exists_variableChange_map_intCast_padic_eq_map_along 0 below · cited by 1 · depth 15
• Factored twist comparison for curves with equal j WeierstrassCurve.exists_variableChange_map_of_j_eq_of_sq_factored 0 below · cited by 1 · depth 15
• Additivity of the Vélu weight across a 2-isogeny fibre WeierstrassCurve.fiberAdd_asymWeight_cleared_sixteen 0 below · cited by 3 · depth 15
• Additivity of the Vélu weight gₓ over 2-isogeny fibres WeierstrassCurve.fiberAdd_veluGx_cleared_four 0 below · cited by 3 · depth 15
• Finiteness of E[p] when p ≠ 0 in F WeierstrassCurve.finite_p_torsion_of_natCast_ne_zero 0 below · cited by 1 · depth 15
• Deuring's criterion via the Hasse invariant WeierstrassCurve.forall_nsmul_eq_zero_iff_hasseInvariant_eq_zero 11 below · cited by 6 · depth 15
• Full-kernel quotient equals the half-system Vélu quotient at odd order WeierstrassCurve.fullKernelQuotient_eq_veluQuotient_of_odd 0 below · cited by 3 · depth 15
• Base change commutes with the Vélu quotient of sums WeierstrassCurve.map_veluQuotientOfSums 0 below · cited by 4 · depth 15
• [ω]-stable cyclic N-subgroups of y²+y=x³ in characteristic 2 WeierstrassCurve.natCard_isAddCyclic_addSubgroup_card_eq_fixed_vcInvFun_eq_nuThree_of_char_two 6 below · cited by 2 · depth 15
• Cyclic N-subgroups of y²=x³+B stable under [ω] WeierstrassCurve.natCard_isAddCyclic_addSubgroup_card_eq_fixed_vcInvFun_eq_nuThree_of_ne_zero 12 below · cited by 1 · depth 15
• Counting [i]-stable cyclic N-subgroups of y²+y=x³ in characteristic 2 WeierstrassCurve.natCard_isAddCyclic_addSubgroup_card_eq_fixed_vcInvFun_eq_nuTwo_of_char_two 6 below · cited by 2 · depth 15
• Cyclic N-subgroups of y²=x³+Ax stable under [i] WeierstrassCurve.natCard_isAddCyclic_addSubgroup_card_eq_fixed_vcInvFun_eq_nuTwo_of_ne_zero 10 below · cited by 3 · depth 15
• Irreducible mod p representation forbids a_ℓ ≡ 2 at all such primes WeierstrassCurve.not_forall_apOfModel_eq_two_of_modRepIsIrreducible 72 below · cited by 4 · depth 15
• Negation is a variable change fixing every Weierstrass curve WeierstrassCurve.variableChange_mk_neg_one_smul_eq_self 0 below · cited by 2 · depth 15
• Nonvanishing discriminant of Vélu's odd cyclic quotient WeierstrassCurve.veluQuotient_oddOrderSummingSet_discriminant_ne_zero_of_addOrderOf_eq 1 below · cited by 19 · depth 15
• Reduction preserves the order of torsion prime to the residue characteristic WeierstrassCurve.addOrderOf_reduceHom_of_natCast_ne_zero 1 below · cited by 8 · depth 16
• Rationally represented homomorphisms are closed under addition WeierstrassCurve.add_mem_rationalHomSet 0 below · cited by 64 · depth 16
• Coefficient of x^{p(p-1)/2} in ψₚ is the Hasse invariant WeierstrassCurve.coeff_prePsi_eq_hasseInvariant 9 below · cited by 1 · depth 16
• Reduction is injective on N-torsion when N is invertible WeierstrassCurve.eq_of_reduceHom_eq_of_nsmul_eq_zero 0 below · cited by 5 · depth 16
• Parabolic diamond-invariant H¹(Γ₁(N)) class with eigenvalues a_ℓ(W) WeierstrassCurve.exists_H1_bot_ne_zero_parabolic_diamondRaw_eq_heckeT_eq_smul_of_isEigensystemH1_one 84 below · cited by 1 · depth 16
• Existence of a point of exact prime order on an elliptic curve WeierstrassCurve.exists_addOrderOf_eq_prime_of_isAlgClosed 6 below · cited by 8 · depth 16
• Kronecker's modular equation at a transcendental j-invariant WeierstrassCurve.exists_equiv_addSubgroup_isAddCyclic_isRoot_modularPolynomial_of_transcendental_j 303 below · cited by 3 · depth 16
• Sign twist by an unramified quadratic character preserves finite flat models WeierstrassCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_signTwist_addEquiv_of_odd_of_not_isSquare 14 below · cited by 1 · depth 16
• Finite free rank p² Hopf algebra for W[p], good reduction WeierstrassCurve.exists_finiteFree_hopfAlgebra_padicInt_torsionBy_rank_psq_of_isUnit_discr 113 below · cited by 1 · depth 16
• Vélu's isogeny with kernel generated by a point of order N WeierstrassCurve.exists_fullKernelHom 76 below · cited by 11 · depth 16
• Cuspidal Weierstrass curves: n-torsion as Hopf algebra points WeierstrassCurve.exists_hopfAlgebra_field_torsionBy_of_not_isElliptic_of_charZero_of_c4_eq_zero 5 below · cited by 1 · depth 16
• Nodal Weierstrass curves: n-torsion as points of a finite Hopf algebra WeierstrassCurve.exists_hopfAlgebra_field_torsionBy_of_not_isElliptic_of_charZero_of_c4_ne_zero 30 below · cited by 1 · depth 16
• E[p] as a finite cocommutative Hopf algebra over ℚ WeierstrassCurve.exists_hopfAlgebra_rat_torsionBy_withConv_equiv_algClosure 82 below · cited by 1 · depth 16
• Inertia-equivariant good reduction of a Weierstrass model WeierstrassCurve.exists_inertia_equivariant_reduction_of_variableChange_eq_map 1 below · cited by 1 · depth 16
• Existence of the n-division field of an elliptic curve WeierstrassCurve.exists_intermediateField_isGalois_card_torsion_eq_sq 3 below · cited by 11 · depth 16
• Potential good Deuring models over a Galois field, inertia faithful on S WeierstrassCurve.exists_isGalois_goodModel_inertia_faithful_of_three_ne_zero 5 below · cited by 4 · depth 16
• Good Legendre models over a finite Galois extension, with faithful inertia WeierstrassCurve.exists_isGalois_goodModel_inertia_faithful_of_two_ne_zero 1 below · cited by 4 · depth 16
• Order-3 points on y²+txy=x³+t⁵ force 8∣ v(t) WeierstrassCurve.exists_isUnit_mul_pow_eight_eq_of_charTwo 0 below · cited by 3 · depth 16
• Rational dual isogeny with integral trace WeierstrassCurve.exists_mem_rationalHomSet_isDualPair_and_add_eq_smul_id 13 below · cited by 6 · depth 16
• In characteristic p, ψₚ is a polynomial in xᵖ WeierstrassCurve.exists_prePsi_eq_expand 5 below · cited by 1 · depth 16
• Lifting ℓ-torsion along good reduction over a valuation subring WeierstrassCurve.exists_reduceHom_eq_of_nsmul_eq_zero_of_natCast_ne_zero 3 below · cited by 3 · depth 16
• Deuring surjectivity: every maximal order is a supersingular endomorphism ring WeierstrassCurve.exists_supersingular_rationalEndSubring_range_eq_of_isMaximalOrder 770 below · cited by 3 · depth 16
• Transcendental element in a valuation ring over a characteristic-0 field WeierstrassCurve.exists_valuationSubring_with_transcendental_of_charZero 0 below · cited by 2 · depth 16
• Endomorphism with β²-sβ+2=0 is Vélu's 2-isogeny WeierstrassCurve.exists_variableChange_smul_eq_veluQuotient2_forall_apply_eq_of_comp_self_add_two_smul_eq_smul 38 below · cited by 1 · depth 16
• Deuring's first step: β equals Vélu's quotient map up to coordinate change WeierstrassCurve.exists_variableChange_smul_eq_veluQuotient_forall_apply_eq_of_comp_self_add_smul_eq_smul 88 below · cited by 2 · depth 16
• Vélu pushforward point map has kernel ℤQ WeierstrassCurve.exists_veluFunctionFieldHom_pointMapOfPushforward_ker_eq_zmultiples_of_oddOrder 51 below · cited by 1 · depth 16
• Vélu isogeny as a point homomorphism over a field WeierstrassCurve.exists_veluPointHom_oddOrderSummingSet 57 below · cited by 3 · depth 16
• Vélu's isogeny for a cyclic kernel of odd order WeierstrassCurve.exists_veluPointHom_oddOrderSummingSet_of_addOrderOf_eq_two_mul_add_one 61 below · cited by 6 · depth 16
• Transfer of the E[p] Hopf-algebra parametrisation to ℚ̄ₚ and an integral model WeierstrassCurve.exists_withConv_equiv_padicInt_of_isIntegralModelOf_of_rat 15 below · cited by 1 · depth 16
• Finiteness of the units of End of an elliptic curve WeierstrassCurve.finite_rationalHomSet_units 2 below · cited by 4 · depth 16
• Bounds on the Weierstrass automorphism group at j=0 and j=1728 WeierstrassCurve.finite_stabilizer_and_natCard_le_of_j 0 below · cited by 3 · depth 16
• Finiteness of the variable-change stabiliser of an elliptic Weierstrass curve WeierstrassCurve.finite_stabilizer_variableChange 0 below · cited by 10 · depth 16
• Even-order Vélu quotient factors through an order-two step WeierstrassCurve.fullKernelHom_eq_veluPointMap2_comp_of_stage_last 79 below · cited by 2 · depth 16
• Nonvanishing discriminant of the full-kernel Vélu quotient WeierstrassCurve.fullKernelQuotient_discriminant_ne_zero 12 below · cited by 21 · depth 16
• Hasse invariant of the family y²+xy=x³-36tx-t WeierstrassCurve.hasseInvariant_jFamily 43 below · cited by 1 · depth 16
• Hasse¹²Δ^{-(q-1)} is an invariant of j WeierstrassCurve.hasseInvariant_pow_mul_delta_pow_eq_of_j_eq 1 below · cited by 4 · depth 16
• Hasse invariant of the Tate curve is 1 WeierstrassCurve.hasseInvariant_tatePowerSeries_map 44 below · cited by 2 · depth 16
• The Hasse invariant has weight q-1 WeierstrassCurve.hasseInvariant_variableChange 0 below · cited by 14 · depth 16
• Level lowering at q² with Steinberg-quotient coefficients WeierstrassCurve.isEigensystemH1_comp_apOfModel_of_isSemistableModel_of_qCoeff_congr_of_steinberg_quotient 10,658 below · cited by 1 · depth 16
• #Aut(E)=#μ₄(F) when j(E)=1728 WeierstrassCurve.natCard_stabilizer_variableChange_eq_natCard_rootsOfUnity_four_of_j_eq_1728 1 below · cited by 2 · depth 16
• Automorphism count for j=0 equals #μ₆(F) WeierstrassCurve.natCard_stabilizer_variableChange_eq_natCard_rootsOfUnity_six_of_j_eq_zero 1 below · cited by 2 · depth 16
• Elliptic curves with j ≠ 0 in characteristic 2 or 3 have two automorphisms WeierstrassCurve.natCard_stabilizer_variableChange_eq_two_of_j_ne_zero_of_char_two_or_three 0 below · cited by 7 · depth 16
• Two variable changes stabilise E when j ≠ 0, 1728 WeierstrassCurve.natCard_stabilizer_variableChange_eq_two_of_j_ne_zero_of_j_ne_1728 0 below · cited by 8 · depth 16
• Unit twist parameter for two multiplicative-reduction curves WeierstrassCurve.nnnorm_twistParam_eq_one 0 below · cited by 1 · depth 16
• Full N-torsion of count N² is (ℤ/N)² WeierstrassCurve.nonempty_torsionBy_addEquiv_zmod_prod_of_natCard_torsion_eq_sq 3 below · cited by 9 · depth 16
• Nonzero rational homomorphisms of elliptic curves are surjective WeierstrassCurve.surjective_of_mem_rationalHomSet 0 below · cited by 66 · depth 16
• Transcendence of j for a transcendental perturbation of (a₄,a₆) WeierstrassCurve.transcendental_j_perturb 0 below · cited by 2 · depth 16
• Velu sum quotient is covariant under variable change WeierstrassCurve.variableChange_veluQuotientOfSums_asymWeights 0 below · cited by 4 · depth 16
• Cleared secant identity for the order-2 Vélu map (ordinate) WeierstrassCurve.velu2_secant_negAddY_cleared_identity 0 below · cited by 1 · depth 16
• Cleared identity behind the Vélu 2-isogeny doubling abscissa WeierstrassCurve.velu2_tangent_addX_cleared_identity 0 below · cited by 1 · depth 16
• Cleared ordinate identity for Vélu's order-2 map: tangent case WeierstrassCurve.velu2_tangent_negAddY_cleared_identity 0 below · cited by 1 · depth 16
• Surjectivity of Vélu maps over an algebraically closed field WeierstrassCurve.veluPointHom_surjective_of_isAlgClosed 1 below · cited by 2 · depth 16
• Surjectivity of Vélu's order-2 map over algebraically closed fields WeierstrassCurve.veluPointMap2_surjective_of_isAlgClosed 2 below · cited by 6 · depth 16
• Wronskian identity for division polynomials: [n]^*ω = n ω WeierstrassCurve.Psi2Sq_mul_wronskian_sq 3 below · cited by 8 · depth 17
• Cyclic N-subgroups biject with the roots of Φ_N(j(E),Y) WeierstrassCurve.bijOn_cyclicQuotientJ_isRoot_modularPolynomial_of_transcendental_j 302 below · cited by 5 · depth 17
• Hasse invariant as a coefficient of the invariant differential WeierstrassCurve.coeff_invariantDifferential_eq_hasseInvariant 5 below · cited by 2 · depth 17
• Rationally represented point maps are closed under composition WeierstrassCurve.comp_mem_rationalHomSet 0 below · cited by 72 · depth 17
• Vélu's explicit 2-isogeny equals the translate-sum map WeierstrassCurve.coordsOrZero_veluPointMap2 0 below · cited by 4 · depth 17
• Base change of the iterated cyclic-quotient j-invariant WeierstrassCurve.cyclicQuotientJ_baseChange_map_eq_of_isAlgClosed 0 below · cited by 8 · depth 17
• Existence of dual endomorphisms in the rational endomorphism subring WeierstrassCurve.dualIsogenyExistence_rationalEndSubring 11 below · cited by 3 · depth 17
• Elliptic-net identity at index 4 WeierstrassCurve.ellipticNet_four 0 below · cited by 0 · depth 17
• Elliptic-net identity at index 3 for a Weierstrass curve WeierstrassCurve.ellipticNet_three 0 below · cited by 0 · depth 17
• Supersingular j-invariants are zeros of the j-family Hasse invariant WeierstrassCurve.eval_hasseInvariant_jFamily_eq_zero_of_mem_ssJSet 13 below · cited by 1 · depth 17
• Galois-equivariant p-torsion transfer to an integral model over ℚₚ WeierstrassCurve.exists_addEquiv_torsionBy_padicAlgClosure_of_isIntegralModelOf 2 below · cited by 1 · depth 17
• Vélu's 2-isogeny: rationality, dual isogeny and factorisation WeierstrassCurve.exists_coe_eq_veluPointMap2_and_mem_rationalHomSet_and_comp_eq_two_smul 18 below · cited by 9 · depth 17
• Frobenius twist of a dual pair of isogenies WeierstrassCurve.exists_frobenius_conjugate_dualPair_mem_rationalHomSet 0 below · cited by 1 · depth 17
• Residual irreducibility, oddness and inertial unipotence for a congruent newform WeierstrassCurve.exists_galoisRepAdic_residual_irreducible_odd_unipotent_of_isSemistableModel_of_qCoeff_congr 1,487 below · cited by 1 · depth 17
• Hopf-algebra model for n-torsion of y²=x³+cx² WeierstrassCurve.exists_hopfAlgebra_field_torsionBy_nodeNormalForm_of_charZero 26 below · cited by 1 · depth 17
• Kernel ideals and endomorphism rings via finite idèles WeierstrassCurve.exists_image_kernelIdealSet_eq_star_smul_ofFiniteIdele_and_range_eq_conjByFiniteIdele 205 below · cited by 3 · depth 17
• Deuring: supersingular endomorphism ring is a maximal order WeierstrassCurve.exists_isMaximalOrder_range_eq_rationalEndSubring_of_isDefiniteRamifiedExactlyAt 185 below · cited by 1 · depth 17
• Integral model of a Vélu quotient compatible with reduction WeierstrassCurve.exists_map_eq_veluQuotient_and_map_residue_eq_veluQuotient_reduceHom 0 below · cited by 2 · depth 17
• Rational homomorphism killing N-torsion is N times one WeierstrassCurve.exists_mem_rationalHomSet_eq_smul_of_forall_smul_eq_zero 6 below · cited by 36 · depth 17
• Vélu quotient with prescribed kernel and its universal property WeierstrassCurve.exists_mem_rationalHomSet_ker_eq_forall_exists_eq_comp 79 below · cited by 9 · depth 17
• Supersingular elliptic curves in characteristic p are isogenous WeierstrassCurve.exists_ne_zero_mem_rationalHomSet_of_forall_nsmul_char_eq_zero 336 below · cited by 2 · depth 17
• Surjectivity of multiplication by n over an algebraically closed field WeierstrassCurve.exists_nsmul_eq_of_isAlgClosed 1 below · cited by 7 · depth 17
• Polynomial form of an injective rational homomorphism WeierstrassCurve.exists_polynomial_rep_of_injective_of_mem_rationalHomSet 0 below · cited by 4 · depth 17
• Isomorphism of enhanced curves via rational maps or variable change WeierstrassCurve.exists_rationalHomSet_comp_eq_id_map_eq_iff_exists_variableChange_smul_eq 9 below · cited by 3 · depth 17
• Atkin–Lehner automorphism transports moduli places along a q-isogeny WeierstrassCurve.exists_rationalHom_ker_eq_zmultiples_toValuationSubring_autOnPlaces_eq_comap_moduliPlace_map_sup_ker_nsmul 480 below · cited by 1 · depth 17
• Supersingular curve with level structure and odd-degree s-power endomorphism WeierstrassCurve.exists_supersingular_endomorphism_natCard_ker_eq_odd_pow_stabilizing_cyclic 227 below · cited by 1 · depth 17
• Deuring normal form from a point of order 3 WeierstrassCurve.exists_variableChange_eq_deuring_of_isUnit_three 0 below · cited by 1 · depth 17
• Vélu's double full-kernel quotient is multiplication by N WeierstrassCurve.exists_variableChange_eq_fullKernelQuotient_fullKernelQuotient_comp_eq_smul 122 below · cited by 5 · depth 17
• Legendre model over a valuation ring with 2 invertible WeierstrassCurve.exists_variableChange_eq_legendreCurve_of_isUnit_two 0 below · cited by 2 · depth 17
• Invertible rational homomorphisms arise from variable changes WeierstrassCurve.exists_variableChange_forall_eq_equivOfVariableChangeEq_of_comp_eq_id 2 below · cited by 4 · depth 17
• Universality of the ℓ-isogeny quotient with level structure WeierstrassCurve.exists_variableChange_heq_vcInvFun_iff_exists_dualPair 14 below · cited by 3 · depth 17
• Node normal form y²=x³+cx² over K WeierstrassCurve.exists_variableChange_smul_eq_nodeNormalForm_of_not_isElliptic_of_c4_ne_zero 0 below · cited by 1 · depth 17
• Vélu function-field extension for an odd cyclic kernel WeierstrassCurve.exists_veluFunctionFieldHom_restrictAlong_placeOfPoint_eq_of_isAlgClosed 50 below · cited by 5 · depth 17
• Vélu isogeny with kernel ⟨ Q⟩ over algebraically closed F WeierstrassCurve.exists_veluPointHom_oddOrderSummingSet_of_isAlgClosed 55 below · cited by 10 · depth 17
• Descent of the Vélu point homomorphism along a field homomorphism WeierstrassCurve.exists_veluPointHom_oddOrderSummingSet_of_ringHom 0 below · cited by 4 · depth 17
• Transfer of A-points and E[p] from ℚ̄ to ℚ̄ₚ WeierstrassCurve.exists_withConv_equiv_torsionBy_padicAlgClosure_of_ratAlgClosure 11 below · cited by 1 · depth 17
• Vanishing q'-torsion transfers along a nonzero rational homomorphism WeierstrassCurve.forall_smul_eq_zero_of_mem_rationalHomSet_of_forall_smul_eq_zero 16 below · cited by 7 · depth 17
• Surjectivity of Vélu's full-kernel map over algebraically closed fields WeierstrassCurve.fullKernelHom_surjective_of_isAlgClosed 77 below · cited by 5 · depth 17
• Vélu quotient by an even cyclic kernel factors through W/{0,T} WeierstrassCurve.fullKernelQuotient_eq_fullKernelQuotient_veluQuotient2 5 below · cited by 5 · depth 17
• j=0 is preserved by Vélu quotients in characteristic 2 or 3 WeierstrassCurve.fullKernelQuotient_j_eq_zero_of_j_eq_zero_of_ringChar 0 below · cited by 2 · depth 17
• Primitive endomorphism with X²-sX+m has cyclic kernel of order m WeierstrassCurve.isAddCyclic_ker_and_card_ker_eq_of_comp_self_add_smul_eq_smul 19 below · cited by 5 · depth 17
• Multiples of a point of odd prime order form an odd Vélu set WeierstrassCurve.isOddVeluSet_oddOrderSummingSet 0 below · cited by 3 · depth 17
• No q'-torsion on one model gives supersingular j WeierstrassCurve.j_mem_ssJSet_of_forall_smul_eq_zero 1 below · cited by 5 · depth 17
• Zeros of the Hasse polynomial of the j-family are supersingular WeierstrassCurve.mem_ssJSet_of_eval_hasseInvariant_jFamily_eq_zero 16 below · cited by 1 · depth 17
• An elliptic curve has p+1 cyclic subgroups of order p WeierstrassCurve.natCard_cycSub_eq_prime_add_one 3 below · cited by 1 · depth 17
• Equinumerous variable-change stabilisers along a Vélu cyclic isogeny WeierstrassCurve.natCard_variableChange_stabilizer_eq_of_fullKernelQuotient 124 below · cited by 2 · depth 17
• Hasse polynomial of the j-family: degree and constant term WeierstrassCurve.natDegree_hasseInvariant_jFamily 0 below · cited by 2 · depth 17
• Odd division polynomials of an elliptic curve are non-zero WeierstrassCurve.prePsi_ne_zero_of_isElliptic 4 below · cited by 2 · depth 17
• Supersingular parameters are simple roots of the Hasse polynomial WeierstrassCurve.rootMultiplicity_hasseInvariant_jFamily_eq_one 21 below · cited by 1 · depth 17
• Trivial n-torsion on a cuspidal Weierstrass curve in characteristic zero WeierstrassCurve.subsingleton_torsionBy_algClosure_point_of_not_isElliptic_of_charZero_of_c4_eq_zero 4 below · cited by 1 · depth 17
• Vélu's quotient map is rational and universal WeierstrassCurve.veluPointHom_mem_rationalHomSet_and_exists_mem_rationalHomSet_comp_eq 6 below · cited by 9 · depth 17
• p-torsion of a Weierstrass curve under ℚ̄hookrightarrowmathbb Qₚ̄ WeierstrassCurve.bijective_torsionBy_pointMap_ratAlgClosure_padicAlgClosure 6 below · cited by 1 · depth 18
• Invariance of the cyclic quotient j-invariant under coordinate change WeierstrassCurve.cyclicQuotientJ_variableChange_eq 1 below · cited by 12 · depth 18
• Iterated Vélu j equals full-kernel quotient j WeierstrassCurve.cyclicQuotientJ_zmultiples_eq_fullKernelQuotient_j 84 below · cited by 2 · depth 18
• Multiplication by a prime to p permutes ψₚ-roots WeierstrassCurve.eval_prePsi_Phi_div_PsiSq_eq_zero_of_eval_prePsi_eq_zero 5 below · cited by 10 · depth 18
• Galois-equivariant identification of n-torsion after base change to ℚₚ WeierstrassCurve.exists_addEquiv_torsionBy_ratBaseChange_eq_padicMap_padicAlgClosure 0 below · cited by 1 · depth 18
• Points of every order invertible in an algebraically closed field WeierstrassCurve.exists_addOrderOf_eq_of_isAlgClosed 9 below · cited by 2 · depth 18
• Enumeration of the ℓ+1 cyclic kernels with nonsingular Vélu quotients WeierstrassCurve.exists_enum_cyclicKernels_veluQuotient_discriminant_ne_zero 11 below · cited by 1 · depth 18
• Three 2-torsion points with nonsingular Vélu quotients WeierstrassCurve.exists_enum_twoTorsion_veluQuotient2_discriminant_ne_zero 6 below · cited by 2 · depth 18
• Hopf-algebra witness for n-torsion of a split node WeierstrassCurve.exists_hopfAlgebra_field_torsionBy_nodeNormalForm_of_charZero_of_isSquare 3 below · cited by 1 · depth 18
• Twisted μₙ Hopf algebra for a non-split node WeierstrassCurve.exists_hopfAlgebra_field_torsionBy_nodeNormalForm_of_charZero_of_not_isSquare 22 below · cited by 1 · depth 18
• Deuring's theorem on supersingular endomorphism rings WeierstrassCurve.exists_isDefiniteRamifiedExactlyAt_isMaximalOrder_range_eq_rationalEndSubring 177 below · cited by 3 · depth 18
• Existence of a dual pair for rational homomorphisms WeierstrassCurve.exists_isDualPair_of_mem_rationalHomSet 15 below · cited by 24 · depth 18
• Vélu's full-kernel quotient commutes with reduction WeierstrassCurve.exists_map_eq_fullKernelQuotient_map_residue_eq_fullKernelQuotient_reduceHom 0 below · cited by 4 · depth 18
• Lifting a variable change of the reduced model WeierstrassCurve.exists_map_residue_eq_and_reduceHom_comp_eq_of_variableChange_smul_eq 0 below · cited by 1 · depth 18
• Variable change as mutually inverse rational homomorphisms WeierstrassCurve.exists_mem_rationalHomSet_apply_eq_equivOfVariableChangeEq 1 below · cited by 5 · depth 18
• Rational homomorphisms extend from k₀-points to k-points WeierstrassCurve.exists_mem_rationalHomSet_apply_map_eq_map_apply 0 below · cited by 4 · depth 18
• Rational homomorphisms separate ℓ-torsion under quaternionic endomorphisms WeierstrassCurve.exists_mem_rationalHomSet_apply_ne_zero_of_prime_nsmul_eq_zero 22 below · cited by 5 · depth 18
• Rational factorisation of a homomorphism through a separable isogeny WeierstrassCurve.exists_mem_rationalHomSet_comp_eq_of_ker_le_of_separable 2 below · cited by 3 · depth 18
• Factorisation through an isogeny with contained kernel and p^e-abscissae WeierstrassCurve.exists_mem_rationalHomSet_comp_eq_of_ker_le_of_xCoord_expand 5 below · cited by 9 · depth 18
• Supersingular curves admit an endomorphism with square -pm² WeierstrassCurve.exists_mem_rationalHomSet_comp_self_add_char_mul_sq_smul_id_eq_zero 104 below · cited by 2 · depth 18
• Dividing a quadratic endomorphism by N along a separable isogeny WeierstrassCurve.exists_mem_rationalHomSet_comp_self_add_smul_eq_smul_of_natCast_mul 88 below · cited by 1 · depth 18
• Reduction of geometric homomorphisms at good reduction WeierstrassCurve.exists_mem_rationalHomSet_reduceHom_comp_eq_comp_reduceHom 6 below · cited by 3 · depth 18
• Deuring: β-[k₀] is p times an endomorphism WeierstrassCurve.exists_mem_rationalHomSet_sub_smul_id_eq_char_smul_of_dvd_of_sq_dvd 17 below · cited by 5 · depth 18
• Separable rational homomorphism onto a supersingular curve WeierstrassCurve.exists_mem_rationalHomSet_wronskian_ne_zero_of_forall_nsmul_eq_zero 108 below · cited by 2 · depth 18
• Isogeny of elliptic curves with the same quadratic multiplication WeierstrassCurve.exists_ne_zero_mem_rationalHomSet_of_comp_self_add_smul_eq_smul 26 below · cited by 1 · depth 18
• Quotient by a finite subgroup: dual pair and kernel ideal WeierstrassCurve.exists_quotient_dualPair_kernelIdealSet_comp_eq 89 below · cited by 2 · depth 18
• Supersingular [p] is Frobenius squared up to isomorphism WeierstrassCurve.exists_ratPointHom_frobenius_comp_ratPointHom_frobenius_eq_comp_nsmul_of_forall_nsmul_eq_zero 12 below · cited by 1 · depth 18
• Double Vélu 2-quotient composes to multiplication by 2 WeierstrassCurve.exists_variableChange_eq_veluQuotient2_veluQuotient2_comp_eq_two_smul 1 below · cited by 1 · depth 18
• Dual of a Vélu 2-isogeny: double quotient equals doubling WeierstrassCurve.exists_variableChange_eq_veluQuotient2_veluQuotient2_comp_eq_two_smul_of_two_ne_zero 1 below · cited by 2 · depth 18
• Mutually inverse rational maps give an F-variable change WeierstrassCurve.exists_variableChange_of_comp_eq_id_of_mem_rationalHomSet 1 below · cited by 3 · depth 18
• Rational isomorphisms of elliptic curves are variable changes WeierstrassCurve.exists_variableChange_smul_eq_and_apply_some_eq_of_comp_eq_id_of_mem_rationalHomSet 1 below · cited by 2 · depth 18
• Deuring's lifting theorem for curves with an endomorphism WeierstrassCurve.exists_variableChange_smul_eq_and_reduceHom_comp_eq_comp_reduceHom_of_mem_rationalHomSet 313 below · cited by 1 · depth 18
• Vanishing c₄ and c₆ in characteristic zero give y²=x³ WeierstrassCurve.exists_variableChange_smul_eq_zero_of_c4_eq_zero_of_c6_eq_zero 0 below · cited by 1 · depth 18
• Vélu's maps for an odd-order point in reduced rational form WeierstrassCurve.exists_veluX_eq_div_and_veluY_eq_div_of_addOrderOf_eq 0 below · cited by 1 · depth 18
• Abscissa representations compose, with degrees multiplying WeierstrassCurve.exists_xCoord_rep_comp 0 below · cited by 1 · depth 18
• Abscissa of a rational additive map depends only on x WeierstrassCurve.exists_xCoord_rep_of_mem_rationalHomSet 1 below · cited by 11 · depth 18
• Deuring: supersingular rational endomorphism ring has ℤ-rank four WeierstrassCurve.free_and_finrank_rationalEndSubring_eq_four 86 below · cited by 4 · depth 18
• Tower law for Vélu full-kernel quotient Weierstrass models WeierstrassCurve.fullKernelQuotient_fullKernelQuotient_eq_of_fullKernelHom 80 below · cited by 3 · depth 18
• Covariance of Vélu's full-kernel quotient under coordinate changes WeierstrassCurve.fullKernelQuotient_variableChange_vcInvFun 1 below · cited by 6 · depth 18
• Principal divisors on an elliptic function field, any characteristic WeierstrassCurve.hasPrincipalDivisors_functionField_of_isElliptic 28 below · cited by 5 · depth 18
• Hasse invariant of the Legendre curve via the Deuring polynomial WeierstrassCurve.hasseInvariant_legendreCurve 0 below · cited by 5 · depth 18
• Vélu's isogeny commutes with a change of Weierstrass coordinates WeierstrassCurve.heq_fullKernelHom_vcInvFun 2 below · cited by 2 · depth 18
• Reduction intertwines Vélu quotient maps on points WeierstrassCurve.heq_reduceHom_fullKernelHom_of_map_eq_fullKernelQuotient 0 below · cited by 3 · depth 18
• The Legendre curve is elliptic iff t≠ 0,1 WeierstrassCurve.isElliptic_legendreCurve_iff 0 below · cited by 4 · depth 18
• The j-invariant of the Legendre curve WeierstrassCurve.j_legendreCurve 0 below · cited by 4 · depth 18
• The subring generated by rational endomorphisms is already the set of rational endomorphisms WeierstrassCurve.mem_rationalEndSubring_iff_mem_rationalHomSet 3 below · cited by 8 · depth 18
• Automorphism-weighted symmetry of the ℓ-isogeny correspondence WeierstrassCurve.natCard_rationalAut_mul_natCard_overgroup_dualPair_eq_natCard_rationalAut_mul_natCard_subgroup_dualPair 12 below · cited by 1 · depth 18
• Abscissa of an additive map has a pole at infinity WeierstrassCurve.natDegree_lt_of_xCoord_rep 4 below · cited by 10 · depth 18
• Negation preserves rationally represented homomorphisms WeierstrassCurve.neg_mem_rationalHomSet 0 below · cited by 8 · depth 18
• Nonsingular points of y²=x³ form Gₐ WeierstrassCurve.nonempty_addEquiv_affine_point_zero_of_charZero 0 below · cited by 1 · depth 18
• Stabiliser of an elliptic Weierstrass curve as unit group WeierstrassCurve.nonempty_stabilizer_variableChange_mulEquiv_units_rationalEndSubring 4 below · cited by 2 · depth 18
• Kernel-ideal dictionary at ℓ for Hom(W,X₀) WeierstrassCurve.relIndex_annihilator_eq_sq_natCard_and_mem_of_forall_apply_torsion_eq_zero 20 below · cited by 5 · depth 18
• Odd Vélu step equals Vélu quotient with image subgroup WeierstrassCurve.stepCurve_stepSubgroup_eq_of_prime_ne_two 1 below · cited by 5 · depth 18
• Degree-two Vélu step equals the order-two Vélu quotient WeierstrassCurve.stepCurve_stepSubgroup_two_eq 0 below · cited by 5 · depth 18
• Vélu's map lands on the quotient curve, odd cyclic kernel WeierstrassCurve.velu_map_equation_of_oddOrderSummingSet_of_isAlgClosed 0 below · cited by 1 · depth 18
• Division polynomial Φₙ of the nodal cubic y²+xy=x³ WeierstrassCurve.Phi_nodalCubic_eq_X_pow 0 below · cited by 1 · depth 19
• Bijectivity of E[p](ℚ̄)→ E[p](mathbb Qₚ̄), elliptic case WeierstrassCurve.bijective_torsionBy_pointMap_ratAlgClosure_padicAlgClosure_of_isElliptic 3 below · cited by 1 · depth 19
• Bijectivity of p-torsion base change along ℚ̄→ℚ̄ₚ, singular case WeierstrassCurve.bijective_torsionBy_pointMap_ratAlgClosure_padicAlgClosure_of_not_isElliptic 2 below · cited by 1 · depth 19
• Weierstrass models with infinitely many common affine points coincide WeierstrassCurve.eq_of_infinite_setOf_equation 0 below · cited by 1 · depth 19
• Behaviour of Φₙ under a Weierstrass variable change WeierstrassCurve.eval_Phi_variableChange 0 below · cited by 3 · depth 19
• Ψₙ^{Sq} under an admissible change of coordinates WeierstrassCurve.eval_PsiSq_variableChange 0 below · cited by 3 · depth 19
• Anticommuting pair of rational endomorphisms when Frobenius is an integer WeierstrassCurve.exists_anticommuting_pair_mem_rationalHomSet_of_frobenius_eq_smul 84 below · cited by 3 · depth 19
• Enumerating the ψ(N) cyclic N-subgroups with nonsingular Vélu quotients WeierstrassCurve.exists_enum_cyclic_fullKernelQuotient_discriminant_ne_zero 23 below · cited by 1 · depth 19
• p-saturation of integral rational endomorphisms (Deuring) WeierstrassCurve.exists_eq_char_smul_of_sq_sub_smul_add_smul_eq_zero_rationalEndSubring 18 below · cited by 1 · depth 19
• Split-node n-torsion is μₙ, Galois-equivariantly WeierstrassCurve.exists_equiv_torsionBy_nodeNormalForm_rootsOfUnity_of_isSquare 1 below · cited by 1 · depth 19
• n-torsion of a non-split nodal cubic is twisted μₙ WeierstrassCurve.exists_equiv_torsionBy_nodeNormalForm_rootsOfUnity_of_not_isSquare 1 below · cited by 1 · depth 19
• Cyclicity of rational p-torsion in characteristic p WeierstrassCurve.exists_forall_mem_zmultiples_of_char_nsmul_eq_zero 6 below · cited by 2 · depth 19
• Rational factorisation up to Frobenius twist WeierstrassCurve.exists_frobenius_comp_rational_of_comp_eq_of_mem_rationalHomSet 3 below · cited by 2 · depth 19
• Inertia-equivariant reduction map on a good integral model WeierstrassCurve.exists_inertia_equivariant_reduceHom_of_variableChange_eq_map 1 below · cited by 1 · depth 19
• Supersingular Frobenius: a power acts as an integer WeierstrassCurve.exists_iterate_frobenius_eq_smul_of_forall_nsmul_char_eq_zero 2 below · cited by 3 · depth 19
• Homomorphisms of elliptic curves do not grow under algebraically closed extensions WeierstrassCurve.exists_mem_rationalHomSet_apply_map_eq_map_apply_of_mem_rationalHomSet_baseChange 1 below · cited by 2 · depth 19
• Lifting ℓ-torsion homomorphisms to rational homomorphisms W→ X₀ WeierstrassCurve.exists_mem_rationalHomSet_forall_torsionBy_apply_eq_of_rationalEndSubring_range_eq_quaternionOrder 20 below · cited by 1 · depth 19
• Vélu quotient by a finite subgroup and its kernel ideal WeierstrassCurve.exists_mem_rationalHomSet_ker_eq_and_forall_comp_and_kernelIdealSet_eq 81 below · cited by 2 · depth 19
• Deuring's criterion: endomorphism with p ∣ q, p ∤ t forces ordinarity WeierstrassCurve.exists_ne_zero_and_char_nsmul_eq_zero_of_comp_self_add_smul_eq_smul_of_dvd_of_not_dvd 20 below · cited by 3 · depth 19
• Rational Verschiebung: [p] via F-rational functions of (xᵖ,yᵖ) WeierstrassCurve.exists_rational_verschiebung_of_charP 9 below · cited by 1 · depth 19
• Variable changes between good-reduction Weierstrass models are integral WeierstrassCurve.exists_variableChange_map_eq_and_reduceHom_vcFun_eq 0 below · cited by 5 · depth 19
• Deuring lifting for an endomorphism with order maximal at p WeierstrassCurve.exists_variableChange_smul_eq_and_reduceHom_comp_eq_comp_reduceHom_of_comp_self_add_smul_eq_smul 311 below · cited by 1 · depth 19
• Function field isomorphism respecting infinity comes from a variable change WeierstrassCurve.exists_variableChange_smul_eq_of_functionField_algEquiv 1 below · cited by 1 · depth 19
• The rational endomorphism ring of an elliptic curve is a domain WeierstrassCurve.isDomain_rationalEndSubring 3 below · cited by 1 · depth 19
• Full-kernel Vélu quotient commutes with base change WeierstrassCurve.map_fullKernelQuotient_mapPoint 0 below · cited by 2 · depth 19
• Left ideals of supersingular endomorphism rings are kernel ideals WeierstrassCurve.mem_ideal_rationalEndSubring_of_forall_apply_eq_zero 15 below · cited by 1 · depth 19
• ℤ_ℓotimesEnd(X)≅ M₂(ℤ_ℓ) for supersingular X WeierstrassCurve.nonempty_padicInt_tensorProduct_rationalEndSubring_algEquiv_matrix 147 below · cited by 1 · depth 19
• Separability of the odd division polynomial ψₙ WeierstrassCurve.separable_prePsi_of_isUnit 3 below · cited by 16 · depth 19
• Integral Frobenius forces a non-commuting pair of rational endomorphisms WeierstrassCurve.exists_comp_ne_comp_of_frobenius_eq_smul 76 below · cited by 1 · depth 20
• Reduction detects divisibility of rational homomorphisms by n WeierstrassCurve.exists_mem_rationalHomSet_eq_smul_of_forall_reduceHom_apply_eq_zero 7 below · cited by 1 · depth 20
• Supersingular curves descend to a finite field with integral Frobenius WeierstrassCurve.exists_subfield_model_frobenius_eq_smul_rationalEndSubring_equiv 12 below · cited by 1 · depth 20
• Deuring lifting over the Witt disc WeierstrassCurve.exists_valuationSubring_residueField_equiv_and_reduceHom_comp_eq_of_isAlgClosed_of_comp_self_add_smul_eq_smul 246 below · cited by 1 · depth 20
• Algebraisation over ℚ̄ of a lifted endomorphism WeierstrassCurve.exists_valuationSubring_variableChange_smul_eq_and_ratPointHom_reduceHom_comp_eq_of_isAlgebraic_j 8 below · cited by 1 · depth 20
• Curves with equal jnotin{0,1728} and a given square root are isomorphic WeierstrassCurve.exists_variableChange_of_j_eq_of_sq 1 below · cited by 3 · depth 20
• Halving a lift of an endomorphism at a place above 2 WeierstrassCurve.exists_variableChange_smul_eq_and_reduceHom_comp_eq_of_exists_reduceHom_comp_eq_two_smul_of_charP_two 156 below · cited by 1 · depth 20
• Biduality of Vélu quotients: j(W''/⟨ Q'⟩)=j(W) WeierstrassCurve.j_fullKernelQuotient_fullKernelQuotient_eq_j 124 below · cited by 1 · depth 20
• Stabiliser orders agree for a cyclic subgroup and its Vélu dual WeierstrassCurve.natCard_stabilizer_zmultiples_eq_natCard_stabilizer_zmultiples_fullKernelQuotient 127 below · cited by 1 · depth 20
• Tate's theorem for T_ℓ when t²=4q WeierstrassCurve.tateModule_end_eq_sum_smul_of_frobenius_equivariant_of_sq_eq 138 below · cited by 1 · depth 20
• Tate's theorem for T_ℓ: non-scalar Frobenius case WeierstrassCurve.tateModule_end_eq_sum_smul_of_frobenius_equivariant_of_sq_ne 65 below · cited by 1 · depth 20
• ωₙ is an exact half of 2ωₙ WeierstrassCurve.two_mul_omega 0 below · cited by 1 · depth 20
• Conjugation by an isogeny agrees with Frobenius transport WeierstrassCurve.comp_ratPointHom_iterateFrobenius_eq_of_comp_eq_comp 19 below · cited by 1 · depth 21
• Determinant of Frobenius on the ℓ-adic Tate module equals q WeierstrassCurve.det_frobenius_tateModule_eq_card 43 below · cited by 3 · depth 21
• Rigidity: an automorphism fixing the N-torsion is the identity WeierstrassCurve.eq_id_of_comp_eq_id_of_forall_torsion_apply_eq_self 22 below · cited by 2 · depth 21
• Automorphism fixing the 2-torsion is ± 1 WeierstrassCurve.eq_id_or_eq_neg_id_of_comp_eq_id_of_forall_two_torsion_apply_eq_self 23 below · cited by 1 · depth 21
• Order-four automorphism on the M-torsion when j=1728 WeierstrassCurve.exists_j_eq_1728_torsion_basis_heq_vcInvFun_of_order_four 10 below · cited by 1 · depth 21
• An order-three automorphism acting regularly on E₀[M] WeierstrassCurve.exists_j_eq_zero_torsion_basis_heq_vcInvFun_of_order_three 14 below · cited by 1 · depth 21
• Lifting a Weierstrass model with prescribed reduction and j WeierstrassCurve.exists_map_residue_eq_and_map_subtype_j_eq 0 below · cited by 2 · depth 21
• Rational isogeny with rational dual killing a Frobenius-stable ℓ-subgroup WeierstrassCurve.exists_mem_rationalHomSet_ker_eq_zmultiples_of_map_mem_zmultiples 64 below · cited by 1 · depth 21
• Ascending a 2-isogeny: halving an endomorphism γ WeierstrassCurve.exists_mem_rationalHomSet_two_smul_comp_eq_comp_of_comp_self_add_smul_eq_smul 88 below · cited by 1 · depth 21
• Removing a Frobenius twist from a lifting statement at a place WeierstrassCurve.exists_reduceHom_comp_eq_of_exists_reduceHom_comp_eq_map_iterateFrobenius 4 below · cited by 1 · depth 21
• Rational endomorphism subring is invariant under variable change WeierstrassCurve.exists_ringEquiv_rationalEndSubring_apply_eq_of_variableChange_smul_eq 0 below · cited by 1 · depth 21
• Rational endomorphisms with equal cyclic kernel differ by an automorphism WeierstrassCurve.exists_unit_rationalHomSet_comp_eq_of_ker_le_of_comp_eq_smul_id 85 below · cited by 1 · depth 21
• Deuring lifting in residue characteristic two, three-torsion form WeierstrassCurve.exists_valuationSubring_lift_variableChange_veluQuotient_reduceHom_eq_of_three_smul_mem_zmultiples_of_two_eq_zero 207 below · cited by 1 · depth 21
• Deuring lift compatible with Vélu quotient on two-torsion test points WeierstrassCurve.exists_valuationSubring_lift_variableChange_veluQuotient_reduceHom_eq_of_two_smul_mem_zmultiples 203 below · cited by 1 · depth 21
• Isomorphisms of unit-discriminant models descend to the valuation ring WeierstrassCurve.exists_variableChange_map_subtype_eq_and_smul_eq_of_isUnit_discriminant 0 below · cited by 1 · depth 21
• Twist comparison of short Weierstrass curves via a square root WeierstrassCurve.exists_variableChange_of_isShortNF_of_sq 0 below · cited by 1 · depth 21
• Level Γ_H(M) structures on y²+y=x³ in characteristic two WeierstrassCurve.natCard_torsionOrbit_and_exists_surjective_doubleCoset_of_char_two 8 below · cited by 1 · depth 21
• Frobenius acting as an integer descends all endomorphisms WeierstrassCurve.rationalEndSubring_baseChange_eq_of_frobenius_eq_smul 8 below · cited by 1 · depth 21
• Surjectivity of reduction for good reduction over a Henselian valuation ring WeierstrassCurve.reduceHom_surjective_of_henselianLocalRing 0 below · cited by 1 · depth 21
• Trace of Frobenius on the Tate module equals q+1-#W(F) WeierstrassCurve.trace_frobenius_tateModule_eq_card_add_one_sub 62 below · cited by 2 · depth 21
• Commutativity of rational endomorphisms of an ordinary curve WeierstrassCurve.comp_eq_comp_of_mem_rationalHomSet_of_char_nsmul_eq_zero 18 below · cited by 1 · depth 22
• Automorphisms [ω], [i] of y²+y=x³ in characteristic two WeierstrassCurve.exists_addMonoidHom_vcInvFun_pow_heq_and_forall_exists_ne_smul_of_char_two 4 below · cited by 4 · depth 22
• Transitivity on points of exact order M for generic j WeierstrassCurve.exists_algEquiv_map_eq_of_addOrderOf_eq_of_transcendental_j 355 below · cited by 5 · depth 22
• A Bézout identity for Ψ₃ and Ψ₃' WeierstrassCurve.exists_mul_Psi3_add_mul_derivative_Psi3 0 below · cited by 2 · depth 22
• Frobenius-stable ℓ-torsion subgroup as an F-rational isogeny kernel WeierstrassCurve.exists_rational_separable_isogeny_of_map_mem_zmultiples 59 below · cited by 1 · depth 22
• Deuring lift with level-three marking and Vélu quotient WeierstrassCurve.exists_valuationSubring_lift_variableChange_veluQuotient_apply_threeTorsion_eq_of_smul_eq_veluQuotient 191 below · cited by 1 · depth 22
• Deuring lift marked by a cyclic subgroup and two 2-torsion points WeierstrassCurve.exists_valuationSubring_lift_variableChange_veluQuotient_apply_twoTorsion_eq_of_smul_eq_veluQuotient 188 below · cited by 1 · depth 22
• Descent of Frobenius-equivariant homomorphisms to a finite field WeierstrassCurve.mem_rationalHomSet_of_mem_rationalHomSet_baseChange_of_forall_apply_smul 7 below · cited by 1 · depth 22
• Reduction commutes with Vélu's abscissa map off the kernel WeierstrassCurve.veluX_mem_and_residue_veluX_eq_of_forall_fst_ne_residue 0 below · cited by 3 · depth 22
• Reduction commutes with Vélu's ordinate map, odd order WeierstrassCurve.veluY_mem_and_residue_veluY_eq_of_forall_fst_ne_residue 0 below · cited by 1 · depth 22
• Monodromy at the cusp: a ±transvection on E[M] WeierstrassCurve.exists_algEquiv_map_eq_smul_and_map_eq_smul_add_of_transcendental_j 58 below · cited by 2 · depth 23
• Deuring's marked deformation over a formal disc, level three WeierstrassCurve.exists_powerSeries_deformation_kohelQuotient_threeTorsion_levelThreeModulus_of_smul_eq_veluQuotient 187 below · cited by 1 · depth 23
• Marked lift with Legendre cross vanishing only at T=0 WeierstrassCurve.exists_powerSeries_deformation_kohelQuotient_twoTorsion_legendreCross_of_smul_eq_veluQuotient 185 below · cited by 1 · depth 23
• Lifting a kernel polynomial of odd order along reduction WeierstrassCurve.exists_reduceHom_eq_and_map_eq_kernelPolynomial_oddOrderSummingSet 7 below · cited by 4 · depth 23
• Canonical Deuring normal form at a three-torsion point WeierstrassCurve.exists_variableChange_eq_deuringCurve_of_three_smul_eq_zero 0 below · cited by 1 · depth 23
• Legendre modulus determines a curve with ordered 2-torsion pair WeierstrassCurve.exists_variableChange_of_legendreLambda_eq 0 below · cited by 2 · depth 23
• Level-three modulus determines a marked curve up to isomorphism WeierstrassCurve.exists_variableChange_of_levelThreeModulus_eq 0 below · cited by 2 · depth 23
• Kohel's kernel-polynomial quotient equals Vélu's quotient WeierstrassCurve.kohelQuotient_kernelPolynomial_eq_veluQuotient 0 below · cited by 6 · depth 23
• Unique lifting of order-three points over an adically complete base WeierstrassCurve.exists_equation_and_eval_Psi3_eq_zero_and_map_eq_of_isAdicComplete 1 below · cited by 1 · depth 24
• Elliptic deformations over 𝒪[[T]] with non-constant reduced j WeierstrassCurve.exists_powerSeries_isElliptic_variableChange_smul_map_eq_and_map_j_ne_C 0 below · cited by 2 · depth 24
• Legendre cross-difference of a non-isotrivial family and its Kohel quotient WeierstrassCurve.map_legendreCross_kohelQuotient_ne_zero_of_map_j_ne_C 181 below · cited by 1 · depth 24
• Level-three moduli of E and E/h differ modulo π WeierstrassCurve.map_levelThreeModulus_kohelQuotient_sub_ne_zero_of_map_j_ne_C 181 below · cited by 1 · depth 24
• Size of the automorphism orbit of a ± point of order M WeierstrassCurve.natCard_torsionOrbit_bot_variableChange_eq_jWidthChar 16 below · cited by 1 · depth 24
• Vélu quotient of odd non-square order has different j WeierstrassCurve.apply_j_ne_apply_j_of_j_map_eq_veluQuotient_j_of_ne_C 168 below · cited by 2 · depth 25
• Rigidity of ± P level structures for M ≥ 4 WeierstrassCurve.natCard_stabilizer_torsionOrbit_bot_eq_two 5 below · cited by 1 · depth 25
• Order of Aut(E) equals 2 wₚ(j) WeierstrassCurve.natCard_stabilizer_variableChange_eq_two_mul_jWidthChar 9 below · cited by 2 · depth 25
• A model automorphism ≠ ± 1 fixes at most three points WeierstrassCurve.card_le_three_of_forall_heq_vcInvFun 0 below · cited by 1 · depth 26
• Twelve automorphisms when j=0 in characteristic 3 WeierstrassCurve.natCard_stabilizer_variableChange_eq_twelve_of_j_eq_zero_of_charP_three 0 below · cited by 1 · depth 26
• In characteristic 2, j=0 gives 24 Weierstrass automorphisms WeierstrassCurve.natCard_stabilizer_variableChange_eq_twentyFour_of_j_eq_zero_of_charP_two 0 below · cited by 1 · depth 26
• Univariate division polynomials under a variable change WeierstrassCurve.eval_prePsi_variableChange 0 below · cited by 6 · depth 29
• Trace relation for the scalar by which an automorphism acts on an M-torsion point WeierstrassCurve.exists_trace_of_equivOfVariableChangeEq_symm_apply_eq_val_smul 24 below · cited by 1 · depth 29
• Root multiplicities of Φ_N(j(E),Y) count cyclic N-subgroups WeierstrassCurve.rootMultiplicity_map_modularPolynomial_j_eq_natCard_cyclicQuotientJ_eq 308 below · cited by 3 · depth 29
• Automorphisms of an elliptic curve satisfy a quadratic relation on points WeierstrassCurve.exists_int_transport_comp_sub_smul_add_eq_zero 22 below · cited by 1 · depth 30
• Splitting of the modular polynomial at every elliptic curve WeierstrassCurve.map_modularPolynomial_j_eq_finprod_X_sub_C_cyclicQuotientJ 307 below · cited by 1 · depth 30
• A universal Weierstrass curve with invertible discriminant WeierstrassCurve.exists_finiteType_universal_of_isUnit_discr 0 below · cited by 4 · depth 31
• Quadratic relation on points for automorphisms with j=1728 WeierstrassCurve.exists_int_transport_comp_sub_smul_add_eq_zero_of_j_eq_1728_of_two_ne_zero 4 below · cited by 1 · depth 31
• Quadratic relation on points for automorphisms of j=0 in characteristic 3 WeierstrassCurve.exists_int_transport_comp_sub_smul_add_eq_zero_of_j_eq_zero_of_charP_three 5 below · cited by 1 · depth 31
• Automorphisms of the j=0 curve in characteristic 2 satisfy a quadratic WeierstrassCurve.exists_int_transport_comp_sub_smul_add_eq_zero_of_j_eq_zero_of_charP_two 9 below · cited by 1 · depth 31
• Quadratic relation on points for automorphisms with j=0 WeierstrassCurve.exists_int_transport_comp_sub_smul_add_eq_zero_of_j_eq_zero_of_two_ne_zero 4 below · cited by 1 · depth 31
• Automorphisms of a Weierstrass model with two-element stabiliser act as pmid WeierstrassCurve.exists_int_transport_comp_sub_smul_add_eq_zero_of_natCard_stabilizer_eq_two 2 below · cited by 1 · depth 31
• Reduction of the cyclic quotient j-invariant WeierstrassCurve.residue_cyclicQuotientJ_eq_cyclicQuotientJ_map_reduceHom 72 below · cited by 3 · depth 31
• Point transport intertwines an automorphism with its conjugate WeierstrassCurve.equivOfVariableChangeEq_symm_conj_vcInvFun 1 below · cited by 4 · depth 32
• Automorphisms of y²+y=x³ in characteristic 2 WeierstrassCurve.exists_addMonoidHom_omega_i_j_vcInvFun_of_char_two 1 below · cited by 1 · depth 32
• Igusa monodromy: SL₂(ℤ/M) lies in the image WeierstrassCurve.exists_algEquiv_map_eq_zsmul_add_zsmul_of_transcendental_j 358 below · cited by 2 · depth 32
• Height at most 2 for the formal group of an elliptic curve WeierstrassCurve.exists_isUnit_nthSeries_eq_mul_X_pow_or_eq_mul_X_pow_mul 15 below · cited by 6 · depth 32
• Generator independence of the half-system x-coordinate polynomial WeierstrassCurve.prod_X_sub_C_coordsOrZero_nsmul_eq_of_zmultiples_eq 8 below · cited by 3 · depth 32
• Existence of the commutative Weierstrass formal group law WeierstrassCurve.exists_formalGroup_isComm_toPowerSeries_eq 2 below · cited by 9 · depth 33
• Commutative lift of widehatE₀ over W₀[[t]] with normalised q-series WeierstrassCurve.exists_isComm_lift_powerSeries_formalGroup_coeff_nthSeries_of_ne_two 29 below · cited by 4 · depth 33
• Roots of preΨ'ₙ are abscissae of n-torsion points outside E[2] WeierstrassCurve.exists_nonsingular_nsmul_eq_zero_and_two_nsmul_ne_zero_of_eval_prePsi_eq_zero 2 below · cited by 2 · depth 33
• Good integral model from integral j and level-ℓ data WeierstrassCurve.exists_variableChange_smul_eq_map_of_isLevelPStructure_of_jOfUnit_mem_range 19 below · cited by 2 · depth 33
• Cyclic generator-kernel polynomial of a point of order p^k WeierstrassCurve.isCyclicGenKernel_prod_X_sub_C_coordsOrZero_nsmul_of_addOrderOf_eq_pow 8 below · cited by 2 · depth 33
• Supersingular j-invariant forces formal height two WeierstrassCurve.isDrinfeldBasisAdic_bot_zero_zero_of_map_j_mem_ssJSet 43 below · cited by 3 · depth 33
• Order-two point gives a degree-one kernel polynomial WeierstrassCurve.isTwoKernel_X_sub_C_coordsOrZero_of_addOrderOf_eq_two 1 below · cited by 2 · depth 33
• Unit 2y+a₁x+a₃ at roots of odd division polynomials WeierstrassCurve.isUnit_two_mul_add_a1_mul_add_a3_of_eval_prePsi_eq_zero_of_odd 2 below · cited by 2 · depth 33
• Multiplication by q in characteristic q has order at most q² WeierstrassCurve.nthSeries_ne_zero_and_not_X_pow_dvd_of_charP 8 below · cited by 1 · depth 33
• Division polynomials form a divisibility sequence WeierstrassCurve.prePsi_dvd_prePsi_of_dvd 1 below · cited by 8 · depth 33
• Separability of even division polynomials preΨ'ₙ WeierstrassCurve.separable_prePsi_of_isUnit_of_even 2 below · cited by 5 · depth 33
• Integral j forces Δ ∣ a³ and Δ ∣ b² WeierstrassCurve.discr_dvd_pow_of_jOfUnit_mem_range_short 0 below · cited by 1 · depth 34
• The X^q-coefficient of [q] equals the Hasse invariant WeierstrassCurve.exists_coeff_nthSeries_eq_mul_hasseInvariant 21 below · cited by 11 · depth 34
• Base change of an Igusa-type factorisation of [q] WeierstrassCurve.exists_formalGroup_toPowerSeries_eq_formalGroupLawFixed_map_and_nthSeries_eq_X_mul_map_mul_map 2 below · cited by 4 · depth 34
• Generic point of the formal group law is the sum of coordinate generic points WeierstrassCurve.exists_genericPoint_formalGroupLawFixed_eq_add 0 below · cited by 2 · depth 34
• Commutative lift over W₀llbracket trrbracket with unit first-order q-series coefficient WeierstrassCurve.exists_isComm_lift_powerSeries_formalGroup_coeff_nthSeries 30 below · cited by 4 · depth 34
• Shape [q]=u· Xⁿ is invariant under Weierstrass coordinate change WeierstrassCurve.exists_isUnit_nthSeries_eq_mul_X_npow_of_variableChange 8 below · cited by 4 · depth 34
• Supersingular curves admit a deformation moving the q-th [q]-coefficient WeierstrassCurve.exists_map_fstHom_eq_and_snd_coeff_nthSeries_ne_zero_of_ne_two 28 below · cited by 2 · depth 34
• Deformation over W₀[[X]] of a supersingular curve with monomial j WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_X_pow_of_five_le 33 below · cited by 2 · depth 34
• Short integral model over the fraction field of a domain WeierstrassCurve.exists_variableChange_smul_eq_map_short_of_isUnit_two_three 0 below · cited by 1 · depth 34
• Commutativity of the Weierstrass formal group law WeierstrassCurve.formalGroupLawFixed_comm_of_commRing 1 below · cited by 13 · depth 34
• Base change of the Weierstrass formal group law WeierstrassCurve.formalW_map_and_formalGroupLawFixed_map 0 below · cited by 46 · depth 34
• Supersingular j-invariant forces formal height two WeierstrassCurve.isDrinfeldBasisAdic_bot_zero_zero_of_map_j_mem_ssJSet_of_prime 44 below · cited by 2 · depth 34
• Serre–Tate: ⋆-isomorphic formal groups force equal j-invariants WeierstrassCurve.jOfUnit_eq_jOfUnit_of_lawIso_of_isAdicComplete 46 below · cited by 1 · depth 34
• Integrality of division-polynomial roots when n is invertible WeierstrassCurve.mem_range_algebraMap_of_equation_of_eval_prePsi_eq_zero 0 below · cited by 3 · depth 34
• Variable changes fixing W match invertible rational automorphisms WeierstrassCurve.natCard_variableChange_smul_eq_subtype_eq_natCard_rationalAut_subtype 5 below · cited by 1 · depth 34
• Linear coefficient of the change-of-parameter series is u WeierstrassCurve.coeff_one_variableChangeSeries 0 below · cited by 5 · depth 35
• Naturality of the cyclic-quotient j-invariant under field maps WeierstrassCurve.cyclicQuotientJ_map_eq_apply_cyclicQuotientJ_of_isAlgClosed 1 below · cited by 6 · depth 35
• Rationality of j(E/H) for Galois-stable cyclic H WeierstrassCurve.cyclicQuotientJ_mem_range_algebraMap_of_forall_map_eq 309 below · cited by 1 · depth 35
• Residue of [q]_F is a unit times X^{q^2} WeierstrassCurve.exists_isUnit_map_residue_nthSeries_eq_mul_X_pow_of_isDrinfeldBasisAdic_zero 2 below · cited by 1 · depth 35
• Laurent frame for the Weierstrass formal group and its invariant differential WeierstrassCurve.exists_laurent_frame_invDiff_mul_eq_derivative 9 below · cited by 2 · depth 35
• Deformation moving the Z^q-coefficient of [q] WeierstrassCurve.exists_map_fstHom_eq_and_snd_coeff_nthSeries_ne_zero 29 below · cited by 1 · depth 35
• First-order deformation with non-zero Hasse-invariant derivative WeierstrassCurve.exists_map_fstHom_eq_and_snd_hasseInvariant_ne_zero 4 below · cited by 5 · depth 35
• Monomial j universal deformation at a supersingular point, case j=1728 WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_X_pow_of_five_le_of_j_eq_1728 26 below · cited by 1 · depth 35
• Universal monomial-j deformation at a supersingular point, case j=0 WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_X_pow_of_five_le_of_j_eq_zero 26 below · cited by 1 · depth 35
• Supersingular deformation with monomial j when j(E₀)≠ 0,1728 WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_X_pow_of_five_le_of_j_ne_zero_of_j_ne 30 below · cited by 1 · depth 35
• Universal Weierstrass lift of a supersingular curve over W₀[[t]] WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_eval 37 below · cited by 1 · depth 35
• Rigidity of Weierstrass lifts over an Artinian local ring WeierstrassCurve.exists_variableChange_map_eq_one_and_smul_eq_of_lawIso_of_isArtinianRing 45 below · cited by 2 · depth 35
• Constant j forces infinitesimal triviality of Weierstrass deformations WeierstrassCurve.exists_variableChange_map_eq_one_and_smul_map_eq_of_snd_j_eq_zero 0 below · cited by 2 · depth 35
• Good integral model over a DVR from a Γ₁(ℓ)-point and integral j WeierstrassCurve.exists_variableChange_smul_eq_map_of_isGamma1Point_of_jOfUnit_mem_range 21 below · cited by 2 · depth 35
• Kernel polynomial of a rational point of odd prime order WeierstrassCurve.isCyclicKernel_kernelPolynomial_oddOrderSummingSet 6 below · cited by 1 · depth 35
• Serre–Tate: strictly isomorphic formal groups give equal j WeierstrassCurve.jOfUnit_eq_jOfUnit_of_lawIso_of_isAdicComplete_of_prime 47 below · cited by 1 · depth 35
• Variable change series is an isomorphism of formal group laws WeierstrassCurve.coeff_one_variableChangeSeries_and_subst_formalGroupLawFixed 4 below · cited by 4 · depth 36
• Potential good reduction over a DVR extension for integral j WeierstrassCurve.exists_dvr_extension_variableChange_smul_eq_map_of_jOfUnit_mem_range 11 below · cited by 1 · depth 36
• Serre–Tate lifting: formal group lifts come from Weierstrass lifts WeierstrassCurve.exists_map_eq_and_lawIso_of_isBaseChange_formalGroup_of_isArtinianRing 51 below · cited by 1 · depth 36
• Transport of the universal-family package along a variable change WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_X_pow_of_coeff_hasseInvariant_map_variableChange 24 below · cited by 3 · depth 36
• Characteristic three: universal deformation of a supersingular curve WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_eval_of_eq_three 24 below · cited by 1 · depth 36
• Characteristic 2 supersingular lift with distinguished j-polynomial WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_eval_of_eq_two 2 below · cited by 1 · depth 36
• One induction step of Serre–Tate uniqueness of lifts WeierstrassCurve.exists_variableChange_map_eq_one_and_map_smul_eq_map_pow_succ_of_lawIso 44 below · cited by 1 · depth 36
• Formal-group isomorphism yields a variable change over an Artinian local ring WeierstrassCurve.exists_variableChange_map_eq_one_and_smul_eq_of_lawIso_of_isArtinianRing_of_prime 46 below · cited by 2 · depth 36
• Laurent frame at the origin of a Weierstrass curve WeierstrassCurve.laurentFrame_wUnitFactor 0 below · cited by 1 · depth 36
• Formal invariant differential equals dx/(2y+a₁x+a₃) in the Laurent frame WeierstrassCurve.ofPowerSeries_invDiff_mul_eq_derivative_laurentFrame 7 below · cited by 1 · depth 36
• Abscissae of exact order p^k are stable under [a], p ∤ a WeierstrassCurve.eval_Phi_div_PsiSq_eq_zero_of_prePsi_pow_eq_mul_of_eval_eq_zero 8 below · cited by 1 · depth 37
• Unique lifting of affine 2-torsion along nilpotent thickenings WeierstrassCurve.existsUnique_equation_two_torsion_map_eq_of_surjective_of_ker_pow_eq_bot 0 below · cited by 1 · depth 37
• Invariance of [q]=u X^q under Weierstrass variable change WeierstrassCurve.exists_isUnit_nthSeries_eq_mul_X_pow_of_variableChange 8 below · cited by 2 · depth 37
• Base step of Serre–Tate lifting modulo 𝔪_T WeierstrassCurve.exists_lift_lawIso_quotient_maximalIdeal_pow_one_of_isBaseChange 2 below · cited by 1 · depth 37
• Serre–Tate lifting step: from 𝔪ⁿ to 𝔪ⁿ⁺¹ WeierstrassCurve.exists_lift_lawIso_quotient_maximalIdeal_pow_succ_of_exists 48 below · cited by 1 · depth 37
• Descending a lift from T/𝔪^N when 𝔪^N=0 WeierstrassCurve.exists_map_eq_and_lawIso_of_exists_quotient_of_pow_eq_bot 2 below · cited by 1 · depth 37
• Serre–Tate existence of Weierstrass lifts of formal groups WeierstrassCurve.exists_map_eq_and_lawIso_of_isBaseChange_formalGroup_of_isArtinianRing_of_prime 52 below · cited by 1 · depth 37
• From an explicit q-adic family to the formal-group package WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_X_pow_of_coeff_hasseInvariant_map 22 below · cited by 1 · depth 37
• Deformation package from a distinguished j-expansion WeierstrassCurve.exists_powerSeries_lift_coeff_nthSeries_sub_mul_X_mem_span_and_jOfUnit_sub_eq_mul_eval_of_coeff_hasseInvariant_map 22 below · cited by 1 · depth 37
• Serre–Tate uniqueness: improving a variable change from 𝔪ⁿ to 𝔪ⁿ⁺¹ WeierstrassCurve.exists_variableChange_map_eq_one_and_map_smul_eq_map_pow_succ_of_lawIso_of_prime 45 below · cited by 1 · depth 37
• Formal-group isomorphisms of congruent lifts come from variable changes WeierstrassCurve.exists_variableChange_map_mk_eq_one_and_smul_eq_of_lawIso_of_mul_maximalIdeal_eq_bot 32 below · cited by 2 · depth 37
• Invariant differential of the Weierstrass formal group WeierstrassCurve.formalW_mul_eq_sub_mul_subst_pderiv_formalGroupLawFixed 5 below · cited by 1 · depth 37
• Base change of the variable-change denominator and series WeierstrassCurve.variableChangeDenom_map_and_variableChangeSeries_map 0 below · cited by 6 · depth 37
• Identity variable change gives the series X WeierstrassCurve.variableChangeSeries_one 0 below · cited by 2 · depth 37
• No first-order automorphisms of an elliptic Weierstrass curve WeierstrassCurve.eq_zero_of_firstOrderVariableChange_eq_zero 0 below · cited by 5 · depth 38
• Universal linear form for the variation of [q] in coefficient q WeierstrassCurve.exists_forall_coeff_nthSeries_sub_eq_sum_of_mul_maximalIdeal_eq_bot 2 below · cited by 3 · depth 38
• Serre–Tate existence, base step modulo 𝔪_T WeierstrassCurve.exists_lift_lawIso_quotient_maximalIdeal_pow_one_of_isBaseChange_of_prime 2 below · cited by 1 · depth 38
• Serre–Tate lifting step: from 𝔪ⁿ to 𝔪ⁿ⁺¹ WeierstrassCurve.exists_lift_lawIso_quotient_maximalIdeal_pow_succ_of_exists_of_prime 49 below · cited by 1 · depth 38
• A non-trivial first-order deformation of a Weierstrass curve WeierstrassCurve.exists_map_eq_and_forall_variableChange_smul_map_ne 0 below · cited by 2 · depth 38
• Transport of a formal-group lift across 𝔪^N = 0 WeierstrassCurve.exists_map_eq_and_lawIso_of_exists_quotient_of_pow_eq_bot_of_prime 2 below · cited by 1 · depth 38
• Realising a formal-group lift by a Weierstrass lift WeierstrassCurve.exists_map_mk_eq_and_lawIso_of_lawIso_quotient_of_mul_maximalIdeal_eq_bot 47 below · cited by 1 · depth 38
• Kernel polynomial of ⟨ P⟩ divides ψ_ℓ WeierstrassCurve.exists_smul_abscissa_prod_X_sub_C_dvd_prePsi 10 below · cited by 1 · depth 38
• Star-isomorphisms of lifts come from variable changes mod I WeierstrassCurve.exists_variableChange_map_mk_eq_one_and_smul_eq_of_lawIso_of_mul_maximalIdeal_eq_bot_of_prime 33 below · cited by 1 · depth 38
• First-order Weierstrass deformations form a line WeierstrassCurve.exists_variableChange_smul_map_eq_of_forall_variableChange_smul_ne 1 below · cited by 2 · depth 38
• Reducedness of R[X]/(Ψ₂²) when 2 and Δ are units WeierstrassCurve.isReduced_adjoinRoot_Psi2Sq_of_isUnit 0 below · cited by 1 · depth 38
• Primitive ℓ^k-division points: [ℓ^{k-1}] has ℓ-torsion abscissa WeierstrassCurve.isUnit_eval_PsiSq_and_eval_prePsi_smul_abscissa_eq_zero_of_eval_primitive_eq_zero 8 below · cited by 1 · depth 38
• #Aut(E) divides 4 when j(E)=1728 WeierstrassCurve.natCard_stabilizer_variableChange_dvd_four_of_j_eq_1728 2 below · cited by 1 · depth 38
• Stabiliser order divides 6 when j(E)=0 WeierstrassCurve.natCard_stabilizer_variableChange_dvd_six_of_j_eq_zero 2 below · cited by 1 · depth 38
• Formal branch at the inverse point: w(i(T))(1-a₁T-a₃w)= -w WeierstrassCurve.subst_fgInv_formalW_mul_fgInvDenom 0 below · cited by 1 · depth 38
• The slope series at X₀ = 0 is w(T)/T WeierstrassCurve.subst_zero_X_fgSlope 0 below · cited by 1 · depth 38
• The X₀-derivative of the slope series at X₀=0 WeierstrassCurve.subst_zero_X_pderiv_fgSlope 0 below · cited by 1 · depth 38
• Realising prescribed q-th coefficients of [q] by lifting WeierstrassCurve.exists_map_mk_eq_and_coeff_nthSeries_sub_eq_of_mul_maximalIdeal_eq_bot 32 below · cited by 2 · depth 39
• Lifting a mod-I isomorphism to a Weierstrass formal group WeierstrassCurve.exists_map_mk_eq_and_lawIso_of_lawIso_quotient_of_mul_maximalIdeal_eq_bot_of_prime 48 below · cited by 1 · depth 39
• Every element of I realised by a q-series coefficient shift WeierstrassCurve.exists_map_mk_eq_and_coeff_nthSeries_sub_eq_of_mul_maximalIdeal_eq_bot_of_prime 33 below · cited by 1 · depth 40
• Frobenius twist over the dual numbers is constant WeierstrassCurve.map_frobenius_dualNumber_eq_map_map_map 0 below · cited by 1 · depth 40
• Triangular coordinate-ring maps come from variable changes WeierstrassCurve.exists_variableChange_smul_eq_of_algHom_coordinateRing_triangular 0 below · cited by 1 · depth 41

WeierstrassCurve.Affine 135

• Finiteness of the point group of a Weierstrass curve over a finite field WeierstrassCurve.Affine.Point.finite_of_finite_field 0 below · cited by 1 · depth 6
• Galois descent for points of a Weierstrass curve WeierstrassCurve.Affine.Point.exists_baseChange_eq_of_forall_smul_eq 0 below · cited by 1 · depth 7
• Torsion bound for nonsingular points of a nodal cubic WeierstrassCurve.Affine.Point.finite_and_ncard_torsion_le_of_isNode 0 below · cited by 1 · depth 7
• Odd n-torsion iff preΨ'ₙ vanishes at the abscissa WeierstrassCurve.Affine.Point.nsmul_some_eq_zero_iff_eval_prePsi 1 below · cited by 79 · depth 7
• Coordinate ring of an elliptic curve is Dedekind WeierstrassCurve.Affine.CoordinateRing.isDedekindDomain 0 below · cited by 53 · depth 8
• nP=O if and only if ψₙ(P)=0 WeierstrassCurve.Affine.Point.smul_some_eq_zero_iff 0 below · cited by 51 · depth 8
• Invariant function with divisor on an [n]-fibre forces T=0 WeierstrassCurve.Affine.eq_zero_of_forall_transEquiv_eq 13 below · cited by 2 · depth 8
• Existence of a centred genus-one place gate with Abel's theorem WeierstrassCurve.Affine.exists_genusOnePlaceGate_isCentred_and_abelTheorem 2 below · cited by 13 · depth 8
• Translation invariance of the Weil function g_T up to a constant WeierstrassCurve.Affine.exists_transEquiv_weilFun_eq 20 below · cited by 7 · depth 8
• Principal divisors on a Weierstrass curve have degree zero WeierstrassCurve.Affine.hasPrincipalDivisors_functionField 25 below · cited by 27 · depth 8
• Valuations along the multiplication-by-n pull-back of functions WeierstrassCurve.Affine.valuation_mulPull_le_of_ne_zero 4 below · cited by 3 · depth 8
• Valuation of the Weil function g_T at an affine place WeierstrassCurve.Affine.valuation_weilFun 5 below · cited by 6 · depth 8
• Multiplicativity of e₀ in the first variable WeierstrassCurve.Affine.weilPairing0_add_left 21 below · cited by 9 · depth 8
• Additivity of e₀(S,·) in the second variable WeierstrassCurve.Affine.weilPairing0_add_right 21 below · cited by 7 · depth 8
• Galois equivariance of the Weil pairing e₀ WeierstrassCurve.Affine.weilPairing0_galois 23 below · cited by 2 · depth 8
• The pairing e₀ is trivial on the diagonal: e₀(T,T)=1 WeierstrassCurve.Affine.weilPairing0_self 19 below · cited by 7 · depth 8
• Maximality of the point ideal at an affine point WeierstrassCurve.Affine.CoordinateRing.XYIdeal_isMaximal 0 below · cited by 18 · depth 9
• Nonvanishing of the ideals (X-x, Y-y) in R[W] WeierstrassCurve.Affine.CoordinateRing.XYIdeal_ne_bot 0 below · cited by 18 · depth 9
• Nonzero primes of a Weierstrass coordinate ring are points WeierstrassCurve.Affine.CoordinateRing.exists_eq_XYIdeal 0 below · cited by 16 · depth 9
• Everywhere trivial valuation forces a constant function WeierstrassCurve.Affine.FunctionField.exists_eq_algebraMap_of_valuation_eq_one 0 below · cited by 5 · depth 9
• Uniqueness of the centred genus-one place gate WeierstrassCurve.Affine.GenusOnePlaceGate.ext_of_isCentred 5 below · cited by 3 · depth 9
• No p-torsion on the nonsingular locus of a nodal cubic WeierstrassCurve.Affine.Point.eq_zero_of_prime_smul_eq_zero_of_isNode 0 below · cited by 2 · depth 9
• Divisibility of E(K) for K algebraically closed WeierstrassCurve.Affine.Point.exists_zsmul_eq_of_isAlgClosed 0 below · cited by 12 · depth 9
• Universal two-coordinate multiplication-by-n formula for Weierstrass curves WeierstrassCurve.Affine.Point.exists_zsmul_some_eq_some_baseChange 0 below · cited by 1 · depth 9
• Irreducibility of mod-n torsion transfers along equivariant isomorphisms WeierstrassCurve.Affine.Point.galoisRepIsIrreducible_iff_of_linearEquiv 0 below · cited by 1 · depth 9
• Integrality of x for odd torsion prime to the residue characteristic WeierstrassCurve.Affine.Point.mem_valuationSubring_of_nsmul_eq_zero 2 below · cited by 1 · depth 9
• Inertia fixes ℓ-torsion points of integral level WeierstrassCurve.Affine.Point.smul_eq_self_of_mem_inertiaSubgroupIn_of_level 0 below · cited by 1 · depth 9
• Inertia fixes node-reducing 2-torsion of integral level WeierstrassCurve.Affine.Point.smul_eq_self_of_two_torsion_of_mem_inertiaSubgroupIn_of_level 1 below · cited by 1 · depth 9
• 2P=O iff x is a root of Ψ₂² WeierstrassCurve.Affine.Point.two_smul_some_eq_zero_iff 0 below · cited by 17 · depth 9
• Abscissa of nP via division polynomials: x(nP)=Φₙ(x)/Ψₙ²(x) WeierstrassCurve.Affine.Point.zsmul_some_eq_some_div 0 below · cited by 41 · depth 9
• At the place of the origin, x is not integral WeierstrassCurve.Affine.algebraMap_mk_C_X_notMem_toValuationSubring_placeOfPoint_zero 5 below · cited by 18 · depth 9
• Division polynomial identity ψₙ(x,y)²=Ψ²ₙ(x) on the curve WeierstrassCurve.Affine.evalEval_psi_sq 0 below · cited by 44 · depth 9
• Galois conjugation of the Weil function up to a constant WeierstrassCurve.Affine.exists_map_weilFun_eq_mul_weilFun_smul 10 below · cited by 1 · depth 9
• Pull-back by [n] has index at most n² WeierstrassCurve.Affine.finrank_fieldRange_mulPull_le 8 below · cited by 2 · depth 9
• Kernel of a pushforward point map has order the degree WeierstrassCurve.Affine.natCard_ker_pointMapOfPushforward_eq_finrankAlong 37 below · cited by 11 · depth 9
• Centred gate: place of an affine point is the (x,y)-adic place WeierstrassCurve.Affine.placeOfPoint_some_eq_ofHeightOneSpectrum 2 below · cited by 20 · depth 9
• Valuation of the translated Weil function at finite places WeierstrassCurve.Affine.valuation_transEquiv_weilFun 16 below · cited by 3 · depth 9
• Divisor of `weilNum`: simple zeros on the [n]-fibre over T WeierstrassCurve.Affine.valuation_weilNum 4 below · cited by 5 · depth 9
• Nonvanishing of the Weil function g_T for T ∈ E[n] WeierstrassCurve.Affine.weilFun_ne_zero 6 below · cited by 8 · depth 9
• No nonzero multiple of the generic point is constant WeierstrassCurve.Affine.zsmul_genericPoint_good 1 below · cited by 2 · depth 9
• Principality of prod 𝔪_{P_i}^{mᵢ} versus sum mᵢ Pᵢ = O WeierstrassCurve.Affine.CoordinateRing.isPrincipal_prod_XYIdeal_zpow_iff 0 below · cited by 1 · depth 10
• Degree of the norm equals the sum of local multiplicities WeierstrassCurve.Affine.CoordinateRing.natDegree_norm_eq_finsum_count 0 below · cited by 3 · depth 10
• The function field of a Weierstrass curve is K(x,y) WeierstrassCurve.Affine.FunctionField.adjoin_X_Y_eq_top 0 below · cited by 1 · depth 10
• Valuation rings of K(W) containing x are finite places WeierstrassCurve.Affine.FunctionField.exists_eq_valuationSubring_of_X_mem 0 below · cited by 4 · depth 10
• Descent: 2E(ℚ) of finite index implies E(ℚ) finitely generated WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex 0 below · cited by 1 · depth 10
• Galois-equivariant group isomorphism restricts to n-torsion WeierstrassCurve.Affine.Point.exists_linearEquiv_torsionBy_of_addEquiv 0 below · cited by 1 · depth 10
• Cyclic kernel of order N forces Φ_N(j(E),j(E'))=0 WeierstrassCurve.Affine.eval_modularPolynomial_map_j_eq_zero_of_isAddCyclic_ker_pointMapOfPushforward 91 below · cited by 5 · depth 10
• Fibres of multiplication by n are finite WeierstrassCurve.Affine.fibSet_finite 1 below · cited by 4 · depth 10
• Fibres of [n] on an elliptic curve have n² points WeierstrassCurve.Affine.ncard_fibSet 3 below · cited by 2 · depth 10
• Pushforward map on points of an elliptic curve is surjective WeierstrassCurve.Affine.pointMapOfPushforward_surjective 5 below · cited by 4 · depth 10
• Translation by S moves the place at infinity to -S WeierstrassCurve.Affine.valuation_placeOf_neg_transEquiv_algebraMap 2 below · cited by 1 · depth 10
• Galois equivariance of the valuations v_P on K(E) WeierstrassCurve.Affine.valuation_placeOf_smul_of_algEquiv 0 below · cited by 1 · depth 10
• Translation pull-back does not decrease order of vanishing WeierstrassCurve.Affine.valuation_transEquiv_le 0 below · cited by 2 · depth 10
• Translation pull-back carries vanishing at 2S to S WeierstrassCurve.Affine.valuation_transEquiv_le_self 0 below · cited by 1 · depth 10
• Non-vanishing of the Weil numerator at n-torsion WeierstrassCurve.Affine.weilNum_ne_zero 5 below · cited by 4 · depth 10
• The place at infinity of a Weierstrass function field WeierstrassCurve.Affine.FunctionField.eq_valuationSubring_of_X_not_mem 0 below · cited by 5 · depth 11
• The valuation at infinity on a Weierstrass function field WeierstrassCurve.Affine.FunctionField.exists_valuation_eq_exp_natDegree_norm 0 below · cited by 3 · depth 11
• Non-integral j forces endomorphisms to be integer multiplications WeierstrassCurve.Affine.IsogenyEndDatum.exists_forall_pointEnd_eq_zsmul_of_not_isIntegral_j 169 below · cited by 1 · depth 11
• Kernel size equals degree of a separable abscissa map WeierstrassCurve.Affine.Point.card_ker_eq_max_natDegree 0 below · cited by 2 · depth 11
• Parallelogram law for degrees of abscissa maps WeierstrassCurve.Affine.Point.natDegree_parallelogram_law 0 below · cited by 3 · depth 11
• x([n]P) ψₙ(P)²=φₙ(P) for affine points WeierstrassCurve.Affine.Point.zsmul_x_mul_psi_sq 1 below · cited by 23 · depth 11
• Base change of a cyclic kernel of order N WeierstrassCurve.Affine.exists_algHom_baseChange_of_isAddCyclic_ker_pointMapOfPushforward 56 below · cited by 1 · depth 11
• Existence of a centred genus-one place gate with Abel's theorem WeierstrassCurve.Affine.exists_genusOnePlaceGate_isCentred_abelTheorem 11 below · cited by 7 · depth 11
• Cyclic degree-N function-field seams descend to countable subfields WeierstrassCurve.Affine.exists_intermediateField_countable_map_eq_of_isAddCyclic_ker_pointMapOfPushforward 59 below · cited by 1 · depth 11
• Norm formula along isogeny endomorphism data in characteristic zero WeierstrassCurve.Affine.forall_normFormulaAlong_of_isAlgClosed_of_charZero 31 below · cited by 2 · depth 11
• Cyclic kernel and its order transport along function-field isomorphisms WeierstrassCurve.Affine.isAddCyclic_ker_pointMapOfPushforward_of_algEquiv_conj 55 below · cited by 1 · depth 11
• Point ideals of a Weierstrass curve determine the point WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq_XYIdeal_iff 0 below · cited by 1 · depth 12
• Degree-N endomorphism forces Φ_N(j(E),j(E))=0 WeierstrassCurve.Affine.IsogenyEndDatum.aeval_j_diag_eq_zero_of_finrankAlong_eq 87 below · cited by 2 · depth 12
• Nonzero elements of the isogeny subring come from isogeny data WeierstrassCurve.Affine.IsogenyEndDatum.exists_pointEnd_eq_of_mem_isogenyEndSubring 41 below · cited by 4 · depth 12
• Non-integral isogeny endomorphism forces an imaginary quadratic degree form WeierstrassCurve.Affine.IsogenyEndDatum.exists_sq_lt_four_mul_and_forall_exists_finrankAlong_eq 51 below · cited by 2 · depth 12
• Factoring an isogeny through one with smaller kernel WeierstrassCurve.Affine.IsogenyHomDatum.exists_pointHom_comp_eq_of_ker_le_of_isCentred 52 below · cited by 3 · depth 12
• Additivity of the variable-change map on points WeierstrassCurve.Affine.Point.vcInvFun_add 0 below · cited by 119 · depth 12
• y([n]P) ψₙ(P)³=ωₙ(P) for affine points WeierstrassCurve.Affine.Point.zsmul_y_mul_psi_cube 1 below · cited by 5 · depth 12
• The function field is generated over F(x) by y WeierstrassCurve.Affine.adjoin_yCoord_eq_top 0 below · cited by 4 · depth 12
• Places of a Weierstrass function field over ̄ F have degree one WeierstrassCurve.Affine.deg_ofHeightOneSpectrum_eq_one 0 below · cited by 2 · depth 12
• Unique degree-one place at infinity of a Weierstrass function field WeierstrassCurve.Affine.exists_infinitePlace_deg_eq_one 2 below · cited by 2 · depth 12
• The function field of a Weierstrass curve is finite over F(x) WeierstrassCurve.Affine.finiteDimensional_ratFunc_functionField 1 below · cited by 4 · depth 12
• Principal divisors have degree zero on an elliptic curve WeierstrassCurve.Affine.hasPrincipalDivisors_of_isAlgClosed 9 below · cited by 10 · depth 12
• Cyclic kernel of order N descends along base change WeierstrassCurve.Affine.isAddCyclic_ker_pointMapOfPushforward_of_baseChange_algHom 56 below · cited by 1 · depth 12
• Existence of dual endomorphism data with norm the degree WeierstrassCurve.Affine.IsogenyEndDatum.exists_dualEndData_dual_mem_and_norm_eq_finrankAlong 44 below · cited by 1 · depth 13
• Transcendental j forces every isogeny endomorphism to be an integer WeierstrassCurve.Affine.IsogenyEndDatum.exists_forall_pointEnd_eq_zsmul_of_transcendental_j 169 below · cited by 3 · depth 13
• Isogeny-induced endomorphisms of E(F) are closed under addition WeierstrassCurve.Affine.IsogenyEndDatum.exists_pointEnd_eq_add 40 below · cited by 1 · depth 13
• Point map of an isogeny datum: restriction minus value at O WeierstrassCurve.Affine.IsogenyHomDatum.pointHom_apply_eq_sub 0 below · cited by 1 · depth 13
• Collinear points (x,y),(ω x,y),(ω² x,y) on y²=x³+B WeierstrassCurve.Affine.Point.some_add_some_eq_neg_some_of_pow_three_eq_one 0 below · cited by 3 · depth 13
• The points (0,y) on y²=x³+B are flexes WeierstrassCurve.Affine.Point.some_zero_add_self_eq_neg_of_a6_model 0 below · cited by 3 · depth 13
• Affine point is 2-torsion iff y = negY(x,y) WeierstrassCurve.Affine.Point.two_nsmul_eq_zero_iff_Y_eq_negY 0 below · cited by 1 · depth 13
• Integral maps into K(E) determined by action on places WeierstrassCurve.Affine.algHom_ext_of_forall_restrictAlong_placeOfPoint_eq 38 below · cited by 1 · depth 13
• Translation by R as a function-field automorphism on places WeierstrassCurve.Affine.exists_algEquiv_restrictAlong_placeOfPoint_eq_add 38 below · cited by 1 · depth 13
• Base change of a finite self-embedding preserves its degree WeierstrassCurve.Affine.exists_algHom_functionField_baseChange_finrankAlong_eq 0 below · cited by 1 · depth 13
• Chord formulas on generic points specialise to the group law WeierstrassCurve.Affine.FunctionField.addX_addY_specialize_at_place 0 below · cited by 1 · depth 14
• Pointwise sum of two isogeny end data is realised WeierstrassCurve.Affine.IsogenyEndDatum.exists_restrictAlong_placeOfPoint_eq_add 38 below · cited by 1 · depth 14
• Point endomorphism of an isogeny datum equals h(P)-h(O) WeierstrassCurve.Affine.IsogenyEndDatum.pointEnd_apply_eq_sub 0 below · cited by 1 · depth 14
• Torsion point coordinates are integral over the base field WeierstrassCurve.Affine.Point.isIntegral_of_smul_eq_zero 2 below · cited by 3 · depth 14
• The variable change (-1,0,-a₁,-a₃) acts as negation on points WeierstrassCurve.Affine.Point.vcInvFun_neg_heq_neg 0 below · cited by 4 · depth 14
• Kernel rigidity for isogenies out of a curve with End=ℤ WeierstrassCurve.Affine.ker_pointMapOfPushforward_eq_of_j_eq_of_forall_pointEnd_eq_zsmul 65 below · cited by 2 · depth 14
• Vanishing of Ψₙ² at the x-coordinate of an n-torsion point WeierstrassCurve.Affine.Point.eval_psiSq_eq_zero_of_smul_eq_zero 1 below · cited by 10 · depth 15
• A place centred at (x,y) is the gate's place of (x,y) WeierstrassCurve.Affine.eq_placeOfPoint_some_of_XClass_mem_nonunits_of_YClass_mem_nonunits 5 below · cited by 2 · depth 15
• A variable change is determined by its map on points WeierstrassCurve.Affine.variableChange_eq_of_forall_equivOfVariableChangeEq_eq 0 below · cited by 2 · depth 16
• Surjectivity of the pushforward point map, separable case WeierstrassCurve.Affine.pointMapOfPushforward_surjective_of_separableAlong 5 below · cited by 3 · depth 17
• Equal-degree separable isogenies with nested kernels: isomorphic targets WeierstrassCurve.Affine.IsogenyHomDatum.exists_algEquiv_of_ker_le_of_finrankAlong_eq 69 below · cited by 1 · depth 18
• Separable isogenies factor through maps with smaller kernel WeierstrassCurve.Affine.IsogenyHomDatum.exists_pointHom_comp_eq_of_ker_le_of_separableAlong 67 below · cited by 2 · depth 18
• Isogeny datum: induced map is place restriction minus origin WeierstrassCurve.Affine.IsogenyHomDatum.pointHom_apply_eq_pointEquivPlace_sub 0 below · cited by 3 · depth 18
• Multiplication by n as an isogeny endomorphism datum WeierstrassCurve.Affine.exists_isogenyEndDatum_restrictAlong_placeOfPoint_eq_smul 28 below · cited by 1 · depth 18
• Isomorphism of function fields matching 𝒪 is a variable change WeierstrassCurve.Affine.exists_variableChange_forall_restrictAlong_placeOfPoint_eq_of_algEquiv 10 below · cited by 1 · depth 18
• Norm formula along every isogeny endomorphism datum over ̄ F WeierstrassCurve.Affine.forall_normFormulaAlong_of_isAlgClosed 46 below · cited by 3 · depth 18
• Kernel size of a separable isogeny equals its degree WeierstrassCurve.Affine.natCard_ker_pointMapOfPushforward_eq_finrankAlong_of_separableAlong 10 below · cited by 2 · depth 18
• An integral K-embedding into K(E) is determined by its action on places WeierstrassCurve.Affine.algHom_eq_of_forall_restrictAlong_placeOfPoint_eq 57 below · cited by 1 · depth 19
• Translation by a point as a function-field automorphism WeierstrassCurve.Affine.exists_algEquiv_forall_restrictAlong_placeOfPoint_eq_add 57 below · cited by 1 · depth 19
• Pushforward norm formula along isogeny endomorphisms in characteristic p WeierstrassCurve.Affine.forall_normFormulaAlong_of_isAlgClosed_of_charP_pos 21 below · cited by 1 · depth 19
• Principal divisors on a Weierstrass function field (separable case) WeierstrassCurve.Affine.hasPrincipalDivisors_functionField_of_two_ne_zero_or 27 below · cited by 1 · depth 19
• Smooth locus of the split node y²=x²(x+d²) is G_m WeierstrassCurve.Affine.Point.exists_addEquiv_nodeNormalForm_additive_units 0 below · cited by 2 · depth 20
• Integrality of torsion coordinates on a non-elliptic Weierstrass curve WeierstrassCurve.Affine.Point.isIntegral_of_smul_eq_zero_of_not_isElliptic 1 below · cited by 1 · depth 20
• Division polynomial φₙ evaluates to Φₙ(x) on the curve WeierstrassCurve.Affine.evalEval_phi 0 below · cited by 13 · depth 20
• Composition law for point transport along variable changes WeierstrassCurve.Affine.Point.vcInvFun_mul_heq 0 below · cited by 5 · depth 25
• The identity variable change transports each point to itself WeierstrassCurve.Affine.Point.vcInvFun_one_heq 0 below · cited by 5 · depth 25
• Non-degeneracy of the Weil pairing: trivial pairing forces T = O WeierstrassCurve.Affine.eq_zero_of_forall_weilPairing0_eq_one 35 below · cited by 5 · depth 29
• Invariance of the point-level Weil pairing under coordinate change WeierstrassCurve.Affine.weilPairing0_toPoint_variableChange 2 below · cited by 8 · depth 30
• Units of the affine coordinate ring are the nonzero constants WeierstrassCurve.Affine.CoordinateRing.isUnit_iff_eq_algebraMap 0 below · cited by 1 · depth 31
• Automorphism acting as ± 1 on ℓ-torsion, ℓ≡ 11 (mod 12) WeierstrassCurve.Affine.Point.some_variableChange_eq_or_eq_neg_of_smul_eq_self_of_mod_twelve_of_charP 3 below · cited by 3 · depth 31
• Presentation independence of the point-level Weil pairing WeierstrassCurve.Affine.weilPairing0_toPoint_eq_of_baseChange_eq 0 below · cited by 4 · depth 31
• Weil pairing of integral torsion points lies in a valuation subring WeierstrassCurve.Affine.exists_algebraMap_eq_weilPairing0_and_map_eq_weilPairing0_of_valuationSubring 30 below · cited by 1 · depth 32
• Weil pairing of a Katz level-ℓ structure is primitive WeierstrassCurve.Affine.isPrimitiveRoot_weilPairing0_toPoint_of_isLevelPStructure 44 below · cited by 3 · depth 32
• Weil pairing under an integral relabelling: eₙ((S,T)g)=eₙ(S,T)^{det g} WeierstrassCurve.Affine.weilPairing0_linComb_linComb_eq_zpow_det 24 below · cited by 4 · depth 32
• At most n² points killed by n when n is invertible WeierstrassCurve.Affine.Point.card_le_sq_of_forall_nsmul_eq_zero 2 below · cited by 1 · depth 33
• Integral Weil numerator along a valuation subring WeierstrassCurve.Affine.exists_smul_basis_eq_algebraMap_mul_weilNum_of_valuationSubring 16 below · cited by 1 · depth 33
• Roots of the reduced n-division polynomial WeierstrassCurve.Affine.Point.eval_prePsi_eq_zero_iff_smul_eq_zero_and_two_smul_ne_zero 5 below · cited by 5 · depth 34
• Galois-invariant torsion gives base-field-rational Weil pairing WeierstrassCurve.Affine.exists_algebraMap_eq_weilPairing0_of_forall_smul_eq 24 below · cited by 4 · depth 35
• Weil pairing commutes with embeddings of algebraically closed fields WeierstrassCurve.Affine.weilPairing0_map_algHom 25 below · cited by 2 · depth 35
• Transport of the cut-out condition under a variable change WeierstrassCurve.Affine.Point.cutOut_smul_of_cutOut_vcFun 1 below · cited by 2 · depth 36
• Base change of the Weil function along an F-embedding WeierstrassCurve.Affine.exists_map_weilFun_eq_mul_weilFun_map_of_algHom 10 below · cited by 1 · depth 36
• Base change of the function field along an F-algebra map WeierstrassCurve.Affine.exists_ringHom_functionField_baseChange_of_algHom 0 below · cited by 1 · depth 36
• Translation pull-back commutes with base change of scalars WeierstrassCurve.Affine.map_transEquiv_eq_transEquiv_map_of_algHom 0 below · cited by 1 · depth 36
• Base change of a function: valuations at old and new points WeierstrassCurve.Affine.valuation_placeOf_map_of_algHom 0 below · cited by 1 · depth 37
• Cut-out point generates a cyclic subgroup of order M' WeierstrassCurve.Affine.Point.zmultiples_eq_of_forall_isRoot_iff_of_addOrderOf_eq 0 below · cited by 2 · depth 38
• Dual-number points over an affine point form a line WeierstrassCurve.Affine.exists_ne_zero_forall_equation_dualNumber_iff 0 below · cited by 1 · depth 39

WeierstrassCurve.DrinfeldGlobal 164

• Drinfeld Γ(q)-bases are trivial without rational q-torsion WeierstrassCurve.DrinfeldGlobal.IsDrinfeldBasis.eq_one_of_forall_nsmul_eq_zero 3 below · cited by 10 · depth 28
• Existence of pinned global group laws and level transport WeierstrassCurve.DrinfeldGlobal.exists_groupLaws_levelTransport_isChordTangent_isOriginIdentity_isSectionTransport 111 below · cited by 39 · depth 28
• Existence of a chord–tangent group-law family pinned at the zero section WeierstrassCurve.DrinfeldGlobal.exists_groupLaws_isChordTangent_isOriginIdentity_one_eq_zeroSect 83 below · cited by 1 · depth 29
• Existence of a section-pinned level transport datum WeierstrassCurve.DrinfeldGlobal.exists_levelTransport_isSectionTransport 39 below · cited by 1 · depth 29
• Global Drinfeld basis predicate equals relative one at id WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_iff_isDrinfeldBasisOver_id 0 below · cited by 10 · depth 29
• A point of order M' whose multiples are cut out by the Γ₀-component WeierstrassCurve.DrinfeldGlobal.exists_addOrderOf_eq_forall_isRoot_level_fst_of_raw_rigidDataPow 5 below · cited by 6 · depth 30
• Aligning raw rigid data with equal Γ₀(M')-moduli class WeierstrassCurve.DrinfeldGlobal.exists_variableChange_curve_eq_level_fst_eq_of_moduliPoint_mk_eq_of_raw_rigidDataPow 2 below · cited by 1 · depth 30
• Proj of a coefficient homomorphism restricts to the Z-chart WeierstrassCurve.DrinfeldGlobal.exists_zChartIota_comp_projMap_eq_specMap_comp_zChartIota 0 below · cited by 9 · depth 30
• Drinfeld Γ(q)-level structures transport along changes of variables WeierstrassCurve.DrinfeldGlobal.isLevel_act_of_comp_projMap_eq 29 below · cited by 1 · depth 30
• Drinfeld level-q structures descend along base change of pinned pairs WeierstrassCurve.DrinfeldGlobal.isLevel_map_of_comp_projMap_eq 32 below · cited by 1 · depth 30
• Proj of a Weierstrass model is cartesian over Spec f WeierstrassCurve.DrinfeldGlobal.isPullback_projMap_of_isCoefficientHom 3 below · cited by 47 · depth 30
• Unit section equals zero section after base change WeierstrassCurve.DrinfeldGlobal.one_eq_zeroSect_of_one_comp_projMap_eq_of_isPullback 2 below · cited by 4 · depth 30
• Commutativity of origin-pinned relative group laws on Weierstrass models WeierstrassCurve.DrinfeldGlobal.GroupLaws.mul_comm_of_isOriginIdentity 99 below · cited by 16 · depth 31
• Relabelling a Drinfeld basis by a matrix with unit determinant mod q WeierstrassCurve.DrinfeldGlobal.IsDrinfeldBasis.zlinComb_zlinComb_of_isUnit_det 0 below · cited by 13 · depth 31
• Relabelling commutes with variable-change transport of Drinfeld pairs WeierstrassCurve.DrinfeldGlobal.LevelTransport.act_relabel_eq_relabel_act 24 below · cited by 7 · depth 31
• Negation variable change transports to group-law inversion WeierstrassCurve.DrinfeldGlobal.LevelTransport.exists_act_neg_comp_eqToHom_eq_inv 85 below · cited by 3 · depth 31
• Base change commutes with GL₂(ℤ)-relabelling of raw Drinfeld pairs WeierstrassCurve.DrinfeldGlobal.LevelTransport.map_relabel_eq_relabel_map 24 below · cited by 17 · depth 31
• Drinfeld basis divisor transports along a coefficient homomorphism WeierstrassCurve.DrinfeldGlobal.comap_basisDivisorOver_eq_basisDivisor 5 below · cited by 2 · depth 31
• Transport of the q-torsion ideal along a coefficient map WeierstrassCurve.DrinfeldGlobal.comap_torsionIdealOver_eq_torsionIdeal 4 below · cited by 2 · depth 31
• Origin-chart sections are compatible under Proj base change WeierstrassCurve.DrinfeldGlobal.comp_projMap_eq_of_isOriginChartSection 0 below · cited by 14 · depth 31
• Transport of a relative group law along a cartesian Proj square WeierstrassCurve.DrinfeldGlobal.comp_projMap_mul_eq_mul_comp_projMap_of_one_comp_eq 22 below · cited by 17 · depth 31
• Sections of the finite chart versus affine Weierstrass points WeierstrassCurve.DrinfeldGlobal.equation_iff_exists_isSectionThrough_and_eq_iff_of_isSectionThrough 2 below · cited by 34 · depth 31
• Points-evaluation transports along a cartesian Proj square WeierstrassCurve.DrinfeldGlobal.exists_isPointsEval_of_mul_comp_projMap_eq_of_isPullback 0 below · cited by 2 · depth 31
• Finite representability of the raw Drinfeld Γ(q)-pair functor WeierstrassCurve.DrinfeldGlobal.exists_moduleFinite_represents_isLevel 63 below · cited by 2 · depth 31
• Sections through an independent q-torsion pair are a Drinfeld basis WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_of_isSectionThrough_of_torsion_basis 118 below · cited by 5 · depth 31
• Unit sections are compatible with Proj base change WeierstrassCurve.DrinfeldGlobal.one_comp_projMap_eq_of_isOriginChartSection 0 below · cited by 10 · depth 31
• Cyclic generator of order M' cut by the Γ₀(M')-tuple WeierstrassCurve.DrinfeldGlobal.exists_addOrderOf_eq_forall_isRoot_level_fst_of_raw_rigidDataH1Pow 5 below · cited by 5 · depth 32
• Diamond invariance of the in-line product polynomial for sections WeierstrassCurve.DrinfeldGlobal.exists_isUnit_inLineMulPoly_eq_C_mul_of_isSectionThrough_zsmulSection 178 below · cited by 2 · depth 32
• Equal Γ₀(M')-moduli points give a common change of variables WeierstrassCurve.DrinfeldGlobal.exists_variableChange_curve_eq_level_fst_eq_of_moduliPoint_mk_eq_of_raw_rigidDataH1Pow 2 below · cited by 1 · depth 32
• Uniqueness of origin-pinned group laws and their level transports WeierstrassCurve.DrinfeldGlobal.groupLaws_eq_and_levelTransport_heq_of_isOriginIdentity_of_isSectionTransport 25 below · cited by 8 · depth 32
• Two H₁-admissible Γ₁(ℓ_g)-points on one curve lie in line WeierstrassCurve.DrinfeldGlobal.inLine_level_snd_fst_xP_of_curve_eq_of_level_fst_eq_rigidDataH1Pow 20 below · cited by 1 · depth 32
• Drinfeld Γ(q)-basis criterion over a field, q invertible WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_of_isPointsEval_of_nsmul_eq_one_of_linComb_inj 43 below · cited by 2 · depth 32
• Level structures transport to relative Drinfeld bases WeierstrassCurve.DrinfeldGlobal.isLevel_iff_isDrinfeldBasisOver_comp_projMap 27 below · cited by 9 · depth 32
• Transport along a change of variables on sections through a point WeierstrassCurve.DrinfeldGlobal.isSectionThrough_act_of_isSectionTransport 0 below · cited by 9 · depth 32
• Sections of a transported Drinfeld pair pass through f-images WeierstrassCurve.DrinfeldGlobal.isSectionThrough_map_of_isSectionTransport 0 below · cited by 14 · depth 32
• Integer combinations of sections pass through the combined points WeierstrassCurve.DrinfeldGlobal.isSectionThrough_zlinComb_of_isSectionThrough 86 below · cited by 11 · depth 32
• Transfer of the Drinfeld level pins under restriction of scalars WeierstrassCurve.DrinfeldGlobal.pins_restrictScalars 0 below · cited by 16 · depth 32
• Drinfeld q-bases lift from K to a DVR R₀ WeierstrassCurve.DrinfeldGlobal.RawDrinfeldPair.exists_map_eq_and_isLevel_of_isLevel_map 70 below · cited by 2 · depth 33
• Drinfeld level-q bases read as Galois-equivariant q-torsion bases WeierstrassCurve.DrinfeldGlobal.exists_basisReading_levelComponent_map_of_isAlgClosed 25 below · cited by 2 · depth 33
• Non-zero multiples of an ℓ-torsion section avoid infinity WeierstrassCurve.DrinfeldGlobal.exists_isSectionThrough_zsmulSection_of_eval_prePsi_eq_zero 119 below · cited by 3 · depth 33
• Relabelling fixing a Drinfeld basis reduces to ± 1 WeierstrassCurve.DrinfeldGlobal.map_eq_of_act_relabel_eq 98 below · cited by 1 · depth 33
• ℓ-torsion of a section versus vanishing of preΨ_ℓ WeierstrassCurve.DrinfeldGlobal.nsmul_eq_one_iff_eval_prePsi_eq_zero_of_isSectionThrough 138 below · cited by 10 · depth 33
• Base-change compatibility of the pinned group law on field points WeierstrassCurve.DrinfeldGlobal.GroupLaws.mul_comp_projMap_eq_at_field_of_isCoefficientHom 23 below · cited by 3 · depth 34
• Base change of the unit section along a coefficient homomorphism WeierstrassCurve.DrinfeldGlobal.GroupLaws.one_comp_projMap_eq_of_isCoefficientHom 1 below · cited by 5 · depth 34
• Global Drinfeld q-basis yields formal Drinfeld basis, supersingular case WeierstrassCurve.DrinfeldGlobal.IsDrinfeldBasis.exists_reducesToOrigin_isDrinfeldBasisAdic_of_toPowerSeries_eq_typeZero 139 below · cited by 2 · depth 34
• Relabellings fixing a Drinfeld q-basis up to sign are ≡ ε · 1 WeierstrassCurve.DrinfeldGlobal.IsDrinfeldBasis.map_eq_smul_one_of_zlinComb_eq_zsmulSection 14 below · cited by 4 · depth 34
• Both members of a global Drinfeld q-basis are q-torsion WeierstrassCurve.DrinfeldGlobal.IsDrinfeldBasis.nsmul_eq_one_and_nsmul_eq_one 3 below · cited by 11 · depth 34
• Level transport identified by its base-changed sections WeierstrassCurve.DrinfeldGlobal.LevelTransport.map_eq_mk_of_comp_projMap_eq 5 below · cited by 1 · depth 34
• Drinfeld basis sections factor through the affine chart WeierstrassCurve.DrinfeldGlobal.RawDrinfeldPair.IsLevel.exists_isSectionThrough_of_isUnit 99 below · cited by 12 · depth 34
• Unit Katz independence elements for Drinfeld Γ(q)-bases WeierstrassCurve.DrinfeldGlobal.RawDrinfeldPair.IsLevel.isUnit_indepElt_of_isSectionThrough 104 below · cited by 8 · depth 34
• Base change of the basis divisor along Proj of φ WeierstrassCurve.DrinfeldGlobal.basisDivisor_comap_fst_eq_basisDivisor_comap_theta 29 below · cited by 1 · depth 34
• Unique extension of K-points of the projective Weierstrass model over a DVR WeierstrassCurve.DrinfeldGlobal.existsUnique_section_comp_eq_of_isFractionRing 1 below · cited by 1 · depth 34
• Rational j of the quotient by a Γ₀(M')-kernel WeierstrassCurve.DrinfeldGlobal.exists_algebraMap_eq_cyclicQuotientJ_of_raw_rigidDataPow 315 below · cited by 1 · depth 34
• Base change comparison of relative group laws on projective Weierstrass models WeierstrassCurve.DrinfeldGlobal.exists_isPullback_comp_nsmul_isSectionThrough_iff_of_one_eq_kwZeroSect 26 below · cited by 3 · depth 34
• Comparison morphism for the base-changed projective Weierstrass model WeierstrassCurve.DrinfeldGlobal.exists_theta_of_isCoefficientHom 4 below · cited by 1 · depth 34
• Flatness of the Drinfeld basis divisor over the base WeierstrassCurve.DrinfeldGlobal.flat_basisDivisor_subschemeIota_comp_snd 13 below · cited by 1 · depth 34
• Flatness of the [n]-torsion subscheme over the base WeierstrassCurve.DrinfeldGlobal.flat_torsionIdeal_subschemeIota_comp_snd_of_flat_schemeKerStr 0 below · cited by 1 · depth 34
• Weil pairing of a Drinfeld Γ(q)-basis is primitive WeierstrassCurve.DrinfeldGlobal.isPrimitiveRoot_weilPairing0_of_isLevel_of_isSectionThrough_ed2 196 below · cited by 8 · depth 34
• Projective Weierstrass model structure maps commute with base change WeierstrassCurve.DrinfeldGlobal.projMap_comp_projModelStrCR_of_isCoefficientHom 4 below · cited by 12 · depth 34
• Sections determined by their image under `Proj.map` of φ WeierstrassCurve.DrinfeldGlobal.section_eq_of_comp_projMap_eq_of_isCoefficientHom 4 below · cited by 8 · depth 34
• Base change of the n-torsion ideal sheaf along θ WeierstrassCurve.DrinfeldGlobal.torsionIdeal_comap_fst_eq_torsionIdeal_comap_theta 26 below · cited by 1 · depth 34
• Drinfeld basis factorisation of the q-division series WeierstrassCurve.DrinfeldGlobal.IsDrinfeldBasis.exists_isUnit_mul_nthSeries_eq_prod_X_sub_C_originParam 135 below · cited by 3 · depth 35
• Uniqueness of the origin-chart map of a section WeierstrassCurve.DrinfeldGlobal.IsOriginChartSection.eq 0 below · cited by 1 · depth 35
• Unique lifting of level-q Drinfeld pairs along nilpotent surjections WeierstrassCurve.DrinfeldGlobal.existsUnique_isLevel_map_eq_of_surjective_of_ker_pow_eq_bot_of_isUnit_of_ne_two 202 below · cited by 2 · depth 35
• Sum of a level-ℓ section and q-torsion meets the affine chart WeierstrassCurve.DrinfeldGlobal.exists_isSectionThrough_mul_of_isLevelPStructure_of_nsmul_eq_one 121 below · cited by 1 · depth 35
• Drinfeld Γ(q)-pairs versus Katz level-q data, naturally WeierstrassCurve.DrinfeldGlobal.exists_rawDrinfeldPair_equiv_levelPData_natural_of_isUnit 199 below · cited by 3 · depth 35
• Origin parameter of [a]P+[b]Q is a formal linear combination WeierstrassCurve.DrinfeldGlobal.exists_reducesToOrigin_linComb_and_originParam_eq_linCombAdic 109 below · cited by 7 · depth 35
• Katz level-q data yield a Drinfeld Γ(q)-basis WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_of_isSectionThrough_of_isLevelPStructure 175 below · cited by 4 · depth 35
• Drinfeld Γ(q)-bases yield Katz level-q structures WeierstrassCurve.DrinfeldGlobal.isLevelPStructure_of_isLevel_of_isSectionThrough 157 below · cited by 5 · depth 35
• Equal raw classes give the same Γ₀(M') moduli point WeierstrassCurve.DrinfeldGlobal.moduliPoint_mk_eq_of_quot_mk_eq_of_raw_rigidDataPow 6 below · cited by 3 · depth 35
• Drinfeld level-q bases over an algebraically closed field are counted by GL₂(ℤ/q) WeierstrassCurve.DrinfeldGlobal.natCard_rawDrinfeldPair_isLevel_eq_natCard_GL_of_isAlgClosed 201 below · cited by 3 · depth 35
• Origin chart ring generated by scalars, X/Y and Z/Y WeierstrassCurve.DrinfeldGlobal.ringHom_originChartRing_ext 0 below · cited by 14 · depth 35
• Weil pairing of a Drinfeld q-basis is variable-change invariant WeierstrassCurve.DrinfeldGlobal.weilPairing0_toPoint_variableChange_of_isLevel_of_isSectionThrough 160 below · cited by 2 · depth 35
• Origin-chart section: restricted graph ideal equals kerχ WeierstrassCurve.DrinfeldGlobal.IsOriginChartSection.map_ideal_comap_ker_eq_ker 1 below · cited by 4 · depth 36
• Graph of a section: kernel pulls back to the section's kernel WeierstrassCurve.DrinfeldGlobal.comap_ker_graphOver_toPullbackId 0 below · cited by 2 · depth 36
• Unique lifting of Drinfeld level-q structures along nilpotent thickenings WeierstrassCurve.DrinfeldGlobal.existsUnique_isLevel_map_eq_of_surjective_of_ker_pow_eq_bot_of_isUnit 208 below · cited by 3 · depth 36
• Sum of an ℓ-division point and a q-torsion section is affine WeierstrassCurve.DrinfeldGlobal.exists_isSectionThrough_mul_of_eval_prePsi_eq_zero_of_nsmul_eq_one 121 below · cited by 1 · depth 36
• Local dichotomy for sections of a projective Weierstrass model WeierstrassCurve.DrinfeldGlobal.exists_isSectionThrough_or_exists_reducesToOrigin 0 below · cited by 4 · depth 36
• Transport of a law isomorphism along a trivial variable change WeierstrassCurve.DrinfeldGlobal.exists_lawIso_appAdic_originParam_eq_of_variableChange_map_eq_one 10 below · cited by 2 · depth 36
• Existence of a unimodular pair with one relation for a Drinfeld basis WeierstrassCurve.DrinfeldGlobal.exists_linComb_eq_one_and_linComb_ne_one_of_isDrinfeldBasis_of_nthSeries_eq_mul_X_pow_of_isOriginChartSection 138 below · cited by 2 · depth 36
• Origin-chart data transport along a coefficient homomorphism WeierstrassCurve.DrinfeldGlobal.exists_reducesToOrigin_map_originParam_eq_of_isCoefficientHom 0 below · cited by 13 · depth 36
• Formal addition law for sections reducing to the origin WeierstrassCurve.DrinfeldGlobal.exists_reducesToOrigin_mul_originParam_eq_eval 108 below · cited by 2 · depth 36
• Power series realisation of the origin chart ring WeierstrassCurve.DrinfeldGlobal.exists_ringHom_originChartRing_powerSeries 0 below · cited by 6 · depth 36
• Sections with prescribed origin parameter over complete local rings WeierstrassCurve.DrinfeldGlobal.exists_section_reducesToOrigin_originParam_eq 0 below · cited by 4 · depth 36
• Formal Drinfeld basis gives a global Drinfeld Γ(q)-basis WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_of_reducesToOrigin_of_isDrinfeldBasisAdic_typeZero 852 below · cited by 2 · depth 36
• Base change of a section through an affine point WeierstrassCurve.DrinfeldGlobal.isSectionThrough_map_of_comp_projMap_eq_of_isCoefficientHom 0 below · cited by 2 · depth 36
• Unit difference of abscissae of distinct multiples of an ℓ-division point WeierstrassCurve.DrinfeldGlobal.isUnit_sub_of_isSectionThrough_zsmulSection_of_eval_prePsi_eq_zero 119 below · cited by 1 · depth 36
• Sections avoiding the origin span the formal chart WeierstrassCurve.DrinfeldGlobal.map_ideal_comap_ker_eq_top_of_not_reducesToOrigin 0 below · cited by 2 · depth 36
• Torsion ideal on the origin chart is ([q]_F) WeierstrassCurve.DrinfeldGlobal.map_ideal_comap_torsionIdeal_eq_span_nthSeries 127 below · cited by 3 · depth 36
• Image of the origin-chart kernel in T[[X]] WeierstrassCurve.DrinfeldGlobal.map_ker_eq_span_X_sub_C_originParam 4 below · cited by 3 · depth 36
• Raw points with origin pairs and equal étale parts coincide WeierstrassCurve.DrinfeldGlobal.rigidDataPow_raw_eq_act_of_curve_eq_of_level_eq_of_pair_eq_one 3 below · cited by 1 · depth 36
• Ordinary case: exactly q combinations of a Drinfeld basis are the origin WeierstrassCurve.DrinfeldGlobal.IsDrinfeldBasis.exists_card_eq_of_nthSeries_eq_mul_X_pow 136 below · cited by 1 · depth 37
• Section ideal restricted to the origin chart is kerχ WeierstrassCurve.DrinfeldGlobal.IsOriginChartSection.comap_ker_originChartInclusion 0 below · cited by 1 · depth 37
• Drinfeld Γ(2)-basis: x_P-x_Q is a unit WeierstrassCurve.DrinfeldGlobal.RawDrinfeldPair.IsLevel.isUnit_sub_of_isSectionThrough_of_two 99 below · cited by 2 · depth 37
• Torsion ideal pulled back along a point equals [q]^* of the origin WeierstrassCurve.DrinfeldGlobal.comap_torsionIdeal_eq_comap_ker_one 0 below · cited by 1 · depth 37
• Lifting Drinfeld q-level structures along Ω[ε]→Ω WeierstrassCurve.DrinfeldGlobal.exists_isLevel_and_map_fstHom_eq_dualNumber_of_isLevel 202 below · cited by 1 · depth 37
• Multiplication by q on the formal point at the origin WeierstrassCurve.DrinfeldGlobal.exists_originChart_comp_schemeNsmul_eq_of_formalChart 120 below · cited by 1 · depth 37
• Formal group law as parameter of the universal sum WeierstrassCurve.DrinfeldGlobal.exists_reducesToOrigin_mul_originParam_eq_formalGroupLawFixed 92 below · cited by 1 · depth 37
• Transport of the origin parameter under a change of variables WeierstrassCurve.DrinfeldGlobal.exists_reducesToOrigin_originParam_eq_evalSeries_of_isVariableChangeHom 2 below · cited by 5 · depth 37
• Section with formal parameter Xᵢ over A[[X₀,X₁]] WeierstrassCurve.DrinfeldGlobal.exists_section_reducesToOrigin_originParam_eq_X 0 below · cited by 1 · depth 37
• Affine 2-torsion pair with unit x-difference gives Drinfeld basis WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_two_of_isSectionThrough_of_isUnit_sub 166 below · cited by 2 · depth 37
• Kernel of a scalar-compatible origin-chart map WeierstrassCurve.DrinfeldGlobal.ker_eq_span_of_originChartRing 0 below · cited by 5 · depth 37
• Preimage of the origin section in the origin chart WeierstrassCurve.DrinfeldGlobal.map_ideal_comap_ker_one_eq_span 4 below · cited by 1 · depth 37
• Equal raw H₁-classes with cut-out generators give equal moduli points WeierstrassCurve.DrinfeldGlobal.moduliPoint_mk_eq_of_quot_mk_eq_of_raw_rigidDataH1Pow 6 below · cited by 3 · depth 37
• Counting level-2 Drinfeld bases over an algebraically closed field WeierstrassCurve.DrinfeldGlobal.natCard_rawDrinfeldPair_isLevel_two_eq_natCard_GL_of_isAlgClosed 188 below · cited by 1 · depth 37
• Two-torsion criterion for a section through an affine point WeierstrassCurve.DrinfeldGlobal.nsmul_two_eq_one_iff_of_isSectionThrough 132 below · cited by 2 · depth 37
• Origin-chart section: w equals w_W at its parameter WeierstrassCurve.DrinfeldGlobal.originW_eq_evalSeries_formalW_originParam_of_isOriginChartSection 1 below · cited by 3 · depth 37
• Sections reducing to the origin cut out prodᵢ (X - zᵢ) WeierstrassCurve.DrinfeldGlobal.prodKerGraph_eq_ker_originChart_of_forall_reducesToOrigin 21 below · cited by 1 · depth 37
• Rigidity of raw H₁-data with origin Drinfeld pairs WeierstrassCurve.DrinfeldGlobal.rigidDataH1Pow_raw_eq_act_of_curve_eq_of_level_eq_of_pair_eq_one 3 below · cited by 1 · depth 37
• Origin-chart sections are determined by their origin parameter WeierstrassCurve.DrinfeldGlobal.section_eq_of_reducesToOrigin_of_originParam_eq 0 below · cited by 12 · depth 37
• q-torsion equals the origin-chart kernel Spec T[[Z]]/(g) WeierstrassCurve.DrinfeldGlobal.torsionIdeal_eq_ker_originChart_of_map_ideal_eq_span 728 below · cited by 1 · depth 37
• Unique section through an affine point of the projective model WeierstrassCurve.DrinfeldGlobal.existsUnique_isSectionThrough 3 below · cited by 1 · depth 38
• Rechartering a field point from D₊(Y) to D₊(Z) WeierstrassCurve.DrinfeldGlobal.exists_eq_comp_zChartInclusion_of_eq_comp_originChartInclusion 0 below · cited by 1 · depth 38
• Lifting an origin-chart point through Proj of a coefficient homomorphism WeierstrassCurve.DrinfeldGlobal.exists_originChartInclusion_comp_projMap_eq_of_isCoefficientHom 0 below · cited by 2 · depth 38
• Origin chart maps from solutions of the dehomogenised Weierstrass cubic WeierstrassCurve.DrinfeldGlobal.exists_ringHom_originChartRing_eq 0 below · cited by 5 · depth 38
• First-order Serre–Tate rigidity at an ordinary point WeierstrassCurve.DrinfeldGlobal.exists_variableChange_map_fstHom_eq_one_and_smul_map_eq_map_map_of_nsmul_eq_one_of_nthSeries_eq_mul_X_pow 914 below · cited by 2 · depth 38
• Cyclic-quotient j reading passes to every algebraically closed overfield WeierstrassCurve.DrinfeldGlobal.forall_algebraMap_eq_cyclicQuotientJ_of_exists_of_raw_rigidDataPow 17 below · cited by 1 · depth 38
• Multiplication by q kills first-order lifts of q-torsion WeierstrassCurve.DrinfeldGlobal.nsmul_eq_one_of_specMap_fstHom_comp_eq_of_nsmul_eq_one 102 below · cited by 2 · depth 38
• Dehomogenised Weierstrass relation in the origin chart WeierstrassCurve.DrinfeldGlobal.originChart_rel 0 below · cited by 7 · depth 38
• Uniqueness of small solutions of the origin-chart Weierstrass relation WeierstrassCurve.DrinfeldGlobal.originChart_rel_unique_of_constantCoeff_eq_zero 0 below · cited by 1 · depth 38
• Sections of a projective Weierstrass model are determined by an injective base change WeierstrassCurve.DrinfeldGlobal.section_eq_of_specMap_comp_eq_of_injective 0 below · cited by 1 · depth 38
• Frobenius on charts gives a homomorphism of group laws WeierstrassCurve.DrinfeldGlobal.comp_mul_eq_mul_comp_of_zChart_pow_originChart_pow 30 below · cited by 1 · depth 39
• Multiplication by q kills the kernel of Φ WeierstrassCurve.DrinfeldGlobal.comp_schemeNsmul_eq_one_of_comp_eq_one_of_zChart_pow_originChart_pow 121 below · cited by 1 · depth 39
• Lifting a K-point in the chart D₊(Z) to a section through an affine point WeierstrassCurve.DrinfeldGlobal.exists_isSectionThrough_of_specMap_comp_eq_zChart 0 below · cited by 1 · depth 39
• Trivialising a deformation from a q-torsion point and Frobenius WeierstrassCurve.DrinfeldGlobal.exists_iso_projModelCR_map_map_of_frobenius_of_comp_schemeNsmul_eq_one_of_nsmul_eq_one 858 below · cited by 1 · depth 39
• Existence of relative Frobenius on the projective Weierstrass model WeierstrassCurve.DrinfeldGlobal.exists_map_frobenius_isFinite_surjective_zChart_pow_originChart_pow 13 below · cited by 1 · depth 39
• Lifting an origin K-point to an origin chart section over a local ring WeierstrassCurve.DrinfeldGlobal.exists_reducesToOrigin_of_specMap_comp_eq_originChart 0 below · cited by 3 · depth 39
• Isomorphisms over k[ε] trivial mod ε come from variable changes WeierstrassCurve.DrinfeldGlobal.exists_variableChange_map_fstHom_eq_one_and_smul_eq_of_iso_of_projMap_comp_eq 22 below · cited by 1 · depth 39
• Flatness of the relative Frobenius of a Weierstrass model WeierstrassCurve.DrinfeldGlobal.flat_of_zChart_pow_originChart_pow_of_isArtinianRing 40 below · cited by 1 · depth 39
• Commutativity of the group law on arbitrary S-points WeierstrassCurve.DrinfeldGlobal.GroupLaws.mul_comm_schemeHomOver_of_isOriginIdentity 101 below · cited by 1 · depth 40
• Equal-rank homomorphisms with a common kernel subscheme vanish together WeierstrassCurve.DrinfeldGlobal.comp_eq_one_iff_comp_eq_one_of_finrank_eq_of_isClosedImmersion 2 below · cited by 1 · depth 40
• Factor through a flat surjection is again a homomorphism WeierstrassCurve.DrinfeldGlobal.comp_mul_eq_mul_comp_of_comp_eq_of_isFinite_of_flat_of_surjective 0 below · cited by 1 · depth 40
• Frobenius descent: Φ is a homomorphism of the group laws WeierstrassCurve.DrinfeldGlobal.comp_mul_eq_mul_comp_of_comp_projMap_eq_frobenius 24 below · cited by 1 · depth 40
• Chart-wise q-power map followed by coefficient projection is absolute Frobenius WeierstrassCurve.DrinfeldGlobal.comp_projMap_eq_frobenius_of_zChart_pow_originChart_pow 7 below · cited by 1 · depth 40
• Unique factorisation through a finite flat surjective isogeny WeierstrassCurve.DrinfeldGlobal.existsUnique_comp_eq_of_isFinite_of_flat_of_surjective_of_forall_eq_one 4 below · cited by 2 · depth 40
• Constant Verschiebung: reduction modulo ε, then constant extension WeierstrassCurve.DrinfeldGlobal.exists_hom_isFinite_flat_finrank_eq_of_map_map_eq_dualNumber 30 below · cited by 1 · depth 40
• Flat degree-q subscheme of ker V_q killed by g WeierstrassCurve.DrinfeldGlobal.exists_isClosedImmersion_finrank_eq_comp_eq_comp_one_of_comp_eq_schemeNsmul_of_nsmul_eq_one 32 below · cited by 1 · depth 40
• Isomorphism between quotients with a common kernel WeierstrassCurve.DrinfeldGlobal.exists_iso_comp_eq_of_isFinite_of_flat_of_surjective_of_forall_eq_one_iff 6 below · cited by 1 · depth 40
• Transfer of the cyclic-quotient j-reading between algebraic closures WeierstrassCurve.DrinfeldGlobal.forall_algebraMap_eq_cyclicQuotientJ_of_exists_of_raw_rigidDataH1Pow 17 below · cited by 1 · depth 40
• Drinfeld bases and roots of the Igusa factor g WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_iff_eval_originParam_eq_zero_and_exists_section_of_nthSeries_eq_X_mul_mul_of_forall_nthSeries_eq_mul_prod 927 below · cited by 2 · depth 40
• Chartwise q-th-power morphism of Weierstrass models is finite and surjective WeierstrassCurve.DrinfeldGlobal.isFinite_locallyOfFinitePresentation_surjective_of_comp_projMap_eq_frobenius_of_zChart_pow_originChart_pow 11 below · cited by 1 · depth 40
• Frobenius kernel on a Weierstrass model is finite flat of rank q WeierstrassCurve.DrinfeldGlobal.isFinite_pullback_snd_kwZeroSect_flat_finrank_eq_of_zChart_pow_originChart_pow 8 below · cited by 1 · depth 40
• Multiplication by n is finite flat of rank n² WeierstrassCurve.DrinfeldGlobal.isFinite_schemeNsmul_flat_surjective_finrank_eq_sq 726 below · cited by 1 · depth 40
• Chartwise q-th power map on Weierstrass models is locally quasi-finite WeierstrassCurve.DrinfeldGlobal.locallyQuasiFinite_of_zChart_pow_originChart_pow 11 below · cited by 1 · depth 40
• Frobenius kernel killed by q: Artinian local points WeierstrassCurve.DrinfeldGlobal.nsmul_eq_one_of_comp_eq_one_of_zChart_pow_originChart_pow_of_isArtinianRing 119 below · cited by 1 · depth 40
• Base change of a morphism of projective Weierstrass models WeierstrassCurve.DrinfeldGlobal.exists_comp_projMap_eq_projMap_comp_isPullback_of_isCoefficientHom 4 below · cited by 1 · depth 41
• Rank q closed subscheme generated by a q-torsion section WeierstrassCurve.DrinfeldGlobal.exists_isClosedImmersion_finrank_eq_of_nsmul_eq_one_of_not_reducesToOrigin 1 below · cited by 1 · depth 41
• Origin chart modulo ((X/Y)^q,(Z/Y)^q) is T[u]/(u^q) WeierstrassCurve.DrinfeldGlobal.exists_ringEquiv_originChartRing_quotient_span_xOverY_pow_zOverY_pow_adjoinRoot_X_pow 4 below · cited by 1 · depth 41
• Drinfeld Γ(q)-basis criterion at an ordinary point WeierstrassCurve.DrinfeldGlobal.isDrinfeldBasis_iff_nsmul_eq_one_and_nthSeries_eq_mul_prod_of_reducesToOrigin 924 below · cited by 1 · depth 41
• Kernel of a chartwise q-th power map is finite flat of rank q WeierstrassCurve.DrinfeldGlobal.isFinite_pullback_snd_kwZeroSect_flat_finrank_eq_of_zChart_pow_originChart_pow_of_ringEquiv_adjoinRoot 2 below · cited by 1 · depth 41
• Multiplication by q kills nilpotent origin-chart points in characteristic q WeierstrassCurve.DrinfeldGlobal.nsmul_eq_one_of_comp_originChartIota_of_pow_eq_zero_of_isAdicComplete 118 below · cited by 1 · depth 41
• Origin cosets: [a]P+[b]Q meets the origin iff b=0 WeierstrassCurve.DrinfeldGlobal.exists_reducesToOrigin_linComb_iff_eq_zero_of_not_reducesToOrigin 1 below · cited by 2 · depth 42
• Equal ranks of E[q] and the Drinfeld divisor WeierstrassCurve.DrinfeldGlobal.isFinite_flat_and_finrank_basisDivisor_eq_finrank_torsionIdeal 727 below · cited by 1 · depth 42
• Torsion at the origin and divisibility of [q]_F WeierstrassCurve.DrinfeldGlobal.nsmul_eq_one_iff_X_sub_C_originParam_dvd_nthSeries 112 below · cited by 1 · depth 42
• Uniqueness of the origin-chart solution v over a local ring WeierstrassCurve.DrinfeldGlobal.originChart_rel_unique_of_mem_maximalIdeal 0 below · cited by 2 · depth 42
• Origin-coset inclusion: basis divisor lies inside E[q] WeierstrassCurve.DrinfeldGlobal.torsionIdeal_le_basisDivisor_of_nsmul_eq_one_of_nthSeries_eq_mul_prod 202 below · cited by 1 · depth 42
• Invariance of the basis divisor under translation by Q WeierstrassCurve.DrinfeldGlobal.basisDivisor_comap_pullback_lift_eq_of_nsmul_eq_one 0 below · cited by 1 · depth 43
• Support of the basis divisor specialises to graph closed points WeierstrassCurve.DrinfeldGlobal.exists_specializes_graphOver_closedPoint_of_mem_support_basisDivisor 1 below · cited by 1 · depth 43
• Closed point of the graph of a section reducing to the origin WeierstrassCurve.DrinfeldGlobal.graphOver_base_closedPoint_eq_of_reducesToOrigin 1 below · cited by 1 · depth 43
• Origin-chart ideals detected by their formal-chart images WeierstrassCurve.DrinfeldGlobal.map_algebraMap_localization_atPrime_eq_of_map_originChart_powerSeries_eq 12 below · cited by 1 · depth 43
• Translation by a q-torsion section preserves the q-torsion ideal WeierstrassCurve.DrinfeldGlobal.torsionIdeal_comap_pullback_lift_eq_of_nsmul_eq_one 0 below · cited by 1 · depth 43
• Faithful flatness of T[[X]] over the origin-chart local ring WeierstrassCurve.DrinfeldGlobal.exists_ringHom_localization_atPrime_powerSeries_comp_eq_and_faithfullyFlat 10 below · cited by 1 · depth 44
• Origin chart is dense in T[[X]] modulo (mathfrak m_T,X)ⁿ WeierstrassCurve.DrinfeldGlobal.exists_sub_map_mem_maximalIdeal_pow_of_originChart_powerSeries 0 below · cited by 1 · depth 45
• Formal chart at the origin detects powers of 𝔭 WeierstrassCurve.DrinfeldGlobal.mem_comap_maximalIdeal_pow_of_map_mem_maximalIdeal_pow 5 below · cited by 1 · depth 45

WeierstrassCurve.Generic 1

• Galois transitivity on cyclic p-subgroups of the generic curve WeierstrassCurve.Generic.exists_algEquiv_inLine_of_eval_prePsi_eq_zero_of_ne_zero 307 below · cited by 2 · depth 20

WeierstrassCurve.IsCyclicGenKernel 4

• Generator-kernel polynomials of level p^k under variable change WeierstrassCurve.IsCyclicGenKernel.variableChange 3 below · cited by 2 · depth 29
• A cyclic generator-kernel polynomial splits over ⟨ Q⟩ WeierstrassCurve.IsCyclicGenKernel.eq_prod_X_sub_C_coordsOrZero_nsmul 8 below · cited by 5 · depth 32
• Generator-kernel polynomials have a root of exact order p^k WeierstrassCurve.IsCyclicGenKernel.exists_addOrderOf_eq_and_isRoot 13 below · cited by 4 · depth 32
• Representability of cyclic generator-kernel polynomials by a finite B-algebra WeierstrassCurve.IsCyclicGenKernel.exists_moduleFinite_represents 0 below · cited by 1 · depth 32

WeierstrassCurve.IsIntegralModelOf 3

• Irreducibility of mod n representation under change of integral model WeierstrassCurve.IsIntegralModelOf.modRepIsIrreducible_iff 5 below · cited by 3 · depth 7
• Galois-equivariant n-torsion isomorphism for an integral model WeierstrassCurve.IsIntegralModelOf.exists_linearEquiv_torsionBy 3 below · cited by 3 · depth 8
• Frobenius trace and determinant on E[p] for an integral model WeierstrassCurve.IsIntegralModelOf.galoisTrace_det_frobenius 50 below · cited by 9 · depth 8

WeierstrassCurve.IsModularModelOfExactConductorLevel 1

• Exact-conductor modularity implies conductor-level modularity WeierstrassCurve.IsModularModelOfExactConductorLevel.isModularModelOfConductorLevel 0 below · cited by 1 · depth 6

WeierstrassCurve.IsTwoKernel 4

• Two-torsion kernel polynomials under Weierstrass changes of variables WeierstrassCurve.IsTwoKernel.variableChange 0 below · cited by 1 · depth 29
• A module-finite algebra representing monic linear divisors of Ψ₂² WeierstrassCurve.IsTwoKernel.exists_moduleFinite_represents 0 below · cited by 1 · depth 32
• Two-kernel polynomials are X-x(Q) with Q of order 2 WeierstrassCurve.IsTwoKernel.exists_addOrderOf_eq_two_and_eq_X_sub_C 0 below · cited by 2 · depth 35
• Unique lifting of Γ₀(2)-kernels along nilpotent thickenings WeierstrassCurve.IsTwoKernel.existsUnique_map_eq_of_surjective_of_ker_pow_eq_bot 1 below · cited by 1 · depth 37

WeierstrassCurve.VariableChange 6

• Galois equivariance of the variable-change isomorphism on ̄ K-points WeierstrassCurve.VariableChange.exists_addEquiv_affine_point_baseChange_gal_equiv 1 below · cited by 1 · depth 17
• A variable change induces an isomorphism of affine point groups WeierstrassCurve.VariableChange.nonempty_addEquiv_affine_point 1 below · cited by 1 · depth 18
• Variable change fixing a Weierstrass curve with u=1 is trivial WeierstrassCurve.VariableChange.eq_one_of_smul_eq_of_u_eq_one_of_isUnit_six 0 below · cited by 1 · depth 37
• Supersingular j forces u^{q+1}=1 for stabilising variable changes WeierstrassCurve.VariableChange.u_pow_add_one_eq_one_of_smul_eq_of_map_j_mem_ssJSet 23 below · cited by 1 · depth 37
• No infinitesimal automorphisms of an elliptic Weierstrass equation WeierstrassCurve.VariableChange.eq_one_of_smul_eq_of_sq_eq_bot 0 below · cited by 2 · depth 39
• Rigidity of Weierstrass variable changes over Artinian local rings WeierstrassCurve.VariableChange.eq_one_of_map_eq_one_of_smul_eq_of_isArtinianRing 1 below · cited by 2 · depth 40