Namespace Representation 50 theorems
- Spanning of an endomorphism algebra is insensitive to base change
Representation.span_range_baseChange_eq_top_iff0 below · cited by 5 · depth 8 - Frobenius density: traces and determinants agree everywhere
Representation.trace_eq_and_det_eq_of_frobenius_agree_of_ker_restrictNormalHom_le21 below · cited by 3 · depth 8 - Non-central order-two image in GL₂ fixes a line
Representation.finrank_invariants_eq_one_of_natCard_map_eq_two0 below · cited by 1 · depth 9 - Burnside's theorem for irreducible representations
Representation.span_range_eq_top_of_isIrreducible0 below · cited by 8 · depth 9 - Boston–Lenstra–Ribet: quadratic annihilation forces W≅ρ^{⊕ n}
Representation.exists_blrDecomposition_of_spanTop_of_quadraticAnnihilation0 below · cited by 4 · depth 10 - Trace determines representations spanning the endomorphism algebra
Representation.exists_linearEquiv_of_span_range_eq_top_of_trace_eq_of_isLocalRing0 below · cited by 2 · depth 10 - Irreducible two-dimensional ρ fails tr = 1 + det
Representation.exists_trace_ne_one_add_det_of_irreducible0 below · cited by 1 · depth 10 - Burnside's criterion for absolute irreducibility
Representation.isAbsolutelyIrreducible_matrix_iff_span_range_eq_top3 below · cited by 1 · depth 10 - Burnside spanning theorem for absolutely irreducible matrix representations
Representation.span_range_eq_top_of_isAbsolutelyIrreducible_matrix2 below · cited by 4 · depth 10 - Cayley–Hamilton spreads from dense Frobenius powers
Representation.cayleyHamilton_of_frobeniusPowerDense0 below · cited by 1 · depth 12 - Representations spanning the endomorphism algebra are irreducible
Representation.isIrreducible_of_span_range_eq_top0 below · cited by 2 · depth 12 - Common eigenvector with eigencharacter 1 or χ
Representation.exists_ne_zero_forall_apply_eq_self_or_eq_char_smul1 below · cited by 1 · depth 13 - Nonzero fixed vector for p-groups in characteristic p
Representation.exists_ne_zero_forall_apply_eq_of_isPGroup0 below · cited by 4 · depth 14 - Burnside spanning for absolutely irreducible representations
Representation.span_range_eq_top_of_isAbsolutelyIrreducible2 below · cited by 2 · depth 14 - Irreducibility transfers along equal traces and determinants
Representation.stable_eq_bot_or_top_of_trace_eq_of_det_eq_of_irreducible0 below · cited by 1 · depth 14 - Descent of an irreducible 2-dimensional representation to a subfield
Representation.exists_basis_toMatrix_mem_subfield_of_trace_det_mem_of_hasEigenvalue0 below · cited by 1 · depth 15 - Descent of an absolutely irreducible representation over a finite field
Representation.exists_conj_eq_map_of_charpoly_coeff_mem_range_of_finite_of_span_range_eq_top1 below · cited by 1 · depth 15 - Pointwise smoothness upgrades to a single finite Galois level
Representation.exists_isGalois_level_forall_apply_eq_self0 below · cited by 3 · depth 15 - Lifting mod-ℓ representations of ℓ'-order groups
Representation.exists_monoidHom_complex_charpoly_map_eq_of_not_dvd_natCard0 below · cited by 1 · depth 15 - Commutant criterion for absolute irreducibility of a representation
Representation.isAbsolutelyIrreducible_iff_isIrreducible_and_surjective_algebraMap_end4 below · cited by 2 · depth 15 - Vanishing of the norm of a cyclic group in characteristic p
Representation.norm_eq_zero_of_dvd_card4 below · cited by 2 · depth 15 - Finite-image GL₂(ℂ) representations with equal characteristic polynomials are conjugate
Representation.exists_conj_eq_of_charpoly_eq_of_finite_range0 below · cited by 1 · depth 16 - Descent of an absolutely irreducible two-dimensional representation to a finite field
Representation.exists_map_eq_conj_and_span_range_eq_top_of_charpoly_coeff_mem_range_of_finite_fin_two0 below · cited by 1 · depth 16 - Decomposition of a cyclic-group representation into characters
Representation.exists_multiplicity_of_isCyclic0 below · cited by 1 · depth 16 - No commuting representation shares the character of a 2-dimensional Burnside representation
Representation.false_of_span_eq_top_of_trace_eq_of_commute0 below · cited by 3 · depth 16 - Equal traces and dimension propagate End-spanning
Representation.span_range_eq_top_of_span_range_eq_top_of_trace_eq0 below · cited by 4 · depth 16 - Boston–Lenstra–Ribet equivariant embedding lemma over a reduced algebra
Representation.exists_injective_equivariant_of_quadraticRelation_of_faithful_of_isReduced6 below · cited by 1 · depth 17 - Rank of a cohomologically trivial lattice over a p-group
Representation.finrank_eq_card_mul_finrank_coinvariants_of_isPGroup1 below · cited by 1 · depth 17 - Boston–Lenstra–Ribet embedding over a reduced Artinian ℚ-algebra
Representation.exists_injective_equivariant_of_quadraticRelation_of_isArtinianRing_of_isReduced3 below · cited by 1 · depth 18 - Equal eigenspace dimensions of an involution with ψ(c)=-1
Representation.finrank_ker_sub_one_eq_finrank_ker_add_one_of_spanTop_of_quadraticAnnihilation1 below · cited by 1 · depth 18 - Normal p-subgroups act trivially on simple mod-p representations
Representation.forall_apply_eq_one_of_normal_isPGroup_of_isSimple0 below · cited by 2 · depth 18 - Injectivity after base change for absolutely irreducible ρ
Representation.injective_liftBaseChange_of_isAbsolutelyIrreducible0 below · cited by 1 · depth 18 - Quadratic relation propagates to conjugates times H, modulo N
Representation.quadraticRelation_apply_mem_of_conj_mul_of_eq_zero0 below · cited by 1 · depth 18 - Quadratic relation forces d=detρ_V in characteristic ≠ 2
Representation.det_eq_of_sq_sub_trace_smul_add_smul_one_eq_zero0 below · cited by 1 · depth 19 - Dual representation has invariants of equal dimension
Representation.finrank_invariants_dual_of_isUnit_card0 below · cited by 1 · depth 19 - Dimension of Hom_Δ(V^∨(χ),k(χ)) equals dim V^Δ
Representation.finrank_invariants_linHom_dual_twist_ofChar0 below · cited by 1 · depth 19 - Schur's lemma: central translation acts by a scalar
Representation.exists_const_apply_central_mul_eq_of_countable_translates_of_irreducible0 below · cited by 1 · depth 20 - Extension of right-translation-equivariant maps into ℂ^G
Representation.exists_extend_forall_apply_mul_of_injective0 below · cited by 4 · depth 20 - Stable complements for continuous representations of compact groups
Representation.exists_isCompl_forall_mem_of_compactSpace_of_continuous0 below · cited by 5 · depth 20 - Additivity of dim_k Hom_Δ(N,-) on short exact sequences
Representation.finrank_invariants_linHom_eq_add_of_exact_of_isUnit_card0 below · cited by 2 · depth 20 - Trace is unchanged by a commuting p-power-order factor
Representation.trace_mul_eq_trace_of_commute_of_pow_prime_pow_eq_one0 below · cited by 1 · depth 20 - Commutant of a simple commuting representation is a field acting simply transitively
Representation.centralizer_eq_adjoin_and_isField_of_isSimple_of_forall_commute1 below · cited by 2 · depth 21 - Schur's lemma for irreducible representations with commuting operators
Representation.existsUnique_mem_centralizer_apply_eq_of_forall_commute0 below · cited by 1 · depth 22 - A[p] ≅ A/pA as G-modules when p ∤ #G
Representation.nonempty_equiv_torsionBy_quotient_of_coprime0 below · cited by 1 · depth 22 - Rational representations of a cyclic group determined by invariant dimensions
Representation.exists_linearEquiv_of_finrank_invariants_eq3 below · cited by 1 · depth 23 - Invariance of h_N under passage to a finite-index Δ-stable subgroup
Representation.finrank_invariants_linHom_modP_add_torsion_eq_of_finiteIndex0 below · cited by 2 · depth 23 - Mod p Hom-invariants unchanged by a finite-index Δ-stable subgroup
Representation.finrank_invariants_linHom_eq_of_finiteIndex_of_torsionFree1 below · cited by 1 · depth 24 - Equivariant maps into a free k[Δ]-module: the dimension count
Representation.finrank_invariants_linHom_of_basis_regular0 below · cited by 1 · depth 24 - Simple quotient of an mathbb Fₚ[Γ]-module is an F-line
Representation.exists_submodule_quotient_line_of_commutator_le_of_isPGroup2 below · cited by 1 · depth 25 - Invariant pairing with an irreducible representation vanishes
Representation.pairing_eq_zero_of_invariant_of_isSimpleOrder_of_exists_ne_zero0 below · cited by 1 · depth 25