← all areas

Namespace TateCurve 57 theorems

• Galois-equivariant parametrisation of the Tate curve's 3-torsion TateCurve.exists_primitiveRoot_equiv_torsion_algebraicClosure_padic_of_eq_three 8 below · cited by 1 · depth 12
• Galois-equivariant parametrisation of Tate-curve p-torsion over ℚ̄ₚ TateCurve.exists_primitiveRoot_equiv_torsion_algebraicClosure_padic_of_five_le 10 below · cited by 2 · depth 12
• Unconditional p-torsion parametrisation of the Tate curve TateCurve.eq_zero_or_eq_tateParam_unconditional 38 below · cited by 0 · depth 13
• Additivity of the Tate curve p-torsion parametrisation TateCurve.tateTorsionEquiv_add 3 below · cited by 3 · depth 13
• Isometric q-fixing endomorphisms act triangularly on Tate torsion points TateCurve.tateTorsionPoint_map 0 below · cited by 1 · depth 13
• Base change to K is bijective on p-torsion of a Tate curve TateCurve.torsionBy_baseChange_bijective_algebraicClosure_padic 3 below · cited by 1 · depth 13
• p-torsion of the Tate curve under `SymAddHyps` TateCurve.eq_zero_or_eq_tateParam_of_prime_nsmul_eq_zero 5 below · cited by 1 · depth 14
• The c₆-invariant of the Tate curve is a unit TateCurve.nnnorm_c_six 0 below · cited by 1 · depth 14
• Splitting of the Tate torsion parametrisation into ζ- and t-directions TateCurve.tateTorsionPoint_decomp 0 below · cited by 1 · depth 14
• The t-line of the Tate torsion parametrisation is cyclic TateCurve.tateTorsionPoint_snd_eq_nsmul 1 below · cited by 1 · depth 14
• p-torsion of a Tate curve prolongs when p ∣ vₚ(q) TateCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_dvd_valuation 22 below · cited by 1 · depth 15
• Twist parameter against the Tate curve is a unit TateCurve.nnnorm_twistParam_curve_eq_one 3 below · cited by 1 · depth 15
• Additivity of the Tate parametrisation along powers of t TateCurve.tpow_succ_point_eq_add 0 below · cited by 1 · depth 15
• Finite flat prolongation of Tate-curve p-torsion, p ≥ 5 TateCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_dvd_valuation_of_five_le 17 below · cited by 1 · depth 16
• Finite flat prolongation of E_q[p] for p<5 TateCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_dvd_valuation_of_lt_five 13 below · cited by 1 · depth 16
• Tate curve discriminant has norm ‖q‖ TateCurve.nnnorm_Delta 0 below · cited by 1 · depth 16
• ‖c₄‖=1 for the Tate curve TateCurve.nnnorm_c4 0 below · cited by 1 · depth 16
• Finite flat prolongation of Tate-curve 3-torsion over ℤ₃ TateCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_dvd_valuation_of_eq_three 8 below · cited by 1 · depth 17
• Finite flat prolongation of Tate-curve 2-torsion over ℤ₂ TateCurve.exists_finiteFlat_prolongation_torsion_padicInt_of_dvd_valuation_of_eq_two 10 below · cited by 1 · depth 17
• Tate parametrisation satisfies the Weierstrass equation TateCurve.equation_pointX_pointY 20 below · cited by 2 · depth 19
• Division polynomial vanishes at Tate N-torsion abscissae TateCurve.isRoot_prePsi_curve_pointX_laurentSeries 35 below · cited by 2 · depth 19
• Divisor-sum q-expansion of the Tate X-coordinate TateCurve.pointX_qExpansion 5 below · cited by 11 · depth 19
• Divisor-sum q-expansion of the Tate curve Y-coordinate TateCurve.pointY_qExpansion 5 below · cited by 11 · depth 19
• Vanishing of the Tate curve defect coefficients TateCurve.defectCoeff_eq_zero 12 below · cited by 1 · depth 20
• Tate parametrisation satisfies the Weierstrass equation, conditionally TateCurve.equation_pointX_pointY_of_defectCoeff_eq_zero 17 below · cited by 6 · depth 20
• Geometric series for w/(1-w)² over an ultrametric field TateCurve.hasSum_xfun 0 below · cited by 3 · depth 20
• Power series expansion of w²/(1-w)³ TateCurve.hasSum_yfun 0 below · cited by 2 · depth 20
• Normal form of the Tate X-coordinate TateCurve.pointX_normalForm 2 below · cited by 1 · depth 20
• Normal form of the Tate Y-coordinate TateCurve.pointY_normalForm 2 below · cited by 1 · depth 20
• Unconditional symmetric addition relations for the Tate curve TateCurve.symAddHyps_unconditional 31 below · cited by 3 · depth 20
• Regrouping a double series into divisor sums TateCurve.tsum_succ_prod_eq_tsum_divisors 0 below · cited by 2 · depth 20
• Unconditional difference identity X(uv)-X(uv⁻¹) for the Tate curve TateCurve.diffHyp_unconditional 29 below · cited by 2 · depth 21
• Vanishing defect coefficients give the Tate curve equation TateCurve.equation_of_defectCoeff_eq_zero 11 below · cited by 1 · depth 21
• A q^ℤ-translate in the Tate annulus TateCurve.exists_zpow_mul_mem_annulus 0 below · cited by 6 · depth 21
• Vanishing of the Tate-curve line coefficients TateCurve.lineCoeff_eq_zero 11 below · cited by 1 · depth 21
• Invariance of the Tate X-series under u ↦ u⁻¹ TateCurve.pointX_inv 0 below · cited by 8 · depth 21
• Invariance of the Tate X-series under u ↦ qu TateCurve.pointX_q_mul 0 below · cited by 9 · depth 21
• Invariance of X under the lattice q^ℤ TateCurve.pointX_zpow_mul 1 below · cited by 7 · depth 21
• Invariance of Y under multiplication by qⁿ TateCurve.pointY_zpow_mul 1 below · cited by 7 · depth 21
• Additivity of Tate's parametrisation on the unit circle TateCurve.point_mul_eq_add_of_norm_eq_one 0 below · cited by 1 · depth 21
• s₁(q) as the sum of qⁿ/(1-qⁿ)² TateCurve.sOne_eq_tsum_xfun 1 below · cited by 2 · depth 21
• Symmetric addition identity for Tate curve X-coordinates, all admissible parameters TateCurve.symAdd_sum_allParams_unconditional 30 below · cited by 1 · depth 21
• Vanishing of the constant term of the Weierstrass defect TateCurve.defectCoeff_zero 1 below · cited by 1 · depth 22
• Weierstrass defect of the Tate parametrisation as a q-series TateCurve.defect_qExpansion 8 below · cited by 2 · depth 22
• Expansion-layer interface for the Tate curve addition law TateCurve.ks17_A_exports 21 below · cited by 6 · depth 22
• Export bundle B: divisor convolutions and Tate-curve defect normal forms TateCurve.ks17_B_exports 22 below · cited by 5 · depth 22
• Envelope-engine interface lemmas for the Tate addition law TateCurve.ks17_C1_exports 23 below · cited by 2 · depth 22
• Tate-curve keystone: collapse of bilinear sums into coefficient lines TateCurve.ks17_C3_exports 24 below · cited by 3 · depth 22
• Half-lattice closure of the Tate addition identities TateCurve.ks17_D2_exports 22 below · cited by 3 · depth 22
• Invariance of the Tate Y-series under u ↦ qu TateCurve.pointY_q_mul 0 below · cited by 7 · depth 22
• Symmetric addition identity for the Tate curve x-series TateCurve.symAdd_sum_regional 28 below · cited by 2 · depth 22
• Vanishing of the first Tate-curve defect coefficient TateCurve.defectCoeff_one 0 below · cited by 5 · depth 23
• Row-form and three-bin identities for the Tate addition defect TateCurve.ks17_C2_exports 23 below · cited by 3 · depth 23
• Group C and D coefficient lines for the Tate curve TateCurve.ks17_D3_exports 25 below · cited by 1 · depth 23
• The Tate parametrisation lands on the nodal cubic TateCurve.nodal_xfun_yfun 0 below · cited by 1 · depth 23
• Inversion formula for the Y-coordinate of the Tate parametrisation TateCurve.pointY_inv 0 below · cited by 6 · depth 23
• Additivity of the Tate parametrisation on the fundamental annulus TateCurve.point_mul_eq_add_of_norm_le_one 0 below · cited by 1 · depth 26