← all areas

Namespace CuspForm 692 theorems

Landmarks here: Bad-prime coefficients of weight-2 newforms on Γ₀(N)

— 330 · AuxLevel 12 · Bfam 2 · Bfam0 1 · HasIntegralStructure 5 · HasNebentypus 7 · HeckeGaloisRepDatum 18 · IsAdelicLiftOf 22 · IsAdelicLiftOfGamma1 17 · IsEigenformWith 18 · IsNewform 70 · IsNormalizedEigenform 31 · IsPrimitiveForm 21 · TWLevel 29 · heckeAlgebra 21 · heckeLocal 88

directly in CuspForm 330

• landmark Bad-prime coefficients of weight-2 newforms on Γ₀(N) CuspForm.newformBadPrimeCoeff 68 below · cited by 3 · depth 7
• Eichler–Shimura: adic Galois representation at a Hecke point CuspForm.exists_galoisRep_of_point 1,296 below · cited by 24 · depth 8
• Gluing point-wise Galois representations into a Hecke–Galois datum CuspForm.exists_heckeGaloisRepDatum_pi_eq_and_isUnramifiedAt_of_exists_galoisRep_of_point 48 below · cited by 12 · depth 8
• Weight-one eigensystem realised mod 3 in weight two CuspForm.exists_isLatticeRealized_of_isWeightOneChiNegThreeRealized_of_three_dvd 12 below · cited by 2 · depth 8
• Normalised eigenforms ascend from level M to any multiple N CuspForm.exists_isNormalizedEigenform_of_dvd 4 below · cited by 6 · depth 8
• Equivalence of two encodings of integrality for S₂(Γ₀(N)) CuspForm.hasIntegralBasis_iff_hasIntegralStructure_two 0 below · cited by 6 · depth 8
• Integral structure on weight-2 cusp forms for Γ₀(N) CuspForm.hasIntegralStructure_two 592 below · cited by 54 · depth 8
• Reducedness of the localised weight-2 Hecke algebra CuspForm.isReduced_heckeLocal_of_primeFactors_subset 8 below · cited by 13 · depth 8
• Vanishing of a_q for newforms with q² ∣ N CuspForm.qCoeff_eq_zero_of_isNewform_of_sq_dvd 57 below · cited by 10 · depth 8
• Atkin–Lehner: a_q(f)²=1 for q ∥ N CuspForm.qCoeff_sq_eq_one_of_isNewform 47 below · cited by 12 · depth 8
• Atkin–Lehner eigenvalue of a weight-2 newform is -a_q CuspForm.atkinLehnerLin_eq_neg_qCoeff_smul_of_isNewform 41 below · cited by 5 · depth 9
• Every functional on the Hecke span is T↦ a₁(Tf) CuspForm.exists_form_of_functional_span_heckeAlgebra 14 below · cited by 1 · depth 9
• Depletion at q of a U_q-multiplicative cusp form CuspForm.exists_gamma1_mul_qCoeff_eq_ite_dvd_of_qCoeff_mul 1 below · cited by 1 · depth 9
• Depletion of a Γ₁(N) cusp form away from Q CuspForm.exists_gamma1_qCoeff_eq_ite_coprime 0 below · cited by 4 · depth 9
• Maximality of the occurrence ideal (3, T_ℓ-a_ℓ) CuspForm.exists_isMaximal_three_mem_heckeT_sub_mem 1 below · cited by 1 · depth 9
• Descent of an eigensystem to a newform of divisor level CuspForm.exists_isNewform_descent 0 below · cited by 11 · depth 9
• Existence of a normalised eigenform in S₂(Γ₀(N)) CuspForm.exists_isNormalizedEigenform 27 below · cited by 1 · depth 9
• Deligne–Serre lifting lemma for weight-two Hecke algebras CuspForm.exists_isNormalizedEigenform_congruent_of_isMaximal 69 below · cited by 1 · depth 9
• p-stabilisation of a normalised eigenform to level Mp CuspForm.exists_isNormalizedEigenform_level_mul 3 below · cited by 1 · depth 9
• Realising a partial Hecke eigensystem by a normalised eigenform CuspForm.exists_isNormalizedEigenform_of_forall_heckeTLin_eq_smul 34 below · cited by 10 · depth 9
• Hecke eigencharacter lifting a maximal ideal of T^S CuspForm.exists_isNormalizedEigenform_of_isMaximal_heckeAlgebra 28 below · cited by 3 · depth 9
• Nonvanishing of S₂(Γ₀(11)) CuspForm.exists_ne_zero_gamma0_eleven 10 below · cited by 1 · depth 9
• Mod-3 lattice module realising the weight-two bridge product CuspForm.exists_reductionModule_of_isLatticeRealized 9 below · cited by 1 · depth 9
• Finite-dimensionality of S_k(Γ₀(N)) CuspForm.finiteDimensional_Gamma0 6 below · cited by 38 · depth 9
• dim_ℂ of the Hecke algebra span equals dim S₂(Γ₀(N)) CuspForm.finrank_span_heckeAlgebra_eq_finrank 14 below · cited by 3 · depth 9
• Eigenform criterion for Tₚ in terms of q-coefficients CuspForm.heckeTLin_apply_eq_smul_iff 6 below · cited by 4 · depth 9
• Tₚ and U_q commute on S_k(Γ₀(N)) CuspForm.heckeTLin_heckeULin_comm 11 below · cited by 6 · depth 9
• Uₚ-eigenform criterion on q-expansion coefficients CuspForm.heckeULin_apply_eq_smul_iff 6 below · cited by 4 · depth 9
• Integral q-expansion lattice in S_k(Γ₀(N)) is finitely generated CuspForm.intLattice_fg 8 below · cited by 13 · depth 9
• Dichotomy at an exactly dividing prime: a_q(f)²=1 or descent to level N CuspForm.isNewAt_or_goodEigensystemOccursAt 45 below · cited by 2 · depth 9
• Normalized eigenforms as simultaneous Tₚ, Uₚ eigenfunctions CuspForm.isNormalizedEigenform_iff_heckeT 14 below · cited by 9 · depth 9
• Normalised eigenforms as simultaneous Hecke eigenvectors in S₂(Γ₀(N)) CuspForm.isNormalizedEigenform_iff_heckeTLin 15 below · cited by 24 · depth 9
• The anemic weight-2 Hecke algebra is reduced CuspForm.isReduced_heckeAlgebra_of_primeFactors_subset 7 below · cited by 6 · depth 9
• ℤ-independent Hecke operators stay independent over ℂ CuspForm.linearIndependent_complex_of_linearIndependent_int 581 below · cited by 1 · depth 9
• The integral Hecke algebra preserves the integral lattice CuspForm.mem_intLattice_of_mem_heckeAlgebra 7 below · cited by 9 · depth 9
• Finiteness of the Hecke algebra over ℤ CuspForm.moduleFinite_heckeAlgebra 668 below · cited by 6 · depth 9
• Integral weight-two Hecke algebra is finite over ℤ CuspForm.moduleFinite_heckeAlgebra_two 0 below · cited by 44 · depth 9
• Evaluation of the n-th q-coefficient functional CuspForm.qCoeffLinear_apply 0 below · cited by 3 · depth 9
• Matching a_ℓ(g) with Frobenius traces of a Weierstrass model CuspForm.qCoeff_eq_apOfModel_of_charpoly_frobenius 3 below · cited by 1 · depth 9
• Vanishing constant term of a cusp form on Γ₀(N) CuspForm.qCoeff_zero 1 below · cited by 24 · depth 9
• Hecke eigen-relations force the nebentypus character CuspForm.slash_eq_dirichlet_smul_of_qCoeff_hecke_eigen 8 below · cited by 4 · depth 9
• Atkin–Lehner eigenvalues on S₂(Γ₀(M)) square to 1 CuspForm.sq_eq_one_of_atkinLehnerLin_eq_smul 3 below · cited by 3 · depth 9
• The Atkin–Lehner operator is an involution in weight 2 CuspForm.atkinLehnerLin_atkinLehnerLin 2 below · cited by 11 · depth 10
• Vanishing of Γ₁(M)-cusp forms invariant under diag(p,1) CuspForm.eq_zero_of_slash_heckeDiagMatrix_slash_eq_of_mem_Gamma1 3 below · cited by 5 · depth 10
• Tₚ preserves cusp forms on Γ₀(N) for p ∤ N CuspForm.exists_coe_eq_heckeT 3 below · cited by 2 · depth 10
• Uₚ preserves cusp forms on Γ₀(N) for p ∣ N CuspForm.exists_coe_eq_heckeU 3 below · cited by 5 · depth 10
• Degeneracy map f(τ)↦ f(dτ) from Γ₀(M) to Γ₀(N) CuspForm.exists_degeneracy_Gamma0 0 below · cited by 8 · depth 10
• η(τ)²η(11τ)² is a weight-two cusp form on Γ₀(11) CuspForm.exists_gamma0_eleven_apply_eq_eta_sq_mul_eta_sq 9 below · cited by 1 · depth 10
• Existence of a coefficient ring for a residual Hecke eigensystem CuspForm.exists_heckeCoefficientRing_of_hasIntegralStructure 8 below · cited by 1 · depth 10
• Hecke–Galois datum over an arbitrary complete discrete valuation ring CuspForm.exists_heckeGaloisRepDatum_pi_eq_and_isUnramifiedAt_of_forall_ringHom_exists_galoisRepAdic 647 below · cited by 1 · depth 10
• Every prime of the integral Hecke algebra comes from a normalised eigenform CuspForm.exists_isNormalizedEigenform_annihilator_le_of_isPrime 26 below · cited by 7 · depth 10
• Eigenform realisation at primes of the integral Hecke algebra CuspForm.exists_isNormalizedEigenform_ker_le_of_isPrime 54 below · cited by 2 · depth 10
• Newform attached to a weight-one Hecke eigenform CuspForm.exists_weightOne_newform_of_qCoeff_hecke_eigen 51 below · cited by 1 · depth 10
• The Hecke algebra of S₂(Γ₀(N)) is a finitely generated ℤ-module CuspForm.fg_toSubmodule_heckeAlgebra 1 below · cited by 3 · depth 10
• Finite-dimensionality of cusp forms for arithmetic G CuspForm.finiteDimensional_of_isArithmetic 5 below · cited by 26 · depth 10
• Integral structure on cusp forms for Γ₀(N) in weight ≥ 2 CuspForm.hasIntegralStructure_of_two_le 656 below · cited by 13 · depth 10
• Hecke operators Tₚ, T_q commute on cusp forms CuspForm.heckeTLin_comm 7 below · cited by 9 · depth 10
• Commutativity of Uₚ and U_q on S_k(Γ₀(N)) CuspForm.heckeULin_comm 7 below · cited by 3 · depth 10
• Flatness at p under absolutely irreducible residual representation CuspForm.isFlatAt_of_point_of_not_dvd_of_residual_isAbsolutelyIrreducible 2,271 below · cited by 2 · depth 10
• Normalised eigenforms via Hecke eigen-equations on q-coefficients CuspForm.isNormalizedEigenform_iff_coeffHecke 2 below · cited by 4 · depth 10
• Ordinarity at odd p of a Uₚ-unit point with irreducible ordinary reduction CuspForm.isOrdinaryAt_of_point_of_isUnit_up_of_residual_isAbsolutelyIrreducible_of_residual_isOrdinaryAt 4,944 below · cited by 1 · depth 10
• ℤ-independence implies ℂ-independence for integral cusp forms CuspForm.linearIndependent_of_mem_intLattice 9 below · cited by 5 · depth 10
• Membership in the integral lattice of cusp forms CuspForm.mem_intLattice_iff 1 below · cited by 10 · depth 10
• Tₚ preserves the integral lattice of cusp forms CuspForm.mem_intLattice_of_coe_eq_heckeT 3 below · cited by 3 · depth 10
• Uₚ preserves the lattice of integral cusp forms CuspForm.mem_intLattice_of_coe_eq_heckeU 3 below · cited by 4 · depth 10
• Dichotomy at p‖N: unit Uₚ after extension, or residual local irreducibility CuspForm.point_dichotomy_at_exactly_dvd_of_ne_two 2,511 below · cited by 2 · depth 10
• q-expansion of Tₚ on weight-2 cusp forms CuspForm.qExpansion_heckeTLin 2 below · cited by 3 · depth 10
• Level-lowering trace annihilates w_q f for a newform CuspForm.traceLin_atkinLehnerLin_eq_zero_of_isNewform 40 below · cited by 3 · depth 10
• w_q² = q^{k-2} on cusp forms for Γ₀(M) CuspForm.atkinLehnerLin_atkinLehnerLin_eq_smul 1 below · cited by 1 · depth 11
• Conjugation of cusp forms commutes with all Hecke operators CuspForm.conjForm_heckeTLin_heckeULin_comm 0 below · cited by 1 · depth 11
• Cusp form periodic under all q'^{-j} vanishes CuspForm.eq_zero_of_forall_vadd_inv_pow_eq 0 below · cited by 2 · depth 11
• Pseudo-eigenvalue of the Fricke involution on a primitive form CuspForm.exists_apply_eq_mul_zpow_mul_apply_of_isPrimitiveForm 38 below · cited by 3 · depth 11
• η(Nτ)²⁴ is a weight-12 cusp form on Γ₀(N) CuspForm.exists_gamma0_apply_eq_eta_mul_pow_twentyfour 1 below · cited by 3 · depth 11
• Conjugate cusp form on Γ₁(M) with conjugated q-coefficients CuspForm.exists_gamma1_apply_eq_conj_and_qCoeff_eq_conj 0 below · cited by 8 · depth 11
• Existence of an adelic lift of a weight-two cusp form CuspForm.exists_isAdelicLiftOf 0 below · cited by 3 · depth 11
• Newform and unit root behind a unit Uₚ-value CuspForm.exists_isNewform_of_point_of_isUnit_up 104 below · cited by 2 · depth 11
• Existence of an attached primitive form (Atkin–Lehner–Li) CuspForm.exists_isPrimitiveForm_of_qCoeff_hecke_eigen 36 below · cited by 4 · depth 11
• p-depletion of a cusp form on Γ₁(N) CuspForm.exists_qCoeff_eq_ite_dvd_of_prime 0 below · cited by 1 · depth 11
• Hecke's functional equation for Fricke-paired weight-one forms CuspForm.exists_weightOne_completedLSeries_functionalEquation_of_fricke 0 below · cited by 1 · depth 11
• dim_ℂ S₂(Γ₀(N)) equals the genus formula CuspForm.finrank_gamma0_weight_two_eq_genusFormula 583 below · cited by 3 · depth 11
• Integral structure of S_k(Γ₀(N)) from the Hecke algebra CuspForm.hasIntegralStructure_of_moduleFinite_of_linearIndependent 9 below · cited by 1 · depth 11
• Flatness at p for Hecke points of level prime to p CuspForm.isFlatAt_of_point_of_not_dvd 2,270 below · cited by 2 · depth 11
• Hecke independence over ℂ from a period package CuspForm.linearIndependent_complex_of_linearIndependent_int_of_periodPackage 0 below · cited by 1 · depth 11
• Li's bound |b_ℓ|² ≤ ℓ^{k-1} at primes dividing the level CuspForm.norm_qCoeff_sq_le_of_isPrimitiveForm 12 below · cited by 1 · depth 11
• Residual irreducibility at p when χ₀(Tₚ) is a non-unit CuspForm.point_residual_stable_eq_bot_or_top_of_not_isUnit_heckeT_of_ne_two 2,494 below · cited by 4 · depth 11
• No weight-4 cusp forms on Γ₀(1) or Γ₀(2) CuspForm.subsingleton_gamma0_four_of_eq_one_or_eq_two 0 below · cited by 1 · depth 11
• Invariance of y under translations by q'^{-j} CuspForm.vadd_inv_pow_eq_of_slash_heckeDiagMatrix_invariant 1 below · cited by 2 · depth 11
• Conjugate Hecke eigenvalue equals ε(p)⁻¹λ CuspForm.conj_heckeEigenvalue_eq_of_hasNebentypus 7 below · cited by 6 · depth 12
• Eisenstein congruence mod m forces m ∣ n(p) CuspForm.dvd_eisensteinNumerator_of_qCoeff_congr_sigmaPrimeTo 572 below · cited by 1 · depth 12
• Multiplicity one at the level of a primitive form CuspForm.eq_smul_of_isPrimitiveForm_of_qCoeff_hecke_eigen 31 below · cited by 6 · depth 12
• Nondegeneracy in the operator variable of the a₁-pairing CuspForm.eq_zero_of_mem_span_heckeAlgebra_of_forall_qCoeff_one_eq_zero 14 below · cited by 3 · depth 12
• A basis of S₂(Γ₀(N)) with rational Hecke matrices CuspForm.exists_basis_repr_heckeTLin_heckeULin_mem_range_ratCast 593 below · cited by 3 · depth 12
• Trace from Γ₀(M) to Γ₀(R) of a cusp form CuspForm.exists_coe_eq_add_smul_heckeU_alSlash 0 below · cited by 5 · depth 12
• Automorphism conjugates of weight-2 normalised eigenforms on Γ₀(M) CuspForm.exists_conj_isNormalizedEigenform_isNewAt 593 below · cited by 1 · depth 12
• Iterated Uₚ of p-th powers: a Frobenius-twisted cusp form CuspForm.exists_cuspForm_mul_ordCompl_qCoeff_congr_pow_of_sq_dvd 6 below · cited by 1 · depth 12
• Hecke eigenplane in the Tate module of J₀(N) CuspForm.exists_eigenPlane_tateModule_jZero_of_point 1,289 below · cited by 3 · depth 12
• Deligne–Serre lifting: eigenform congruent to a mod-𝔪 eigensystem CuspForm.exists_eigenform_qCoeff_congr_of_heckeT_sub_mem 22 below · cited by 1 · depth 12
• Fundamental character of level two for non-unit Tₚ, p odd CuspForm.exists_galoisRepAdic_inertia_eigenvector_tameCharacter_of_not_isUnit_heckeT_of_ne_two 2,460 below · cited by 2 · depth 12
• Fricke involution preserves cusp forms on Γ₁(M) CuspForm.exists_gamma1_apply_eq_zpow_mul_apply_of_mul_eq_neg_one 0 below · cited by 1 · depth 12
• U_ℓ lowers the level when ℓ² ∣ N CuspForm.exists_gamma1_div_coe_eq_heckeU_of_dvd_div 3 below · cited by 2 · depth 12
• Hecke eigen-relations produce a nebentypus character CuspForm.exists_hasNebentypus_of_qCoeff_hecke_eigen 8 below · cited by 5 · depth 12
• Away-from-S Hecke points factor through newform eigencharacters CuspForm.exists_isNewform_point_factor 639 below · cited by 12 · depth 12
• Deligne–Serre realisation inside the q-new trace kernel CuspForm.exists_isNormalizedEigenform_isNewAt_of_heckeAlgebra_support 47 below · cited by 1 · depth 12
• Normalised joint Hecke eigenform with integral eigenvalue coefficients CuspForm.exists_normalized_eigenvector 23 below · cited by 1 · depth 12
• Oldspace expansion of an eigenform matching a newform CuspForm.exists_qCoeff_eq_sum_divisors_of_isNewform_matching 99 below · cited by 3 · depth 12
• Newform decomposition of cusp forms with nebentypus CuspForm.exists_qCoeff_eq_sum_isPrimitiveForm_of_hasNebentypus 33 below · cited by 7 · depth 12
• Integral cusp form with Eisenstein Hecke eigenvalues modulo m CuspForm.exists_qIntegral_eisenstein_eigen_mod_of_injective 27 below · cited by 2 · depth 12
• Congruence of a level-pN' cusp form to higher weight level N' CuspForm.exists_weight_ge_qCoeff_congr_level_div_of_alSlash_p_integral 10 below · cited by 1 · depth 12
• The Hecke field of a weight-2 eigenform is a number field CuspForm.finiteDimensional_adjoin_qCoeff 20 below · cited by 3 · depth 12
• Upper bound dim S₂(Γ₀(N)) ≤ g CuspForm.finrank_gamma0_weight_two_le_genusFormula 35 below · cited by 2 · depth 12
• Algebraic integrality of all q-coefficients of a normalised eigenform CuspForm.forall_exists_qCoeff_eq_of_isNormalizedEigenform 19 below · cited by 4 · depth 12
• Genus formula bounds dim_ℂ S₂(Γ₀(N)) from below CuspForm.genusFormula_le_finrank_gamma0_weight_two 551 below · cited by 6 · depth 12
• Fricke transform inverts nebentypus and twists Tₚ-eigenvalues CuspForm.hasNebentypus_inv_and_qCoeff_hecke_eigen_of_fricke 4 below · cited by 1 · depth 12
• Hecke words annihilating the new lattice kill new parabolic homomorphisms CuspForm.heckeWordHom_eq_zero_of_forall_newLattice 629 below · cited by 1 · depth 12
• Conjugate of a primitive form is primitive with inverse nebentypus CuspForm.isPrimitiveForm_inv_of_qCoeff_eq_conj 2 below · cited by 6 · depth 12
• Li's theorem: |b_ℓ|²=ℓ^{k-2} at an exact level divisor CuspForm.norm_qCoeff_sq_eq_pow_of_isPrimitiveForm_of_not_sq_dvd 8 below · cited by 3 · depth 12
• U_ℓ-eigenvalues at a prime ramified in the nebentypus CuspForm.norm_sq_eq_pow_of_qCoeff_mul_eq_of_not_factorsThrough 0 below · cited by 3 · depth 12
• Eigenvalue aₚ² ≠ (1+p)² at primes not dividing the level CuspForm.qCoeff_sq_ne_one_add_sq_of_isNormalizedEigenform 1,195 below · cited by 1 · depth 12
• Hecke operators killing the new lattice kill the new subspace CuspForm.apply_eq_zero_of_traceLin_eq_zero_of_forall_mem_newLattice 624 below · cited by 1 · depth 13
• w_q commutes with U_ℓ for ℓ ≠ q CuspForm.atkinLehnerLin_heckeULin 0 below · cited by 2 · depth 13
• Lower bound for dim S_k(Γ₀(N)), k≥ 4 even CuspForm.dimFormula_le_finrank_gamma0 548 below · cited by 2 · depth 13
• Eisenstein congruences on Γ₀(p) force m ∣ (p-1)/2 CuspForm.dvd_half_sub_one_of_qCoeff_congr_sigmaPrimeTo 565 below · cited by 1 · depth 13
• Eisenstein congruence forces m ∣ (p²-1)/24 CuspForm.dvd_sq_sub_one_div_of_qCoeff_congr_sigmaPrimeTo 22 below · cited by 1 · depth 13
• Eisenstein congruences detect m-divisibility in the Hecke algebra CuspForm.eisenstein_injective_of_qCoeff_congr_sigmaPrimeTo 2 below · cited by 1 · depth 13
• Simultaneous eigenbasis for nebentypus and Hecke operators on Γ₁(N) CuspForm.exists_basis_hasNebentypus_qCoeff_hecke_eigen 16 below · cited by 7 · depth 13
• Level lowering by one power of p via Uₚ(gᵖ) CuspForm.exists_coe_eq_heckeU_pow_and_qCoeff_sub_pow_mem_span 5 below · cited by 1 · depth 13
• Degeneracy map g(dτ) from level M to level N CuspForm.exists_degeneracy_gamma1_hasNebentypus 1 below · cited by 12 · depth 13
• Eichler–Shimura representation as a quotient of Tₚ(J₀(N)) CuspForm.exists_galoisRep_of_point_tateModule_jZero_quotient 1,296 below · cited by 1 · depth 13
• U_ℓ preserves cusp forms on Γ₁(N) when ℓ ∣ N CuspForm.exists_gamma1_coe_eq_heckeU_of_dvd 3 below · cited by 4 · depth 13
• Atkin–Lehner level lowering along a nebentypus CuspForm.exists_hasNebentypus_qCoeff_eq_sum_primeFactors_of_forall_coprime_qCoeff_eq_zero 30 below · cited by 3 · depth 13
• Normalized eigenform in a Hecke-stable subspace supporting a prime CuspForm.exists_isNormalizedEigenform_mem_annihilator_le_of_isPrime 26 below · cited by 1 · depth 13
• Hecke algebra realises all q-coefficients through a₁ CuspForm.exists_mem_heckeAlgebra_qCoeff_apply_one_eq 2 below · cited by 2 · depth 13
• A non-zero multiple of Tₚ lies in T^S CuspForm.exists_ne_zero_nsmul_heckeTLin_mem_heckeAlgebra 694 below · cited by 1 · depth 13
• Conjugate cusp form with conjugated q-coefficients on Γ₀(N) CuspForm.exists_qCoeff_conj 0 below · cited by 4 · depth 13
• Mod m functionals on the Hecke algebra realised by cusp forms CuspForm.exists_qIntegral_qCoeff_apply_one_eq_of_hasIntegralBasis 23 below · cited by 1 · depth 13
• Eisenstein congruence modulo n(p) for weight-two cusp forms CuspForm.exists_qIntegral_qCoeff_congr_sigmaPrimeTo_eisensteinNumerator 882 below · cited by 1 · depth 13
• Eisenstein character mod m on the weight-two Hecke algebra CuspForm.exists_ringHom_zmod_of_eisenstein_injective 2 below · cited by 1 · depth 13
• Finite-dimensionality of S_k(Γ₀(N)) CuspForm.finiteDimensional_cuspForm 0 below · cited by 4 · depth 13
• Hecke operators at ℓ commute with degeneracy rescaling CuspForm.heckeTLin_rescaleLin 3 below · cited by 18 · depth 13
• The prime-level weight-two lattice Hecke algebra is reduced CuspForm.isReduced_heckeLatticeAlgebra 611 below · cited by 3 · depth 13
• Sesquilinearity of the Petersson product on cusp forms CuspForm.peterssonOn_add_smul_conj 0 below · cited by 2 · depth 13
• Adjointness of Tₚ on a nebentypus component CuspForm.peterssonOn_hecke_eq_conj_mul_of_hasNebentypus 0 below · cited by 2 · depth 13
• Positive definiteness of the Petersson self-product CuspForm.peterssonOn_self_re_nonneg_im_eq_zero_eq_zero_iff 0 below · cited by 2 · depth 13
• Vanishing of Tr(w_qf) forces a_q(f)²=1 CuspForm.qCoeff_sq_eq_one_of_traceLin_atkinLehnerLin_eq_zero 20 below · cited by 2 · depth 13
• Rescaled newforms span the weight-2 cusp forms for Γ₀(M) CuspForm.span_rescaleLin_isNewform_eq_top 53 below · cited by 13 · depth 13
• Level-lowering trace commutes with T_ℓ for ℓ ∤ M CuspForm.traceLin_heckeTLin 13 below · cited by 2 · depth 13
• Level-lowering trace commutes with U_ℓ, ℓ≠ q CuspForm.traceLin_heckeULin 9 below · cited by 1 · depth 13
• U_q stabilises the q-new kernel of the trace pair CuspForm.traceLin_heckeULin_eq_zero_of_traceLin_eq_zero_of_traceLin_atkinLehnerLin_eq_zero 3 below · cited by 1 · depth 13
• 24m divides a₁(p-1)τ(p) for Eisenstein congruences CuspForm.dvd_mul_qCoeff_discriminant_prime_of_qCoeff_congr_sigmaPrimeTo 10 below · cited by 1 · depth 14
• 24m ∣ a₁(p-1)bigl(τ(p²)-p¹²bigr) CuspForm.dvd_mul_qCoeff_discriminant_prime_sq_sub_pow_of_qCoeff_congr_sigmaPrimeTo 10 below · cited by 1 · depth 14
• Cusp forms of odd weight on Γ₀(N) vanish CuspForm.eq_zero_of_odd_gamma0 0 below · cited by 1 · depth 14
• Vanishing of a cusp form supported on multiples of p ∤ m CuspForm.eq_zero_of_prime_not_dvd_of_qCoeff_eq_zero 10 below · cited by 4 · depth 14
• Slash-invariant combinations of rational slashes are cusp forms CuspForm.exists_eq_sum_smul_slash_of_forall_slash_eq 0 below · cited by 2 · depth 14
• Eisenstein congruence produces a weight-two form divisible by 24m CuspForm.exists_modularForm_qCoeff_eq_of_qCoeff_congr_sigmaPrimeTo 4 below · cited by 5 · depth 14
• Nonzero level-N form with prescribed T_ℓ and U_q eigenvalues CuspForm.exists_ne_zero_heckeTLin_eq_smul_heckeULin_eq_of_isNewform_of_sq_dvd 6 below · cited by 1 · depth 14
• Atkin–Lehner: coefficients vanishing off K force lower level CuspForm.exists_qCoeff_eq_sum_primeFactors_of_forall_coprime_qCoeff_eq_zero 11 below · cited by 1 · depth 14
• Rationality of q-coefficients of level-lowering traces CuspForm.exists_ratCast_qCoeff_traceLin_of_forall_intCast_qCoeff 603 below · cited by 3 · depth 14
• Ring homomorphisms on the weight-2 Hecke algebra are determined by the T_ℓ CuspForm.heckeAlgebra_ringHom_ext_of_primeFactors_subset 0 below · cited by 2 · depth 14
• Surjectivity of the abstract Hecke evaluation on S_k(Γ₀(N)) CuspForm.heckeEvalForms_range_eq_top 0 below · cited by 6 · depth 14
• T_{ℓ_0} lies in the algebra generated by T_ℓ, ℓ notin S CuspForm.heckeTLin_mem_adjoin_heckeTLin_of_finite 99 below · cited by 4 · depth 14
• At prime level ℓ: U_ℓ = -w_ℓ on S₂(Γ₀(ℓ)) CuspForm.heckeULin_eq_neg_atkinLehnerLin_of_prime_level 4 below · cited by 1 · depth 14
• Integral lattice of cusp forms is free of finite rank CuspForm.intLattice_free_and_finite 9 below · cited by 7 · depth 14
• Vanishing of coefficients coprime to N forces oldform CuspForm.mem_span_rescaleLin_prime_of_forall_coprime_qCoeff_eq_zero 15 below · cited by 4 · depth 14
• A prime p cannot divide the Eisenstein modulus CuspForm.not_prime_dvd_of_qCoeff_congr_sigmaPrimeTo 11 below · cited by 2 · depth 14
• Additivity of the Petersson pairing in the first variable CuspForm.petersson_add_left 0 below · cited by 5 · depth 14
• Conjugate symmetry of the Petersson pairing on Γ₀(N) CuspForm.petersson_conj_symm 0 below · cited by 5 · depth 14
• Self-adjointness of Tₚ for the Petersson product at p ∤ N CuspForm.petersson_heckeTLin 0 below · cited by 5 · depth 14
• Vanishing of the Petersson norm characterises the zero cusp form CuspForm.petersson_self_eq_zero_iff 0 below · cited by 5 · depth 14
• Petersson pairing is conjugate-linear in its first argument CuspForm.petersson_smul_left 0 below · cited by 5 · depth 14
• Vanishing of coefficients coprime to the level for Hecke eigenvectors CuspForm.qCoeff_eq_zero_of_coprime_of_forall_heckeTLin_eq_smul_of_qCoeff_one_eq_zero 1 below · cited by 1 · depth 14
• Good Hecke eigenvectors span S₂(Γ₀(M)) CuspForm.span_heckeTLin_eigen_eq_top 21 below · cited by 3 · depth 14
• χ(U_q)=± 1 at a prime q ∥ N with ρ̄ ramified CuspForm.apply_U_eq_intCast_of_point_of_not_isUnramifiedAt 1,425 below · cited by 2 · depth 15
• Divisibility forced by an Eisenstein congruence on Γ₀(p) CuspForm.dvd_240_mul_qCoeff_one_sq_of_qCoeff_congr_sigmaPrimeTo 8 below · cited by 1 · depth 15
• Forcing 24m ∣ 504 a₁³(p-1)³(p²-1) from Eisenstein congruences CuspForm.dvd_504_mul_qCoeff_one_cube_of_qCoeff_congr_sigmaPrimeTo 8 below · cited by 1 · depth 15
• Vanishing of weight-two cusp forms for Γ₀(1) CuspForm.eq_zero_of_gamma0_one_weight_two 0 below · cited by 1 · depth 15
• Vanishing of S₂(Γ₀(N)) for N ∣ 4 or N ∣ 9 CuspForm.eq_zero_of_level_dvd_four_or_dvd_nine 48 below · cited by 1 · depth 15
• A rational q-expansion basis for S_k(Γ₁(N)) CuspForm.exists_basis_gamma1_qCoeff_mem_range_ratCast 41 below · cited by 4 · depth 15
• U_q lowers the level when q² divides it CuspForm.exists_coe_eq_heckeU_of_mul_eq_of_dvd 0 below · cited by 1 · depth 15
• Deligne–Serre lifting over a complete DVR, weight two CuspForm.exists_ringHom_heckeAlgebra_residue_eq_map_of_hasIntegralStructure 3 below · cited by 5 · depth 15
• Splitting a Γ₁(N)-invariant sum into Γ₁(N/p)-invariant pieces CuspForm.exists_sum_eq_forall_gamma1_div_slash_eq 1 below · cited by 1 · depth 15
• Nonnegativity of the self-Petersson pairing's real part CuspForm.petersson_self_re_nonneg 0 below · cited by 2 · depth 15
• Frobenius charpoly congruence at the excluded primes ℓ ∤ Np CuspForm.point_residual_charpoly_frobenius_eq_of_forall_not_mem 1,321 below · cited by 3 · depth 15
• Residual Tₚ-eigenvalue as Frobenius trace on inertia coinvariants CuspForm.point_residual_trace_coinvariants_eq_residue_T 2,611 below · cited by 3 · depth 15
• Reduction of χ(U_q) as Frobenius trace on inertia coinvariants CuspForm.point_residual_trace_coinvariants_eq_residue_U_of_isUnit 4,978 below · cited by 4 · depth 15
• Trace zero on inertia coinvariants in the supersingular case CuspForm.point_residual_trace_coinvariants_eq_zero_of_not_isUnit_U 2,563 below · cited by 3 · depth 15
• Coefficients prime to K vanish implies coefficients prime to N vanish CuspForm.qCoeff_eq_zero_of_coprime_level_of_forall_coprime_qCoeff_eq_zero 6 below · cited by 1 · depth 15
• q-coefficients of the rescaling map V_d on cusp forms CuspForm.qCoeff_rescaleLin 2 below · cited by 5 · depth 15
• Diamond slashes of Γ_H(M) cusp forms vanish at cusps CuspForm.stableD 2 below · cited by 57 · depth 15
• Stability of the Γ_H Hecke operator T_ℓ on cusp forms CuspForm.stableT 5 below · cited by 24 · depth 15
• U_q preserves cusp forms on Γ_H(M) CuspForm.stableU 3 below · cited by 28 · depth 15
• Joint vanishing of x+y∣_kdiag(q',1) for cusp forms CuspForm.eq_zero_of_coe_add_slash_heckeDiagMatrix_eq_zero 3 below · cited by 1 · depth 16
• Antiholomorphic conjugation preserves cusp forms for J-stable Γ CuspForm.exists_apply_eq_conj_apply_J_smul_of_forall_jConjSL_mem 0 below · cited by 3 · depth 16
• Cyclotomic basis for cusp forms on Γ₁(N) CuspForm.exists_basis_gamma1_qCoeff_mem_adjoin_exp 34 below · cited by 1 · depth 16
• Integral q-expansion basis for S_k(Γ₁(N)) CuspForm.exists_basis_gamma1_qCoeff_slash_mem_range_intCast 52 below · cited by 8 · depth 16
• Oldforms at p∤ M in weight two: eigensystem descent CuspForm.exists_eq_rescaleLin_add_rescaleLin_of_heckeTLin_eq_smul_of_exists_level 101 below · cited by 1 · depth 16
• Bounded p-denominators of (⟨ d⟩ F)∣ W at 𝔪 CuspForm.exists_forall_qCoeff_alSlash_diamondLinH_p_integral_of_isIntegralQExp 36 below · cited by 1 · depth 16
• Serre's Eisenstein-trace congruence at level Γ_H(M) CuspForm.exists_forall_weight_add_mul_qCoeff_congr_gammaH_level_div_of_alSlash_diamondLinH_p_integral 16 below · cited by 1 · depth 16
• Adic Galois representation at q ‖ N with U_q a unit CuspForm.exists_galoisRepAdic_of_point_stableLine_frobenius_sub_smul_mem_of_isUnit_U 4,965 below · cited by 2 · depth 16
• Galois stability of K-rational cusp forms on Γ₁(N) CuspForm.exists_gamma1_qCoeff_eq_algEquiv_apply 27 below · cited by 1 · depth 16
• U_q on S₂(Γ₀(N)) killed by X R(X) with R(0)∣ qᵃ CuspForm.exists_heckeULin_mul_aeval_eq_zero_of_sq_dvd_of_not_cube_dvd 95 below · cited by 1 · depth 16
• Existence of an adelic lift for Γ₁(M) cusp forms of weight two CuspForm.exists_isAdelicLiftOfGamma1 0 below · cited by 1 · depth 16
• Newform behind a weight-two Hecke point with uₚ ∣ p CuspForm.exists_isNewform_of_point_of_up_dvd 104 below · cited by 6 · depth 16
• Existence of an attached primitive form for Tₚ-eigenvalues, p∤ N CuspForm.exists_isPrimitiveForm_of_hasNebentypus_qCoeff_hecke_eigen 34 below · cited by 10 · depth 16
• Ribet's lemma: Hecke subring of index prime to p CuspForm.exists_not_dvd_and_smul_mem_heckeAlgebra_of_finite 1,231 below · cited by 2 · depth 16
• Weight-two cusp forms are cyclic over the complex Hecke algebra CuspForm.exists_top_eq_heckeAlgebra_adjoin_smul 101 below · cited by 1 · depth 16
• Vanishing of cusp forms when k ψ(N) < 12 CuspForm.gamma0_eq_zero_of_mul_dedekindPsi_lt_twelve 11 below · cited by 1 · depth 16
• Vanishing of S₂(Γ₀(N)) when the genus formula gives 0 CuspForm.gamma0_weight_two_eq_zero_of_genusFormula_eq_zero 37 below · cited by 1 · depth 16
• Vanishing of cusp forms supported on multiples of p CuspForm.gamma1_eq_zero_of_prime_not_dvd_of_qCoeff_eq_zero 4 below · cited by 1 · depth 16
• A Frobenius functional on the complex weight-2 Hecke algebra CuspForm.heckeAlgebra_adjoin_exists_frobenius_form 104 below · cited by 1 · depth 16
• T_ℓ commutes with the Γ₀(M)-action on S_k(Γ₁(M)) CuspForm.heckeTLinOne_slashOfMemGamma0 0 below · cited by 3 · depth 16
• U_q acts by a_q(g) on the g-eigenpacket CuspForm.heckeULin_eq_qCoeff_smul_of_isNewform_of_dvd_of_not_dvd_div 100 below · cited by 3 · depth 16
• Reducedness of algebras generated by the anemic weight-two Hecke algebra CuspForm.isReduced_of_adjoin_range_heckeAlgebra_eq_top 9 below · cited by 1 · depth 16
• Vanishing of S₄(Γ₀(2)) CuspForm.levelTwo_weight_four_eq_zero 0 below · cited by 1 · depth 16
• Cuspidal T_q-eigenvalues at good primes lie below q+1 CuspForm.norm_lt_of_heckeTLin_eq_smul 8 below · cited by 2 · depth 16
• q-expansion of Tₚ on S_k(Γ₁(M)) CuspForm.qCoeff_heckeTLinOne 3 below · cited by 15 · depth 16
• Lower-unipotent coset sum of the doubly q-rescaled cusp form CuspForm.sum_range_slash_heckeDiagMatrix_heckeDiagMatrix_conj_eq 3 below · cited by 1 · depth 16
• Trace of a cusp form from Γ_H(M) to Γ_{H'}(M/p) CuspForm.exists_GammaH_coe_eq_add_smul_heckeU_alSlash_diamondLinH 6 below · cited by 1 · depth 17
• Atkin–Lehner slash preserves cusp forms on Γ_H(M) CuspForm.exists_GammaH_coe_eq_alSlash 6 below · cited by 22 · depth 17
• Integral q-expansion map on S_k(Γ₀(N);ℤ) is saturated CuspForm.exists_addMonoidHom_intLattice_qCoeff_saturated 3 below · cited by 4 · depth 17
• Cyclotomic rational basis for S_k(Γ₁(N)), k even CuspForm.exists_basis_gamma1_qCoeff_mem_adjoin_exp_of_even 30 below · cited by 1 · depth 17
• Integral basis for weight-two cusp forms on Γ₁(M) CuspForm.exists_basis_gamma1_two_qCoeff_mem_range_intCast 53 below · cited by 3 · depth 17
• Weight-two cusp forms form a cyclic Hecke module CuspForm.exists_cyclic_span_heckeAlgebra 100 below · cited by 2 · depth 17
• Finite family of newforms spanning S₂(Γ₀(M)), separated at good primes CuspForm.exists_finite_separated_newform_family 99 below · cited by 2 · depth 17
• Flat p-adic Galois representation attached to a weight-two Hecke eigensystem, p ∤ N CuspForm.exists_galoisRep_isFlatAt_of_point_of_not_dvd 2,275 below · cited by 3 · depth 17
• Hecke eigensystem representation with a Frobenius-stable line at q CuspForm.exists_galoisRep_of_point_stableLine_frobenius_sub_smul_mem_of_not_dvd 1,303 below · cited by 1 · depth 17
• Galois stability of even-weight K-rational cusp forms on Γ₁(N) CuspForm.exists_gamma1_qCoeff_eq_algEquiv_apply_of_even 23 below · cited by 1 · depth 17
• Annihilating polynomial for U_q when q² exactly divides N CuspForm.exists_heckeULin_mul_aeval_eq_zero_isIntegral_of_sq_dvd_of_not_cube_dvd 89 below · cited by 1 · depth 17
• Denominator at most p for Wₚ on integral weight-two cusp forms CuspForm.exists_int_mul_qCoeff_alSlash_of_mem_intLattice 1,068 below · cited by 1 · depth 17
• Deligne–Serre lifting for the full weight-2 Hecke algebra CuspForm.exists_isNormalizedEigenform_ker_of_isMaximal 631 below · cited by 1 · depth 17
• Tᵣ is congruent mod p to Hecke operators away from r CuspForm.exists_mem_heckeAlgebra_insert_heckeTLin_eq_add_smul_of_ne 1,077 below · cited by 2 · depth 17
• Tₚ is congruent mod p to Hecke operators away from p CuspForm.exists_mem_heckeAlgebra_singleton_heckeTLin_eq_add_smul_of_ne_two 918 below · cited by 1 · depth 17
• Serre's weight p+1 congruence for Uₚ of a weight-2 form CuspForm.exists_mem_intLattice_weight_succ_qCoeff_congr_heckeU_of_alSlash_integral 12 below · cited by 1 · depth 17
• Fourier coefficients of U_q on S_k(Γ_H(M)) for q ∣ M CuspForm.qCoeff_heckeULinH_eq_qCoeff_mul 5 below · cited by 7 · depth 17
• Trace of the rescaling equals T_{q'} CuspForm.traceLin_rescaleLin 1 below · cited by 1 · depth 17
• Square of the Atkin–Lehner slash equals p^{k-2}⟨ d⟩ CuspForm.alSlash_alSlash_eq_pow_smul_diamondLinH 3 below · cited by 9 · depth 18
• Determinant of Uₚ on S₂(Γ₀(Rp)) is ± p^{dim S₂(Γ₀(R))} CuspForm.det_heckeULin_two_eq_pow_finrank_or_eq_neg 17 below · cited by 1 · depth 18
• A Γ₀(M) cusp form as a Γ₁(M) form with trivial nebentypus CuspForm.exists_gamma1_coe_eq_and_hasNebentypus_one 0 below · cited by 2 · depth 18
• Galois transport of Γ₁(N) cusp forms with Fricke expansions CuspForm.exists_gamma1_frickeRational_sigmaTransport 16 below · cited by 1 · depth 18
• Refining a partial Hecke eigenform to a full eigenform CuspForm.exists_hasNebentypus_qCoeff_hecke_eigen_forall_of_qCoeff_hecke_eigen_of_not_mem 15 below · cited by 1 · depth 18
• Atkin–Lehner slash at p has denominator dividing p CuspForm.exists_int_mul_qCoeff_alSlash_of_mem_intLattice_of_ne_two 980 below · cited by 1 · depth 18
• Mod 3 congruence between U₃ f and a weight-4 form CuspForm.exists_mem_intLattice_four_qCoeff_congr_heckeU_three_of_alSlash_integral 9 below · cited by 1 · depth 18
• Recognising cusp forms through F = f E₄ᵃE₆ᵇ/Δ^m CuspForm.exists_mul_E4_pow_mul_E6_pow_eq_iff 2 below · cited by 3 · depth 18
• Rank one and multiplicity one for S₂(Γ_H(M)) CuspForm.nonempty_basis_fin_one_gammaH_and_finrank_eigenspace_eq_one 83 below · cited by 1 · depth 18
• Normalisation of a Hecke eigenform with nebentypus CuspForm.qCoeff_one_ne_zero_and_isEigenformWith_smul_of_hasNebentypus_of_qCoeff_hecke_eigen_forall 3 below · cited by 2 · depth 18
• Rational fractions in j and Fricke functions span cusp forms CuspForm.span_frickeRational_E4_pow_E6_pow_eq_top 22 below · cited by 1 · depth 18
• Uᵣ-eigenvalues are roots of X²-aᵣ(g₀)X+r CuspForm.sq_sub_qCoeff_mul_add_eq_zero_of_heckeULin_eq_smul_of_isNewform 101 below · cited by 1 · depth 18
• Trace of the second oldform embedding is T_q CuspForm.traceLin_of_coe_eq_slash_heckeDiagMatrix 0 below · cited by 1 · depth 18
• 𝔪-torsion in L/pL embeds into T/𝔪 CuspForm.exists_injective_linearMap_torsionBySet_intLattice_quotient 6 below · cited by 1 · depth 19
• Atkin–Lehner–Li basis of S_k(Γ_H(M)) CuspForm.exists_isPrimitiveForm_basis_gammaH_and_heckeTLinH_and_diamondLinH_and_heckeULinH_apply 78 below · cited by 4 · depth 19
• Conjugation by diag(q,1) transports weight-two cusp forms and periods CuspForm.exists_linearEquiv_gamma_inf_gamma0_gammaH_slash_heckeDiagMatrix_and_periodOf_eq 4 below · cited by 2 · depth 19
• Commutativity of T_ℓ, U_q and ⟨ d⟩ on S_k(Γ_H(M)) CuspForm.heckeTLinH_heckeULinH_diamondLinH_comm 79 below · cited by 9 · depth 19
• Commutativity of U_q and U_{q'} on S_k(Γ_H(M)) CuspForm.heckeULinH_comm 5 below · cited by 3 · depth 19
• Vanishing horocycle integral of a cusp form at every cusp CuspForm.intervalIntegral_slash_vadd_eq_zero 0 below · cited by 1 · depth 19
• Strict bound |a|²<(p+1)²p^{k-2} for Hecke eigenvalues CuspForm.norm_sq_lt_of_hasNebentypus_qCoeff_hecke_eigen 0 below · cited by 4 · depth 19
• Vanishing constant q-coefficient of Γ₁(M) cusp forms CuspForm.qCoeff_zero_eq_zero_gamma1 1 below · cited by 2 · depth 19
• Action of ⟨ d⟩, T_ℓ, U_q on a nebentypus form CuspForm.coe_diamondLinH_and_coe_heckeTLinH_and_coe_heckeULinH_of_hasNebentypus 10 below · cited by 3 · depth 20
• Nebentypus decomposition of cusp forms for Γ_H(M) CuspForm.exists_finset_dirichlet_sum_eq_and_independent_of_gammaH 0 below · cited by 1 · depth 20
• A cusp form for Γ_H(M) is one for Γ₁(M) CuspForm.exists_gamma1_coe_eq_of_gammaH 0 below · cited by 3 · depth 20
• Cusp forms with nebentypus trivial on H descend to Γ_H(M) CuspForm.exists_gammaH_coe_eq_of_hasNebentypus 0 below · cited by 2 · depth 20
• From Γ_H(M) eigenvectors to normalised eigenforms on Γ₁(M) CuspForm.exists_isEigenformWith_qCoeff_eq_of_heckeTLinH_eq_smul_of_heckeULinH_eq_smul_of_diamondLinH_eq_smul 87 below · cited by 1 · depth 20
• Atkin–Lehner–Li basis of S_k(M,ε) from primitive forms CuspForm.exists_isPrimitiveForm_linearIndependent_degeneracy_and_mem_span_of_hasNebentypus 64 below · cited by 2 · depth 20
• Extracting aₙ via the integral Hecke algebra CuspForm.exists_mem_heckeAlgebra_qCoeff_one_eq_qCoeff_of_one_le 2 below · cited by 1 · depth 20
• Finite-dimensionality of S_k(Γ₁(M)) CuspForm.finiteDimensional_Gamma1 5 below · cited by 2 · depth 20
• Atkin–Lehner–Li dichotomy at p ∥ M with unramified character CuspForm.qCoeff_sq_eq_mul_zpow_or_exists_hasNebentypus_qCoeff_hecke_eigen_of_dvd_of_not_sq_dvd 8 below · cited by 2 · depth 20
• Full-level Hecke sum transports to T_ℓ on Γ_H(q²M') CuspForm.sum_slash_map_inv_slash_heckeDiagMatrix_eq_coe_heckeTLinH 6 below · cited by 1 · depth 20
• Linear independence of degeneracy images of Hecke eigenforms CuspForm.linearIndependent_degeneracy_of_isEigenformWith_of_pairwise_qCoeff_ne 13 below · cited by 1 · depth 21
• Eta products of level 4 are cusp forms on Γ₀(4) CuspForm.exists_gamma0_four_apply_eq_eta_pow_mul 2 below · cited by 4 · depth 23
• Diamond operators preserve rationality of weight-two q-expansions CuspForm.qCoeff_diamondLinOne_two_mem_range_ratCast_of_qCoeff_mem_range_intCast 0 below · cited by 1 · depth 23
• ℤ₍ₚ₎-lattice of weight-two cusp forms in C[[q]] CuspForm.exists_addMonoidHom_baseChange_intLattice_qExpansion_injective_of_ratLocalizedAt 665 below · cited by 1 · depth 25
• Multiplicity one for ordinary two-cusp eigenspaces mod π CuspForm.exists_ne_zero_and_smul_add_smul_eq_zero_of_mem_twoCuspEigenspace_of_apply_U_ne_zero 16 below · cited by 1 · depth 25
• Completing a mod-π Hecke eigensystem away from S CuspForm.exists_twoCuspEigenspace_two_le_twoCuspEigenspace_empty_of_finset 1,250 below · cited by 1 · depth 25
• Eichler–Shimura p-adic Galois lattice for the weight-two Hecke ring CuspForm.exists_padicGaloisModule_heckeRingH_two_frobenius_relation 1,228 below · cited by 1 · depth 26
• Mod p two-cusp forms as supersingular-polar differentials CuspForm.exists_isInfReductionMap_range_eq_ssPolarDifferentials 1,752 below · cited by 2 · depth 27
• Mod-I two-cusp forms as a base change from mod p CuspForm.exists_linearEquiv_tensorProduct_intTwoCuspForms_apply_tmul_eq_smul_twoCuspReduce 207 below · cited by 1 · depth 27
• Supersingular polar differentials as reductions of two-cusp integral weight-two forms CuspForm.exists_diffQExp_eq_sum_smul_intSeriesC_of_mem_ssPolarDifferentials 1,751 below · cited by 1 · depth 28
• Two-cusp lattice at p ‖ M has a coefficient-independent basis CuspForm.exists_linearIndependent_forall_twoCuspLattice_eq_span 206 below · cited by 8 · depth 28
• Supersingular-polar differential with prescribed mod p q-expansion CuspForm.exists_mem_ssPolarDifferentials_diffQExp_eq_intSeriesC_of_mem_twoCuspIntegralSet 1,493 below · cited by 2 · depth 28
• Uₚ kills reductions of p-divisible two-cusp forms CuspForm.intTwoCuspGenMod_genU_self_intTwoCuspReduce_eq_zero_of_forall_qCoeff_eq_mul_of_isInfReductionMap 1,380 below · cited by 1 · depth 28
• Regularity of Cω_f+ω_{⟨ d⟩ h} in characteristic p CuspForm.add_mem_regularDifferentials_of_isFrobPushDiff_of_diffQExp_eq_intSeriesC 954 below · cited by 2 · depth 29
• Mod p differential from an integral weight-two cusp form CuspForm.exists_forall_isRegularAt_of_not_mem_ssPlacesQExp_diffQExp_eq_intSeriesC_of_isIntegralQExp 1,327 below · cited by 1 · depth 29
• Two q-expansion-pinned reduction maps into ss-polar differentials CuspForm.exists_infReductionMap_and_wReductionMap_range_le_ssPolarDifferentials 1,496 below · cited by 2 · depth 29
• Integrality of q-expansions of two-cusp integral weight-two forms CuspForm.exists_isIntegralQExp_and_alSlash_of_mem_twoCuspIntegralSet 0 below · cited by 4 · depth 29
• Atkin–Lehner transport of two-cusp integral weight-two forms mod p CuspForm.exists_linearEquiv_intTwoCuspForms_intTwoCuspReduce_eq_of_coe_eq_alSlash_diamondLinH 94 below · cited by 1 · depth 29
• Two-cusp q-expansion principle mod p in weight two CuspForm.exists_mem_twoCuspLattice_eq_smul_of_forall_qCoeff_eq_mul_of_forall_qCoeff_alSlash_eq_mul 1,319 below · cited by 2 · depth 29
• Atkin–Lehner congruence aₙ((Uₚy)∣ W)≡ -aₙ(⟨ d⟩ y)(mod p) CuspForm.exists_qCoeff_alSlash_heckeULinH_add_qCoeff_diamondLinH_eq_mul_of_mem_twoCuspLattice 205 below · cited by 1 · depth 29
• Atkin–Lehner slash preserves rational q-coefficients in weight 2 CuspForm.exists_ratCast_qCoeff_alSlash_of_forall_qCoeff_ratCast_gammaH 204 below · cited by 2 · depth 29
• Glued supersingular polar pair from two integral q-expansions CuspForm.mem_twoCompRegularDifferentials_of_diffQExp_eq_intSeriesC_of_diffQExp_eq_intSeriesC_alSlash 1,364 below · cited by 2 · depth 29
• Two-cusp integral lattice equals the two-cusp integral set CuspForm.mem_twoCuspIntegralSet_of_mem_twoCuspLattice 7 below · cited by 7 · depth 29
• q-expansion of T_ℓ on cusp forms for Γ_H(M) CuspForm.qCoeff_heckeTLinH_eq_qCoeff_mul_add_pow_mul_qCoeff_diamondLinH 11 below · cited by 7 · depth 29
• Forms with integral Hecke translates span S₂(Γ_H(M)) CuspForm.span_setOf_forall_heckeRingH_qCoeff_intCast_eq_top 196 below · cited by 3 · depth 29
• Pure tensors 1⊗̄ f span the base change CuspForm.span_tmul_intTwoCuspReduce_eq_top 0 below · cited by 2 · depth 29
• Diamond-twisted level lowering from Γ_H(M) to Γ_{H'}(M/p) CuspForm.exists_GammaH_coe_eq_diamondLinH_add_smul_heckeU_alSlash 6 below · cited by 4 · depth 30
• Two Atkin–Lehner slashes compose to p^{k-2} times a diamond CuspForm.exists_alSlash_alSlash_eq_pow_smul_coe_diamondLinH 3 below · cited by 6 · depth 30
• Atkin–Lehner operator intertwines diamond operators on Γ_H(M) CuspForm.exists_alSlash_diamondLinH_eq_diamondLinH_alSlash 3 below · cited by 7 · depth 30
• Rational basis of cusp forms on Γ_H(N) CuspForm.exists_basis_gammaH_qCoeff_mem_range_ratCast 45 below · cited by 1 · depth 30
• Weight-two cusp forms give differentials regular off supersingular places CuspForm.exists_forall_isRegularAt_of_not_mem_ssPlacesQExp_diffQExp_eq_intSeriesC_of_isIntegralQExp_residueField 1,316 below · cited by 1 · depth 30
• Base change of mod-p two-cusp integral weight-two forms CuspForm.finiteDimensional_and_finrank_tensorProduct_intTwoCuspForms_eq_finrank_cuspForm 207 below · cited by 1 · depth 30
• Diamond operators preserve p-divisibility of q-coefficients CuspForm.forall_qCoeff_diamondLinH_eq_mul_of_forall_qCoeff_eq_mul_of_exists_isInfReductionMap 1,257 below · cited by 1 · depth 30
• Two-cusp integrality of (⟨ e⟩ f)∣₂ W CuspForm.mem_twoCuspIntegralSet_of_coe_eq_alSlash_diamondLinH 94 below · cited by 3 · depth 30
• Diamond-twisted integrality implies membership in the two-cusp integral set CuspForm.mem_twoCuspIntegralSet_of_forall_qCoeff_diamondLinH_mem 93 below · cited by 3 · depth 30
• Hecke stability of two-cusp ℤ₍ₚ₎-integrality, weight two CuspForm.mem_twoCuspIntegralSet_ratLocalizedAt_of_forall_qCoeff_mem 1,317 below · cited by 1 · depth 30
• p-saturation of the integral two-cusp lattice CuspForm.mem_twoCuspLattice_bot_of_mem_twoCuspIntegralSet_ratLocalizedAt_of_pow_smul_mem 7 below · cited by 1 · depth 30
• Regular Kähler differential with q-expansion p_f CuspForm.exists_kaehlerDifferential_diffQExp_eq_ofPowerSeries_and_forall_valuationSubring_of_isIntegralQExp 423 below · cited by 1 · depth 31
• Hecke generators preserve two-cusp integrality of diamond twists CuspForm.forall_qCoeff_diamondLinH_heckeGenH_mem_of_forall_qCoeff_diamondLinH_mem 92 below · cited by 1 · depth 31
• Diamond operators preserve two-cusp ℤ₍ₚ₎-integrality in weight two CuspForm.forall_qCoeff_diamondLinH_mem_ratLocalizedAt_of_forall_qCoeff_mem 1,244 below · cited by 1 · depth 31
• Hecke operators T_ℓ preserve two-cusp A-integrality CuspForm.forall_qCoeff_heckeTLinH_mem_of_forall_qCoeff_diamondLinH_mem 16 below · cited by 1 · depth 31
• U_q preserves two-cusp A-integrality, given the diamonds CuspForm.forall_qCoeff_heckeULinH_mem_of_forall_qCoeff_diamondLinH_mem 88 below · cited by 1 · depth 31
• Atkin–Lehner operator at p commutes with T_ℓ CuspForm.alSlash_coe_heckeTLinH_eq_coe_heckeTLinH 8 below · cited by 3 · depth 32
• Atkin–Lehner slash commutes with U_q on Γ_H(M) CuspForm.alSlash_coe_heckeULinH_eq_coe_heckeULinH 4 below · cited by 3 · depth 32
• Diamond operators preserve ℤ₍ₚ₎-integrality of q-expansions CuspForm.forall_qCoeff_diamondLinH_mem_ratLocalizedAt_of_forall_qCoeff_mem_ratLocalizedAt 1,242 below · cited by 2 · depth 32
• Atkin–Lehner W_q preserves cusp forms on Γ_H(M) CuspForm.exists_GammaH_coe_eq_alSlash_of_forall_unitsMap_atkinLehnerFactor_eq_one 1 below · cited by 10 · depth 33
• Atkin–Lehner slash intertwines diamond operators on Γ_H(M) CuspForm.exists_alSlash_diamondLinH_eq_diamondLinH_alSlash_atkinLehnerDatum 1 below · cited by 2 · depth 33
• Bounded denominators for rational cusp forms on Γ_H(M) CuspForm.exists_ne_zero_forall_natCast_mul_qCoeff_mem_bot_of_forall_qCoeff_mem_range 25 below · cited by 1 · depth 33
• Algebraic integrality of a prime-to-p multiple of ⟨ e⟩ f∣ W_d CuspForm.exists_not_dvd_and_algInt_qExpansion_smul_alSlash_diamond_of_mem_twoCuspIntegralSet_of_ker_le 362 below · cited by 3 · depth 33
• Prime-to-p multiple of an Atkin–Lehner–diamond translate is integral CuspForm.exists_not_dvd_and_coe_eq_smul_alSlash_diamond_and_mem_twoCuspIntegralSet_integralClosure 603 below · cited by 5 · depth 33
• Mod p vanishing of an Atkin–Lehner–diamond translate CuspForm.map_eq_zero_of_qExpansion_smul_alSlash_diamond_of_forall_dvd_coeff_of_mem_twoCuspIntegralSet 1,261 below · cited by 2 · depth 33
• The ℤ̄ two-cusp lattice is spanned by the ℤ-integral set CuspForm.twoCuspLattice_integralClosure_eq_span_twoCuspIntegralSet_bot 210 below · cited by 5 · depth 33
• Atkin–Lehner translate of a diamond operator on Γ₁(M) CuspForm.exists_gamma1_coe_eq_alSlash_diamondLinH 1 below · cited by 1 · depth 34
• Transposed U_q and Atkin–Lehner pins on two-cusp integral forms CuspForm.exists_not_dvd_and_coe_eq_smul_sum_slash_transpose_and_heckeU_eq_of_mem_twoCuspIntegralSet 613 below · cited by 1 · depth 34
• Prime-to-p multiple of ⟨ e⟩ f∣ W_d is two-cusp integral CuspForm.exists_not_dvd_and_smul_mem_twoCuspIntegralSet_integralClosure_of_coe_eq_alSlash_diamondLinH 601 below · cited by 1 · depth 34
• Atkin–Lehner transform preserves 𝔪-local q-expansions CuspForm.forall_exists_eq_mul_qExpansion_alSlash_of_mem_maximal_of_forall_unitsMap_of_even 362 below · cited by 2 · depth 34
• Atkin–Lehner slash preserves cusp forms on Γ₁(M) CuspForm.exists_gamma1_coe_eq_alSlash 0 below · cited by 2 · depth 35
• Bounded denominators for the Atkin–Lehner translate of ⟨ e⟩ f CuspForm.exists_ne_zero_forall_isIntegral_mul_qExpansion_alSlash_diamondLinH 42 below · cited by 1 · depth 35
• Atkin–Lehner–diamond twist preserves vanishing modulo p CuspForm.map_eq_zero_of_qExpansion_alSlash_diamond_of_coe_eq_smul_alSlash_diamond_of_forall_dvd_coeff 1,335 below · cited by 1 · depth 35
• Transpose of U_q preserves the two-cusp rational set CuspForm.mem_twoCuspIntegralSet_range_of_coe_eq_sum_slash_transpose_of_mem_twoCuspIntegralSet_range 243 below · cited by 1 · depth 35
• Two-cusp A-integrality from its diamond translates CuspForm.mem_twoCuspIntegralSet_two_of_forall_qCoeff_diamondLinH_mem_and_qCoeff_alSlash_diamondLinH_mem 92 below · cited by 1 · depth 35
• Eisenstein trace congruence with Fricke transform at level M/p CuspForm.exists_isIntegralQExp_congr_and_qExpansion_slash_fricke_congr_of_mem_twoCuspIntegralSet 114 below · cited by 1 · depth 36
• Rationality of the q-expansion of T_ℓ g at infinity CuspForm.qCoeff_heckeU_add_slash_mem_range_of_forall_qCoeff_mem_range 31 below · cited by 1 · depth 36
• Slashing by Γ₀(M) preserves rational q-expansions CuspForm.qCoeff_slash_mem_range_of_mem_Gamma0_of_forall_qCoeff_mem_range 19 below · cited by 1 · depth 36
• Transposed Uᵣ preserves rationality of q-coefficients CuspForm.qCoeff_sum_slash_heckeDiagMatrix_mul_transpose_mem_range_of_forall_qCoeff_mem_range 38 below · cited by 1 · depth 36

CuspForm.AuxLevel 12

• Auxiliary prime r: ML is two copies of baseML CuspForm.AuxLevel.exists_linearEquiv_baseML_prod_ML 4,468 below · cited by 2 · depth 13
• Nontriviality of the auxiliary-level residual Hecke module M_L CuspForm.AuxLevel.nontrivial_ML_of_prime_not_dvd 596 below · cited by 4 · depth 13
• Auxiliary prime: rank at most twice the base rank CuspForm.AuxLevel.finrank_ML_le_two_mul_finrank_baseML 4,425 below · cited by 1 · depth 14
• Ihara's lemma at an auxiliary prime: kernel pairs are Eisenstein CuspForm.AuxLevel.isEis_of_iDeg_one_add_iDeg_eq_zero 41 below · cited by 1 · depth 14
• Minimal level: corner of H¹ is the anemic localisation CuspForm.AuxLevel.exists_linearEquiv_cornerSubmodule_baseML_apply_eq_toML_of_squarefree 5,345 below · cited by 1 · depth 15
• Failure of level raising at r: rank bound for `midML` CuspForm.AuxLevel.finrank_midML_le_two_mul_finrank_baseML 3,895 below · cited by 1 · depth 15
• Diamond operators act trivially after localising at θ CuspForm.AuxLevel.toML_diamondRaw_eq_toML 1,543 below · cited by 1 · depth 15
• Triviality of residual diamonds at auxiliary level r CuspForm.AuxLevel.apply_diamondL_eq_one_of_forall_apply_op_eq 1,542 below · cited by 1 · depth 16
• Freeness of the minimal-level Hecke module over its operator algebra CuspForm.AuxLevel.baseML_free_range_lsmul 8,188 below · cited by 1 · depth 16
• At minimal level U_q acts by ± 1 on localised cohomology CuspForm.AuxLevel.exists_heckeTL_baseML_eq_smul_of_prime_dvd 5,314 below · cited by 2 · depth 16
• Nilpotence of Tᵣ-θ(Tᵣ) on the localised cohomology CuspForm.AuxLevel.exists_toML_heckeTL_sub_opAlgHom_pow_mem_of_prime_of_not_dvd 1,380 below · cited by 1 · depth 16
• No level raising at r after localising at 𝔪 CuspForm.AuxLevel.toML_eq_zero_of_jDeg_one_eq_zero_of_jDeg_eq_zero 3,888 below · cited by 1 · depth 16

CuspForm.Bfam 2

• Degeneracy adjointness of the chosen pairing family B CuspForm.Bfam.degeneracyBlock 21 below · cited by 1 · depth 11
• Level block for the chosen pairing family B CuspForm.Bfam.levelBlock 21 below · cited by 2 · depth 11

CuspForm.Bfam0 1

• Chosen pairing family on parabolic cohomology: perfect and adjoint CuspForm.Bfam0.block 14 below · cited by 3 · depth 15

CuspForm.HasIntegralStructure 5

• Characters of the Hecke algebra come from normalised eigenforms CuspForm.HasIntegralStructure.exists_isNormalizedEigenform_qCoeff_eq 42 below · cited by 8 · depth 8
• Finiteness over ℤ of the Hecke algebra on cusp forms CuspForm.HasIntegralStructure.moduleFinite_heckeAlgebra 17 below · cited by 22 · depth 8
• Endomorphism vanishing on the integral lattice is zero CuspForm.HasIntegralStructure.eq_zero_of_forall_mem_intLattice 0 below · cited by 6 · depth 9
• Every character of the Hecke algebra is an eigenform CuspForm.HasIntegralStructure.exists_ne_zero_forall_apply_eq_smul 20 below · cited by 3 · depth 9
• Freeness over ℤ of the anemic Hecke algebra CuspForm.HasIntegralStructure.moduleFree_heckeAlgebra 18 below · cited by 2 · depth 10

CuspForm.HasNebentypus 7

• Nebentypus components of a sum of cusp forms CuspForm.HasNebentypus.sum_filter_eq_of_sum_eq 0 below · cited by 3 · depth 13
• Central units at q act on an adelic lift through ε(d) CuspForm.HasNebentypus.apply_mul_padicToAdelic_centralGL_eq_of_isAdelicLiftOfGamma1 5 below · cited by 1 · depth 16
• Diamond operators act by ε(d) on forms of nebentypus ε CuspForm.HasNebentypus.diamondLinOne_apply_eq_smul 0 below · cited by 11 · depth 17
• Central character of the adelic lift of a nebentypus form CuspForm.HasNebentypus.exists_isFiniteOrderHeckeChar_centralScalar_mul_of_isAdelicLiftOfGamma1 11 below · cited by 1 · depth 17
• Adelic Hecke eigenvalue at ℓ ∤ N gives T_ℓ coefficient relation CuspForm.HasNebentypus.qCoeff_hecke_eq_of_isAdelicLiftOfGamma1_of_sum_apply_padicToAdelic_eq 3 below · cited by 3 · depth 17
• Adelic Hecke eigenvalue of a lift at ℓ ∤ M CuspForm.HasNebentypus.sum_apply_padicToAdelic_eq_mul_of_isAdelicLiftOfGamma1_of_qCoeff_hecke_eq 13 below · cited by 1 · depth 17
• Trace from level qt to t preserves vanishing at indices prime to K CuspForm.HasNebentypus.qCoeff_eq_zero_of_coprime_of_apply_eq_sum_slash 0 below · cited by 1 · depth 21

CuspForm.HeckeGaloisRepDatum 18

• Ordinary or flat deformation condition at p for a Hecke–Galois datum CuspForm.HeckeGaloisRepDatum.ordinaryCondition_or_flatCondition_of_apOfModel 5,247 below · cited by 2 · depth 7
• Hecke–Galois datum's residual representation is equivalent to ρ̄_{W,p} CuspForm.HeckeGaloisRepDatum.residual_isEquiv_baseChangeAlong_residualGaloisRepOf 76 below · cited by 3 · depth 7
• Cyclotomic determinant of the Hecke-side Galois representation CuspForm.HeckeGaloisRepDatum.detIsCyclotomic 23 below · cited by 7 · depth 8
• Flatness at p∤ N of a Hecke–Galois datum's representation CuspForm.HeckeGaloisRepDatum.isFlatAt_of_primeFactors_subset 2,314 below · cited by 5 · depth 8
• Ordinarity at p of a Hecke–Galois datum from residual ordinarity CuspForm.HeckeGaloisRepDatum.isOrdinaryAt_of_primeFactors_subset 5,148 below · cited by 4 · depth 8
• Unramifiedness of the Hecke–Galois representation outside S CuspForm.HeckeGaloisRepDatum.isUnramifiedAt_of_notMem 1,360 below · cited by 4 · depth 8
• Residual ordinarity at p of a Hecke–Galois datum CuspForm.HeckeGaloisRepDatum.ofResidualGaloisRep_residual_isOrdinaryAt_of_apOfModel 143 below · cited by 1 · depth 8
• Frobenius traces generate T: surjectivity of φ : R → T CuspForm.HeckeGaloisRepDatum.surjective_of_isEquiv_baseChangeAlong 5 below · cited by 7 · depth 8
• Unramified-outside-S replacement for a Hecke–Galois datum CuspForm.HeckeGaloisRepDatum.exists_pi_eq_and_forall_isUnramifiedAt 1,353 below · cited by 1 · depth 9
• Flat-at-p twin of a Hecke–Galois datum CuspForm.HeckeGaloisRepDatum.exists_pi_eq_and_isFlatAt_of_primeFactors_subset 2,310 below · cited by 1 · depth 9
• Ordinary twin datum at p with the same Hecke map CuspForm.HeckeGaloisRepDatum.exists_pi_eq_and_isOrdinaryAt_of_primeFactors_subset 5,147 below · cited by 2 · depth 9
• Transport of flatness at p along a Hecke-datum factorisation CuspForm.HeckeGaloisRepDatum.exists_pi_eq_and_isFlatAt_of_comp_pi_eq 8 below · cited by 1 · depth 10
• Ordinarity at p transports along a factorisation of Hecke–Galois data CuspForm.HeckeGaloisRepDatum.exists_pi_eq_and_isOrdinaryAt_of_comp_pi_eq 7 below · cited by 1 · depth 10
• Ordinarity contradicts decomposition-irreducibility of a second eigensystem CuspForm.HeckeGaloisRepDatum.false_of_isOrdinaryAt_of_forall_decompositionStable_eq_bot_or_top 35 below · cited by 1 · depth 10
• Hecke–Galois datum with ρ base changed along φ CuspForm.HeckeGaloisRepDatum.exists_pi_eq_and_rho_eq_baseChangeAlong 5 below · cited by 2 · depth 11
• Unipotent inertia at q ‖ N, q≠ p, for Hecke–Galois data CuspForm.HeckeGaloisRepDatum.isUnipotentOnInertiaAt_of_dvd_of_not_sq_dvd 3,763 below · cited by 2 · depth 11
• Jointly injective local points on a Hecke–Galois datum CuspForm.HeckeGaloisRepDatum.exists_points_jointly_injective 11 below · cited by 1 · depth 12
• Normalising a Hecke–Galois datum by a twist τ of T CuspForm.HeckeGaloisRepDatum.exists_algHom_comp_eq_and_linearEquiv_semilinear_auxLevel_ML 8,300 below · cited by 2 · depth 13

CuspForm.IsAdelicLiftOf 22

• Nonvanishing of an adelic lift of a cusp form CuspForm.IsAdelicLiftOf.ne_zero 0 below · cited by 6 · depth 11
• Unramifiedness of the central character μ₁μ₂ CuspForm.IsAdelicLiftOf.isUnramified_mul_of_linearMap_psCarrier_ne_zero 6 below · cited by 6 · depth 12
• Central K₁(qᵃ)-fixed vector inside the GL₂(ℚ_q)-span CuspForm.IsAdelicLiftOf.exists_mem_span_fixed_padicK1_of_fixedSubmodule_padicK1_ne_bot 6 below · cited by 2 · depth 13
• Twisting a ramified-ratio principal series to K₁(qᵇ)-fixed vectors CuspForm.IsAdelicLiftOf.exists_mem_span_fnTwist_fixed_padicK1_of_principalSeries_of_not_isUnramified_ratio 11 below · cited by 1 · depth 13
• Adelic lifts of Γ₀(M)-forms are right K₀(M)-invariant CuspForm.IsAdelicLiftOf.levelZero_inv 5 below · cited by 22 · depth 13
• Central K(qⁿ)-fixed vector in the local span of an adelic lift CuspForm.IsAdelicLiftOf.exists_mem_span_fixed_gl2CongruenceSubgroup_of_fixedSubmodule_gl2CongruenceSubgroup_ne_bot 9 below · cited by 3 · depth 14
• Finite-dimensionality of qⁿ-fixed vectors in the local span CuspForm.IsAdelicLiftOf.finite_fixedSubmodule_gl2CongruenceSubgroup_inf_span_range_padic_smul_self 12 below · cited by 4 · depth 14
• Central scalars act trivially on the K(q)-invariants CuspForm.IsAdelicLiftOf.gl2ReductionRep_scalarElem_eq_id_of_linearMap_range_eq_span 7 below · cited by 6 · depth 14
• Both characters ramified at q forces q² ∣ M CuspForm.IsAdelicLiftOf.sq_dvd_of_linearMap_psCarrier_ne_zero_of_not_isUnramified_of_not_isUnramified 1 below · cited by 1 · depth 14
• Central invariance of an adelic lift of a weight-two form CuspForm.IsAdelicLiftOf.apply_centralScalar_mul 6 below · cited by 2 · depth 15
• Quadratic twist produces a K₁(q)-fixed vector with trivial central action CuspForm.IsAdelicLiftOf.exists_mem_span_fnTwist_fixed_padicK1_one_of_principalSeries 15 below · cited by 1 · depth 15
• Descent of a K₁(qᵃ)-fixed twisted vector to Γ₁ nebentypus CuspForm.IsAdelicLiftOf.exists_hasNebentypus_isAdelicLiftOfGamma1_of_mem_span_fnTwist_of_fixed 7 below · cited by 2 · depth 17
• Weight-two adelic lifts have archimedean type two CuspForm.IsAdelicLiftOf.hasArchType0_archWeightCharFamily_two 5 below · cited by 1 · depth 17
• Adelic lifts of weight-two Γ₀(M) cusp forms are bounded-genuine CuspForm.IsAdelicLiftOf.isBoundedGenuineFn_productionPinsGeneral_stdAddChar 26 below · cited by 2 · depth 17
• Level and nebentypus of a K₁(qᵃ)-fixed vector in a twisted lift CuspForm.IsAdelicLiftOf.apply_mul_finEmbed_levelZero_eq_of_mem_span_fnTwist_of_fixed 6 below · cited by 2 · depth 18
• Realisation of the GL₂(ℚ_q)-span of an adelic lift CuspForm.IsAdelicLiftOf.exists_realization_range_eq_span_range_padic_smul_self 13 below · cited by 1 · depth 18
• Component at u of a k-translate is F∣₂γ⁻¹ CuspForm.IsAdelicLiftOf.apply_mul_padicToAdelic_diagOne_mul_eq_slash_inv_slash_of_component 0 below · cited by 2 · depth 19
• Vanishing of a K(q)-fixed vector in the span of an adelic lift CuspForm.IsAdelicLiftOf.eq_zero_of_forall_apply_mul_padicToAdelic_diagOne_eq_zero_of_mem_span_of_mem_fixedSubmodule 6 below · cited by 2 · depth 19
• Classical components at full level q of adelic span vectors CuspForm.IsAdelicLiftOf.exists_cuspForm_gamma_inf_gamma0_apply_mul_padicToAdelic_diagOne_eq_slash_of_mem_span_of_mem_fixedSubmodule 6 below · cited by 2 · depth 19
• Hecke action on full-level components of an adelic newform CuspForm.IsAdelicLiftOf.heckeTLinH_eq_qCoeff_smul_of_components_of_isNewform 19 below · cited by 2 · depth 19
• Components of K(q)-fixed vectors as linear families of cusp forms CuspForm.IsAdelicLiftOf.exists_linearMap_components_of_fixedSubmodule_of_range_eq_span 10 below · cited by 1 · depth 20
• Adelic Hecke sum at a good prime equals a_ℓ(g) CuspForm.IsAdelicLiftOf.sum_toFn_mul_eq_qCoeff_mul_of_mem_span_of_isHeckeCosetSystem 10 below · cited by 1 · depth 20

CuspForm.IsAdelicLiftOfGamma1 17

• Nebentypus action of K₀(M) on adelic lifts of Γ₁(M)-forms CuspForm.IsAdelicLiftOfGamma1.apply_mul_finEmbed_eq_inv_nebentypus_mul_of_mem_finiteLevelZero 6 below · cited by 4 · depth 17
• Descent from a nebentypus eigenvector to S₂(Γ₁(N),ε) CuspForm.IsAdelicLiftOfGamma1.exists_hasNebentypus_isAdelicLiftOfGamma1_of_mem_span_of_apply_mul_finEmbed_eq_inv_mul 5 below · cited by 1 · depth 17
• Adelic lifts of weight-two forms have archimedean type 2 CuspForm.IsAdelicLiftOfGamma1.hasArchType0_archWeightCharFamily_two 5 below · cited by 1 · depth 17
• Central character of an adelic lift at a good place CuspForm.IsAdelicLiftOfGamma1.apply_centralScalar_det_gen_mul_eq_nebentypus_mul 7 below · cited by 2 · depth 18
• Positive central scalars act trivially on the adelic lift CuspForm.IsAdelicLiftOfGamma1.apply_centralScalar_mul_eq_of_forall_snd_eq_one_of_archCoord_pos 5 below · cited by 1 · depth 18
• Right invariance of the adelic lift under the level group CuspForm.IsAdelicLiftOfGamma1.apply_mul_eq_of_mem_productionPinsGeneral_U 0 below · cited by 1 · depth 18
• Continuity of the adelic lift of a weight-two Γ₁(M) cusp form CuspForm.IsAdelicLiftOfGamma1.continuous 5 below · cited by 3 · depth 18
• Adelic lifts of weight-two cusp forms are bounded-genuine CuspForm.IsAdelicLiftOfGamma1.isBoundedGenuineFn_productionPinsGeneral_stdAddChar 24 below · cited by 1 · depth 18
• Cuspidality of the adelic lift of a weight-two cusp form CuspForm.IsAdelicLiftOfGamma1.isCuspidalFn_productionPinsGeneral 17 below · cited by 1 · depth 18
• Classical Tₚ eigenvalue transfers to the adelic Hecke operator CuspForm.IsAdelicLiftOfGamma1.isHeckeCosetEigenfunctionAt_productionPinsGeneral_of_heckeU_add_smul_slash_heckeDiagMatrix_eq 10 below · cited by 1 · depth 18
• K_f-smoothness of adelic lifts of weight-two cusp forms CuspForm.IsAdelicLiftOfGamma1.isKfSmooth 0 below · cited by 2 · depth 18
• Square-integrability of a weight-two adelic lift on the production window CuspForm.IsAdelicLiftOfGamma1.memLp_two_restrict_productionPinsGeneral 5 below · cited by 1 · depth 18
• Adelic lifts are left-invariant under rational unipotents CuspForm.IsAdelicLiftOfGamma1.apply_unipotentGL2_algebraMap_mul 0 below · cited by 1 · depth 19
• Adelic lifts of weight-two cusp forms are C² along the unipotent line CuspForm.IsAdelicLiftOfGamma1.contDiff_two_unipotentGL2_ratArchLine_mul 5 below · cited by 1 · depth 19
• Unipotent line through an integral point: adelic lift equals a slash of h CuspForm.IsAdelicLiftOfGamma1.exists_forall_apply_unipotentGL2_add_ratArchLine_mul_eq_slash_apply_I 5 below · cited by 1 · depth 19
• Boundedness of the adelic lift of a weight-two cusp form CuspForm.IsAdelicLiftOfGamma1.exists_forall_norm_le 5 below · cited by 2 · depth 19
• Adelic lift of a Γ₁(M) cusp form on γ x u CuspForm.IsAdelicLiftOfGamma1.apply_globalPoints_mul_mul_eq_slash_ratArchGL2_apply_I 0 below · cited by 1 · depth 20

CuspForm.IsEigenformWith 18

• λ-adic representation attached to a weight-two eigenform CuspForm.IsEigenformWith.exists_galoisRepAdic_charpoly_frobenius_eq_and_isUnramifiedAt 1,478 below · cited by 11 · depth 16
• Finite generation of an eigenform's coefficient ring CuspForm.IsEigenformWith.fg_adjoin_qCoeff 54 below · cited by 8 · depth 16
• Inertia eigenvalue 1 at q when v_q(M)=v_q(condε)=1 CuspForm.IsEigenformWith.isRoot_charpoly_one_of_mem_inertiaSubgroupIn_of_factorization_eq_one_of_conductor_factorization_eq_one 5,306 below · cited by 1 · depth 16
• Inertia at a Taylor–Wiles prime exactly dividing the level CuspForm.IsEigenformWith.exists_basis_inertia_apply_eq_smul_of_dvd_of_not_sq_dvd_of_dvd_sub_one_of_residual_isAbsolutelyIrreducible 6,320 below · cited by 1 · depth 17
• p-adic eigencharacter on the rational Hecke algebra of J₁(M) CuspForm.IsEigenformWith.exists_ringHom_rationalHeckeAlgebraOne_mul_eq 926 below · cited by 8 · depth 17
• Hecke operator T_ℓ, ℓ∤ M, on degeneracy images of an eigenform CuspForm.IsEigenformWith.heckeU_add_smul_slash_heckeDiagMatrix_degeneracy_eq_qCoeff_smul 10 below · cited by 5 · depth 17
• Adelic lift of a weight-two Γ₁(M) eigenform is isotypic CuspForm.IsEigenformWith.isIsotypicCuspFormAt_of_isAdelicLiftOfGamma1 37 below · cited by 2 · depth 17
• Finiteness of the coefficient ring of a weight-two eigenform CuspForm.IsEigenformWith.OperatorAlgebra.finite_adjoin_qCoeff 55 below · cited by 1 · depth 18
• Frobenius at q for eigenforms new at q CuspForm.IsEigenformWith.charpoly_eq_of_isFrobeniusAt_of_not_dvd_conductor_of_not_eigenpacketOccursAt_div 4,078 below · cited by 1 · depth 18
• λ-adic representation of a weight-two eigenform on Γ₁(M) CuspForm.IsEigenformWith.exists_galoisRepAdic_charpoly_frobenius_eq_tateModule_jOne_quotient 1,478 below · cited by 3 · depth 18
• Level raising of eigenforms with nebentypus along M ∣ N CuspForm.IsEigenformWith.exists_isEigenformWith_changeLevel_qCoeff_eq_of_dvd 2 below · cited by 3 · depth 18
• Inertia eigenlines at q ‖ M dividing the nebentypus conductor CuspForm.IsEigenformWith.exists_linearIndependent_inertia_apply_eq_smul_of_dvd_of_not_sq_dvd_of_dvd_conductor_of_residual_isAbsolutelyIrreducible 5,330 below · cited by 1 · depth 18
• Coefficient eigenform relations give the operator identity Uₚ h+ε(p)h|₂diag(p,1)=aₚ h CuspForm.IsEigenformWith.heckeU_add_smul_slash_heckeDiagMatrix_eq_qCoeff_smul 9 below · cited by 1 · depth 18
• Unramified at q with a_q a Frobenius eigenvalue CuspForm.IsEigenformWith.inertia_eq_one_and_isRoot_charpoly_of_eigenpacketOccursAt_div 1,517 below · cited by 1 · depth 18
• Uₚ-eigenvalue at a prime exactly dividing the level CuspForm.IsEigenformWith.dvd_and_qCoeff_eq_or_not_dvd_and_qCoeff_sq_sub_eq_zero_of_isPrimitiveForm_of_not_sq_dvd 56 below · cited by 4 · depth 19
• p-new/p-old dichotomy at a prime exactly dividing the level CuspForm.IsEigenformWith.exists_changeLevel_and_qCoeff_sq_eq_or_exists_isEigenformWith_of_dvd_of_not_sq_dvd_of_not_dvd_conductor 40 below · cited by 3 · depth 19
• Newform source and Hecke polynomial at q for an eigenform old at q CuspForm.IsEigenformWith.exists_isPrimitiveForm_sq_sub_mul_add_eq_zero_of_eigenpacketOccursAt_div 58 below · cited by 1 · depth 19
• U_q on the degeneracy string of an eigenform CuspForm.IsEigenformWith.heckeU_degeneracy_of_dvd_level 6 below · cited by 2 · depth 20

CuspForm.IsNewform 70

• Adic Galois representation of a newform, Steinberg Frobenius polynomials CuspForm.IsNewform.exists_galoisRepAdic_charpoly_frobenius_eq_of_dvd_of_not_sq_dvd 3,812 below · cited by 3 · depth 9
• Newform eigenplane in the Tate module of J₀(M), with Steinberg lines CuspForm.IsNewform.exists_eigenPlane_torLine_tateModule_jZero 3,797 below · cited by 1 · depth 10
• Newform λ-adic representation: non-unipotent inertia at exponent-two primes CuspForm.IsNewform.exists_galoisRepAdic_not_isUnipotentOnInertiaAt_of_factorization_eq_two_of_absIrred_odd_of_ne_two 10,747 below · cited by 3 · depth 10
• Inertia at q with q² ‖ M: principal series versus supercuspidal CuspForm.IsNewform.exists_charpoly_inertia_eq_principalSeries_supercuspidal_of_galoisRepAdic_of_two_laws_of_irreducible_odd_of_ne_two_of_factorization_eq_two 10,725 below · cited by 1 · depth 11
• λ-adic eigenplane of a weight-two newform in T_λ(J₀(M)) CuspForm.IsNewform.exists_eigenPlane_tateModule_jZero 1,290 below · cited by 6 · depth 11
• Hecke-pinned λ-adic eigenplane in the Tate module of J₀(M) CuspForm.IsNewform.exists_heckePinnedEigenPlane_tateModule_jZero 1,327 below · cited by 1 · depth 11
• Ramified first character in a principal series at q² ∣ M CuspForm.IsNewform.exists_mem_higherUnits_apply_ne_one_of_linearMap_psCarrier_ne_zero_of_sq_dvd 57 below · cited by 2 · depth 11
• Ordinary line in the eigenplane at a multiplicative prime CuspForm.IsNewform.exists_ordLine_eigenPlane_tateModule_jZero_of_dvd 4,787 below · cited by 1 · depth 11
• Eigenplanes in T_λ J₀(M): eigen off the level, determinant q CuspForm.IsNewform.killedOffLevel_cyclotomicDet_of_eigenPlane_tateModule_jZero 1,102 below · cited by 5 · depth 11
• Inertia at a principal-series prime q with v_q(M)=2 CuspForm.IsNewform.exists_charpoly_inertia_eq_and_pow_eq_one_iff_of_linearMap_psCarrier_ne_zero_of_factorization_eq_two 7,035 below · cited by 3 · depth 12
• Inertia at q is split with a^{q-1}≠ 1 CuspForm.IsNewform.exists_charpoly_inertia_eq_and_pow_sub_one_ne_one_of_forall_linearMap_psCarrier_eq_zero_of_factorization_eq_two_of_irreducible_odd_of_ne_two 6,863 below · cited by 2 · depth 12
• Rank-two Hecke eigenspace in the λ-adic Tate module of J₀(M) CuspForm.IsNewform.exists_heckeEigenspace_tateModule_jZero_finrank_eq_two 841 below · cited by 6 · depth 12
• Eigenplane monodromy span at λ ‖ M has dimension ≤ 1 CuspForm.IsNewform.finrank_monodromySpan_eigenPlane_tateModule_jZero_le_one_of_dvd 4,786 below · cited by 2 · depth 12
• Frobenius trace a_ℓ(g) on a newform eigenplane CuspForm.IsNewform.frobeniusTrace_of_eigenPlane_tateModule_jZero 1,305 below · cited by 2 · depth 12
• Newform level equals local newvector conductor at each prime CuspForm.IsNewform.hasNewvectorConductor_adelicSpan_factorization_of_isAdelicLiftOf 46 below · cited by 5 · depth 12
• U_λ-eigenvalue on Hecke eigenvectors in the Tate module CuspForm.IsNewform.heckeU_smul_of_mem_heckeEigenspace_tateModule_jZero 886 below · cited by 1 · depth 12
• Strong multiplicity one for weight-two newforms on Γ₀(M) CuspForm.IsNewform.eq_of_isNormalizedEigenform_forall_prime_notMem_qCoeff_eq 102 below · cited by 4 · depth 13
• Inertia at q≠λ: principal series with unramified ratio CuspForm.IsNewform.exists_charpoly_inertia_eq_and_pow_eq_one_iff_of_linearMap_psCarrier_ne_zero_of_isUnramified_ratio 3,781 below · cited by 1 · depth 13
• Inertial charpolys at a ramified principal-series prime, v_q(M)=2 CuspForm.IsNewform.exists_galoisRepAdic_charpoly_inertia_eq_cyclotomicCharacter_of_linearMap_psCarrier_ne_zero_of_not_isUnramified_ratio_of_factorization_eq_two 6,229 below · cited by 1 · depth 13
• Ordinary line for the λ-adic representation of a newform CuspForm.IsNewform.exists_galoisRepAdic_ordinaryLine_frobenius_sub_unitRoot_smul_mem_of_not_dvd 2,415 below · cited by 4 · depth 13
• Principal-series map from split tame inertia labels at q CuspForm.IsNewform.exists_linearMap_psCarrier_ne_zero_of_charpoly_inertia_eq_of_pow_sub_one_eq_one_of_factorization_eq_two_of_irreducible_odd_of_ne_two 6,836 below · cited by 1 · depth 13
• Dual multiplicity one for newforms away from finitely many primes CuspForm.IsNewform.finrank_iInf_eigenspace_dualMap_heckeTLin_eq_one 101 below · cited by 4 · depth 13
• Strong multiplicity one across levels for weight-2 newforms CuspForm.IsNewform.level_eq_and_qCoeff_eq_of_forall_qCoeff_eq 98 below · cited by 9 · depth 13
• Local type at a prime exactly squared in the level CuspForm.IsNewform.psCarrier_lam_dvd_sub_one_or_no_psCarrier_lam_dvd_add_one_of_factorization_eq_two_of_residual_isUnipotent_of_irreducible_odd_of_absIrred_odd 10,753 below · cited by 1 · depth 13
• Strong multiplicity one for newforms of a fixed level CuspForm.IsNewform.eq_of_forall_qCoeff_eq 56 below · cited by 2 · depth 14
• Ramified principal series at q with v_q(M)=2: twist of level exactly q CuspForm.IsNewform.exists_isPrimitiveForm_adelicLiftGamma1_psCarrier_isUnramified_of_not_isUnramified_ratio_of_factorization_eq_two 473 below · cited by 1 · depth 14
• Ordinary line in the λ-adic eigenplane of J₀(M) CuspForm.IsNewform.exists_ordLine_eigenPlane_tateModule_jZero_of_not_dvd 2,351 below · cited by 1 · depth 14
• Quadratic twist lowering the q-exponent of a newform CuspForm.IsNewform.exists_quadraticTwistToExponentOne_of_sq_dvd_of_adelicLift_principalSeries_isUnramified_ratio 67 below · cited by 1 · depth 14
• Depth zero at q when v_q(M)≤ 2 CuspForm.IsNewform.fixedSubmodule_gl2CongruenceSubgroup_one_adelicSpan_ne_bot_of_factorization_le_two 47 below · cited by 3 · depth 14
• Eichler–Shimura quadratic relation for Frobenius on the eigenplane CuspForm.IsNewform.frobenius_quadratic_mem_of_inertia_sub_mem_eigenPlane_tateModule_jZero_of_not_dvd 2,331 below · cited by 1 · depth 14
• Unipotent-fixed vectors vanish when no map to a principal series exists CuspForm.IsNewform.gl2ReductionRep_unipotent_fixed_eq_zero_of_forall_linearMap_psCarrier_eq_zero 16 below · cited by 4 · depth 14
• Inertia labels at q given by the cuspidal type θ or θ^q CuspForm.IsNewform.inertia_labels_eq_or_eq_pow_of_isCuspidalOfType_subrepresentation_of_irreducible_odd_of_range 6,800 below · cited by 1 · depth 14
• Equality of levels for weight-2 newforms with matching eigenvalues CuspForm.IsNewform.level_eq_of_forall_prime_not_dvd_qCoeff_eq 97 below · cited by 2 · depth 14
• Principal-series characters trivial on 1+qℤ_q when v_q(M)=2 CuspForm.IsNewform.apply_eq_one_of_mem_higherUnits_one_of_factorization_eq_two_of_linearMap_psCarrier_ne_zero 10 below · cited by 1 · depth 15
• Ramification away from p forces q to divide the newform level CuspForm.IsNewform.dvd_level_of_point_of_not_isUnramifiedAt 1,329 below · cited by 3 · depth 15
• Ramified special λ-adic realisation at q ∥ M CuspForm.IsNewform.exists_galoisRepAdic_inertia_apply_ne_and_stableLine_frobenius_eq_qCoeff_smul_of_dvd_of_not_sq_dvd 3,807 below · cited by 1 · depth 15
• Twisting a newform to unramified principal-series character at q CuspForm.IsNewform.exists_isPrimitiveForm_adelicLiftGamma1_psCarrier_isUnramified_of_not_isUnramified_ratio 457 below · cited by 1 · depth 15
• Unipotent-fixed vector gives a map to a principal series CuspForm.IsNewform.exists_linearMap_psCarrier_of_gl2ReductionRep_unipotent_fixed_ne_zero 15 below · cited by 1 · depth 15
• Good-reduction specialization ordinary on the λ-adic eigenplane CuspForm.IsNewform.exists_specialization_jZeroOrdConn_eigenPlane_tateModule_jZero_of_not_dvd 2,342 below · cited by 1 · depth 15
• Ordinary eigenvectors dying under reduction span at most a line CuspForm.IsNewform.finrank_le_one_of_le_reductionKernelSpan_tateModule_jZero_of_isUnit 2,269 below · cited by 2 · depth 15
• Difference of newforms of distinct q-levels avoids the old span CuspForm.IsNewform.rescaleLin_sub_rescaleLin_notMem_span_sup_span 83 below · cited by 1 · depth 15
• Multiplicity one: twisted newform lift and primitive form span CuspForm.IsNewform.adelicSpanSubmodule_eq_of_isPrimitiveForm_adelicLiftGamma1_fnTwist 408 below · cited by 1 · depth 16
• Stable line at λ ∥ M with a_λ = ± 1 CuspForm.IsNewform.exists_galoisRepAdic_ordinaryLine_frobenius_sub_qCoeff_smul_mem_of_dvd_of_not_sq_dvd 4,877 below · cited by 3 · depth 16
• Non-trivial inertia at q ∥ M on a Hecke eigenplane CuspForm.IsNewform.exists_mem_inertiaSubgroupIn_baseChange_apply_ne_of_eigenPlane_tateModule_jZero 3,737 below · cited by 1 · depth 16
• Toric line in the eigenplane with Frobenius scalar a_q(g) q CuspForm.IsNewform.exists_torLine_of_eigenPlane_tateModule_jZero_eq_qCoeff 3,742 below · cited by 2 · depth 16
• No cuspidal type in the mod-q reduction at level q²M' CuspForm.IsNewform.not_isCuspidalOfType_subrepresentation_gl2ReductionRep_of_dvd 47 below · cited by 2 · depth 16
• Trace of f∣ D_q over Γ₀(qN₀)-cosets equals a_q f CuspForm.IsNewform.sum_range_slash_heckeDiagMatrix_conj_eq_qCoeff_smul 69 below · cited by 1 · depth 16
• Trace of a weight-2 newform vanishes when q² ∣ R CuspForm.IsNewform.sum_slash_S_mul_T_zpow_mul_S_inv_eq_zero 46 below · cited by 1 · depth 16
• Equivariant Hecke eigenclass attached to a newform of level Nq² CuspForm.IsNewform.exists_H1_gammaH_dual_ne_zero_equivariant_heckeT_eq_qCoeff_smul_of_isCuspidalOfType 43 below · cited by 1 · depth 17
• Inertia at q with v_q(M)=2 is non-tame of order ∤ q-1 CuspForm.IsNewform.exists_charpoly_inertia_eq_and_pow_sub_one_ne_one_of_forall_linearMap_psCarrier_eq_zero_of_factorization_eq_two_of_irreducible_odd_of_ne_two_of_cast_eq_neg_one 6,598 below · cited by 1 · depth 17
• Newform λ-adic representation is special at q ‖ M CuspForm.IsNewform.exists_galoisRepAdic_stableLine_frobenius_eq_qCoeff_smul_of_dvd_of_not_sq_dvd 3,806 below · cited by 2 · depth 17
• Cuspidal type θ for the level-zero component at q CuspForm.IsNewform.exists_isCuspidalOfType_gl2ReductionRep_of_inertia_labels_eq_pow_of_irreducible_odd_of_cast_eq_neg_one 10,520 below · cited by 1 · depth 17
• Inertia-fixed vector with Frobenius acting as q U_q CuspForm.IsNewform.exists_ne_zero_frobenius_eq_prime_smul_heckeU_of_eigenPlane_tateModule_jZero 3,737 below · cited by 1 · depth 17
• Frobenius acts by ± q on a line in the eigenplane CuspForm.IsNewform.exists_torLine_of_eigenPlane_tateModule_jZero 3,737 below · cited by 1 · depth 17
• Frobenius acts as U_λ modulo monodromy on the eigenplane CuspForm.IsNewform.frobenius_sub_heckeU_smul_mem_monodromySpan_eigenPlane_tateModule_jZero_of_dvd 4,814 below · cited by 1 · depth 17
• U_q acts by a_q(g)∈{0,± 1} on λ-adic eigenvectors CuspForm.IsNewform.heckeU_eq_intCast_smul_of_mem_heckeEigenspace_tateModule_jZero 841 below · cited by 2 · depth 17
• Supercuspidal type character at q has λ-power order CuspForm.IsNewform.ne_one_and_exists_pow_pow_eq_one_of_isCuspidalOfType_of_unipotentOnInertia_of_irreducible_odd 6,546 below · cited by 1 · depth 17
• Principal series map from tame split inertia at q CuspForm.IsNewform.exists_linearMap_psCarrier_ne_zero_of_charpoly_inertia_eq_of_pow_sub_one_eq_one_of_factorization_eq_two_of_irreducible_odd_of_ne_two_of_cast_eq_neg_one 6,571 below · cited by 1 · depth 18
• Irreducibility of the K(q)-fixed reduction representation CuspForm.IsNewform.gl2ReductionRep_toSubmodule_eq_top_of_ne_bot_of_forall_linearMap_psCarrier_eq_zero 533 below · cited by 1 · depth 18
• Inertia labels at q given by a cuspidal type θ CuspForm.IsNewform.inertia_labels_eq_or_eq_pow_of_isCuspidalOfType_subrepresentation_of_irreducible_odd_of_range_of_cast_eq_neg_one 6,535 below · cited by 3 · depth 18
• No equivariant map to a principal series at q when q² ‖ M CuspForm.IsNewform.linearMap_psCarrier_eq_zero_of_charpoly_inertia_eq_mul_of_eq_pow_of_pow_sub_one_ne_one_exponent_two 7,036 below · cited by 1 · depth 18
• Exactly one residually zero root at a prime with q²∣ N CuspForm.IsNewform.sum_rootMultiplicity_residual_zero_eq_one_of_sq_dvd_of_ne 71 below · cited by 1 · depth 18
• Cuspidal K(q)-type of a newform inside H¹(Γ_H(Nq²),ℂ) CuspForm.IsNewform.exists_linearMap_fixedSubmodule_H1_gammaH_laws_of_isCuspidalOfType 36 below · cited by 1 · depth 19
• Irreducibility of the local representation realised in the adelic span CuspForm.IsNewform.isIrreducibleGLRep_of_linearMap_range_eq_span_padic_smul_self 496 below · cited by 1 · depth 19
• Local factor of a weight-two newform at q ≠ p CuspForm.IsNewform.qCoeff_eq_zero_and_sq_eq_one_and_not_residual_zero_of_mem_roots_of_ne 69 below · cited by 1 · depth 19
• Adelic lift of a weight-two newform as genuine cuspidal realization CuspForm.IsNewform.exists_isGenuineCuspRealizationAt_productionPinsOf_toFun_eq_of_isAdelicLiftOf 63 below · cited by 1 · depth 20
• Local newvectors from a newform span at most a line CuspForm.IsNewform.exists_smul_add_smul_eq_zero_of_mem_span_of_mem_fixedSubmodule_padicK1_of_centralGL_smul_eq 116 below · cited by 1 · depth 20
• Multiplicity one: the Hecke eigenspace of a newform is its line CuspForm.IsNewform.iInf_eigenspace_heckeTLin_eq_span_singleton 101 below · cited by 1 · depth 21
• Oldform degeneracy basis and semisimplicity of good T_ℓ CuspForm.IsNewform.maxGenEigenspace_heckeTLinH_le_and_exists_oldClasses_span_eq_iInf_eigenspace 81 below · cited by 1 · depth 21
• Weight-two Γ₀(N) newforms are primitive with trivial nebentypus CuspForm.IsNewform.exists_gamma1_coe_eq_and_isPrimitiveForm_one 38 below · cited by 1 · depth 22

CuspForm.IsNormalizedEigenform 31

• Normalised eigenforms give characters of the Hecke algebra CuspForm.IsNormalizedEigenform.exists_ringHom_heckeAlgebra 16 below · cited by 26 · depth 9
• Hecke eigencharacter of a normalised weight-two eigenform is integral CuspForm.IsNormalizedEigenform.exists_ringHom_heckeAlgebra_integralClosure 41 below · cited by 7 · depth 9
• Normalized eigenforms are T_ℓ-eigenvectors with eigenvalue a_ℓ CuspForm.IsNormalizedEigenform.heckeTLin_apply_eq_qCoeff_smul 0 below · cited by 19 · depth 9
• Prime coefficients of normalized weight-2 eigenforms are algebraic integers CuspForm.IsNormalizedEigenform.primeCoeffsIntegral_of_neZero 18 below · cited by 8 · depth 9
• Integrality of the ℓ-th coefficient of a normalised eigenform CuspForm.IsNormalizedEigenform.exists_integralClosure_coe_eq_qCoeff 28 below · cited by 2 · depth 10
• Level raising at q' for weight-two normalised eigenforms CuspForm.IsNormalizedEigenform.exists_isNewAt_congr_of_levelRaisingCongruence 725 below · cited by 1 · depth 10
• Residual Galois representation of a weight-two eigenform CuspForm.IsNormalizedEigenform.exists_residualGaloisRep_isAttachedTo 1,311 below · cited by 3 · depth 10
• Normalized eigenforms are U_q-eigenvectors at bad primes CuspForm.IsNormalizedEigenform.heckeULin_apply_eq_qCoeff_smul 0 below · cited by 5 · depth 10
• Adic Galois representation attached to a weight-two eigenform CuspForm.IsNormalizedEigenform.exists_galoisRepAdic_frobenius_quadratic 1,310 below · cited by 1 · depth 11
• Eigencharacter at raised level Nq' of a normalised eigenform CuspForm.IsNormalizedEigenform.exists_heckeAlgebraChar_raisedLevel 20 below · cited by 1 · depth 11
• p-stabilisation of a normalised eigenform to level Mp CuspForm.IsNormalizedEigenform.exists_stabilization_qCoeff_eq 1 below · cited by 1 · depth 11
• Weight-two eigenform: eigencharacter into a characteristic-zero DVR CuspForm.IsNormalizedEigenform.exists_isDiscreteValuationRing_heckeChar_rationalHeckeAlgebra_jZero 1,021 below · cited by 1 · depth 12
• Finiteness of the eigenform coefficient ring over ℤ CuspForm.IsNormalizedEigenform.eigenCoeffRing_moduleFinite 18 below · cited by 1 · depth 13
• Residual eigensystem of g occurs in the Tate-module Hecke algebra CuspForm.IsNormalizedEigenform.exists_ringHom_adjoin_tateHeckeRep_jZero_eq_residual 1,020 below · cited by 1 · depth 13
• Level lowering at q from a K₁(qᵃ)-fixed vector CuspForm.IsNormalizedEigenform.goodEigensystemOccursAt_of_adelicLift_of_mem_span_of_fixed 43 below · cited by 1 · depth 13
• Weak multiplicity one for normalised eigenforms on Γ₀(N) CuspForm.IsNormalizedEigenform.eq_of_forall_prime_qCoeff_eq 4 below · cited by 4 · depth 14
• Twisted descent: a K₁(q)-fixed vector yields a parabolic class on Γ₁(L/q) CuspForm.IsNormalizedEigenform.exists_H1_diamondRaw_eq_smul_heckeT_eq_smul_of_mem_fixedSubmodule_fnTwist 11 below · cited by 1 · depth 14
• Weight-two eigenform as non-zero parabolic class for Γ_H(M) CuspForm.IsNormalizedEigenform.exists_ne_zero_mem_parabolicHoms_gammaH_heckeT_eq_qCoeff_smul 590 below · cited by 1 · depth 14
• Oldforms of level N with prescribed coefficients at bad primes CuspForm.IsNormalizedEigenform.exists_isNormalizedEigenform_of_dvd_qCoeff_eq_zero_qCoeff_eq_root 3 below · cited by 3 · depth 15
• Twisted descent: lowered-level eigenform with η-twisted coefficients CuspForm.IsNormalizedEigenform.exists_isNormalizedEigenform_qCoeff_eq_mul_of_adelicLift_fnTwist_of_mem_span_of_fixed 43 below · cited by 1 · depth 15
• Coefficients at indices coprime to M agree CuspForm.IsNormalizedEigenform.qCoeff_eq_of_coprime_of_forall_prime_not_dvd 0 below · cited by 3 · depth 15
• Coefficient agreement of weight-2 eigenforms at indices coprime to L CuspForm.IsNormalizedEigenform.qCoeff_eq_of_coprime_of_forall_prime_not_dvd_of_dvd 17 below · cited by 1 · depth 15
• Agreement at primes forces agreement of all q-coefficients CuspForm.IsNormalizedEigenform.qCoeff_eq_of_forall_prime_qCoeff_eq 2 below · cited by 1 · depth 15
• Γ₁(N) descent of a K₁(qᵃ)-fixed twisted vector CuspForm.IsNormalizedEigenform.exists_gamma1_hasNebentypus_hecke_eigen_of_adelicLift_fnTwist_of_mem_span_of_fixed 14 below · cited by 1 · depth 16
• Existence of the q-depleted eigenform at level Mq^e CuspForm.IsNormalizedEigenform.exists_isNormalizedEigenform_level_mul_pow_qCoeff_eq_ite 2 below · cited by 1 · depth 16
• Adelic lift of a normalised eigenform on Γ₀(M) is isotypic CuspForm.IsNormalizedEigenform.isIsotypicCuspFormAt_one_of_isAdelicLiftOf 43 below · cited by 2 · depth 17
• Hecke eigenvalue η(varpi_ℓ)⁻¹a_ℓ(g) on the twisted adelic span CuspForm.IsNormalizedEigenform.sum_apply_padicToAdelic_eq_mul_of_mem_span_fnTwist 7 below · cited by 2 · depth 17
• λ-adic representation of a weight-two eigenform at a prescribed reduction CuspForm.IsNormalizedEigenform.exists_galoisRepAdic_charpoly_frobenius_eq_of_ringHom_integralClosure 1,338 below · cited by 1 · depth 18
• Normalised Γ₀(N) eigenform as trivial-nebentypus Γ₁(N) eigenform CuspForm.IsNormalizedEigenform.isEigenformWith_one_of_coe_eq 2 below · cited by 1 · depth 18
• Eichler–Shimura: λ-adic representations of a weight-two eigenform CuspForm.IsNormalizedEigenform.exists_galoisRepAdic_charpoly_frobenius_eq_of_isMaximal 1,335 below · cited by 1 · depth 19
• All q-coefficients of a normalized eigenform are algebraic integers CuspForm.IsNormalizedEigenform.exists_integralClosure_coe_eq_qCoeff_nat 29 below · cited by 2 · depth 19

CuspForm.IsPrimitiveForm 21

• Nonzero inertia invariants at q when v_q(M)=1 CuspForm.IsPrimitiveForm.exists_ne_zero_forall_inertiaSubgroupIn_apply_eq_self_of_linearMap_psCarrier_isUnramified_of_factorization_eq_one 5,713 below · cited by 1 · depth 14
• Inertia invariants at q for v_q(M)=1, unramified principal series CuspForm.IsPrimitiveForm.exists_galoisRepAdic_forall_inertiaSubgroupIn_apply_eq_self_of_linearMap_psCarrier_isUnramified_of_factorization_eq_one 5,712 below · cited by 1 · depth 15
• Principal series with unramified character: v_q(M) versus v_q(cond ε) CuspForm.IsPrimitiveForm.factorization_eq_conductor_factorization_or_of_linearMap_psCarrier_isUnramified 33 below · cited by 2 · depth 15
• Casselman lower bound: K₁(q^m)-fixed vector forces v_q(M)≤ m CuspForm.IsPrimitiveForm.factorization_le_of_mem_span_of_mem_fixedSubmodule_padicK1 20 below · cited by 1 · depth 16
• Newform λ-adic representation with inertia eigenvalue 1 at q ‖ M CuspForm.IsPrimitiveForm.exists_galoisRepAdic_charpoly_frobenius_eq_and_isRoot_charpoly_one_of_dvd_of_factorization_eq_conductor_factorization_of_not_sq_dvd 5,302 below · cited by 1 · depth 17
• Inertia-fixed and nebentypus lines at q exactly dividing M CuspForm.IsPrimitiveForm.exists_galoisRepAdic_linearIndependent_inertia_apply_eq_smul_of_dvd_of_not_sq_dvd_of_dvd_conductor 5,319 below · cited by 1 · depth 19
• Strong multiplicity one across levels for primitive forms CuspForm.IsPrimitiveForm.level_eq_and_qCoeff_eq_of_forall_prime_notMem_qCoeff_eq 55 below · cited by 6 · depth 19
• Ordinary line at p ‖ M for a weight-two primitive form CuspForm.IsPrimitiveForm.exists_galoisRepAdic_ordinaryLine_frobenius_sub_qCoeff_smul_mem_of_dvd_of_not_sq_dvd_of_not_dvd_conductor 3,533 below · cited by 1 · depth 20
• Ordinary line of the λ-adic representation of a primitive form CuspForm.IsPrimitiveForm.exists_galoisRepAdic_ordinaryLine_frobenius_sub_unitRoot_smul_mem_of_not_dvd 2,337 below · cited by 1 · depth 20
• Inertia at q acting non-trivially on a primitive eigenquotient CuspForm.IsPrimitiveForm.exists_mem_inertiaSubgroupIn_tmul_rep_sub_notMem_span_tateModule_jOne_of_dvd_of_not_sq_dvd_of_not_dvd_conductor 3,914 below · cited by 1 · depth 20
• Divisibility of M₂ by powers of q when q² ∣ M₁ CuspForm.IsPrimitiveForm.pow_dvd_of_pow_dvd_of_sq_dvd_of_factorsThrough_of_forall_coprime_qCoeff_eq 51 below · cited by 1 · depth 20
• U_q-eigenvalue times a_q(g) equals q at auxiliary level CuspForm.IsPrimitiveForm.ringHom_rationalHeckeOne_mul_eq_of_dvd_of_not_sq_dvd_of_dvd_conductor_of_dvd_level 670 below · cited by 1 · depth 20
• Value of Λ at U_q for q exactly dividing M CuspForm.IsPrimitiveForm.ringHom_rationalHeckeOne_mul_eq_of_dvd_of_not_sq_dvd_of_not_dvd_conductor 656 below · cited by 2 · depth 20
• U_q acts by a_q(G) on the old packet, q² ∤ N CuspForm.IsPrimitiveForm.heckeU_eigenvalue_eq_qCoeff_of_common_eigenvector_of_dvd_level 63 below · cited by 1 · depth 21
• Hecke eigenspace of Tₚ J₁(M) at a primitive form CuspForm.IsPrimitiveForm.iInf_ker_hecke_sub_ne_bot_and_inf_span_eq_bot_tateModule_jOne 928 below · cited by 1 · depth 21
• No primitive form of level M occurs in Tₚ J₁(N) for N∣ M, N≠ M CuspForm.IsPrimitiveForm.linearMap_eq_zero_of_hecke_coeigen_tateModule_jOne_of_dvd_of_ne 711 below · cited by 2 · depth 21
• Vanishing of a_q for primitive forms when q² ∣ M CuspForm.IsPrimitiveForm.qCoeff_eq_zero_of_dvd_div 4 below · cited by 1 · depth 21
• Strong multiplicity one for p-adic Hecke characters on J₁(M) CuspForm.IsPrimitiveForm.ringHom_rationalHeckeOne_mul_eq_of_eq_conj_qCoeff_mul 645 below · cited by 1 · depth 21
• Lower-unipotent coset sum of a primitive form at q ∣ M CuspForm.IsPrimitiveForm.sum_slash_S_mul_T_zpow_mul_S_inv_apply_eq_of_dvd 42 below · cited by 1 · depth 21
• Coset sum for the q-old form g(qτ) of a primitive form CuspForm.IsPrimitiveForm.sum_slash_S_mul_T_zpow_mul_S_inv_comp_heckeDiagMatrix_apply_eq_of_not_dvd 42 below · cited by 1 · depth 21
• Good Hecke operators suffice on the primitive packet of J₁(M) CuspForm.IsPrimitiveForm.exists_mem_adjoin_good_aeval_ne_zero_mul_smul_eq_smul_jOne 642 below · cited by 1 · depth 22

CuspForm.TWLevel 29

• Taylor–Wiles construction: R_Q acting on the localised cohomology module CuspForm.TWLevel.exists_algHom_deformationRing_moduleEnd_ML_flat 6,535 below · cited by 1 · depth 13
• R_Q acting on the Taylor–Wiles module, très ramifié case CuspForm.TWLevel.exists_algHom_deformationRing_moduleEnd_ML_of_not_isFlatAt_strictOrdinary 6,931 below · cited by 1 · depth 13
• Taylor–Wiles Hecke module free over 𝒪[Δ_Q] CuspForm.TWLevel.exists_basis_ML_monoidAlgebra_and_linearMap_ML_auxLevel_of_charpoly_frobenius_eq 1,588 below · cited by 4 · depth 13
• Freeness of the Taylor–Wiles module over 𝒪[Δ_Q] CuspForm.TWLevel.exists_algHom_monoidAlgebra_and_basis_ML_HQ 36 below · cited by 1 · depth 14
• Galois representation over the Taylor–Wiles Hecke ring acting on M_Q CuspForm.TWLevel.exists_galoisRepAdic_moduleEnd_ML_flat 6,527 below · cited by 1 · depth 14
• Galois representation on the Taylor–Wiles Hecke module, strict ordinary case CuspForm.TWLevel.exists_galoisRepAdic_moduleEnd_ML_of_not_isFlatAt_strictOrdinary 6,925 below · cited by 1 · depth 14
• Taylor–Wiles level comparison: M_Q(Hᵣ)≅ M, T_ℓ-equivariantly CuspForm.TWLevel.exists_linearEquiv_ML_HR_auxLevel_of_charpoly_frobenius_eq 1,571 below · cited by 1 · depth 14
• Surjective trace ML(H_Q)toML(H_R) with augmentation kernel CuspForm.TWLevel.exists_linearMap_ML_HQ_HR_surjective_and_ker_eq_span 11 below · cited by 2 · depth 14
• Inertia at a Taylor–Wiles prime acts by diamond operators CuspForm.TWLevel.HeckeRing.exists_basis_inertia_apply_eq_diamond_smul 6,378 below · cited by 2 · depth 15
• Galois representation over the Taylor–Wiles Hecke ring CuspForm.TWLevel.HeckeRing.exists_galoisRepAdic_trace_frobenius_eq_T 1,578 below · cited by 2 · depth 15
• The Taylor–Wiles Hecke ring is complete local and 𝒪-finite CuspForm.TWLevel.HeckeRing.finite_and_isLocalRing_and_isAdicComplete 13 below · cited by 4 · depth 15
• Flatness at p of the Taylor–Wiles level Galois representation CuspForm.TWLevel.HeckeRing.isFlatAt_of_not_dvd_level 2,165 below · cited by 1 · depth 15
• Strict ordinarity at p of the Taylor–Wiles Hecke-ring representation CuspForm.TWLevel.HeckeRing.isStrictOrdinaryAt_of_dvd_level_of_not_isFlatAt 4,307 below · cited by 1 · depth 15
• Unipotent inertia at q for the Taylor–Wiles Hecke-ring representation CuspForm.TWLevel.HeckeRing.isUnipotentOnInertiaAt_of_dvd_of_not_isUnramifiedAt 3,280 below · cited by 2 · depth 15
• Unramifiedness at the auxiliary prime of the Taylor–Wiles Hecke representation CuspForm.TWLevel.HeckeRing.isUnramifiedAt_of_not_dvd_sub_one_of_trace_frobenius_sq_ne 3,303 below · cited by 2 · depth 15
• Removing the last Taylor–Wiles prime when diamonds act trivially CuspForm.TWLevel.exists_linearEquiv_ML_HR_init_of_toML_diamondL_eq 31 below · cited by 1 · depth 15
• π_Q maps Hᵣ onto Δ_Q, with index p^{sum vₚ(qᵢ-1)} CuspForm.TWLevel.exists_mem_HR_piQ_eq_and_card_Delta_and_relIndex_HQ_HR 0 below · cited by 1 · depth 15
• Diamond operators act trivially after localisation at the residual eigensystem CuspForm.TWLevel.toML_diamondL_eq_toML 1,543 below · cited by 1 · depth 15
• Local–global compatibility at a Taylor–Wiles prime, pointwise form CuspForm.TWLevel.HeckeRing.exists_basis_inertia_apply_eq_diamond_smul_of_algHom 6,362 below · cited by 1 · depth 16
• Realising ρ' mod I in p-power torsion of J_{H_Q} CuspForm.TWLevel.HeckeRing.exists_finiteLevel_surjective_pi_torsion_jH_levelQuotient_of_not_dvd_level 1,391 below · cited by 1 · depth 16
• Galois representation attached to a point of the Taylor–Wiles Hecke ring CuspForm.TWLevel.HeckeRing.exists_galoisRepAdic_of_algHom 1,561 below · cited by 1 · depth 16
• Points of the Taylor–Wiles Hecke ring: eigenform or Eisenstein CuspForm.TWLevel.HeckeRing.exists_isEigenformWith_or_eisenstein_of_algHom 259 below · cited by 4 · depth 16
• Reducedness of the Taylor–Wiles level Hecke ring CuspForm.TWLevel.HeckeRing.isReduced 275 below · cited by 7 · depth 16
• Strict ordinarity at p for Hecke-ring points with non-flat ρ̄ CuspForm.TWLevel.HeckeRing.isStrictOrdinaryAt_of_algHom_of_dvd_level_of_not_isFlatAt 4,282 below · cited by 1 · depth 16
• Unipotent inertia at the auxiliary prime over T_Q CuspForm.TWLevel.HeckeRing.isUnipotentOnInertiaAt_of_auxPrime 3,287 below · cited by 1 · depth 16
• Faithful Hecke lattice with Eichler–Shimura relation inside J_H[pⁿ] CuspForm.TWLevel.HeckeRing.exists_finiteLevel_faithful_galoisHeckeLattice_frobenius_torsionEmbedding_jH_of_not_dvd_level 1,271 below · cited by 1 · depth 17
• Points of the Taylor–Wiles Hecke ring are classical CuspForm.TWLevel.HeckeRing.exists_isEigenformWith_qCoeff_sub_mem_or_eisenstein_of_algHom 322 below · cited by 1 · depth 17
• Eigenvectors in H¹ for points of the Taylor–Wiles Hecke ring CuspForm.TWLevel.HeckeRing.OperatorAlgebra.exists_U_eigenvector_H1_of_algHom 11 below · cited by 1 · depth 18
• Dual of localised cohomology as a summand of 𝒪⊗ TₚJ_H CuspForm.TWLevel.exists_heckeEquivariant_dual_ML_range_eq_idempotent_baseChange_tateModule_jH 713 below · cited by 1 · depth 18

CuspForm.heckeAlgebra 21

• Restriction of Hecke algebras along a division of levels CuspForm.heckeAlgebra.exists_surjective_ringHom_of_dvd 0 below · cited by 5 · depth 11
• Mod-𝔪 eigenvalue system yields a maximal ideal of the Hecke algebra CuspForm.heckeAlgebra.exists_isMaximal_heckeT_sub_mem_of_qCoeff_congr 2 below · cited by 1 · depth 12
• Weight–twist determinant congruence ℓ¹⁺²ⁱ=ℓ^{k-1} in characteristic p CuspForm.heckeAlgebra.natCast_pow_twist_eq_natCast_pow_weight_sub_one_of_twist_mem 1,543 below · cited by 1 · depth 12
• Weight p+1 with θ(Tₚ)=0 descends to weight 2 CuspForm.heckeAlgebra.exists_isMaximal_two_ringHom_of_succ_of_map_T_eq_zero_of_five_le_or_exists_prime_dvd 1,253 below · cited by 1 · depth 13
• Odd weight: the Hecke algebra is a subsingleton CuspForm.heckeAlgebra.subsingleton_of_odd 1 below · cited by 2 · depth 13
• Characters of the Hecke algebra give mod p cuspidal eigensystems CuspForm.heckeAlgebra.exists_mem_modPCusp_isModPEigen_of_ringHom 669 below · cited by 2 · depth 14
• Mod p Hecke eigensystems come from characters of T CuspForm.heckeAlgebra.exists_ringHom_apply_eq_of_isModPEigen_of_heckeU_eq_smul 11 below · cited by 2 · depth 14
• Residual Hecke eigensystems lift to complete discrete valuation rings CuspForm.heckeAlgebra.exists_ringHom_ker_residue_comp_eq_ker_of_one_le 23 below · cited by 1 · depth 14
• Residual Hecke eigensystem on the full Hecke algebra at level N CuspForm.heckeAlgebra.exists_ringHom_of_subset_of_charpoly_frobenius_eq 5,149 below · cited by 2 · depth 14
• Extension of an anemic eigensystem at squarefree level, with Uₚ a unit CuspForm.heckeAlgebra.exists_ringHom_apply_inclusion_eq_and_apply_U_ne_zero_of_squarefree 5,147 below · cited by 1 · depth 15
• Extending anemic Hecke points with prescribed U_q-eigenvalues CuspForm.heckeAlgebra.exists_ringHom_extension_apply_U_eq_zero_and_dvd 681 below · cited by 1 · depth 15
• Extending an anemic weight-two Hecke point with U_q normalised CuspForm.heckeAlgebra.exists_ringHom_extension_apply_U_eq_zero_and_isUnit_apply_U_or 681 below · cited by 4 · depth 15
• Weight p+1 level N to weight 2 level Np CuspForm.heckeAlgebra.thetaCycle_exists_ringHom_mul_two_apply_eq_of_ringHom_succ_of_eq_three_imp_exists_prime_dvd_mod_three_eq_two 1,207 below · cited by 1 · depth 15
• Extending a Hecke point from level S to S₀ CuspForm.heckeAlgebra.exists_ringHom_extension_residue_eq_of_charpoly_frobenius_eq 5,147 below · cited by 1 · depth 16
• Annihilating U_q²-1 near θ' at a ramified prime CuspForm.heckeAlgebra.exists_apply_ne_zero_and_mul_U_sq_sub_one_eq_zero_of_not_isUnramifiedAt 1,511 below · cited by 2 · depth 17
• Extending a Hecke character across a good prime r CuspForm.heckeAlgebra.exists_ringHom_apply_T_eq_of_insert_of_residue_eq 1,108 below · cited by 2 · depth 17
• Descent of an eigensystem from level Nr to level N CuspForm.heckeAlgebra.exists_ringHom_apply_T_eq_of_not_dvd_of_trace_frobenius_sq_ne 3,840 below · cited by 2 · depth 17
• Integral factorisation of a Hecke eigencharacter with prescribed reduction CuspForm.heckeAlgebra.exists_ringHom_comp_eq_and_residue_eq_of_forall_isRoot_of_map_residue_eq_pow 2 below · cited by 1 · depth 17
• Strict ordinarity from non-flatness for modular mod p representations CuspForm.heckeAlgebra.isStrictOrdinaryAt_of_ringHom_of_dvd_of_not_isFlatAt 5,038 below · cited by 2 · depth 17
• Monic squarefree relation for Uₚ at p ∥ N, ordinary case CuspForm.heckeAlgebra.exists_apply_ne_zero_and_squarefree_and_mul_aeval_U_eq_zero_of_apply_U_ne_zero 102 below · cited by 1 · depth 19
• Joint descent of ̄ K-points to a finite complete DVR CuspForm.heckeAlgebra.exists_dvr_algHom_comp_eq_and_ringHom_comp_eq_of_algHom_algebraicClosure 671 below · cited by 2 · depth 19

CuspForm.heckeLocal 88

• Local Hecke algebra generated over 𝒪 by Hecke operators CuspForm.heckeLocal.adjoin_range_pi 3 below · cited by 28 · depth 8
• Cotangent-length inequality at the localised Hecke algebra, p=3 CuspForm.heckeLocal.exists_algHom_length_cotangent_le_of_isResiduallyModular_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd_of_level_not_cube_dvd 22,983 below · cited by 1 · depth 8
• Cotangent–congruence length inequality at cube-free levels CuspForm.heckeLocal.exists_algHom_length_cotangent_le_of_isResiduallyModular_of_level_of_not_sq_dvd_of_not_cube_dvd_of_level_not_cube_dvd 22,659 below · cited by 1 · depth 8
• Lifts of residual eigensystems give points of T_θ CuspForm.heckeLocal.exists_point 0 below · cited by 12 · depth 8
• Residue of the local Hecke algebra structure map equals θ CuspForm.heckeLocal.residue_pi 0 below · cited by 29 · depth 8
• Residue field of the local Hecke algebra comes from 𝒪 CuspForm.heckeLocal.residue_surjective 0 below · cited by 14 · depth 8
• Taylor–Wiles patching data at p=3, cube-free level CuspForm.heckeLocal.exists_patchingDatum_of_isResiduallyModular_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd_of_level_not_cube_dvd 22,980 below · cited by 1 · depth 9
• Patching data over the localised Hecke algebra, cube-free levels CuspForm.heckeLocal.exists_patchingDatum_of_isResiduallyModular_of_level_of_not_sq_dvd_of_not_cube_dvd_of_level_not_cube_dvd 22,656 below · cited by 1 · depth 9
• R=T and complete intersection at cube-free ordinary level CuspForm.heckeLocal.bijective_and_exists_presentation_of_ordinaryCondition_of_finiteAt_of_not_cube_dvd 12,167 below · cited by 2 · depth 10
• Points of the local Hecke algebra from congruent eigensystems CuspForm.heckeLocal.exists_factor_algHom 0 below · cited by 9 · depth 10
• Integral point on the localised Hecke algebra after enlarging 𝒪 CuspForm.heckeLocal.exists_finite_extension_nonempty_algHom 3 below · cited by 2 · depth 10
• Hecke–Galois datum over the localised Hecke algebra, with local conditions CuspForm.heckeLocal.exists_heckeGaloisRepDatum_localConditions 5,184 below · cited by 3 · depth 10
• Hecke modules on a cube-free level ladder with Taylor–Wiles levels CuspForm.heckeLocal.exists_heckeModules_levelRaising_and_taylorWiles_of_index_two_irreducible_strictOrdinary_of_not_cube_dvd 9,979 below · cited by 3 · depth 10
• Surjection of localised Hecke algebras for N ∣ N' CuspForm.heckeLocal.exists_surjective_algHom_of_dvd 7 below · cited by 4 · depth 10
• Free corner datum on H¹(Γ₀(N)∩Γ₁(r),𝒪) with Σ-pin CuspForm.heckeLocal.exists_h1CornerData_fullCorner_sigmaPin_pairing_eq_bfam_and_free 8,310 below · cited by 1 · depth 11
• Level-raising rung at p with η-factor α²-1 CuspForm.heckeLocal.exists_heckeModule_rung_at_residueChar_unitRoot_of_cornerData_of_fullCorner_of_not_cube_dvd 8,352 below · cited by 1 · depth 11
• Hecke modules on a cube-free ladder and at Taylor–Wiles levels CuspForm.heckeLocal.exists_heckeModules_levelRaising_and_taylorWiles_auxLevel_of_isEis_kernel_pair_strictOrdinary_of_not_cube_dvd 9,972 below · cited by 1 · depth 11
• Finiteness of the residue field of the local Hecke algebra CuspForm.heckeLocal.finite_residueField 0 below · cited by 1 · depth 11
• Ordinary unit root at p satisfies α² ≠ 1 CuspForm.heckeLocal.unitRoot_sq_ne_one_of_point 2,738 below · cited by 1 · depth 11
• Full Σ-corner at level Nr with B-family pairing CuspForm.heckeLocal.exists_h1CornerData_fullCorner_pairing_eq_bfam_sigmaResidue_guarded 5,582 below · cited by 1 · depth 12
• Unit-root rung at p over a level-Nr corner package CuspForm.heckeLocal.exists_h1CornerData_refinement_degeneracy_level_mul_of_cornerData_of_fullCorner_of_trace_sq_ne_of_not_cube_dvd 8,319 below · cited by 1 · depth 12
• Hecke-module ladder, cube-free levels, auxiliary level r CuspForm.heckeLocal.exists_heckeModules_levelRaising_auxLevel_and_linearEquiv_ML_of_isEis_kernel_pair_of_not_cube_dvd 6,105 below · cited by 1 · depth 12
• Newform behind an 𝒪-point, with Tₚ adjoined CuspForm.heckeLocal.exists_isNewform_chig_iota_of_point_of_not_dvd 703 below · cited by 2 · depth 12
• Taylor–Wiles modules over 𝒪[Δ_Q] in the flat minimal case CuspForm.heckeLocal.exists_taylorWilesModule_of_linearEquiv_ML_flat 9,719 below · cited by 1 · depth 12
• Taylor–Wiles modules, strict ordinary non-flat case CuspForm.heckeLocal.exists_taylorWilesModule_of_linearEquiv_ML_of_not_isFlatAt_strictOrdinary 9,809 below · cited by 1 · depth 12
• Freeness of the guarded Σ-corner over its corner ring CuspForm.heckeLocal.free_cornerModule_of_guardedSigmaCorner_of_absolutelyIrreducible 7,462 below · cited by 1 · depth 12
• Ordinary Frobenius scalar is a unit root of X²-Tₚ X+p CuspForm.heckeLocal.sq_sub_apply_corner_mul_add_eq_zero_of_isOrdinaryAt_point_of_isUnit_of_corner_le_parabolic 2,465 below · cited by 1 · depth 12
• Corner Tₚ at an 𝒪-point equals ι(aₚ(g)) CuspForm.heckeLocal.apply_corner_eq_iota_T_of_point_of_corner_le_parabolic 704 below · cited by 1 · depth 13
• Corner ring ≅ local Hecke algebra at auxiliary level Mr CuspForm.heckeLocal.exists_algEquiv_sigmaCornerRing_auxLevel 5,494 below · cited by 2 · depth 13
• Level lowering to the unit-root corner ring across Nr ∣ Nrp CuspForm.heckeLocal.exists_algHom_cornerRing_levelLowering_unitRoot_of_degeneracy_level_mul 1,564 below · cited by 1 · depth 13
• Level Nrp unit-root refinement package at p CuspForm.heckeLocal.exists_cornerData_unitRoot_refinement_package_level_mul_of_not_cube_dvd 8,292 below · cited by 1 · depth 13
• Hecke modules along a cube-free level-raising ladder CuspForm.heckeLocal.exists_heckeModules_levelRaising_and_linearEquiv_baseML_of_isEis_kernel_pair_of_not_cube_dvd 5,641 below · cited by 1 · depth 13
• Tₚ is a unit in the corner ring at auxiliary level Nr CuspForm.heckeLocal.exists_isUnit_corner_heckeT_residueChar_of_isOrdinaryAt_of_subfamily_point_of_maximalIdeal 5,408 below · cited by 1 · depth 13
• Occurrence of the residual eigensystem in a corner at level Nr CuspForm.heckeLocal.exists_subfamily_idempotentSplitting_point_level_mul_auxPrime 3,918 below · cited by 1 · depth 13
• Anemic and full local Hecke algebras agree at ρ̄ CuspForm.heckeLocal.bijective_of_subset_of_charpoly_frobenius_eq 5,379 below · cited by 1 · depth 14
• Independence of the local Hecke algebra of the avoided primes CuspForm.heckeLocal.bijective_of_subset_of_forall_prime_mem_of_charpoly_frobenius_eq 1,452 below · cited by 5 · depth 14
• Localised Hecke algebra as a cohomological corner ring CuspForm.heckeLocal.exists_algEquiv_cornerRing_H1_of_not_isEisenstein 597 below · cited by 3 · depth 14
• Change of avoided set for localised Hecke algebras CuspForm.heckeLocal.exists_algHom_of_subset 2 below · cited by 12 · depth 14
• Realisation of Tₚ in the sub-family corner ring CuspForm.heckeLocal.exists_corner_smul_eq_heckeT_and_apply_eq_trace_of_subfamily_point 5,404 below · cited by 1 · depth 14
• An element of mathbb T_θ interpolating the U_q-eigenvalues ± 1 CuspForm.heckeLocal.exists_forall_point_apply_eq_qCoeff_of_not_isUnramifiedAt_of_ne_two 3,847 below · cited by 3 · depth 14
• Corner realisation at minimal level and its base identification CuspForm.heckeLocal.exists_isCornerRealization_and_linearEquiv_baseML_of_squarefree 5,354 below · cited by 1 · depth 14
• Level raising at q ∣ N for Hecke corner realisations CuspForm.heckeLocal.exists_isCornerRealization_and_rung_of_isCornerRealization_of_dvd_of_not_sq_dvd_of_not_cube_dvd 5,552 below · cited by 1 · depth 14
• Level-raising rung at q for cube-free corner realisations CuspForm.heckeLocal.exists_isCornerRealization_and_rung_of_isCornerRealization_of_not_dvd_of_not_cube_dvd 5,528 below · cited by 1 · depth 14
• Surjection of localised Hecke algebras for M ∣ M' CuspForm.heckeLocal.exists_surjective_algHom_apply_pi_T_eq_of_dvd 5 below · cited by 1 · depth 14
• Eigen-rank bound across the degeneracy rung at p CuspForm.heckeLocal.finrank_eigen_unitRoot_corner_le_of_degeneracy_level_mul 1,516 below · cited by 1 · depth 14
• Freeness over the minimal-level local Hecke algebra at auxiliary level CuspForm.heckeLocal.free_of_linearEquiv_auxLevel_ML 8,299 below · cited by 1 · depth 14
• Self-adjoint perfect pairing and rank formula on a Hecke corner CuspForm.heckeLocal.selfAdjoint_and_bijective_and_finrank_eq_of_isCornerRealization_of_not_cube_dvd 5,477 below · cited by 2 · depth 14
• Localised Hecke algebra into a corner ring of H¹ CuspForm.heckeLocal.exists_algHom_cornerRing_apply_pi_T_eq_of_dvd 595 below · cited by 3 · depth 15
• T_ℓ at an avoided prime lies in the image of Ψ CuspForm.heckeLocal.exists_apply_eq_pi_T_of_mem_of_charpoly_frobenius_eq 1,360 below · cited by 1 · depth 15
• Surjectivity of Ψ onto Tₚ at the residue characteristic CuspForm.heckeLocal.exists_apply_eq_pi_T_of_not_dvd_of_charpoly_frobenius_eq 3,988 below · cited by 2 · depth 15
• Uₚ lies in the image of Ψ for p ∥ N CuspForm.heckeLocal.exists_apply_eq_pi_U_of_dvd_of_isOrdinaryAt_of_charpoly_frobenius_eq 5,294 below · cited by 1 · depth 15
• Steinberg U_q lies in the image of Ψ CuspForm.heckeLocal.exists_apply_eq_pi_U_of_not_sq_dvd_of_not_isUnramifiedAt_of_charpoly_frobenius_eq 3,958 below · cited by 2 · depth 15
• Realising Tₚ in the corner Hecke ring with residual trace CuspForm.heckeLocal.exists_corner_smul_eq_heckeT_residueChar_gammaZero 5,330 below · cited by 1 · depth 15
• Hecke corner modules are nearly free over T^S(N)_θ CuspForm.heckeLocal.exists_injective_linearMap_pi_and_smul_mem_range_of_isCornerRealization_of_not_cube_dvd 5,465 below · cited by 1 · depth 15
• Minimal-level cohomology is free over the local Hecke algebra CuspForm.heckeLocal.exists_moduleFree_linearEquiv_auxLevel_baseML 8,189 below · cited by 1 · depth 15
• Realising T_q in the local Hecke algebra with value a CuspForm.heckeLocal.exists_smul_eq_heckeT_and_apply_eq_trace_frobenius_of_not_dvd 1,366 below · cited by 1 · depth 15
• Rank comparison of localised Hecke algebras via extension of lifts CuspForm.heckeLocal.finrank_le_of_forall_point_exists_extension 17 below · cited by 2 · depth 15
• Rank comparison for local Hecke algebras at level S₀ ⊆ S CuspForm.heckeLocal.finrank_le_of_subset_of_charpoly_frobenius_eq 5,156 below · cited by 1 · depth 15
• Multiplicity four at p non-ordinary, cube-free level CuspForm.heckeLocal.finrank_torsionBySet_ker_eq_four_mul_finrank_quotient_of_isCornerRealization_of_not_isOrdinaryAt_of_not_cube_dvd 5,465 below · cited by 2 · depth 15
• Multiplicity two for corner realisations at cube-free level CuspForm.heckeLocal.finrank_torsionBySet_ker_eq_two_mul_finrank_quotient_of_isCornerRealization_of_not_cube_dvd 5,465 below · cited by 2 · depth 15
• Eigen-rank does not grow when raising the level by q² CuspForm.heckeLocal.finrank_torsionBySet_le_of_isCornerRealization_of_not_dvd_of_not_cube_dvd 5,468 below · cited by 1 · depth 15
• Points of T_θ are local and reduce to θ CuspForm.heckeLocal.isLocalHom_and_residue_apply_pi 1 below · cited by 7 · depth 15
• Vanishing of U_q in the local Hecke algebra when q² ‖ N CuspForm.heckeLocal.pi_U_eq_zero_of_sq_dvd_of_not_cube_dvd 96 below · cited by 3 · depth 15
• Surjectivity of the Hecke comparison map for S₁ ⊆ S CuspForm.heckeLocal.surjective_of_subset_of_charpoly_frobenius_eq 1,359 below · cited by 4 · depth 15
• Pointwise recognition of π(U_q) in the localised Hecke algebra CuspForm.heckeLocal.apply_eq_pi_U_of_forall_point_apply_eq_qCoeff_of_isAbsolutelyIrreducible 1,544 below · cited by 1 · depth 16
• Uₚ as the unit root in the localised Hecke algebra CuspForm.heckeLocal.apply_eq_pi_U_of_forall_point_apply_eq_unitRoot_of_isAbsolutelyIrreducible 1,542 below · cited by 1 · depth 16
• Faithful local Hecke action on the cohomology module CuspForm.heckeLocal.exists_algHom_moduleEnd_baseML_injective 1,479 below · cited by 2 · depth 16
• Unit Uₚ-eigenvalue interpolated in the localised anemic Hecke algebra CuspForm.heckeLocal.exists_forall_point_apply_eq_unitRoot_of_isOrdinaryAt 5,201 below · cited by 3 · depth 16
• Eigenspace rank four when p ∣ L and ρ̄ is non-ordinary CuspForm.heckeLocal.finrank_iInf_eigenspace_baseChange_eq_four_of_isCornerRealization_of_not_isOrdinaryAt_of_not_cube_dvd 5,463 below · cited by 1 · depth 16
• Rank two for χ-eigenspaces of the corner Hecke module CuspForm.heckeLocal.finrank_iInf_eigenspace_baseChange_eq_two_of_isCornerRealization_of_not_cube_dvd 5,463 below · cited by 1 · depth 16
• Newform multiplicity two, four when non-ordinary at p CuspForm.heckeLocal.newformMultiplicity_finrank_iInf_eigenspace_algebraicClosure_eq_of_isCornerRealization_of_not_cube_dvd 5,462 below · cited by 3 · depth 16
• U_q²=1 in the localised Hecke algebra at a Steinberg prime CuspForm.heckeLocal.pi_U_sq_eq_one_of_not_sq_dvd_of_not_isUnramifiedAt 1,512 below · cited by 1 · depth 16
• Cube-free saturation forces equal levels and identical Hecke localisations CuspForm.heckeLocal.exists_algEquiv_apply_pi_T_eq_of_dvd_of_sq_dvd_of_not_cube_dvd 0 below · cited by 1 · depth 17
• Eichler–Shimura: local anemic Hecke algebra as a corner ring CuspForm.heckeLocal.exists_algEquiv_cornerRing_baseHeckeData_of_not_isEisenstein 597 below · cited by 1 · depth 17
• Joint injectivity of points of the localised Hecke algebra T_{θ'} CuspForm.heckeLocal.exists_points_jointly_injective_of_charpoly_frobenius_eq_of_isAbsolutelyIrreducible 1,536 below · cited by 2 · depth 17
• A uniform sign for U_q at minimal squarefree level CuspForm.heckeLocal.exists_sign_forall_point_heckeULin_mul_eq_smul_of_squarefree 5,265 below · cited by 1 · depth 17
• Newform multiplicity two, or four, in a same-level Hecke corner CuspForm.heckeLocal.newformMultiplicity_finrank_iInf_eigenspace_algebraicClosure_eq_of_isCornerRealization_level_self 5,450 below · cited by 1 · depth 17
• A ̄ K-point occupying a local corner of H¹ CuspForm.heckeLocal.exists_algHom_algebraicClosure_residual_isRoot_of_linearEquiv_cornerSubmodule 278 below · cited by 1 · depth 18
• Sign interpolating U_q-eigenvalues in the local Hecke algebra CuspForm.heckeLocal.exists_forall_point_apply_eq_qCoeff_of_not_isUnramifiedAt 3,887 below · cited by 1 · depth 18
• Newform behind a geometric point of the local Hecke algebra CuspForm.heckeLocal.exists_isNewform_chig_full_iota_of_algHom_algebraicClosure 640 below · cited by 3 · depth 18
• Ordinary local root count one at p ‖ N CuspForm.heckeLocal.exists_isNewform_sum_rootMultiplicity_residual_eq_one_of_isOrdinaryAt 5,285 below · cited by 1 · depth 18
• Ordinary unit root at p ‖ N for every geometric point CuspForm.heckeLocal.exists_ne_zero_forall_algHom_algebraicClosure_isNewform_residual_unitRoot_of_isOrdinaryAt 5,283 below · cited by 2 · depth 18
• Eigenspace dimensions for a corner realisation at level N CuspForm.heckeLocal.finrank_iInf_eigenspace_baseChange_eq_finrank_range_inf_iInf_eigenspace_heckeTL_of_linearEquiv_cornerSubmodule_level_self 0 below · cited by 1 · depth 18
• Reducedness of the localised weight-two Hecke algebra at θ' CuspForm.heckeLocal.isReduced_of_charpoly_frobenius_eq_of_isAbsolutelyIrreducible 1,535 below · cited by 1 · depth 18
• Local root count one at q ∥ N, q ≠ p CuspForm.heckeLocal.sum_rootMultiplicity_residual_eq_one_of_dvd_of_not_sq_dvd_of_ne 3,931 below · cited by 1 · depth 18
• Residual root count two at p when ρ̄ is not ordinary CuspForm.heckeLocal.sum_rootMultiplicity_residual_eq_two_of_not_isOrdinaryAt 5,051 below · cited by 1 · depth 18
• Newform behind a point of the ordinary local Hecke algebra CuspForm.heckeLocal.exists_moduleFinite_dvr_isNewform_chig_iota_isUnit_of_isOrdinaryAt_of_algHom 2,659 below · cited by 1 · depth 19
• Non-ordinary residual points: p∤ M and aₚ a non-unit CuspForm.heckeLocal.not_dvd_level_and_not_isUnit_qCoeff_of_point_of_not_isOrdinaryAt 4,966 below · cited by 1 · depth 19