← all areas

Namespace GaloisRepAdic 135 theorems

— 133 · IsEquiv 2

directly in GaloisRepAdic 133

• Characteristic polynomials commute with base change of coefficients GaloisRepAdic.charpoly_baseChangeAlong 0 below · cited by 50 · depth 8
• Equivalent adic Galois representations have equal characteristic polynomials GaloisRepAdic.charpoly_eq_of_isEquiv 0 below · cited by 6 · depth 8
• Characteristic polynomial of the residual representation GaloisRepAdic.charpoly_residual 0 below · cited by 34 · depth 8
• Cyclotomic determinant is preserved under local base change GaloisRepAdic.detIsCyclotomic_baseChangeAlong 0 below · cited by 14 · depth 8
• Flatness at p is stable under base change GaloisRepAdic.isFlatAt_baseChangeAlong_of_finite_residueField 1 below · cited by 14 · depth 8
• Ordinarity at p is preserved by base change along a local homomorphism GaloisRepAdic.isOrdinaryAt_baseChangeAlong 0 below · cited by 13 · depth 8
• Unramifiedness is preserved by coefficient base change GaloisRepAdic.isUnramifiedAt_baseChangeAlong 0 below · cited by 11 · depth 8
• Frobenius characteristic polynomials determine the whole representation GaloisRepAdic.charpoly_eq_of_charpoly_frobenius_eq 21 below · cited by 38 · depth 9
• Adic continuity gives a continuous map to GL₂(A) GaloisRepAdic.continuous_unitsMap_toMatrix_of_isAdicContinuous 1 below · cited by 3 · depth 9
• Determinant is cyclotomic from Frobenius determinants GaloisRepAdic.detIsCyclotomic_of_forall_frobenius_det_eq 22 below · cited by 25 · depth 9
• Base change of the flat deformation condition along a local homomorphism GaloisRepAdic.flatCondition_baseChangeAlong_of_finite_residueField 4 below · cited by 7 · depth 9
• Flat condition of type S detected on Artinian quotients GaloisRepAdic.flatCondition_of_forall_quotient 3 below · cited by 1 · depth 9
• Equivalence-invariance of the flat condition flatCondition 𝒪 p S GaloisRepAdic.flatCondition_of_isEquiv 3 below · cited by 1 · depth 9
• Flat condition reflected by jointly injective local maps GaloisRepAdic.flatCondition_of_jointly_injective 6 below · cited by 1 · depth 9
• Continuous GL₂(A)-representations act 𝔪-adically continuously GaloisRepAdic.galoisActionIsAdicContinuous_toLin_of_continuous 0 below · cited by 4 · depth 9
• Carayol's lemma: equal traces force equivalence GaloisRepAdic.isEquiv_of_residual_isAbsolutelyIrreducible_of_trace_eq 5 below · cited by 17 · depth 9
• Flatness at p is invariant under equivalence GaloisRepAdic.isFlatAt_of_isEquiv 0 below · cited by 8 · depth 9
• Ordinarity at p is invariant under equivalence GaloisRepAdic.isOrdinaryAt_of_isEquiv 0 below · cited by 11 · depth 9
• Unipotent inertia at q survives base change GaloisRepAdic.isUnipotentOnInertiaAt_baseChangeAlong 0 below · cited by 18 · depth 9
• Unramifiedness at q is invariant under equivalence GaloisRepAdic.isUnramifiedAt_of_isEquiv 0 below · cited by 5 · depth 9
• Equal Frobenius characteristic polynomials off S transport local types GaloisRepAdic.localType_congr_of_charpoly_frobenius_eq 22 below · cited by 8 · depth 9
• Non-unipotent inertia and Steinberg Frobenius for newform representations GaloisRepAdic.not_isUnipotentOnInertiaAt_and_charpoly_frobenius_of_factorization_eq_two_of_absIrred_odd_of_ne_two 10,837 below · cited by 1 · depth 9
• Ordinary condition is preserved by base change along local homomorphisms GaloisRepAdic.ordinaryCondition_baseChangeAlong 0 below · cited by 5 · depth 9
• Invariance of the ordinary condition under equivalence GaloisRepAdic.ordinaryCondition_of_isEquiv 0 below · cited by 5 · depth 9
• Cyclotomic determinant descends from the quotients A/𝔪^{m+1} GaloisRepAdic.detIsCyclotomic_of_forall_quotient 0 below · cited by 4 · depth 10
• Cyclotomic determinant is invariant under equivalence GaloisRepAdic.detIsCyclotomic_of_isEquiv 0 below · cited by 1 · depth 10
• Descent of the cyclotomic determinant condition along a jointly injective pair GaloisRepAdic.detIsCyclotomic_of_jointly_injective 0 below · cited by 3 · depth 10
• Determinant character commutes with base change GaloisRepAdic.det_baseChangeAlong 0 below · cited by 1 · depth 10
• Inertia at a Taylor–Wiles prime acts as χ⊕χ⁻¹ GaloisRepAdic.exists_inertiaCharacter_of_detIsCyclotomic_of_regular 36 below · cited by 3 · depth 10
• Iterated base change equals base change along the composite GaloisRepAdic.isEquiv_baseChangeAlong_baseChangeAlong 0 below · cited by 4 · depth 10
• Equality of Frobenius characteristic polynomials forces equivalence GaloisRepAdic.isEquiv_of_charpoly_frobenius_eq 28 below · cited by 4 · depth 10
• Flatness at p descends along coefficient field extension GaloisRepAdic.isFlatAt_ofResidualGaloisRep_of_isFlatAt_baseChangeAlong 1 below · cited by 3 · depth 10
• Flatness at p detected by finitely many bounded-index local points GaloisRepAdic.isFlatAt_of_forall_point_of_finite_index 3 below · cited by 1 · depth 10
• Flatness at p is detected on the quotients A/𝔪^{m+1} GaloisRepAdic.isFlatAt_of_forall_quotient 0 below · cited by 1 · depth 10
• Flatness at p descends along jointly injective local maps GaloisRepAdic.isFlatAt_of_jointly_injective 3 below · cited by 1 · depth 10
• Residual ordinarity at p survives base change of coefficients GaloisRepAdic.isOrdinaryAt_ofResidualGaloisRep_residual_baseChangeAlong 7 below · cited by 2 · depth 10
• Ordinarity at p descends along a jointly injective family of local points GaloisRepAdic.isOrdinaryAt_of_forall_point 4 below · cited by 1 · depth 10
• Ordinarity at odd p descends from the quotients A/𝔪^{m+1} GaloisRepAdic.isOrdinaryAt_of_forall_quotient 1 below · cited by 3 · depth 10
• Ordinarity at odd p descends along jointly injective local maps GaloisRepAdic.isOrdinaryAt_of_jointly_injective 1 below · cited by 4 · depth 10
• Strict ordinarity at p is preserved by local base change GaloisRepAdic.isStrictOrdinaryAt_baseChangeAlong 0 below · cited by 5 · depth 10
• Unramified at q implies unipotent on inertia at q GaloisRepAdic.isUnipotentOnInertiaAt_of_isUnramifiedAt 0 below · cited by 5 · depth 10
• Unramifiedness descends from the Artinian quotients A/𝔪^{m+1} GaloisRepAdic.isUnramifiedAt_of_forall_quotient 0 below · cited by 3 · depth 10
• Unramifiedness descends along a jointly injective pair of local maps GaloisRepAdic.isUnramifiedAt_of_jointly_injective 0 below · cited by 3 · depth 10
• Residual representation commutes with coefficient base change GaloisRepAdic.residual_baseChangeAlong_isEquiv 5 below · cited by 25 · depth 10
• Residual identification and determinant of an adic lift GaloisRepAdic.residual_isEquiv_and_det_sub_mem_of_charpoly_frobenius_eq 48 below · cited by 4 · depth 10
• Nakayama span lemma for absolutely irreducible residual reduction GaloisRepAdic.span_range_eq_top_of_residual_isAbsolutelyIrreducible 3 below · cited by 4 · depth 10
• Strict ordinary condition of type S is stable under base change GaloisRepAdic.strictOrdinaryCondition_baseChangeAlong 3 below · cited by 6 · depth 10
• Wild inertia at q ≠ p acts trivially GaloisRepAdic.apply_eq_one_of_mem_inertiaSubgroupIn_of_wild 2 below · cited by 1 · depth 11
• Cyclotomic determinant is trivial on inertia at q ≠ p GaloisRepAdic.det_eq_one_of_detIsCyclotomic_of_mem_inertiaSubgroupIn 1 below · cited by 3 · depth 11
• Nontriviality on inertia above p for cyclotomic determinant GaloisRepAdic.exists_mem_inertiaSubgroupIn_apply_ne_one_of_detIsCyclotomic 2 below · cited by 3 · depth 11
• Base change of an ordinary line along a local homomorphism GaloisRepAdic.exists_ordinaryLine_baseChangeAlong 0 below · cited by 1 · depth 11
• Flat lifts of ordinary residual representations are ordinary GaloisRepAdic.isOrdinaryAt_of_isFlatAt_of_isOrdinaryAt_ofResidualGaloisRep_residual 31 below · cited by 2 · depth 11
• Descent of ordinarity at p along an injective local homomorphism GaloisRepAdic.isOrdinaryAt_of_isOrdinaryAt_baseChangeAlong_of_injective 0 below · cited by 1 · depth 11
• Strict ordinarity from cyclotomic determinant and z²=1 GaloisRepAdic.isStrictOrdinaryAt_of_detIsCyclotomic_of_forall_quotientScalar_sq_eq_one 0 below · cited by 1 · depth 11
• Unipotence on inertia descends from all 𝔪^{m+1}-quotients GaloisRepAdic.isUnipotentOnInertiaAt_of_forall_quotient 1 below · cited by 3 · depth 11
• Unipotent inertia at q is invariant under equivalence GaloisRepAdic.isUnipotentOnInertiaAt_of_isEquiv 0 below · cited by 6 · depth 11
• Unipotence on inertia descends along a jointly injective pair GaloisRepAdic.isUnipotentOnInertiaAt_of_jointly_injective 1 below · cited by 7 · depth 11
• Non-ordinarity at p from a residually irreducible twin GaloisRepAdic.not_isOrdinaryAt_ofResidualGaloisRep_of_isEquiv_baseChangeAlong 3 below · cited by 1 · depth 11
• Transfer of the square-one quotient scalar between places above p GaloisRepAdic.ordinaryLine_quotientScalar_sq_eq_one_of_liesOverPrime_of_liesOverPrime 4 below · cited by 1 · depth 11
• Quotient scalars are ± 1 for très ramifiée residual representations GaloisRepAdic.quotientScalar_sq_eq_one_of_sq_sub_one_mem_span_socle_of_residual_tresRamifiee 145 below · cited by 1 · depth 11
• Quotient scalars on an ordinary line satisfy z²≡ 1 GaloisRepAdic.quotientScalar_sq_sub_one_mem_maximalIdeal_of_residual_isStrictOrdinaryAt 1 below · cited by 1 · depth 11
• Residual non-triviality persists under base change of coefficients GaloisRepAdic.residual_baseChangeAlong_apply_ne_one 0 below · cited by 1 · depth 11
• Residually unramified inertia acts trivially modulo 𝔪 GaloisRepAdic.toMatrix_sub_one_apply_mem_maximalIdeal_of_residual_isUnramifiedAt 0 below · cited by 1 · depth 11
• Exact tame relation for representations unipotent on inertia GaloisRepAdic.conj_mul_conj_eq_pow_of_isUnipotentOnInertiaAt 0 below · cited by 1 · depth 12
• Cyclotomic determinant over k[ε] means trace-zero cochain GaloisRepAdic.detIsCyclotomic_iff_forall_trace_dualLiftToCochain_eq_zero 0 below · cited by 1 · depth 12
• Cyclotomic determinant is trivial on inertia away from p GaloisRepAdic.det_eq_one_of_mem_inertiaSubgroupIn 0 below · cited by 6 · depth 12
• Ordinarity at λ of a newform's λ-adic representation GaloisRepAdic.exists_ordinaryLine_frobenius_sub_unitRoot_smul_mem_of_isNewform_of_not_dvd 2,433 below · cited by 4 · depth 12
• Socle thickening forces residual peu-ramifié splitting by (1+p)^{1/p} GaloisRepAdic.exists_root_one_add_prime_inertia_sub_mem_of_quotientScalar_sq_sub_one_mem_span_socle 142 below · cited by 1 · depth 12
• Local bound for flat first-order deformation classes at p GaloisRepAdic.exists_submodule_finrank_le_invariants_add_one_mem_of_isFlatAt 756 below · cited by 1 · depth 12
• Strictly ordinary first-order classes lie in a small local subspace at p GaloisRepAdic.exists_submodule_finrank_le_invariants_add_one_mem_of_isStrictOrdinaryAt 76 below · cited by 1 · depth 12
• Unipotent deformations restrict into a small local subspace at ℓ GaloisRepAdic.exists_submodule_finrank_le_invariants_mem_of_isUnipotentOnInertiaAt 85 below · cited by 1 · depth 12
• Très ramifiée witness contradicts inertia acting trivially mod 𝔪 GaloisRepAdic.false_of_residual_tresRamifiee_of_root_one_add_prime_inertia_sub_mem 3 below · cited by 1 · depth 12
• Local constancy and inertial vanishing of a dual-lift cochain GaloisRepAdic.isLocallyConstant_dualLiftToCochain_and_eq_zero_of_isUnramifiedAt 0 below · cited by 3 · depth 12
• Flat plus ordinary reduction gives ordinary: finite coefficients GaloisRepAdic.isOrdinaryAt_of_isFlatAt_of_isOrdinaryAt_ofResidualGaloisRep_residual_of_finite 18 below · cited by 1 · depth 12
• Ordinarity over a DVR from a stable line over the fraction field GaloisRepAdic.isOrdinaryAt_of_stableLine_baseChange 0 below · cited by 1 · depth 12
• Unipotence on inertia at a prime exactly dividing the level GaloisRepAdic.isUnipotentOnInertiaAt_of_isNewform_of_dvd_of_not_sq_dvd 3,711 below · cited by 2 · depth 12
• Uniqueness of the ordinary line and Frobenius scalar at a ramified place GaloisRepAdic.ordinaryLine_eq_and_frobeniusScalar_eq_of_exists_inertia_ne_one 0 below · cited by 3 · depth 12
• Wild inertia with unipotent characteristic polynomial acts trivially GaloisRepAdic.apply_eq_one_of_wild_of_charpoly_eq 2 below · cited by 2 · depth 13
• Unipotent-modulo-𝔪 triangular action is trivial on V/𝔪 V GaloisRepAdic.apply_sub_mem_maximalIdeal_smul_top_of_triangular 0 below · cited by 1 · depth 13
• Wild inertia eigenvalue of order prime to q is 1 GaloisRepAdic.eq_one_of_pow_eq_one_of_coprime_of_wild_of_charpoly_map_eq 3 below · cited by 2 · depth 13
• A framed first-order deformation is a dual-lift module GaloisRepAdic.exists_addEquiv_prod_dualLiftModuleAct_of_isDualLift 0 below · cited by 1 · depth 13
• Inertia augmentation equals the ordinary line, acting cyclotomically GaloisRepAdic.exists_basis_iSup_range_sub_one_eq_span_of_isOrdinaryAt_of_detIsCyclotomic 1 below · cited by 2 · depth 13
• Tame inertia eigenvalues are (q²-1)-th roots of unity GaloisRepAdic.exists_charpoly_inertia_eq_and_pow_sq_sub_one_eq_one_of_forall_mem_inertiaSubgroupIn_wild_apply_eq_one 5 below · cited by 5 · depth 13
• Flatness at p yields a finite flat ℤₚ-model of ρ GaloisRepAdic.exists_finiteFlat_padicInt_model_of_isFlatAt 0 below · cited by 1 · depth 13
• Tame inertia eigenvector for a flat rank-two representation GaloisRepAdic.exists_inertia_eigenvector_tameCharacter_of_isFlatAt 152 below · cited by 1 · depth 13
• Decomposition elements act through local Galois elements GaloisRepAdic.exists_localGaloisToGlobal_apply_eq_of_mem_decompositionSubgroup_padicPlace 2 below · cited by 1 · depth 13
• Upper-triangular local package for an ordinary line at p GaloisRepAdic.exists_local_triangular_package_of_ordinaryLine_padicPlace 0 below · cited by 1 · depth 13
• Frobenius-eigenvalue stable line at an unramified prime GaloisRepAdic.exists_stableLine_frobenius_sub_smul_mem_of_inertia_eq_one_of_charpoly_eq 5 below · cited by 6 · depth 13
• Inertia augmentation and Galois-stable submodules of a finite flat level GaloisRepAdic.iSup_map_levelAction_sub_id_inf_eq_of_finiteFlat_level 14 below · cited by 1 · depth 13
• Unipotent inertia descends to rank-two quotients of a Tate module GaloisRepAdic.isUnipotentOnInertiaAt_of_tateModule_quotient 1 below · cited by 1 · depth 13
• Strict ordinary condition is invariant under equivalence GaloisRepAdic.strictOrdinaryCondition_of_isEquiv 0 below · cited by 1 · depth 13
• Twisting an adic Galois representation by a finite-order character GaloisRepAdic.exists_charpoly_eq_scaleRoots_of_character 0 below · cited by 1 · depth 14
• Twisting a two-dimensional adic Galois representation by a character GaloisRepAdic.exists_charpoly_eq_twist 0 below · cited by 1 · depth 14
• Multiplicative inertia labels for a tame rank-two representation GaloisRepAdic.exists_inertia_labels_mul_dichotomy_of_forall_wild_apply_eq_one 8 below · cited by 4 · depth 14
• One finite level trivialising all depth-K base changes GaloisRepAdic.exists_level_forall_baseChangeAlong_apply_eq_one 0 below · cited by 1 · depth 14
• Integral model for a Galois-stable plane in K⊗_𝒪M GaloisRepAdic.exists_linearMap_baseChange_of_galoisStable_plane 0 below · cited by 2 · depth 14
• Inertia at p acts non-trivially on the residual representation GaloisRepAdic.exists_mem_inertiaSubgroupIn_residual_ne_one_of_detIsCyclotomic 2 below · cited by 4 · depth 14
• Wild inertia at q acts with q-power order GaloisRepAdic.exists_pow_prime_pow_eq_one_of_wild 2 below · cited by 1 · depth 14
• Unit-Kummer ordinary deformations are flat at p GaloisRepAdic.isFlatAt_of_ordinary_of_unitKummer_decomposition 70 below · cited by 1 · depth 14
• Unipotent inertia at primes q∤ M, q≠λ GaloisRepAdic.isUnipotentOnInertiaAt_of_charpoly_frobenius_eq_of_not_dvd 1,323 below · cited by 1 · depth 14
• Uniqueness of the inertia-stable line under residual ramification GaloisRepAdic.ordinaryLine_eq_of_exists_inertia_residual_ne_one 0 below · cited by 2 · depth 14
• Traces commute with base change of coefficients GaloisRepAdic.trace_baseChangeAlong 0 below · cited by 12 · depth 14
• Determinant of the residual representation is the residue of the determinant GaloisRepAdic.det_residual 0 below · cited by 1 · depth 15
• Eigenvalue one on inertia at q forces an invariant vector GaloisRepAdic.exists_ne_zero_forall_inertiaSubgroupIn_apply_eq_self_of_forall_isRoot_charpoly 2 below · cited by 3 · depth 15
• Unramified twists preserve finite flatness at p GaloisRepAdic.isFlatAt_twist_of_forall_inertia_apply_eq_one 12 below · cited by 1 · depth 15
• Carayol descent for a jointly faithful family of T-algebras GaloisRepAdic.exists_baseChangeAlong_isEquiv_of_jointly_injective 30 below · cited by 1 · depth 16
• Unramified residual representations are finite flat at p GaloisRepAdic.isFlatAt_ofResidualGaloisRep_of_isUnramifiedAt 12 below · cited by 1 · depth 16
• Unipotence on inertia at a prime exactly dividing the level GaloisRepAdic.isUnipotentOnInertiaAt_of_isPrimitiveForm_of_dvd_of_not_sq_dvd 3,210 below · cited by 3 · depth 16
• Unramifiedness descends along a jointly injective family of points GaloisRepAdic.isUnramifiedAt_of_forall_point 0 below · cited by 1 · depth 16
• Unramifiedness passes to the residual representation GaloisRepAdic.isUnramifiedAt_residual 0 below · cited by 1 · depth 16
• Steinberg trace identity at a ramified unipotent prime GaloisRepAdic.natCast_mul_trace_sq_eq_det_mul_sq_of_isUnipotentOnInertiaAt_of_apply_ne_one 3 below · cited by 1 · depth 16
• Adic traces determined by Frobenius traces outside S GaloisRepAdic.trace_eq_of_trace_frobenius_eq 17 below · cited by 6 · depth 16
• Wild inertia at q acts trivially under unipotent reduction GaloisRepAdic.apply_eq_one_of_mem_inertiaSubgroupIn_of_wild_of_residual_isUnipotentOnInertiaAt 2 below · cited by 1 · depth 17
• Weight-two eigenform traces: finite flat or strictly ordinary at p GaloisRepAdic.eigenformTraceNebentypus_isFlatAt_or_isStrictOrdinaryAt_of_not_sq_dvd_of_not_dvd_conductor 3,679 below · cited by 1 · depth 17
• Eisenstein Frobenius traces force a reducible residual representation GaloisRepAdic.eisensteinTrace_not_isAbsolutelyIrreducible_residual 24 below · cited by 1 · depth 17
• Carayol descent of Galois representations to T, semi-local form GaloisRepAdic.exists_baseChangeAlong_isEquiv_of_forall_trace_eq 3 below · cited by 1 · depth 17
• Ordinary line at λ exactly dividing the level, a_λ=±1 GaloisRepAdic.exists_ordinaryLine_frobenius_sub_qCoeff_smul_mem_of_isNewform_of_dvd_of_not_sq_dvd 4,892 below · cited by 2 · depth 17
• Chebotarev spreading of a Frobenius quadratic relation GaloisRepAdic.exists_quadraticRelation_forall_of_frobenius 26 below · cited by 1 · depth 17
• Strict ordinarity descends along an injective local homomorphism GaloisRepAdic.isStrictOrdinaryAt_of_isStrictOrdinaryAt_baseChangeAlong_of_injective 3 below · cited by 3 · depth 17
• Determinant on inertia at q from Frobenius determinants GaloisRepAdic.det_eq_of_mem_inertiaSubgroupIn_of_det_frobenius_eq_mul 26 below · cited by 2 · depth 18
• Traces of an adic Galois representation are locally constant modulo J GaloisRepAdic.exists_intermediateField_trace_mul_sub_trace_mem 0 below · cited by 1 · depth 18
• Finite flatness at p for a primitive form of level prime to p GaloisRepAdic.isFlatAt_of_isPrimitiveForm_of_not_dvd 2,275 below · cited by 1 · depth 18
• Strict ordinarity from cyclotomic determinant and an ordinary line GaloisRepAdic.isStrictOrdinaryAt_of_detIsCyclotomic_of_ordinaryLine 5 below · cited by 1 · depth 18
• Strict ordinarity at p is invariant under equivalence GaloisRepAdic.isStrictOrdinaryAt_of_isEquiv 0 below · cited by 1 · depth 18
• Strict ordinarity at p exactly dividing the level GaloisRepAdic.isStrictOrdinaryAt_of_isPrimitiveForm_of_dvd_of_not_sq_dvd_of_not_dvd_conductor 3,644 below · cited by 1 · depth 18
• Unramifiedness at q from inertia-invariant characteristic polynomials GaloisRepAdic.apply_eq_one_of_mem_inertiaSubgroupIn_of_charpoly_mul_eq_of_ne 3 below · cited by 1 · depth 19
• Frobenius charpoly at a prime exactly dividing the level GaloisRepAdic.charpoly_eq_of_isFrobeniusAt_of_isPrimitiveForm_of_dvd_of_not_sq_dvd_of_not_dvd_conductor 4,077 below · cited by 1 · depth 19
• Ordinary line at p with Frobenius acting by aₚ GaloisRepAdic.exists_ordinaryLine_frobenius_sub_smul_mem_of_isEigenformWith_of_isUnit_of_dvd_of_not_sq_dvd_of_not_dvd_conductor 3,640 below · cited by 1 · depth 19
• Local structure at a prime exactly dividing the level GaloisRepAdic.exists_stableLine_frobenius_eq_qCoeff_smul_of_isNewform_of_dvd_of_not_sq_dvd 3,840 below · cited by 1 · depth 19
• Rank-one inertia coinvariants with scalar Frobenius action GaloisRepAdic.exists_stableLine_frobenius_sub_smul_mem_of_isUnipotentOnInertiaAt_of_residual_ne_one 0 below · cited by 1 · depth 19
• Flatness at p via an equivariant quotient of a Tate module GaloisRepAdic.isFlatAt_of_surjective_tateModule_of_forall_exists_finiteFlat_pi_torsion 3 below · cited by 1 · depth 19
• Determinant at a Frobenius above q from a congruent prime GaloisRepAdic.det_eq_mul_of_isFrobeniusAt_of_det_frobenius_eq_mul_of_not_dvd_conductor 25 below · cited by 1 · depth 20
• Inertia acts commutatively when 1 is an eigenvalue GaloisRepAdic.rho_mul_comm_of_mem_inertiaSubgroupIn_of_forall_isRoot_charpoly 2 below · cited by 1 · depth 20

GaloisRepAdic.IsEquiv 2

• Unipotence on inertia at q is invariant under equivalence GaloisRepAdic.IsEquiv.isUnipotentOnInertiaAt 1 below · cited by 3 · depth 10
• Equivalence invariance of the ordinary condition GaloisRepAdic.IsEquiv.ordinaryCondition 1 below · cited by 2 · depth 10