Namespace GaloisRep 127 theorems
Landmarks here: Existence of a surjection R ↠ T
— 99 · DeformationRingData 24 · ratLocalizedAt 4
directly in GaloisRep 99
- The flat condition is a deformation condition
GaloisRep.isDeformationCondition_flatCondition23 below · cited by 2 · depth 8 - Ordinariness at odd p is a deformation condition
GaloisRep.isDeformationCondition_ordinaryCondition16 below · cited by 2 · depth 8 - Existence of a universal deformation ring of type D
GaloisRep.nonempty_deformationRingData40 below · cited by 5 · depth 8 - Finiteness of the flat deformation tangent space
GaloisRep.tangentFinite_flatCondition6 below · cited by 2 · depth 8 - Finiteness of the ordinary-condition tangent space
GaloisRep.tangentFinite_ordinaryCondition6 below · cited by 3 · depth 8 - Uniqueness of the classifying map of a type-D lift
GaloisRep.algHom_unique_of_baseChangeAlong_isEquiv_of_corepresentableBy8 below · cited by 1 · depth 9 - Condition subfunctor is contained in the framed lift functor
GaloisRep.conditionSubfunctor_le_liftFunctor0 below · cited by 1 · depth 9 - Conjugation-stability of the deformation-condition subfunctor
GaloisRep.conjStable_conditionSubfunctor1 below · cited by 1 · depth 9 - Existence of the classifying map to a universal deformation ring
GaloisRep.exists_algHom_baseChangeAlong_isEquiv_of_corepresentableBy6 below · cited by 1 · depth 9 - Equal Frobenius characteristic polynomials force conjugacy of GL₂ representations
GaloisRep.exists_conj_of_charpoly_frobenius_eq_of_absolutelyIrreducible12 below · cited by 3 · depth 9 - Equivariant quotients of points of finite flat Hopf algebras
GaloisRep.exists_finiteFlat_quotient_of_equivariant_surjection0 below · cited by 10 · depth 9 - Framed lifts in `conditionLifts` are of type D
GaloisRep.isOfType_framed_of_mem_conditionLifts2 below · cited by 1 · depth 9 - ℤ₍ₚ₎ is a principal ideal ring
GaloisRep.isPrincipalIdealRing_ratLocalizedAt0 below · cited by 74 · depth 9 - Residual representation of type D lies in `conditionLifts`
GaloisRep.mem_conditionLifts_residueField_of_isOfType2 below · cited by 1 · depth 9 - Finiteness of the tangent space of a conditioned deformation ring
GaloisRep.moduleFinite_tangentSubmodule_of_tangentFinite1 below · cited by 1 · depth 9 - No irreducible mod 3 representation unramified outside 3
GaloisRep.not_isIrreducible_matrixRepresentation_of_isUnramifiedAt_of_det_eq_modThreeCyclotomicChar15 below · cited by 1 · depth 9 - Ordinary condition detected on the quotients A/𝔪^{m+1}
GaloisRep.ordinaryCondition_of_forall_quotient4 below · cited by 1 · depth 9 - Ordinary condition descends along an injective local map
GaloisRep.ordinaryCondition_of_injective4 below · cited by 2 · depth 9 - Ordinary condition descends along a jointly injective pair
GaloisRep.ordinaryCondition_of_jointly_injective4 below · cited by 2 · depth 9 - Limit preservation for the deformation-condition subfunctor
GaloisRep.preservesLimits_conditionSubfunctor2 below · cited by 1 · depth 9 - Injective morphisms reflect the deformation-condition subfunctor
GaloisRep.reflectedByInjective_conditionSubfunctor3 below · cited by 1 · depth 9 - Residual representation of a framed lift of ρ₀
GaloisRep.residual_framed_isEquiv_baseChangeAlong0 below · cited by 1 · depth 9 - Tangent finiteness passes to smaller deformation conditions
GaloisRep.tangentFinite_of_imp0 below · cited by 5 · depth 9 - Tangent finiteness for deformations unramified outside S
GaloisRep.tangentFinite_unramifiedOutside4 below · cited by 2 · depth 9 - Kernel field of a Galois representation with open kernel
GaloisRep.exists_intermediateField_isGalois_fixingSubgroup_eq_ker0 below · cited by 1 · depth 10 - Injectivity of reduction for ℓ-power points of finite flat group schemes
GaloisRep.finiteFlat_point_eq_of_decomposition_fixed_of_valuation_sub_lt_one_of_pow_eq_one10 below · cited by 1 · depth 10 - Cyclotomic determinant forces the kernel field to be totally complex
GaloisRep.isTotallyComplex_of_fixingSubgroup_le_ker_of_det_eq_modThreeCyclotomicChar0 below · cited by 1 · depth 10 - Universal deformation ring: flat of type S, unipotent inertia on U
GaloisRep.nonempty_deformationRingData_flatCondition_and_isUnipotentOnInertiaAt77 below · cited by 3 · depth 10 - Representability of the ordinary deformation problem with unipotent inertia at U
GaloisRep.nonempty_deformationRingData_ordinaryCondition_and_isUnipotentOnInertiaAt70 below · cited by 2 · depth 10 - Universal deformation ring for strict ordinary type with unipotent inertia
GaloisRep.nonempty_deformationRingData_strictOrdinaryCondition_and_isUnipotentOnInertiaAt80 below · cited by 2 · depth 10 - Reducibility of small mod-3 representations unramified outside 3
GaloisRep.not_isIrreducible_matrixRepresentation_of_finrank_le_24_of_det_eq_modThreeCyclotomicChar2 below · cited by 1 · depth 10 - Ordinary deformations of a très ramifiée residual representation are strict
GaloisRep.strictOrdinaryCondition_of_ordinaryCondition_of_residual_tresRamifiee159 below · cited by 2 · depth 10 - Finite tangent space from a uniform level
GaloisRep.tangentFinite_of_uniform_level0 below · cited by 1 · depth 10 - Finite flat quotient model covering an equivariant surjection
GaloisRep.exists_finiteFlat_quotient_of_equivariant_surjection_with_restriction0 below · cited by 1 · depth 11 - Galois-stable subgroups of points arise from finite flat Hopf algebras
GaloisRep.exists_finiteFlat_sub_of_equivariant_injection0 below · cited by 18 · depth 11 - Injectivity of reduction from triviality of kernel points
GaloisRep.finiteFlat_point_eq_of_forall_kernel_point_eq_one0 below · cited by 1 · depth 11 - Raynaud's lemma transferred to D_A-fixed ℚ̄-points
GaloisRep.finiteFlat_point_eq_one_of_pow_prime_pow_of_forall_dvr7 below · cited by 1 · depth 11 - Strict ordinary plus unipotent inertia on U is a deformation condition
GaloisRep.isDeformationCondition_strictOrdinaryCondition_and_isUnipotentOnInertiaAt31 below · cited by 1 · depth 11 - Deligne ordinary shape at p=3 for unit Tₚ-eigenvalue
GaloisRep.deligneOrdinaryShape_of_theta_T_ne_zero_of_det_eq_pow_of_eq_three5,175 below · cited by 1 · depth 12 - Inertia eigenvector of level-two tame type at p=3
GaloisRep.exists_inertia_eigenvector_tameCharacter_pow_of_theta_heckeT_eq_zero_of_det_eq_pow_of_katz_of_eq_three2,903 below · cited by 1 · depth 12 - Strict ordinary condition is a deformation condition, p odd
GaloisRep.isDeformationCondition_strictOrdinaryCondition25 below · cited by 1 · depth 12 - ℤ₍ₚ₎ is a discrete valuation ring
GaloisRep.isDiscreteValuationRing_ratLocalizedAt0 below · cited by 142 · depth 12 - ℚ is the fraction field of `ratLocalizedAt p`
GaloisRep.isFractionRing_ratLocalizedAt0 below · cited by 119 · depth 12 - ℤ₍ₚ₎ as the localisation of ℤ at (p)
GaloisRep.isLocalization_ratLocalizedAt0 below · cited by 114 · depth 12 - Generic fibre of a finite flat Hopf algebra over ℤ_{(q)} splits
GaloisRep.bijective_lift_pi_algHom_of_finiteFlatHopf11 below · cited by 5 · depth 13 - Galois representation attached to a mod-p Hecke eigensystem
GaloisRep.exists_galoisFactorsThroughFiniteLevel_trace_eq_theta_heckeT_and_det_eq_pow1,485 below · cited by 1 · depth 13 - Supersingular inertia eigenvector via level-two fundamental characters, weight two
GaloisRep.exists_inertia_eigenvector_tameCharacter_pow_of_theta_heckeT_eq_zero_of_det_eq_pow_of_eq_two2,583 below · cited by 1 · depth 13 - Ordinary eigenline at p=3, weights 2 ≤ k ≤ 4
GaloisRep.exists_stableLine_of_theta_T_ne_zero_of_det_eq_pow_of_eq_three5,173 below · cited by 1 · depth 13 - The prime q is irreducible in ℤ_{(q)}
GaloisRep.irreducible_natCast_ratLocalizedAt2 below · cited by 45 · depth 13 - Multiplicative-type quotient counts 𝔽̄_q-points of a finite flat Hopf algebra
GaloisRep.natCard_quotient_eq_natCard_ringHom_algClosure_of_finiteFlatHopf_of_multiplicativeTypeNat28 below · cited by 1 · depth 13 - Generic point count of a finite flat Hopf algebra over ℤ_{(q)}
GaloisRep.natCard_withConv_algHom_eq_finrank_of_finiteFlatHopf10 below · cited by 17 · depth 13 - Strict ordinariness detected on the quotients A/𝔪^{m+1}
GaloisRep.strictOrdinaryCondition_of_forall_quotient4 below · cited by 1 · depth 13 - Strict ordinarity descends along injective local homomorphisms
GaloisRep.strictOrdinaryCondition_of_injective9 below · cited by 1 · depth 13 - Strict ordinarity descends along jointly injective pairs of projections
GaloisRep.strictOrdinaryCondition_of_jointly_injective9 below · cited by 1 · depth 13 - Characteristic of a ℤ_{(ℓ)}-algebra field is 0 or ℓ
GaloisRep.charZero_or_charP_of_algebra_ratLocalizedAt1 below · cited by 8 · depth 14 - Reduction of Hopf-algebra points at a place over q
GaloisRep.exists_addSubgroup_natCard_quotient_eq_natCard_ringHom_algClosure_of_finiteFlatHopf15 below · cited by 7 · depth 14 - Mod-𝔪 Galois representation of a Hecke maximal ideal
GaloisRep.exists_finiteField_galoisRep_trace_eq_heckeT_mod_of_isMaximal1,457 below · cited by 1 · depth 14 - Finite flat Hopf quotient realising a stable subgroup of points
GaloisRep.exists_finiteFlat_sub_of_equivariant_injection_of_operators_surjective0 below · cited by 4 · depth 14 - Frobenius twist of coefficients preserves the level-two inertia alternative
GaloisRep.exists_inertia_eigenvector_tameCharacter_pow_map_of_forall_eq_pow0 below · cited by 1 · depth 14 - Transfer of an inertia tame-character eigenvector along a conjugation
GaloisRep.exists_inertia_eigenvector_tameCharacter_pow_of_conj_map0 below · cited by 1 · depth 14 - Ordinary eigenline at p in weight 2, p odd
GaloisRep.exists_stableLine_of_theta_T_ne_zero_of_det_eq_pow_of_eq_two2,183 below · cited by 1 · depth 14 - Ordinary line and tame shape at p=3, weights 3≤ k≤ p+1
GaloisRep.exists_stableLine_of_theta_T_ne_zero_of_det_eq_pow_of_three_le_of_eq_three5,142 below · cited by 1 · depth 14 - Points reducing to the identity lie in inertia displacements (q odd)
GaloisRep.finiteFlat_point_mem_of_valuation_sub_counit_lt_one_of_inertia_displacement_mem10 below · cited by 2 · depth 14 - Level-two inertia eigenvector forces no stable line
GaloisRep.forall_stableLine_false_of_inertia_eigenvector_tameCharacter_pow17 below · cited by 1 · depth 14 - Inertia acts on admissible reduction kernels via n
GaloisRep.multiplicativeTypeNat_reductionKernel_inf_of_finiteFlatHopf_of_admissibleChain28 below · cited by 2 · depth 14 - Inertia displacements are congruent to the counit at A
GaloisRep.valuation_sub_counit_lt_one_of_mem_closure_inertia_displacement1 below · cited by 1 · depth 14 - Inertia at p values of a finite-level character lie in 𝔽ₚ^×
GaloisRep.character_pow_sub_one_eq_one_of_mem_inertiaSubgroupIn5 below · cited by 2 · depth 15 - Determinant equals the m-th power of the cyclotomic character
GaloisRep.det_eq_cycloChar_pow_of_det_frobenius_eq_pow26 below · cited by 4 · depth 15 - Determinant a^m on inertia at p from Frobenius determinants ℓ^m
GaloisRep.det_eq_pow_of_forall_rootsOfUnity_of_det_frobenius_eq_pow27 below · cited by 3 · depth 15 - Deligne–Serre: conjugacy from equal Frobenius characteristic polynomials
GaloisRep.exists_conj_eq_of_charpoly_frobenius_eq_of_galoisFactorsThroughFiniteLevel24 below · cited by 1 · depth 15 - Deligne's ordinary eigenline at p in weight two
GaloisRep.exists_conj_map_stableLine_of_theta_T_ne_zero_of_absolutelyIrreducible_of_eq_two2,172 below · cited by 1 · depth 15 - Mod 𝔪 Galois representation for weight-two Hecke algebras
GaloisRep.exists_finiteField_galoisRep_trace_eq_heckeT_mod_of_isMaximal_two1,316 below · cited by 2 · depth 15 - Descent of a finite flat Hopf algebra to an unramified DVR
GaloisRep.exists_finiteFlat_inertia_displacement_quotient_of_finiteFlatHopf7 below · cited by 1 · depth 15 - Residual Galois representation of a weight k≥ 3 eigenform
GaloisRep.exists_galoisRep_trace_eq_eigenchar_and_det_eq_pow_of_three_le1,389 below · cited by 1 · depth 15 - Unit-Kummer ordinary Galois modules from finite flat ℤ₍ₚ₎-Hopf algebras
GaloisRep.exists_hopfAlgebra_withConv_equiv_of_ordinary_of_unitKummer_decomposition69 below · cited by 1 · depth 15 - Descent of an ordinary stable-line package along conjugation
GaloisRep.exists_stableLine_of_conj_map5 below · cited by 2 · depth 15 - No stable line after base change when det is an odd power on inertia
GaloisRep.forall_stableLine_false_of_irreducible_of_det_inertia_pow_odd8 below · cited by 1 · depth 15 - Labelling q-power points that reduce to the identity
GaloisRep.label_mem_of_forall_decomposition_smul_sub_mem_of_finiteFlatHopf21 below · cited by 1 · depth 15 - Reduction kernel is of multiplicative type at q=2
GaloisRep.multiplicativeTypeNat_reductionKernel_inf_of_finiteFlatHopf_of_admissibleChain_two40 below · cited by 3 · depth 15 - Chebotarev density for Gal(ℚ̄/ℚ), lower Dirichlet form
GaloisRep.sub_mul_log_le_tsum_rpow_neg_of_frobenius_mem_of_surjective18 below · cited by 2 · depth 15 - Ordinary line at p when p ∥ M and θ(Uₚ) ≠ 0
GaloisRep.thetaCycle_exists_stableLine_of_theta_U_ne_zero_of_dvd_of_not_sq_dvd4,944 below · cited by 1 · depth 15 - Weil restriction of a finite flat group scheme along an unramified Galois set
GaloisRep.exists_finiteFlat_pi_of_forall_smul_eq_of_not_dvd_discr6 below · cited by 3 · depth 16 - Finite flat descent of the inertia-displacement quotient
GaloisRep.exists_finset_forall_dvr_finiteFlat_inertia_displacement_quotient_of_finiteFlatHopf4 below · cited by 1 · depth 16 - Residual Galois representation attached to an H¹ Hecke eigensystem
GaloisRep.exists_galoisRep_trace_eq_of_isEigensystemH1_binaryFormRepSL_of_ringHom1,370 below · cited by 1 · depth 16 - Galois representation attached to an eigensystem in Hom(Γ₀(N),κ)
GaloisRep.exists_galoisRep_trace_eq_of_isEigensystemH1_one_of_ringHom1,349 below · cited by 3 · depth 16 - Descent of a finite-level GL₂ Galois representation to a finite field
GaloisRep.exists_isSemisimpleRepresentation_charpoly_map_eq_of_trace_det_frobenius_mem_range29 below · cited by 1 · depth 16 - Membership in ℤ₍ₚ₎ via denominators
GaloisRep.mem_ratLocalizedAt_iff0 below · cited by 8 · depth 16 - Frobenius traces and determinants determine characteristic polynomials
GaloisRep.charpoly_eq_map_charpoly_of_frobenius_trace_eq_of_det_eq22 below · cited by 1 · depth 17 - Galois-equivariant Hopf orders give finite flat models
GaloisRep.exists_finiteFlat_of_subalgebra_pi_algebraicClosure3 below · cited by 2 · depth 17 - Reducible mod p representation with prescribed Frobenius traces
GaloisRep.exists_galoisRep_trace_eq_add_mul_of_unitsHom2 below · cited by 1 · depth 17 - Mod p Galois representation from a weight-two Hecke character
GaloisRep.exists_galoisRep_trace_eq_of_ringHom_heckeAlgebra_two1,317 below · cited by 1 · depth 17 - Points of the Cartier dual of a multiplicative-type Hopf algebra
GaloisRep.cartierDual_points_of_galoisCyclotomic0 below · cited by 2 · depth 18 - Cyclotomic finite flat Hopf algebras over ℤ_{(q)} are monoid algebras
GaloisRep.exists_bialgEquiv_monoidAlgebra_of_finiteFlatHopf_of_galoisCyclotomic11 below · cited by 1 · depth 18 - Galois-trivial finite flat Hopf algebras over ℤ_{(q)} are constant
GaloisRep.exists_algEquiv_pi_of_finiteFlatHopf_of_galoisTrivial7 below · cited by 1 · depth 19 - Schematic closure of a stable subgroup as Hopf quotient
GaloisRep.exists_bialgHom_surjective_finiteFlat_model_addSubgroup_of_stable15 below · cited by 1 · depth 19 - Galois-trivial points of a module-finite Hopf algebra are ℤ_{(q)}-valued
GaloisRep.apply_mem_range_algebraMap_of_galoisTrivial2 below · cited by 1 · depth 20 - Finite flat sub-models with a family of operators
GaloisRep.exists_finiteFlat_sub_of_equivariant_injection_of_operators0 below · cited by 1 · depth 20 - ℤ₍ₚ₎ = ℚ ∩ ℤₚ via p-adic norm
GaloisRep.mem_ratLocalizedAt_iff_padic_norm_le_one1 below · cited by 1 · depth 21 - Going down along O → κ ⊗_ℤ₍ₚ₎ O at primes containing p
GaloisRep.exists_ideal_le_comap_includeRight_eq_of_natCast_mem1 below · cited by 1 · depth 28
GaloisRep.DeformationRingData 24
- landmark Existence of a surjection R ↠ T
GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum6 below · cited by 5 · depth 7 - Uniqueness of classifying maps out of a deformation ring
GaloisRep.DeformationRingData.algHom_eq_of_isEquiv0 below · cited by 6 · depth 10 - Relaxation map kills the inertia character at q
GaloisRep.DeformationRingData.algHom_inertiaCharacter_eq_one_of_forall_isUnramifiedAt2 below · cited by 4 · depth 10 - Functoriality of deformation ring data under implication of conditions
GaloisRep.DeformationRingData.exists_algHom_of_forall_imp0 below · cited by 3 · depth 10 - Patching datum from a ladder of deformation conditions
GaloisRep.DeformationRingData.exists_patchingDatum_of_ladder43 below · cited by 3 · depth 10 - Kernel of R_Q→ R_{min} generated by diamonds minus one (flat case)
GaloisRep.DeformationRingData.ker_algHom_eq_span_of_relaxed_flat9 below · cited by 3 · depth 10 - Kernel of R_Q→ R_{min} is the augmentation ideal
GaloisRep.DeformationRingData.ker_algHom_eq_span_of_relaxed_strictOrdinary9 below · cited by 2 · depth 10 - Cotangent length is unchanged under an isomorphism of deformation rings
GaloisRep.DeformationRingData.length_cotangent_eq_of_forall_iff0 below · cited by 3 · depth 10 - Flat cotangent bound for level raising at an auxiliary prime
GaloisRep.DeformationRingData.length_cotangent_le_add_of_flatCondition_insert_isUnipotentOnInertiaAt13 below · cited by 3 · depth 10 - Cotangent growth on relaxing unipotent inertia at q, flat case
GaloisRep.DeformationRingData.length_cotangent_le_add_of_flatCondition_isUnipotentOnInertiaAt_erase16 below · cited by 3 · depth 10 - Cotangent bound ≤ length of 𝒪/(q²-1) when unipotency at q is relaxed
GaloisRep.DeformationRingData.length_cotangent_le_add_of_isUnipotentOnInertiaAt_point18 below · cited by 2 · depth 10 - Cotangent bound on adding an unramified prime q
GaloisRep.DeformationRingData.length_cotangent_le_add_of_isUnramifiedAt_point12 below · cited by 2 · depth 10 - Surjectivity of a comparison map between universal deformation rings
GaloisRep.DeformationRingData.surjective_of_isEquiv_baseChangeAlong_of_isOfType_quotient10 below · cited by 3 · depth 10 - Tangent space bound on generators of the deformation ring
GaloisRep.DeformationRingData.exists_generators_maximalIdeal_card_le_finrank_span_dualNumberClasses6 below · cited by 1 · depth 11 - Cotangent length bound: ordinary versus flat at p
GaloisRep.DeformationRingData.length_cotangent_le_add_of_ordinaryCondition_of_flatCondition112 below · cited by 1 · depth 11 - Cotangent length bound along a surjection of deformation rings
GaloisRep.DeformationRingData.length_cotangent_le_of_level_bounds0 below · cited by 5 · depth 11 - Level-wise cotangent bound by the length of 𝒪/(q²-1)
GaloisRep.DeformationRingData.length_level_quotient_le_of_isUnipotentOnInertiaAt8 below · cited by 2 · depth 11 - Level-wise relative cotangent bound at an auxiliary prime q
GaloisRep.DeformationRingData.length_level_quotient_le_of_isUnramifiedAt4 below · cited by 2 · depth 11 - Factoring a point of the laxer deformation ring through θ
GaloisRep.DeformationRingData.exists_algHom_comp_eq_of_isOfType0 below · cited by 3 · depth 12 - Cotangent functionals killing inertia traces vanish on relaxation kernel
GaloisRep.DeformationRingData.forall_apply_eq_zero_of_forall_toCotangent_trace3 below · cited by 1 · depth 12 - Per-level cotangent bound by ℓ(𝒪/(α²-1)) at the ordinary line
GaloisRep.DeformationRingData.length_level_quotient_le_of_ordinaryLine107 below · cited by 1 · depth 12 - A local invariant killed by α²-1 on ordinary lines
GaloisRep.DeformationRingData.exists_localInvariant_of_ordinaryLine104 below · cited by 1 · depth 13 - Cotangent functional vanishing on the relaxation kernel
GaloisRep.DeformationRingData.comp_subtype_ker_mapCotangent_eq_zero_of_isOfType_lift1 below · cited by 1 · depth 14 - Universal deformation ring topologically generated by Frobenius traces
GaloisRep.DeformationRingData.exists_mem_adjoin_trace_frobenius_sub_mem_maximalIdeal_pow33 below · cited by 2 · depth 14
GaloisRep.ratLocalizedAt 4
- Units of ℤ₍ₚ₎: numerator not divisible by p
GaloisRep.ratLocalizedAt.isUnit_iff0 below · cited by 7 · depth 9 - ℤ₍ₚ₎ is a local ring
GaloisRep.ratLocalizedAt.isLocalRing0 below · cited by 40 · depth 14 - Maximal ideal of ℤ_{(ℓ)} is generated by ℓ
GaloisRep.ratLocalizedAt.maximalIdeal_eq_span_natCast1 below · cited by 59 · depth 14 - Residue field of Specℤ at (ℓ) as quotient of ℤ_{(ℓ)}
GaloisRep.ratLocalizedAt.exists_specMap_comp_eq_fromSpecResidueField1 below · cited by 1 · depth 17