← all areas

Namespace DrinfeldCurve 71 theorems

— 38 · LocalChart 33

directly in DrinfeldCurve 38

• ℓ-power torsion of Pic⁰ of the Drinfeld curve DrinfeldCurve.abelJacobiCard_drinfeldFunctionField 963 below · cited by 3 · depth 15
• The Drinfeld function field is a curve over k DrinfeldCurve.isCurveOver_drinfeldFunctionField 38 below · cited by 11 · depth 15
• The Drinfeld curve coordinate ring is a domain DrinfeldCurve.isDomain_coordRing_of_ne_one 0 below · cited by 44 · depth 15
• Quadratic relation for SL₂-equivariant maps into the Drinfeld Tate module DrinfeldCurve.slEquivariant_quadratic_of_isCuspidalOfType_of_perfectField 1,275 below · cited by 2 · depth 15
• Quadratic relation passes to products of Tate modules DrinfeldCurve.tateProdRep_quadratic_of_forall 0 below · cited by 2 · depth 15
• Iterated Frobenius endomorphism of the Drinfeld curve function field DrinfeldCurve.exists_algHom_drinfeldFunctionField_apply_x_eq_pow 2 below · cited by 3 · depth 16
• Coefficient extension commutes with the ℓ-adic Drinfeld curve representation DrinfeldCurve.exists_linearEquiv_rationalTateModule_baseChange_comp_eq 0 below · cited by 1 · depth 16
• Genus of the Drinfeld curve function field is q(q-1)/2 DrinfeldCurve.genusFF_drinfeldFunctionField 113 below · cited by 3 · depth 16
• Vanishing of ψ-twisted intertwiners over a perfect base field DrinfeldCurve.intertwiningMap_twist_eq_zero_of_isCuspidalOfType_of_perfectField 1,272 below · cited by 1 · depth 16
• Constants of the Drinfeld function field are the base field DrinfeldCurve.constantsAreBase_drinfeldFunctionField 66 below · cited by 2 · depth 17
• Base change of rational Tate modules for Drinfeld curves DrinfeldCurve.exists_rationalTateModule_linearEquiv_baseChange_of_injective_of_card_torsionBy_eq 3 below · cited by 1 · depth 17
• Injectivity of Pic⁰ base change for the Drinfeld curve DrinfeldCurve.injective_pic0_baseChange_drinfeldFunctionField_of_perfectField 71 below · cited by 1 · depth 17
• Twists by characters other than θ^{± 1} do not occur DrinfeldCurve.intertwiningMap_twist_eq_zero_of_isCuspidalOfType_of_isAlgClosed 1,248 below · cited by 1 · depth 17
• Character of H on the Drinfeld curve's Tate module DrinfeldCurve.cast_mul_trace_eq_natCard_restrictAlong_eq_smul_sub 1,231 below · cited by 2 · depth 18
• Dimensions of μ_{q+1}-eigenspaces on the Drinfeld curve DrinfeldCurve.finrank_eigenspace_rootsOfUnity_rationalTateModule_eq 1,237 below · cited by 1 · depth 18
• Frobenius-type endomorphisms of the Drinfeld function field are integral DrinfeldCurve.isIntegral_of_apply_x_eq_pow_of_apply_y_eq_pow 0 below · cited by 2 · depth 18
• Twisted place count on the Drinfeld curve at elliptic classes DrinfeldCurve.natCard_place_restrictAlong_eq_smul_of_torus 119 below · cited by 1 · depth 18
• Twisted 𝔽_{q²}-forms of the Drinfeld curve function field DrinfeldCurve.exists_isCurveOver_adjoin_range_eq_top_apply_hFunctionFieldAction_eq_pow 47 below · cited by 2 · depth 19
• Fixed places of a twisted q²-Frobenius on the Drinfeld curve DrinfeldCurve.natCard_place_restrictAlong_eq_hFunctionFieldAction_smul 117 below · cited by 1 · depth 19
• Drinfeld curve: q³+1 places fixed by (-1)-twisted Frobenius DrinfeldCurve.natCard_place_restrictAlong_eq_neg_one_smul 116 below · cited by 1 · depth 19
• Twisted Frobenius fixed places on the Drinfeld curve: N(1,η)=q+1 DrinfeldCurve.natCard_restrictAlong_eq_hFunctionFieldAction_one_smul_of_ne_neg_one 115 below · cited by 1 · depth 19
• Counting solutions of the elliptically twisted Drinfeld equations DrinfeldCurve.ncard_setOf_ellTwistedFrobenius_affineFixed 0 below · cited by 1 · depth 19
• Twisted Lefschetz trace formula on Pic⁰[ℓ^m] of the Drinfeld curve DrinfeldCurve.trace_torsion_eq_sq_add_one_sub_natCard_restrictAlong_eq_smul 1,208 below · cited by 1 · depth 19
• Affine places of the Drinfeld curve are its k-points DrinfeldCurve.affinePlaces_census 115 below · cited by 6 · depth 20
• Transport of the Drinfeld Tate representation along a constant-field isomorphism DrinfeldCurve.exists_linearEquiv_tateProd_comp_tateProdRep_eq_of_algEquiv 5 below · cited by 3 · depth 20
• Fixed affine points of twisted q²-Frobenius on the Drinfeld curve DrinfeldCurve.finite_and_ncard_setOf_twistedFrobenius_affineFixed 0 below · cited by 2 · depth 20
• The q+1 places at infinity of the Drinfeld curve DrinfeldCurve.placesAtInfinity_census 113 below · cited by 9 · depth 20
• Transport of the Drinfeld function field along a constant-field isomorphism DrinfeldCurve.exists_ringEquiv_drinfeldFunctionField_algebraMap_eq_and_hFunctionFieldAction_eq_of_algEquiv 0 below · cited by 1 · depth 21
• Frobenius conjugacy between the actions of (g,α) and (g,α^q) DrinfeldCurve.exists_linearEquiv_comp_tateRep_eq_tateRep_pow_comp 0 below · cited by 3 · depth 23
• Genus of quotients of the Drinfeld curve by μ_{q+1}-subgroups DrinfeldCurve.natCard_mul_two_mul_genusFF_quotField_add_eq 117 below · cited by 3 · depth 24
• Genus of quotients of the Drinfeld curve by μ_{q+1} DrinfeldCurve.two_mul_genusFF_fixedField_rootsOfUnity 116 below · cited by 1 · depth 25
• SL₂(𝔽_q) is transitive on places at infinity DrinfeldCurve.exists_sl_hFunctionFieldAction_smul_eq_of_not_mem 117 below · cited by 4 · depth 26
• Invariants in the Drinfeld coordinate ring describe `quotField` DrinfeldCurve.algebraMap_mem_quotField_iff_forall_muAction_eq_and_exists_of_mem_quotField 0 below · cited by 13 · depth 27
• Regularity at affine places forces membership in the coordinate ring DrinfeldCurve.coe_algEquiv_mem_range_algebraMap_of_forall_place_quotField 5 below · cited by 3 · depth 27
• Freeness of the H-action at affine places of the Drinfeld curve DrinfeldCurve.exists_eq_smul_one_of_comap_hFunctionFieldAction_eq_of_affine_of_sq_eq_one 116 below · cited by 3 · depth 27
• Functions on the quotient Drinfeld curve regular at all affine places DrinfeldCurve.exists_muAction_eq_and_algebraMap_eq_of_mem_quotField_of_forall_place 4 below · cited by 4 · depth 27
• Fixed fields of μ_{q+1}-subgroups on the Drinfeld curve are curves over k DrinfeldCurve.isCurveOver_fixedField_hFunctionFieldAction 44 below · cited by 6 · depth 27
• Coordinate ring of the affine Drinfeld curve is Dedekind DrinfeldCurve.isDedekindDomain_coordRing 2 below · cited by 11 · depth 27

DrinfeldCurve.LocalChart 33

• Shifting the constant a₀ by c^N in a Drinfeld chart DrinfeldCurve.LocalChart.exists_sub_C_eq_mk_of_sub_eq_pow_mul 0 below · cited by 2 · depth 29
• Transporting initial-form unit conditions across Drinfeld chart isomorphisms DrinfeldCurve.LocalChart.exists_mem_pow_isUnit_homogeneous_apply_sub_C_eq_mk_of_ringEquiv_of_forall_apply_mk_C 3 below · cited by 2 · depth 30
• Branch tangent lines on the Drinfeld chart descend along ψ DrinfeldCurve.LocalChart.exists_mem_sq_map_add_mem_of_linearPart_mem_of_isPrime 8 below · cited by 2 · depth 30
• Rigidity of constants in a Drinfeld chart ring DrinfeldCurve.LocalChart.exists_ringHom_forall_apply_eq_mk_C_of_apply_eq_mk_C_of_forall_pow_pow_eq 1 below · cited by 2 · depth 30
• Transport of a semilinear chart datum between two Drinfeld charts DrinfeldCurve.LocalChart.exists_semilinear_linearPart_transport_of_forall_specialLinearGroup_of_dense 7 below · cited by 1 · depth 30
• The q+1 branch primes of a Drinfeld chart ring DrinfeldCurve.LocalChart.branchPrimes_of_sub_drinfeldForm_mem_pow 8 below · cited by 23 · depth 31
• Drinfeld form as a product of q+1 linear forms DrinfeldCurve.LocalChart.card_eq_and_prod_linear_eq_drinfeldForm_and_isUnit_det_of_prod_X_sub_C_eq 0 below · cited by 4 · depth 31
• Degree-e coefficients of π v - fu relations lie in (π) DrinfeldCurve.LocalChart.coeff_mem_span_of_eq_add_rel_mul_of_forall_coeff_eq_zero 0 below · cited by 3 · depth 31
• Rational directions preserved by a Drinfeld chart isomorphism DrinfeldCurve.LocalChart.exists_apply_mk_X_eq_mk_linearPart_rational_of_ringEquiv_of_forall_apply_mk_C 2 below · cited by 1 · depth 31
• Transport of linear parts under a centred Drinfeld chart isomorphism DrinfeldCurve.LocalChart.exists_linearPart_conj_ringEquiv_of_apply_mk_X_mem_span 1 below · cited by 2 · depth 31
• Units times powers of pure series in a Drinfeld chart DrinfeldCurve.LocalChart.exists_mem_pow_isUnit_homogeneous_mul_mk_pow_eq_mk 2 below · cited by 2 · depth 31
• Transport of a semilinear chart automorphism between Drinfeld charts DrinfeldCurve.LocalChart.exists_semilinear_linearPart_transport_of_forall_specialLinearGroup_of_dense_of_prime 7 below · cited by 1 · depth 31
• Linear forms vanishing in J² on a Drinfeld chart have coefficients in I DrinfeldCurve.LocalChart.mem_of_mk_sum_C_mul_X_mem_span_sq 1 below · cited by 3 · depth 31
• Centredness of a Drinfeld chart isomorphism intertwining automorphisms DrinfeldCurve.LocalChart.ringEquiv_apply_mk_X_mem_span_of_comp_eq_of_isUnit_det_one_sub 1 below · cited by 2 · depth 31
• Blow-up chart of a local Drinfeld chart at a parameter DrinfeldCurve.LocalChart.exists_algEquiv_coordRing_and_isDiscreteValuationRing_blowupChart_of_mem_maximalIdeal 4 below · cited by 1 · depth 32
• Unit times distinguished polynomial in a Drinfeld chart DrinfeldCurve.LocalChart.exists_mem_pow_isUnit_homogeneous_mul_eval_map_eq_mk_of_monic 2 below · cited by 1 · depth 32
• Moore–Dickson identity modulo π over a local ring DrinfeldCurve.LocalChart.exists_prod_prod_X_sub_C_eq_moore_add_C_C_mul 1 below · cited by 1 · depth 32
• Transport of a residually trivial automorphism through a Drinfeld chart DrinfeldCurve.LocalChart.exists_ringEquiv_conj_linearPart_C_eq_of_ringEquiv_mvPowerSeries_quotient_of_forall_sub_mem_maximalIdeal 2 below · cited by 2 · depth 32
• Branch quotients of a Drinfeld chart are discrete valuation rings DrinfeldCurve.LocalChart.isDiscreteValuationRing_quotient_branchPrime_of_sub_drinfeldForm_mem_pow 10 below · cited by 4 · depth 32
• Radical special fibre of a Drinfeld chart ring DrinfeldCurve.LocalChart.isRadical_span_C_of_sub_drinfeldForm_mem_pow 8 below · cited by 4 · depth 32
• Dickson cofactor is a unit at 𝔽_q-rational directions DrinfeldCurve.LocalChart.isUnit_sum_pow_mul_pow_of_pow_mul_sub_mul_pow_mem_maximalIdeal 0 below · cited by 1 · depth 32
• Special fibre of the Drinfeld blow-up chart DrinfeldCurve.LocalChart.exists_isPrime_algEquiv_coordRing_blowupChart_quotient_of_mem_maximalIdeal 2 below · cited by 1 · depth 33
• Branch-prime pull-back along a chart automorphism with linear part c₁g DrinfeldCurve.LocalChart.isPrime_comap_and_exists_linear_add_mem_comap_of_ringEquiv_linearPart_of_branchPrime 0 below · cited by 5 · depth 33
• Moore–Dickson product of 𝔽_q-linear forms in two variables DrinfeldCurve.LocalChart.prod_prod_X_sub_C_natCast_mul_add_eq_moore 0 below · cited by 1 · depth 33
• Transport of the Drinfeld form under a semilinear endomorphism DrinfeldCurve.LocalChart.smul_drinfeldForm_eq_aeval_linearPart_of_ringHom_semilinear 2 below · cited by 2 · depth 33
• Completion at an end of the blown-up Drinfeld chart DrinfeldCurve.LocalChart.exists_ringEquiv_adicCompletion_blowupChartAt_uvCrossingModel_pow_of_mem_span_of_div_mem 43 below · cited by 2 · depth 34
• Integral slopes at closed points of the blown-up Drinfeld chart DrinfeldCurve.LocalChart.exists_chart_and_natCast_slope_of_isMaximal_blowupChartAt_of_div_mem 0 below · cited by 1 · depth 35
• Crossing model in the X₁-chart of the blown-up Drinfeld chart DrinfeldCurve.LocalChart.exists_ringEquiv_adicCompletion_blowupChartAt_uvCrossingModel_pow_of_X_one_div_not_mem 41 below · cited by 1 · depth 35
• Completed local ring of the blown-up Drinfeld chart, X₀-branch DrinfeldCurve.LocalChart.exists_ringEquiv_adicCompletion_blowupChartAt_uvCrossingModel_pow_of_X_zero_div_not_mem 38 below · cited by 2 · depth 35
• Swapping the two coordinates of a Drinfeld chart presentation DrinfeldCurve.LocalChart.ChartPresentation.exists_swap_ringEquiv 0 below · cited by 1 · depth 36
• Flatness and non-zero-divisors in a Drinfeld chart ring DrinfeldCurve.LocalChart.ChartPresentation.mem_nonZeroDivisors_and_flat_of_mem_maximalIdeal 0 below · cited by 2 · depth 36
• Node chart of the blown-up Drinfeld curve: completion O[[U,V]]/(UV-π^m) DrinfeldCurve.LocalChart.exists_isMaximal_ringEquiv_adicCompletion_atPrime_uvCrossingModel_pow_of_mem_maximalIdeal 34 below · cited by 1 · depth 36
• T-saturation of (T,X₀,X₁)-powers in a Drinfeld chart ring DrinfeldCurve.LocalChart.mem_span_pow_of_mul_mem_span_pow_succ_of_sub_drinfeldForm_mem_pow 1 below · cited by 2 · depth 36