← all areas

Namespace CohCarrier 192 theorems

— 180 · HeckeData 10 · OperatorAlgebra 1 · heckeDiamondRing 1

directly in CohCarrier 180

• Kernel pairs of the degeneracy maps are Eisenstein modulo level N CohCarrier.exists_isEis_of_iDeg_add_eq_zero 2 below · cited by 2 · depth 11
• Ihara's lemma at every prime q ∤ N: kernel pairs are Eisenstein CohCarrier.exists_isEis_of_iDeg_add_eq_zero_of_prime 41 below · cited by 1 · depth 11
• Congruence characters of Γ₀(N) are Eisenstein at T_ℓ CohCarrier.heckeT_eq_smul_of_forall_mem_Gamma_apply_eq_zero 6 below · cited by 4 · depth 11
• Ihara's lemma: degeneracy kernel pairs are Eisenstein CohCarrier.isEis_kernel_pair_of_prime 40 below · cited by 6 · depth 11
• Ihara's lemma: Eisenstein kernel pairs along the q-tower CohCarrier.isEis_kernel_pair_unconditional 38 below · cited by 1 · depth 11
• Corestriction of a restricted additive character is [G:K]·φ CohCarrier.coresAdd_comp_subtype 0 below · cited by 5 · depth 12
• Perfect Hecke-self-adjoint degeneracy-adjoint pairing at Γ_H level CohCarrier.exists_perfect_selfAdjoint_degeneracyAdjoint_pairing_map_iDegL_parabolicHoms 20 below · cited by 3 · depth 12
• Congruence characters of Γ₀(N) are Eisenstein at good ℓ CohCarrier.heckeT_eq_smul_of_forall_mem_Gamma_apply_eq_zero_of_not_dvd 3 below · cited by 1 · depth 12
• Interchange of U_q with the degeneracy maps ι₁^*,ι_q^* CohCarrier.heckeT_iDeg_interchange 0 below · cited by 4 · depth 12
• Degeneracy pullback commutes with T_ℓ at coprime ℓ CohCarrier.iDeg_heckeT_comm_of_coprime 0 below · cited by 31 · depth 12
• Index ℓ+1 for Γ_H(M)∩Γ⁰(ℓ) CohCarrier.index_GammaHUpper_of_prime 0 below · cited by 15 · depth 12
• Degeneracy images at level Nq: indices q+1, q+1, 1, 1 CohCarrier.index_range_iotaDeg_of_prime_comap 1 below · cited by 1 · depth 12
• Ihara's lemma at Γ_H from Γ₀ at unit index CohCarrier.isEis_of_iDeg_add_eq_zero_of_diamond_invariant 4 below · cited by 3 · depth 12
• Finite generation of Hom(Γ_H(M), A) over a noetherian ring CohCarrier.H1_moduleFinite 0 below · cited by 70 · depth 13
• Corners with residually trivial nebentypus lie in W(M,Hₛ) CohCarrier.corner_le_map_iDegL_one_parabolicHoms_of_parabolic_of_diamond_sub_one_mem 3 below · cited by 3 · depth 13
• Residually trivial diamond operators fix corner submodules CohCarrier.diamondL_apply_eq_self_of_mem_cornerSubmodule_of_sub_one_mem 2 below · cited by 1 · depth 13
• Degeneracy maps and Hecke at q: U_qι₁^*=ι₁^*T_q-ι_q^*⟨ q⟩ CohCarrier.exists_gamma0_heckeT_iDeg_interchange_diamondRaw 1 below · cited by 4 · depth 13
• Perfect Hecke-self-adjoint degeneracy-compatible pairings on parabolic homomorphisms CohCarrier.exists_perfect_selfAdjoint_degeneracyAdjoint_pairing_parabolicHoms 13 below · cited by 2 · depth 13
• Freeness of the ordinary Σ-corner at level Mr CohCarrier.free_ordinary_sigmaCorner_level_mul 7,461 below · cited by 2 · depth 13
• Hecke operators at coprime indices commute CohCarrier.heckeT_comm_of_prime 0 below · cited by 37 · depth 13
• Naturality of T_ℓ in the coefficient group CohCarrier.heckeT_comp_coeff 0 below · cited by 35 · depth 13
• U_qι_q^* = q ι₁^* at level Γ_{H_r}(Nq) CohCarrier.heckeT_iDeg_q_eq_smul_r 0 below · cited by 3 · depth 13
• Hecke operator T_ℓ preserves parabolic homomorphisms CohCarrier.heckeT_mem_parabolicHoms 0 below · cited by 12 · depth 13
• Hecke T_ℓ acts by ℓ+1 modulo parabolic homomorphisms CohCarrier.heckeT_sub_smul_mem_parabolicHoms_gammaH_of_modEq_one 2 below · cited by 15 · depth 13
• Composition of degeneracy pullbacks on H1 CohCarrier.iDeg_comp 0 below · cited by 6 · depth 13
• Degeneracy pullback commutes with raw diamond operators CohCarrier.iDeg_diamondRaw_comm 0 below · cited by 6 · depth 13
• T_ℓ commutes with the degeneracy pullback CohCarrier.iDeg_heckeT_comm_of_dvd 0 below · cited by 17 · depth 13
• Index is preserved under pullback along (ℤ/M')^×→(ℤ/M)^× CohCarrier.index_comap_unitsMap 0 below · cited by 4 · depth 13
• Degree-one restriction and transfer between Γ_H(M) and Γ₀(M) CohCarrier.injective_iDeg_one_and_range_eq_of_isUnit_index 1 below · cited by 6 · depth 13
• Index of the mod-r congruence subgroup is a unit CohCarrier.isUnit_index_of_forall_mem_iff_castHom_eq_one 0 below · cited by 9 · depth 13
• Corestriction after degeneracy pullback is multiplication by the index CohCarrier.jDeg_comp_iDegP_self 1 below · cited by 7 · depth 13
• Degeneracy pushforward commutes with diamond conjugation CohCarrier.jDeg_diamondRaw_comm 0 below · cited by 6 · depth 13
• T_ℓ commutes with the degeneracy trace map CohCarrier.jDeg_heckeT_comm_flat 0 below · cited by 13 · depth 13
• U_ℓ commutes with the degeneracy trace map j_d CohCarrier.jDeg_heckeT_comm_of_dvd_of_coprime 0 below · cited by 4 · depth 13
• Cross degeneracy composite is an index multiple of T_q CohCarrier.jDeg_iDeg_cross_eq_index_smul_heckeT 0 below · cited by 5 · depth 13
• Degeneracy cross-composition as index multiple of lower Hecke operator CohCarrier.jDeg_iDeg_cross_eq_index_smul_heckeTlower 1 below · cited by 4 · depth 13
• Degeneracy transfer commutes with restriction to Γ_H CohCarrier.jDeg_iDeg_one_eq_iDeg_one_jDeg_of_comap 0 below · cited by 1 · depth 13
• Level compatibility at d=1 and d=q for full preimages CohCarrier.levelLE_comap_one_and_q 0 below · cited by 2 · depth 13
• Image of parabolic H¹(Γ₀(M)) equals diamond-invariant parabolic part CohCarrier.mem_map_iDegL_one_parabolicHoms_iff 2 below · cited by 4 · depth 13
• Commutativity of the level-(L,H) Hecke operator family on H¹ CohCarrier.opFamily_comm 4 below · cited by 10 · depth 13
• Occupancy and rank factorisation of the Σ-corner at level Mr CohCarrier.torsionBySet_ne_bot_and_finrank_sigmaCornerSubmodule_auxLevel_eq_mul 3,963 below · cited by 2 · depth 13
• Corestriction of a restricted character is [L:K] times corestriction CohCarrier.coresAdd_comp_inclusion 0 below · cited by 3 · depth 14
• Corner modules at Γ_H(Mr) and Γ₀(Mr) coincide CohCarrier.cornerSubmodule_sigmaCorner_gammaH_eq_map_iDegL_one_of_isUnit_index 8 below · cited by 4 · depth 14
• r-oldness of the Σ-corner at level Mr CohCarrier.cornerSubmodule_sigmaCorner_gammaZero_auxLevel_eq_iDegL_sup_iDegL 69 below · cited by 4 · depth 14
• Diamond operators are multiplicative, unital and trivial on H CohCarrier.diamondL_mul_and_diamondL_one_and_diamondL_eq_one_of_mem 0 below · cited by 4 · depth 14
• Diamond operators on Hom(Γ_H(M),V) commute CohCarrier.diamondRaw_comm 0 below · cited by 4 · depth 14
• Parabolic homomorphism lattice for Γ₀(N): free of rank 2dim S₂ CohCarrier.exists_basis_parabolicHoms_top_two_mul_finrank 578 below · cited by 6 · depth 14
• Subgroups between Γ₁(M) and Γ₀(M) are Γ_H(M) CohCarrier.exists_eq_gammaH_of_gamma1_le_of_le_gamma0 0 below · cited by 11 · depth 14
• Lower Hecke operator equals T_q twisted by a diamond CohCarrier.exists_gamma0_heckeTlower_eq_heckeT_diamondRaw 2 below · cited by 2 · depth 14
• Lifting units mod M to Γ₀(M) with ℓ M ∣ c CohCarrier.exists_gamma0_lift_dvd 0 below · cited by 10 · depth 14
• Change of presentation for corners of the Hecke algebra CohCarrier.exists_hdata_corner_of_subfamily_corner_top 3 below · cited by 4 · depth 14
• Integral Eichler–Shimura: Hecke algebra acting on H¹ₚₐᵣ CohCarrier.exists_injective_ringHom_heckeAlgebra_moduleEnd_parabolicHoms 591 below · cited by 11 · depth 14
• Mod p eigensystem on Γ_H(N) occurs in weight two for Γ₀(N) CohCarrier.exists_isMaximal_heckeAlgebra_mem_of_mem_parabolicHoms_of_isAbsolutelyIrreducible 629 below · cited by 2 · depth 14
• Parabolic Tₚ-eigenvalue as an integral polynomial in the T_ℓ-eigenvalues CohCarrier.exists_mvPolynomial_heckeT_eigenvalue_of_mem_parabolicHoms_gammaH_top 679 below · cited by 2 · depth 14
• Integral Eichler–Shimura eigenclass at level Nr CohCarrier.exists_primitive_mem_parabolicHoms_heckeT_eq_smul_level_mul_of_heckeTLin_eq_smul_of_notMem 195 below · cited by 1 · depth 14
• Occupancy at Γ₀(Mr) from Γ_H(Mr) CohCarrier.exists_sigmaCorner_gammaZero_of_sigmaCorner_gammaH 24 below · cited by 4 · depth 14
• Lowering an occupied Hecke corner from level Mr to level M CohCarrier.exists_sigmaCorner_gammaZero_of_sigmaCorner_gammaZero_auxLevel 3,897 below · cited by 4 · depth 14
• Ordinary unit-root refinement at level Nrp: witness existence CohCarrier.exists_subfamily_corner_refinement_level_mul_of_corner_cofull 91 below · cited by 1 · depth 14
• Rank of a non-Eisenstein corner of H¹(Γ₀(N),𝒪) CohCarrier.finrank_cornerSubmodule_H1_eq_two_mul_of_not_isEisenstein 691 below · cited by 3 · depth 14
• Multiplicity-two rank bound at the auxiliary prime r CohCarrier.finrank_cornerSubmodule_sigmaCorner_gammaZero_auxLevel_le_two_mul 3,889 below · cited by 4 · depth 14
• Freeness of the Σ-corner of H¹(Γ₀(M),𝒪) CohCarrier.free_sigmaCorner_gammaZero 6,150 below · cited by 1 · depth 14
• Residue of U_q as Frobenius trace on inertia coinvariants CohCarrier.hdata_residue_U_eq_trace_frobenius_inertiaCoinvariants_of_not_sq_dvd 5,017 below · cited by 2 · depth 14
• Hecke operator T_ℓ as a coset-indexed sum CohCarrier.heckeT_apply_eq_sumEquiv 0 below · cited by 4 · depth 14
• Hecke T_ℓ commutes with the raw diamond action CohCarrier.heckeT_diamondRaw_comm 0 below · cited by 14 · depth 14
• The transfer Hecke operator T_ℓ preserves parabolic homomorphisms CohCarrier.isParabolicHom_heckeT_top 3 below · cited by 1 · depth 14
• Corestriction along degeneracy maps preserves parabolic homomorphisms CohCarrier.jDegL_mem_parabolicHoms 0 below · cited by 1 · depth 14
• Hecke generators preserve parabolic homomorphisms on Γ_H(N) CohCarrier.opFamily_apply_mem_parabolicHoms_gammaH 0 below · cited by 6 · depth 14
• Saturation of the eigen-ideal submodule in the ordinary corner CohCarrier.saturated_torsionBySet_ordinary_sigmaCorner_level_mul 7,463 below · cited by 1 · depth 14
• Pushforward along g kills varpi·φ CohCarrier.coeff_comp_smul_eq_zero 0 below · cited by 1 · depth 15
• Joint injectivity of the two degeneracy pull-backs in weight two CohCarrier.eq_zero_of_iDegL_one_add_iDegL_eq_zero_of_mem_parabolicHoms 590 below · cited by 1 · depth 15
• Σ-corner at level Mr meets ker j₁∩ker jᵣ trivially CohCarrier.eq_zero_of_mem_sigmaCorner_gammaZero_auxLevel_of_jDegL_eq_zero 3,886 below · cited by 2 · depth 15
• Integral p-primitive parabolic class lifting a mod p eigenvector CohCarrier.exists_H1_int_mem_parabolicHoms_not_exists_eq_smul_of_mem_parabolicHoms_of_diamondRaw_eq_of_heckeT_eq_smul 10 below · cited by 2 · depth 15
• Residual Hecke eigensystem realised on a corner of H¹ CohCarrier.exists_algHom_cornerRing_of_ringHom_heckeAlgebra 594 below · cited by 1 · depth 15
• Freeness of a corner of H¹(Γ_H(L),𝒪) over 𝒪[Δ] CohCarrier.exists_basis_cornerSubmodule_H1_monoidAlgebra_of_not_isEisenstein_subfamily 22 below · cited by 1 · depth 15
• Steinberg-quotient eigensystem at level Nq, or Eisenstein CohCarrier.exists_diamondRaw_eq_heckeT_eq_smul_gammaH_bot_mul_or_eisenstein_of_isEigensystemH1_of_steinberg_quotient_of_four_le 28 below · cited by 1 · depth 15
• Hecke-equivariant weight-two Eichler–Shimura isomorphism for Γ_H(M) CohCarrier.exists_eichlerShimura_H1_gammaH 191 below · cited by 5 · depth 15
• Hecke-equivariant Eichler–Shimura map into H¹ at H=top CohCarrier.exists_eichlerShimura_H1_top 582 below · cited by 6 · depth 15
• Parabolic eigenclasses at level Mp occurring at level M are old CohCarrier.exists_eq_iDegL_one_add_iDegL_of_mem_parabolicHoms_of_heckeT_eq_smul 680 below · cited by 1 · depth 15
• Raised local component at level Nq with θ̄(U_q)=0 CohCarrier.exists_idempotentSplitting_algHom_apply_toCornerRing_eq_level_mul_of_prime_of_dvd 9 below · cited by 1 · depth 15
• Raised local component at level Nq² with U_q=0 CohCarrier.exists_idempotentSplitting_algHom_apply_toCornerRing_eq_level_mul_sq_of_prime 12 below · cited by 1 · depth 15
• Polynomial separating an absent eigensystem from a Hecke maximal ideal CohCarrier.exists_mvPolynomial_aeval_eq_zero_and_aeval_notMem_of_forall_eq_zero 3 below · cited by 1 · depth 15
• Parabolic Hecke eigenclasses and points of the Hecke algebra CohCarrier.exists_ringHom_heckeAlgebra_and_forall_exists_eigenclass_of_ker_eq 594 below · cited by 3 · depth 15
• Residual eigensystem of a parabolic cohomology corner is modular CohCarrier.exists_ringHom_heckeAlgebra_apply_T_eq_of_cornerRing_point_of_corner_le_parabolicHoms 600 below · cited by 2 · depth 15
• Two generators modulo kerπ_k for a corner of H¹ CohCarrier.exists_span_pair_union_ker_smul_eq_top_cornerSubmodule_H1_top_of_isAbsolutelyIrreducible 3,101 below · cited by 2 · depth 15
• U_q = ± 1 on a ramified local component of H¹(Γ₀(L)) CohCarrier.exists_sq_eq_one_and_heckeT_eq_smul_of_mem_cornerSubmodule_of_not_isUnramifiedAt_of_ringHom 1,540 below · cited by 1 · depth 15
• Freeness of an ordinary Hecke corner of H¹ CohCarrier.free_cornerSubmodule_H1_of_isAbsolutelyIrreducible_of_ordinary_of_level_trivial_at_p_of_mem_map_unitsMap 4,922 below · cited by 2 · depth 15
• Fricke involution intertwines the lower and upper Hecke operators CohCarrier.frickeH1_heckeTlower_eq_heckeT_frickeH1 0 below · cited by 2 · depth 15
• Hecke relation U_q U_q^∨ = 1+(q-1)ι^*j at q ∥ Mq CohCarrier.heckeT_heckeTlower_eq_add_smul_iDeg_jDeg_of_prime 0 below · cited by 1 · depth 15
• U_q∘ι_q^*=q ι₁^* at level Nq CohCarrier.heckeT_iDeg_q_eq_smul 0 below · cited by 4 · depth 15
• T_ℓ acts as ℓ+1 modulo parabolic homomorphisms CohCarrier.heckeT_sub_smul_mem_parabolicHoms_of_forall_modEq_one 5 below · cited by 9 · depth 15
• Transfer and coset-sum Hecke operators agree at H=top CohCarrier.heckeT_top_apply_eq_heckeOperatorHom 1 below · cited by 8 · depth 15
• Restriction after corestriction equals the sum of diamond operators CohCarrier.iDegP_jDeg_eq_finsum_diamondL 0 below · cited by 1 · depth 15
• Index of Γ_H(M) as product of indices CohCarrier.index_gammaH_eq_index_gamma0_mul_index 0 below · cited by 22 · depth 15
• Ihara: injectivity and varpi-saturation on a non-Eisenstein corner CohCarrier.injective_and_residual_cornerSubmodule_of_isEis 8 below · cited by 1 · depth 15
• Ihara's lemma: injectivity and varpi-saturation of level raising CohCarrier.injective_and_residual_cornerSubmodule_of_isEis_of_dvd 4 below · cited by 1 · depth 15
• Both degeneracy traces vanish on a q-new local component CohCarrier.jDeg_apply_eq_zero_of_mem_cornerSubmodule_of_forall_notMem 2 below · cited by 1 · depth 15
• U_ℓ commutes with the level trace map CohCarrier.jDeg_heckeT_comm_of_dvd 0 below · cited by 2 · depth 15
• Degeneracy composition table at levels N and Nq CohCarrier.jDeg_iDeg_four_identities_of_dvd 5 below · cited by 1 · depth 15
• Level raising at q preserves θ̄-corner components CohCarrier.levelRaisingComb_mem_cornerSubmodule_of_prime 8 below · cited by 1 · depth 15
• Level raising at q ∣ N preserves corner components CohCarrier.levelRaisingComb_mem_cornerSubmodule_of_prime_of_dvd 6 below · cited by 1 · depth 15
• Level raising at q ∣ N: parabolicity, adjointness, Hecke commutation CohCarrier.levelRaisingComb_mem_parabolicHoms_and_adjoint_and_comm_of_prime_of_dvd 18 below · cited by 1 · depth 15
• Level-raising maps between levels N and Nq²: properties CohCarrier.levelRaisingComb_mem_parabolicHoms_and_adjoint_and_comp_of_prime 36 below · cited by 1 · depth 15
• Tₚ on parabolic cohomology lies in the T_ℓ algebra CohCarrier.mem_adjoin_heckeT_parabolicHoms_gammaH_top_of_finite 675 below · cited by 1 · depth 15
• Non-Eisenstein corners of H¹(Γ₀(N),𝒪) are parabolic CohCarrier.mem_parabolicHoms_of_mem_cornerSubmodule_H1_of_notMem 6 below · cited by 3 · depth 15
• Parabolic cohomology is free of rank two over the Hecke algebra CohCarrier.nonempty_basis_fin_two_parabolicHoms_and_finrank_eigenspace_eq_two 683 below · cited by 1 · depth 15
• Surjectivity and kernel of the diamond transfer on H¹ CohCarrier.surjective_jDeg_one_and_jDeg_eq_zero_iff_of_four_le 7 below · cited by 3 · depth 15
• Transfer of a restricted character is the [G:K]-th power CohCarrier.transfer_restrict_eq_pow_index 0 below · cited by 2 · depth 15
• Residual Hecke characters are trivial on the diamond operators CohCarrier.apply_diamondL_eq_one_of_residual_heckeDiamondChar_of_charpoly_frobenius_eq 1,542 below · cited by 1 · depth 16
• The character involution commutes with the Hecke generators CohCarrier.charInvolution_comp_opFamily 0 below · cited by 3 · depth 16
• No r-new parabolic eigenclass at level Mr CohCarrier.eq_zero_of_mem_parabolicHoms_gammaZero_auxLevel_of_heckeT_eq_smul_of_jDeg_eq_zero 3,874 below · cited by 1 · depth 16
• Atkin–Lehner operator at q: five degeneracy identities CohCarrier.exists_atkinLehnerOp_iDegL_jDegL_five_identities_of_prime 9 below · cited by 1 · depth 16
• Faithful Hecke action on H¹ₚₐᵣ(Γ₀(N),ℂ) via Eichler–Shimura CohCarrier.exists_heckeAlgebra_ringHom_parabolicHoms_H1_top 583 below · cited by 1 · depth 16
• Eichler–Shimura map from H¹ onto the dual of J₀(M')[𝔪] CohCarrier.exists_ideal_H1_top_to_dual_baseChange_heckeTorsion_jZero_of_isAbsolutelyIrreducible 1,409 below · cited by 1 · depth 16
• Base change of parabolic cohomology of Γ₁(N), N≥ 4 CohCarrier.exists_linearMap_baseChange_parabolicHoms_gammaH_bot_range_eq_parabolicHoms_of_four_le 6 below · cited by 1 · depth 16
• Hecke eigenclass over K from an idempotent corner of H¹ CohCarrier.exists_ringHom_cornerRing_heckeT_eq_smul_of_idempotentSplitting 4 below · cited by 1 · depth 16
• Two generators for an ordinary p-distinguished corner of H¹ CohCarrier.exists_span_pair_union_ker_smul_eq_top_cornerSubmodule_H1_of_isAbsolutelyIrreducible_of_ordinary_of_level_trivial_at_p_of_mem_infSubgroup 4,918 below · cited by 1 · depth 16
• Corner rank of H¹ scales by the index [H':H] CohCarrier.finrank_cornerSubmodule_H1_eq_relIndex_mul_of_not_isEisenstein_subfamily 20 below · cited by 1 · depth 16
• Rank of a non-Eisenstein corner of H¹(Γ_H(M),𝒪) CohCarrier.finrank_cornerSubmodule_H1_eq_two_mul_finrank_cornerRing_of_not_isEisenstein 264 below · cited by 2 · depth 16
• Level-raising combination killed by U_q at level Nq² CohCarrier.heckeT_comb_eq_zero 3 below · cited by 2 · depth 16
• U_q commutes with the degree-one degeneracy map CohCarrier.heckeT_iDeg_one_comm_of_dvd 0 below · cited by 3 · depth 16
• Residual Tₚ is the Frobenius trace on inertia coinvariants CohCarrier.heckeT_sub_algebraMap_mem_of_isMaximal_of_not_dvd 2,654 below · cited by 1 · depth 16
• Index ℓ of the upper-triangular subgroup of Γ_H(M) CohCarrier.index_GammaHUpper_of_dvd 0 below · cited by 3 · depth 16
• Injectivity and varpi-divisibility for the localised level-raising map CohCarrier.injective_and_residual_of_isEis 4 below · cited by 1 · depth 16
• Injectivity of degeneracy restriction when relative index is invertible CohCarrier.injective_iDeg_one_of_isUnit_relIndex 0 below · cited by 1 · depth 16
• Transfer-Hecke eigencharacters of Γ₀(N) give eigensystems in H¹ CohCarrier.isEigensystemH1_one_of_heckeT_eq_smul 2 below · cited by 2 · depth 16
• The nine degeneracy compositions at level Nq² CohCarrier.jDeg_iDeg_nine_identities_of_prime 17 below · cited by 1 · depth 16
• Corestriction descent of corner submodules and corner Hecke rings CohCarrier.map_jDegL_one_cornerSubmodule_eq_and_exists_algHom_cornerRing_subfamily 11 below · cited by 2 · depth 16
• Vanishing of H²(Γ₀(M),A) when [(ℤ/M)^× : H] is invertible CohCarrier.subsingleton_H2_gamma0_of_isUnit_index 8 below · cited by 1 · depth 16
• Diamond operators act trivially at level H=top CohCarrier.diamondL_top_apply 0 below · cited by 2 · depth 17
• Vanishing of r-old parabolic eigenclasses killed by both trace maps CohCarrier.eq_zero_of_mem_parabolicHoms_of_jDeg_eq_zero_of_apply_T_sq_ne 722 below · cited by 2 · depth 17
• Balanced ±1 eigenspaces of the conjugation involution on a corner of H¹ CohCarrier.exists_charInvolution_cornerSubmodule_H1_linearEquiv_eigenspace_map_mkQ_of_isAbsolutelyIrreducible 1,262 below · cited by 1 · depth 17
• Deligne–Serre lifting for Hecke eigenclasses on Γ_H(N) CohCarrier.exists_complex_heckeT_eigen_reduction_eq_of_mem_span_int 5 below · cited by 1 · depth 17
• Non-parabolic Hecke eigenclasses in H¹(Γ_H(M),ℂ) are Eisenstein CohCarrier.exists_dirichletCharacter_pair_of_not_mem_parabolicHoms_of_heckeT_eq_smul 5 below · cited by 3 · depth 17
• Hecke operator acts by its degree on diamond-invariant classes CohCarrier.exists_iDeg_eq_heckeT_sub_smul_of_forall_diamondRaw_eq 4 below · cited by 1 · depth 17
• Maximal Hecke ideal attached to a residual eigenvector on J₀(M')[p] CohCarrier.exists_ideal_forall_heckeAlg_baseChange_eq_smul_of_exists_jZero_pTorsion_eigenvector 1,365 below · cited by 1 · depth 17
• Hecke-equivariant injection of base-changed H¹ CohCarrier.exists_injective_linearMap_baseChange_H1_heckeTL 2 below · cited by 2 · depth 17
• Ordinary p-distinguished corner of H¹: free line plus 𝒪-dual CohCarrier.exists_isCompl_linearEquiv_cornerRing_linearEquiv_dual_cornerSubmodule_H1_of_ordinary_of_level_trivial_at_p_of_mem_infSubgroup 4,901 below · cited by 1 · depth 17
• Parabolic eigenclasses in H¹(Γ_H(M),ℂ) come from weight-two eigenforms CohCarrier.exists_isEigenformWith_of_mem_parabolicHoms_of_heckeT_eq_smul 203 below · cited by 4 · depth 17
• Hecke eigenvalue systems in parabolic cohomology are cuspidal CohCarrier.exists_ringHom_heckeAlgebra_apply_smul_eq_heckeT_of_mem_parabolicHoms 593 below · cited by 4 · depth 17
• A squarefree polynomial annihilates T_ℓ on H¹ CohCarrier.exists_squarefree_aeval_heckeTL_eq_zero 274 below · cited by 1 · depth 17
• Upper and lower Hecke operators agree at H=top CohCarrier.heckeSym_top 0 below · cited by 1 · depth 17
• T_ℓ acts by ℓ+1 at elements of finite order CohCarrier.heckeT_top_apply_eq_smul_of_isOfFinOrder 2 below · cited by 1 · depth 17
• Degeneracy maps from level Nq² have index q(q+1) CohCarrier.index_range_iotaDeg_of_prime_sq 3 below · cited by 1 · depth 17
• Coefficient naturality of the degeneracy trace jDeg CohCarrier.jDeg_comp_coeff 0 below · cited by 1 · depth 17
• Corner compositions of degeneracy maps at level Nq² CohCarrier.jDeg_iDeg_corner_of_prime_sq 12 below · cited by 1 · depth 17
• Non-Eisenstein corner of H¹(Γ_H(N),𝒪) is parabolic CohCarrier.mem_parabolicHoms_of_mem_cornerSubmodule_H1_gammaH_of_notMem 3 below · cited by 1 · depth 17
• Homomorphisms killing torsion lie in the integral span CohCarrier.mem_span_int_of_forall_isOfFinOrder_apply_eq_zero 1 below · cited by 2 · depth 17
• Parabolic cohomology of Γ_H(M) is free of rank two CohCarrier.nonempty_basis_fin_two_parabolicHoms_gammaH_and_finrank_eigenspace_eq_two 260 below · cited by 2 · depth 17
• Vanishing of H²(Γ_H(N), A) for all coefficients CohCarrier.subsingleton_H2_GammaH 6 below · cited by 2 · depth 17
• Injectivity of the localised three-copy degeneracy map CohCarrier.threeCopy_injective_of_isEis 0 below · cited by 1 · depth 17
• Galois-stable Hecke line and dual quotient mod r in e H¹ CohCarrier.exists_galoisAction_ordinaryLine_mod_cornerSubmodule_H1_of_ordinary_of_level_trivial_at_p_of_mem_infSubgroup 4,899 below · cited by 1 · depth 18
• Dual Galois module for localised H¹(Γ_H(M)) with Eichler–Shimura relation CohCarrier.exists_galoisModule_H1_to_dual_charInvolution_frobenius_of_isAbsolutelyIrreducible 1,257 below · cited by 1 · depth 18
• Manin–Drinfeld: Hecke-stable complement of the parabolic part CohCarrier.exists_isCompl_parabolicHoms_mem_invtSubmodule_heckeTL 212 below · cited by 1 · depth 18
• Descent to ℚ of a squarefree annihilator of T_ℓ CohCarrier.exists_squarefree_aeval_heckeTL_eq_zero_of_complex 1 below · cited by 1 · depth 18
• Squarefree annihilator of T_ℓ on parabolic cohomology CohCarrier.exists_squarefree_aeval_heckeTL_eq_zero_of_mem_parabolicHoms 255 below · cited by 1 · depth 18
• A squarefree polynomial sending H¹ into H¹ₚₐᵣ CohCarrier.exists_squarefree_aeval_heckeTL_mem_parabolicHoms 4 below · cited by 1 · depth 18
• Newform multiplicity in a local corner of H¹(Γ₀(N),𝒪) CohCarrier.finrank_range_baseChange_cornerSubmodule_inf_iInf_eigenspace_heckeTL_eq_two_mul_prod_sum_rootMultiplicity 274 below · cited by 1 · depth 18
• Γ_H(M)∩Γ₀(Mℓ)=Γ_{H'}(Mℓ) for H' the unit preimage CohCarrier.gammaH_inf_gamma0_mul_eq_gammaH_comap_unitsMap 0 below · cited by 11 · depth 18
• Upper and lower Hecke operators agree at full level for q coprime to M CohCarrier.heckeSym_top_of_coprime 1 below · cited by 1 · depth 18
• Uᵣ is an involution on r-new classes CohCarrier.heckeT_heckeT_eq_self_of_jDeg_one_eq_zero_of_jDeg_eq_zero 0 below · cited by 1 · depth 18
• Composition of degeneracy maps ι_{d_1 d_2} = ι_{d_1}∘ι_{d_2} CohCarrier.iotaDeg_comp 0 below · cited by 2 · depth 18
• Degeneracy cross-composition as an index multiple of T_q^∨ CohCarrier.jDeg_iDeg_cross_eq_index_smul_heckeTlower_of_coprime 1 below · cited by 1 · depth 18
• Transitivity of the transfer for K ≤ L ≤ G CohCarrier.transfer_transitive 0 below · cited by 1 · depth 18
• Ordinary filtration mod r on a corner of H¹ CohCarrier.exists_galoisAction_ordinaryFiltration_quotient_dual_mod_cornerSubmodule_H1_of_ordinary_of_level_trivial_at_p_of_mem_infSubgroup 4,879 below · cited by 1 · depth 19
• Eichler–Shimura duality mod p for parabolic H¹ of Γ_H(M) CohCarrier.exists_galoisModule_parabolicHoms_to_dual_charInvolution_frobenius 1,231 below · cited by 1 · depth 19
• Parabolic Hecke eigenclasses on Γ_H(M) come from weight-two eigenforms CohCarrier.exists_isEigenformWith_qCoeff_eq_of_mem_parabolicHoms_of_heckeT_eq_smul 262 below · cited by 1 · depth 19
• Base change of Γ_H(N)-homomorphisms along 𝒪→ F CohCarrier.exists_linearEquiv_tensorProduct_H1_tmul_eq_and_heckeTL_baseChange_and_map_parabolicHoms 1 below · cited by 2 · depth 19
• Base change of the parabolic lattice of Γ₀(N) CohCarrier.exists_linearMap_baseChange_parabolicHoms_gamma0_range_eq_parabolicHoms_top 5 below · cited by 1 · depth 19
• Perfect antisymmetric pairing on a non-Eisenstein corner of H¹ CohCarrier.exists_perfectPairing_antisymm_cornerSubmodule_H1_of_not_isEisenstein 22 below · cited by 1 · depth 19
• Newform part of parabolic cohomology over any algebraically closed field CohCarrier.finrank_parabolicHoms_inf_iInf_eigenspace_heckeTL_inf_iInf_maxGenEigenspace_eq_two_mul_prod_rootMultiplicity 269 below · cited by 2 · depth 19
• Ordinary filtration, trace and determinant mod r on a non-Eisenstein corner CohCarrier.exists_galoisAction_trace_ordinaryFiltration_quotient_dual_mod_cornerSubmodule_H1_of_ordinary_of_not_isEisenstein_of_mem_infSubgroup 4,877 below · cited by 1 · depth 20
• Base change of parabolic cohomology with Hecke operators CohCarrier.exists_linearMap_baseChange_parabolicHoms_top_comp_eq_comp_heckeTL_restrict_baseChange 11 below · cited by 1 · depth 20
• Dimension of g-isotypic parabolic classes at level N CohCarrier.finrank_parabolicHoms_complex_inf_iInf_eigenspace_inf_iInf_maxGenEigenspace_eq_two_mul_prod_rootMultiplicity 261 below · cited by 1 · depth 20
• Hecke adjointness, diamond and Fricke invariance of the cup pairing CohCarrier.pair_heckeT_eq_pair_heckeTlower_and_pair_diamondRaw_and_pair_frickeH1 9 below · cited by 1 · depth 20
• Bottom rows mod M and cosets of ±Γ_H(M) CohCarrier.exists_bottomRow_eq_and_torsionOrbit_bottomRow_eq_iff 1 below · cited by 6 · depth 21
• Integral matrix form of the ordinary p-adic package on Γ_H(M) CohCarrier.exists_intMatrix_galoisRep_ordinaryFiltration_parabolicHoms_padicInt_of_ordinary_of_not_isEisenstein_of_mem_infSubgroup 4,873 below · cited by 1 · depth 21
• Ordinary Galois representation on a non-Eisenstein corner of parabolic cohomology CohCarrier.exists_galoisRep_ordinaryFiltration_cornerSubmodule_parabolicHoms_padicInt_of_ordinary_of_not_isEisenstein_of_mem_infSubgroup 4,870 below · cited by 1 · depth 22
• Integral matrix model for Hecke operators on parabolic cohomology CohCarrier.exists_intMatrix_opFamily_basis_parabolicHoms 3 below · cited by 1 · depth 22
• Primitive vectors parametrise double cosets Γ_H(M)backslashSL₂(ℤ)/⟨ g⟩ CohCarrier.exists_surjective_doubleCoset_gammaH_zpowers_of_addOrderOf_eq 1 below · cited by 1 · depth 22
• Division values of wp detect Γ_H(N)-orbits CohCarrier.exists_mem_GammaH_smul_eq_of_forall_sum_weierstrassP_pow_eq 7 below · cited by 1 · depth 25

CohCarrier.HeckeData 10

• Finiteness and freeness of the localised Hecke module CohCarrier.HeckeData.finite_ML_and_free_ML 7 below · cited by 15 · depth 14
• Finiteness of the Hecke operator algebra and corner alternative CohCarrier.HeckeData.finite_opSubalgebra_and_subsingleton_ML_or_exists_corner 5 below · cited by 6 · depth 14
• Deligne–Serre lifting for transfer Hecke operators on H¹(Γ_H(M)) CohCarrier.HeckeData.exists_eigenvector_H1_of_toML_ne_zero 8 below · cited by 3 · depth 15
• Idempotent splitting of the Hecke algebra of a Hecke datum CohCarrier.HeckeData.nonempty_idempotentSplitting_opSubalgebra 2 below · cited by 12 · depth 15
• Enlarging a commuting family preserves a corner of V CohCarrier.HeckeData.exists_corner_of_genMap_of_forall_isMaximal 4 below · cited by 1 · depth 16
• Abstract α-stabilisation from degeneracy and Atkin–Lehner identities CohCarrier.HeckeData.exists_linearEquiv_ML_of_degeneracy_atkinLehner_identities 10 below · cited by 1 · depth 16
• Adjoining a residually redundant Hecke operator preserves the localisation CohCarrier.HeckeData.exists_linearEquiv_ML_of_toML_op_sub_opAlgHom_pow_mem 8 below · cited by 1 · depth 16
• Hensel splitting of a companion module at a simple root CohCarrier.HeckeData.exists_linearEquiv_ML_prod_of_companion 9 below · cited by 1 · depth 17
• Residual nilpotence tested on simultaneous eigenvectors over K CohCarrier.HeckeData.exists_toML_sub_opAlgHom_pow_mem_of_forall_baseChange_eigenvector 0 below · cited by 1 · depth 17
• Residual eigenvalues cut out the corner in F ⊗_𝒪 H CohCarrier.HeckeData.iInf_maxGenEigenspace_baseChange_le_range_and_inf_eq_bot_and_eq_iSup_of_cornerRing_point 0 below · cited by 2 · depth 19

CohCarrier.OperatorAlgebra 1

• Eigensystems in H¹(Γ_H(L),ℂ): cuspidal or Eisenstein CohCarrier.OperatorAlgebra.exists_isEigenformWith_qCoeff_eq_or_eisenstein_of_heckeT_eq_smul 266 below · cited by 1 · depth 18

CohCarrier.heckeDiamondRing 1

• Characteristic-zero primes of the Hecke–diamond ring are eigencharacters CohCarrier.heckeDiamondRing.exists_ringHom_ker_eq_eigenvector 4 below · cited by 3 · depth 17