← all areas

Namespace CuspidalType 45 theorems

— 37 · IsCuspidalOfType 7 · NV3Arch 1

directly in CuspidalType 37

• Irreducible cuspidal representations of GL₂(𝔽_q) have a type CuspidalType.exists_isCuspidalOfType_of_irreducible_of_cuspidal_of_central 26 below · cited by 4 · depth 14
• Cuspidal character equals -1 at non-trivial unipotents CuspidalType.character_unipotent 1 below · cited by 2 · depth 15
• Vanishing of cuspidal characters on split classes through 1 CuspidalType.character_unipotent_mul_diagElem 0 below · cited by 2 · depth 15
• Characteristic polynomial of P¹ at a non-split torus element CuspidalType.charpoly_ind_torus_eq_prod_X_sub_C_of_forall_mem_iff 1 below · cited by 1 · depth 15
• Exactly q+1 characters of 𝔽_{q²}^× trivial on 𝔽_q^× CuspidalType.exists_finset_monoidHom_mem_iff_forall_apply_eq_one_and_card_eq 1 below · cited by 2 · depth 15
• Torus charpoly of a cuspidal-type character: ρ|_T = bigoplus_μ ≠ θ,θ⁻¹μ CuspidalType.exists_sq_ne_one_and_forall_charpoly_torus_mul_eq_prod_of_forall_character_eq 18 below · cited by 1 · depth 15
• Cuspidal irreducible representations of GL₂(𝔽_q) have dimension q-1 CuspidalType.finrank_eq_of_irreducible_of_cuspidal 0 below · cited by 2 · depth 15
• Characters of 𝔽_{q²}^× killed by q+1 CuspidalType.pow_add_one_eq_one_iff_forall_theta_scalarUnit_eq_one 0 below · cited by 3 · depth 15
• Character of a cuspidal representation sums to zero CuspidalType.sum_character_eq_zero 0 below · cited by 1 · depth 15
• Self-orthogonality of an irreducible character of GL₂(𝔽_q) CuspidalType.sum_character_mul_character_inv 0 below · cited by 1 · depth 15
• A cuspidal type is trivial on 𝔽_q^× CuspidalType.theta_scalarUnit_eq_one_of_isCuspidalOfType 0 below · cited by 2 · depth 15
• Characteristic polynomial of a torus element on K[P¹(mathbb F_q)] CuspidalType.charpoly_ind_torus_eq_X_pow_orderOf_sub_one_pow 0 below · cited by 3 · depth 16
• No SL₂(𝔽_q)-invariants in Steinberg modulo constants CuspidalType.eq_zero_of_forall_specialLinearGroup_apply_eq_of_steinberg_quotient 0 below · cited by 1 · depth 16
• Equivariant quotient of the Steinberg module by constant functions CuspidalType.exists_linearMap_steinberg_toSubmodule_surjective_and_eq_zero_iff_smul_constFun 0 below · cited by 2 · depth 16
• Two missing torus characters form a regular inverse pair CuspidalType.exists_sq_ne_one_and_forall_apply_eq_zero_iff_of_card_eq_of_forall_apply_pow_eq 1 below · cited by 1 · depth 16
• Frobenius invariance of torus character multiplicities CuspidalType.finsupp_apply_pow_eq_of_forall_character_torus_eq_sum 1 below · cited by 1 · depth 16
• Elliptic character sums for a cuspidal-type representation of GL₂(𝔽_q) CuspidalType.sum_character_torus_and_sum_character_torus_mul_character_torus_inv 11 below · cited by 1 · depth 16
• Torus image of a prime-field unit is scalar CuspidalType.torus_unitsMap_algebraMap 0 below · cited by 2 · depth 16
• Upper-triangular elements of GL₂(𝔽_q) in normal form CuspidalType.eq_scalarElem_mul_unipotent_or_eq_unipotent_mul_scalarElem_mul_diagElem_of_apply_one_zero_eq_zero 0 below · cited by 3 · depth 17
• Eigenvalue in 𝔽_q forces conjugacy into the Borel CuspidalType.exists_conj_apply_one_zero_eq_zero_of_isRoot_charpoly 0 below · cited by 3 · depth 17
• Frobenius conjugates the non-split torus of GL₂(𝔽_q) CuspidalType.exists_conj_torus_eq_torus_pow 0 below · cited by 2 · depth 17
• Recognising ρ as Steinberg modulo constants from characteristic polynomials CuspidalType.exists_surjective_steinberg_toSubmodule_eq_zero_iff_smul_constFun_of_charpoly_ind_eq_X_sub_one_sq_mul 3 below · cited by 1 · depth 17
• Count of non-central elements with square characteristic polynomial CuspidalType.natCard_not_mem_center_and_charpoly_eq_X_sub_C_sq 0 below · cited by 1 · depth 17
• Conjugate non-split torus elements differ by Frobenius CuspidalType.eq_or_eq_pow_of_isConj_torus 0 below · cited by 1 · depth 18
• Elements with no eigenvalue in 𝔽_q are conjugate into the non-split torus CuspidalType.exists_conj_eq_torus 0 below · cited by 3 · depth 18
• Steinberg quotients over k descend to 𝔽ₚ, basis to basis CuspidalType.exists_semilinearMap_steinberg_quotient_forall_apply_eq_and_exists_basis_eq_of_steinberg_quotient_zmod 0 below · cited by 1 · depth 18
• Centraliser of a regular non-split torus element in GL₂(𝔽_q) CuspidalType.mul_torus_eq_torus_mul_iff 0 below · cited by 1 · depth 18
• Regular non-split torus elements have no eigenvalue in 𝔽_q CuspidalType.not_isRoot_charpoly_torus 0 below · cited by 2 · depth 18
• Injectivity of the non-split torus in GL₂(𝔽_q) CuspidalType.torus_injective 0 below · cited by 1 · depth 18
• Characters with trivial scalar action are invariant under scalars CuspidalType.character_scalar_mul 0 below · cited by 1 · depth 19
• Characteristic polynomial of diag(a,1) on K[P¹(𝔽_q)] CuspidalType.charpoly_ind_diagElem_eq 0 below · cited by 1 · depth 19
• Characteristic polynomial of a unipotent element on P¹(mathbb F_q) CuspidalType.charpoly_ind_unipotent_eq 0 below · cited by 1 · depth 19
• Charpoly of z diag(a,1) in a cuspidal representation CuspidalType.charpoly_scalarElem_mul_diagElem_eq_X_pow_orderOf_sub_one_pow_of_cuspidal 0 below · cited by 1 · depth 19
• Cuspidal representations: unipotent charpoly is Φ_q CuspidalType.charpoly_scalarElem_mul_unipotent_eq_cyclotomic_of_cuspidal 0 below · cited by 1 · depth 19
• Vanishing of unipotent sums on the image of an intertwiner CuspidalType.sum_unipotent_mul_apply_apply_eq_zero_of_forall_unipotent_apply_eq 0 below · cited by 3 · depth 19
• Equivariant projector onto the cuspidal part of ρ CuspidalType.exists_linearMap_apply_eq_self_of_forall_sum_unipotent_eq_zero_and_comm 0 below · cited by 3 · depth 22
• Cuspidal vectors meet N-induced span trivially and are τ-fixed CuspidalType.iInf_ker_sum_unipotent_comp_inf_eq_bot_and_apply_eq_self_of_le_span_unipotent_fixed_of_sub_mem 0 below · cited by 3 · depth 23

CuspidalType.IsCuspidalOfType 7

• Cuspidal types are trivial on mathbb F_q^×, and regular CuspidalType.IsCuspidalOfType.forall_apply_pow_eq_one_and_exists_apply_sq_ne_one 2 below · cited by 5 · depth 14
• Cuspidality of type θ is preserved by scalar extension CuspidalType.IsCuspidalOfType.baseChange 0 below · cited by 1 · depth 16
• The dual of a cuspidal type is cuspidal of the same type CuspidalType.IsCuspidalOfType.dual 0 below · cited by 1 · depth 18
• Mod p congruence of characteristic polynomials for cuspidal types CuspidalType.IsCuspidalOfType.exists_charpoly_eq_map_and_charpoly_ind_eq_X_sub_one_sq_mul_map 8 below · cited by 1 · depth 18
• Uniqueness of cuspidal representations of type θ CuspidalType.IsCuspidalOfType.exists_linearEquiv_comm_of_isCuspidalOfType 8 below · cited by 1 · depth 18
• Cuspidality of type θ transports along equivariant isomorphisms CuspidalType.IsCuspidalOfType.of_linearEquiv 0 below · cited by 3 · depth 18
• Cuspidal representations of a given type are irreducible CuspidalType.IsCuspidalOfType.toSubmodule_eq_top_of_ne_bot 0 below · cited by 4 · depth 18

CuspidalType.NV3Arch 1

• Elliptic class sums versus non-split torus sums in GL₂ CuspidalType.NV3Arch.sum_elliptic_eq 6 below · cited by 1 · depth 17