← all areas

Namespace ModPForms 65 theorems

• Mod p eigensystems occur, up to twist, in weight ≤ p+1 ModPForms.exists_weight_le_succ_mem_modPMod_isModPEigen_pow_mul_of_isModPEigen_algebraicClosure 1,310 below · cited by 1 · depth 13
• Mod-p cusp forms sit inside mod-p modular forms ModPForms.modPCusp_le_modPMod 0 below · cited by 8 · depth 13
• Mod-3 eigensystems of level prime to 3 occur in weight ≤ 4 ModPForms.exists_three_weight_le_four_mem_modPMod_isModPEigen_pow_mul_of_exists_prime_dvd_mod_three_eq_two 790 below · cited by 1 · depth 14
• Weight drop from 4 to 2 for mod 3 forms ModPForms.mem_modPMod_two_of_mem_modPMod_four_of_forall_coeff_three_mul_eq_zero_of_exists_prime_dvd_mod_three_eq_two 928 below · cited by 1 · depth 14
• Filtration drop in weight p+1 for forms killed by Uₚ ModPForms.mem_modPMod_two_of_mem_modPMod_of_forall_coeff_mul_eq_zero 1,003 below · cited by 1 · depth 14
• Existence of a supersingular datum over 𝔽̄ₚ ModPForms.nonempty_ssDatum_algebraicClosure 1,309 below · cited by 1 · depth 14
• Mod p eigensystems occur, up to twist, in H¹ ModPForms.exists_isEigensystemH1_binaryFormRepSL_of_isModPEigen 42 below · cited by 1 · depth 15
• Eichler–Shimura modulo 3 in weight at most 4 ModPForms.exists_mem_modPMod_isModPEigen_of_isEigensystemH1_binaryFormRepSL_three_of_exists_prime_dvd_mod_three_eq_two 781 below · cited by 1 · depth 15
• Hecke stability of spans of reduced integral q-expansions ModPForms.heckePS_mem_modPMod 4 below · cited by 2 · depth 15
• Agreement of the two normalisations of T_ℓ on power series ModPForms.heckeT_apply_eq_heckePS 0 below · cited by 1 · depth 15
• Mod p forms of weight k lie in weight k+p-1 ModPForms.modPMod_le_modPMod_add_sub_one 1 below · cited by 1 · depth 15
• Weight raising by two in characteristic 3 at suitable levels ModPForms.modPMod_le_modPMod_add_two_of_exists_prime_dvd_mod_three_eq_two 7 below · cited by 1 · depth 15
• Theta raises weight by four in characteristic 3 ModPForms.thetaPS_mem_modPMod_add_four_of_exists_prime_dvd_mod_three_eq_two 84 below · cited by 1 · depth 15
• The theta operator raises mod p weight by p+1 ModPForms.thetaPS_mem_modPMod_add_of_mem 2 below · cited by 1 · depth 15
• Theta raises the filtration when p ∤ k ModPForms.thetaPS_not_mem_modPMod_add_two_of_not_mem_sub_of_not_dvd 999 below · cited by 2 · depth 15
• Theta raises the mod-3 filtration past weight k+2 ModPForms.thetaPS_not_mem_modPMod_add_two_of_not_mem_sub_two_of_not_three_dvd_of_dvd_of_mod_three_eq_two 924 below · cited by 1 · depth 15
• Mod p forms of weight 2m come from modular functions ModPForms.exists_isModPFormFn_qexpOfWeight_eq_of_mem_modPMod 788 below · cited by 20 · depth 16
• Weight-2m q-expansions of mod-p modular functions lie in `modPMod` ModPForms.exists_mem_modPMod_ofPowerSeries_eq_qexpOfWeight_of_isModPFormFn 857 below · cited by 6 · depth 16
• Descent of the space modPMod along a field homomorphism ModPForms.mem_modPMod_of_map_mem_modPMod 0 below · cited by 3 · depth 16
• Weight descent by p-1 under multiplication by P ModPForms.mem_modPMod_sub_of_qP_mul_mem 995 below · cited by 1 · depth 16
• Weight p+1 level N' embeds in weight 2 level N'p ModPForms.modPCusp_add_one_le_modPCusp_mul_two_of_eq_three_imp_exists_prime_dvd_mod_three_eq_two 1,196 below · cited by 1 · depth 16
• Mod p cusp forms of negative weight vanish ModPForms.modPCusp_eq_bot_of_neg 1 below · cited by 2 · depth 16
• Vanishing of mod-p forms of negative weight ModPForms.modPMod_eq_bot_of_neg 1 below · cited by 3 · depth 16
• Vanishing of the mod-p forms of odd weight on Γ₀(N) ModPForms.modPMod_eq_bot_of_odd 0 below · cited by 3 · depth 16
• Mod-p forms of level M embed in level N when M ∣ N ModPForms.modPMod_le_modPMod_of_dvd 0 below · cited by 5 · depth 16
• Weights add under multiplication of reduced modular forms ModPForms.mul_mem_modPMod_add 0 below · cited by 2 · depth 16
• Reduction of ℓ E₂(ℓτ)-E₂(τ) lies in mod-p weight-2 forms ModPForms.natCast_smul_heckeV_qP_sub_qP_mem_modPMod 4 below · cited by 3 · depth 16
• Characteristic 3: the constant 1 is a weight-two form at such levels ModPForms.one_mem_modPMod_two_of_exists_prime_dvd_mod_three_eq_two 5 below · cited by 2 · depth 16
• First Rankin–Cohen bracket on mod-p spans of integral forms ModPForms.smul_mul_thetaPS_sub_smul_thetaPS_mul_mem_modPMod_add_add_two 77 below · cited by 1 · depth 16
• Serre derivative on mod-p q-expansions of level Γ₀(N) ModPForms.smul_thetaPS_sub_smul_mem_modPMod_add_two 1 below · cited by 2 · depth 16
• θ raises the exact weight in characteristic 3 ModPForms.thetaPS_not_mem_modPMod_add_two_of_not_mem_sub_two_of_not_three_dvd_of_dvd_of_mod_three_eq_two_of_isAlgClosed 923 below · cited by 1 · depth 16
• Theta raises the filtration when p ∤ k ModPForms.thetaPS_not_mem_of_sub_smul_mem 0 below · cited by 1 · depth 16
• Dimension lower bound for mod-F cusp forms of weight 2m ModPForms.dimFormulaCusp_le_finrank_modPCusp 662 below · cited by 2 · depth 17
• Mod p forms lie in (θ̄ j)^m F(̄ j,̄ j_N) ModPForms.exists_coe_mul_thetaL_jqModC_pow_eq_ofPowerSeries_of_mem_modPMod 207 below · cited by 2 · depth 17
• Reductions of integral cusp forms give cuspidal mod-p modular functions ModPForms.exists_isModPCuspFormFn_qexpOfWeight_eq_of_mem_modPCusp 789 below · cited by 3 · depth 17
• Cuspidal mod p modular functions lift to cusp forms ModPForms.exists_mem_modPCusp_ofPowerSeries_eq_qexpOfWeight_of_isModPCuspFormFn 985 below · cited by 2 · depth 17
• Mod p weight-2m functions on X₀(N) lift, K algebraically closed ModPForms.exists_mem_modPMod_ofPowerSeries_eq_qexpOfWeight_of_isModPFormFn_of_isAlgClosed 854 below · cited by 2 · depth 17
• Weight-zero mod-p forms are reductions of classical forms ModPForms.exists_mem_modPMod_zero_ofPowerSeries_eq_qexpOfWeight_zero_of_isModPFormFn 0 below · cited by 1 · depth 17
• Kernel of Uₚ on mod-p weight-2 forms of level Np ModPForms.finrank_ker_heckeU_modPCusp_mul_two_le_finrank_modPCusp_two 616 below · cited by 1 · depth 17
• Commutativity of the weight-k coefficient Hecke operators ModPForms.heckePS_heckePS_comm 0 below · cited by 1 · depth 17
• T_ℓ stability of mod-p cusp forms ModPForms.heckePS_mem_modPCusp 4 below · cited by 1 · depth 17
• U₃ sends mod-3 cusp forms of level 3N to weight 4 ModPForms.heckeU_mem_modPCusp_four_of_mem_modPCusp_mul_three_of_exists_prime_dvd_mod_three_eq_two 991 below · cited by 1 · depth 17
• U_ℓ preserves mod-p cusp forms when ℓ ∣ M ModPForms.heckeU_mem_modPCusp_of_dvd 1 below · cited by 1 · depth 17
• Descent of filtration implications from mathbb Fₚ to characteristic p fields ModPForms.mem_modPMod_of_mul_mem_of_forall_zmod 0 below · cited by 1 · depth 17
• Weight detection by B_d over 𝔽̄₃ ModPForms.mem_modPMod_sub_two_of_ladder_mul_mem_modPMod_add_two_of_not_three_dvd_of_dvd_of_mod_three_eq_two_of_isAlgClosed 912 below · cited by 1 · depth 17
• Mod p modular forms base change from 𝔽ₚ ModPForms.modPMod_eq_span_map_modPMod_zmod 0 below · cited by 1 · depth 17
• Characteristic 3: θ raises weight by two, twisted by B_d ModPForms.thetaPS_add_smul_mul_mem_modPMod_add_two 15 below · cited by 1 · depth 17
• Integral cusp forms: reduction preserves rank ModPForms.card_le_finrank_modPCusp_of_linearIndependent 10 below · cited by 2 · depth 18
• Dimension formula bounds the rank of reduced weight-2m forms ModPForms.dimFormula_le_finrank_modPMod 805 below · cited by 2 · depth 18
• Reduced cusp forms with ψ(qᵖ) also reduced vanish ModPForms.eq_zero_of_mem_modPCusp_of_expand_mem_modPCusp 10 below · cited by 2 · depth 18
• Theta operator is injective on weight-two mod p cusp forms ModPForms.eq_zero_of_thetaPS_eq_zero_of_mem_modPCusp_two 900 below · cited by 2 · depth 18
• Multiplicativity of supersingular residues in characteristic 3 ModPForms.exists_forall_res_mul_eq_of_exists_prime_dvd_mod_three_eq_two_of_isAlgClosed 808 below · cited by 1 · depth 18
• Finite-dimensionality of the mod-p forms M_k(N;F) ModPForms.finiteDimensional_modPMod 10 below · cited by 4 · depth 18
• V_ℓ maps mod-p forms of level N to level Nℓ ModPForms.heckeV_mem_modPMod_mul 4 below · cited by 2 · depth 18
• Cuspidality of a mod-p form detected by its weight-2m function ModPForms.mem_modPCusp_of_mem_modPMod_of_isModPCuspFormFn 984 below · cited by 1 · depth 18
• Descent from weight 2m+2 to 2m for mod-3 forms ModPForms.mem_modPMod_of_coe_mul_thetaJ_pow_eq_of_forall_ord_pos_of_exists_prime_dvd_mod_three_eq_two 880 below · cited by 2 · depth 18
• A weight-four form mod 3 with coefficients σ₁(n)-σ₁(n/d) ModPForms.mk_sigma_one_sub_sigma_one_div_mem_modPMod_four_of_dvd 3 below · cited by 2 · depth 18
• Vanishing of supersingular residues for weight 2m in characteristic 3 ModPForms.res_eq_zero_of_mem_modPMod_of_exists_prime_dvd_mod_three_eq_two 790 below · cited by 1 · depth 18
• Non-vanishing at supersingular places of a weight-four series mod 3 ModPForms.res_one_ne_zero_of_not_three_dvd_of_dvd_of_mod_three_eq_two_of_isAlgClosed 908 below · cited by 1 · depth 18
• Integral q-expansions: independence descends to the mod-F span ModPForms.card_le_finrank_modPMod_of_linearIndependent 10 below · cited by 2 · depth 19
• Geometric mod-3 forms of even weight are reductions ModPForms.exists_mem_modPMod_ofPowerSeries_eq_qexpOfWeight_of_isModPFormFn_three_of_exists_prime_dvd_mod_three_eq_two 876 below · cited by 1 · depth 19
• Dimension bound for mod-p reductions of weight-two forms ModPForms.finrank_modPMod_two_le_genusFormula_add_cuspCount_sub_one 818 below · cited by 1 · depth 19
• Weight-2m geometric mod 3 forms come from modular forms ModPForms.exists_mem_modPMod_ofPowerSeries_eq_qexpOfWeight_of_isModPFormFn_of_isAlgClosed_of_charP_three 873 below · cited by 1 · depth 20
• The constant 1 lies in weight-0 mod-p forms ModPForms.one_mem_modPMod_zero 0 below · cited by 1 · depth 20
• The power-series and Laurent-series forms of q d/dq agree ModPForms.ofPowerSeries_thetaPS_eq_thetaL_ofPowerSeries 0 below · cited by 1 · depth 27