← all areas

Namespace IsDiscreteValuationRing 78 theorems

• Finite extension whose residue field splits quadratics IsDiscreteValuationRing.exists_finite_extension_residueField_splits_quadratic 2 below · cited by 2 · depth 10
• A DVR with fraction field ℚ and uniformiser p maps to ℤₚ IsDiscreteValuationRing.exists_ringHom_padicInt_of_isFractionRing_rat 0 below · cited by 1 · depth 13
• Length of a-torsion in 𝒪/𝔪ⁿ⁺¹ bounded by ℓ(𝒪/(a)) IsDiscreteValuationRing.length_ker_lsmul_quotient_maximalIdeal_pow_le 0 below · cited by 1 · depth 13
• Valuation shift in a DVR: av∈𝔪^M, anotin𝔪^{k+1} give v∈𝔪^{M-k} IsDiscreteValuationRing.mem_maximalIdeal_pow_sub_of_mul_mem_of_not_mem 0 below · cited by 1 · depth 14
• Hilbert's different formula for a faithful finite action on a DVR IsDiscreteValuationRing.differentEqPowFiltrationSum_fixedPoints_subring 2 below · cited by 1 · depth 15
• Herbrand's theorem in weighted-sum form IsDiscreteValuationRing.finsum_card_lowerRamificationGroup_mul_apply_map_mk_eq_of_apply_bot_eq_zero 11 below · cited by 1 · depth 15
• Image of a DVR with fraction field ℚ and uniformiser p IsDiscreteValuationRing.algebraMap_rat_range_eq_ratLocalizedAt_of_irreducible 0 below · cited by 1 · depth 16
• Monogenicity of a finite extension of discrete valuation rings IsDiscreteValuationRing.exists_adjoin_singleton_eq_top_of_isSeparable_residueField 0 below · cited by 5 · depth 16
• Reduced finite free 𝒪-algebras embed into products of complete DVRs IsDiscreteValuationRing.exists_algHom_pi_of_module_finite_free 2 below · cited by 1 · depth 16
• Hasse–Arf integrality for degree-one characters IsDiscreteValuationRing.exists_finsum_lowerRamificationGroup_indicator_eq_natCast 20 below · cited by 1 · depth 16
• Surjectivity of n-th powers U^{(k)}→ U^{(k+e)} in a complete DVR IsDiscreteValuationRing.exists_mem_principalUnits_pow_eq 0 below · cited by 4 · depth 16
• Powers of a non-unit clear denominators over a discrete valuation ring IsDiscreteValuationRing.exists_pow_mul_mem_range 0 below · cited by 3 · depth 16
• Swan sum of a character is invariant under inflation IsDiscreteValuationRing.finsum_lowerRamificationGroup_indicator_comp_mk_eq 11 below · cited by 2 · depth 16
• Herbrand's theorem in the lower numbering IsDiscreteValuationRing.map_lowerRamificationGroup_mk_eq_of_isSeparable_residueField 7 below · cited by 6 · depth 16
• Equality case of sum eᵢ fᵢ = [F:E] over a discrete valuation ring IsDiscreteValuationRing.primesOver_integralClosure_eq_range_of_finrank_le_sum_inertiaDeg 0 below · cited by 7 · depth 16
• Herbrand's theorem in the upper numbering for a DVR IsDiscreteValuationRing.upperRamificationQuotientCompat_of_isSeparable_residueField 10 below · cited by 4 · depth 16
• Valuation on a DVR restricted to its fixed subring IsDiscreteValuationRing.addVal_coe_eq_lowerRamificationCard_zero_mul_addVal_fixedPoints 1 below · cited by 7 · depth 17
• Characteristic polynomial of × u on R/xR splits into single-slope factors IsDiscreteValuationRing.charpoly_mulLeft_quotient_eq_finprod_single_slope 1 below · cited by 1 · depth 17
• Graded norm cokernel bound via upper ramification groups IsDiscreteValuationRing.exists_finset_card_mul_card_upperRamificationGroup_le_forall_exists_sub_mul_finprod_smul_mem_pow 28 below · cited by 1 · depth 17
• Hasse–Arf condition for cyclic lower ramification chains IsDiscreteValuationRing.hasseArfChain_lowerRamificationGroup_of_isCyclic 6 below · cited by 2 · depth 17
• Dedekind's criterion over a DVR: O[α] integrally closed IsDiscreteValuationRing.isIntegrallyClosedIn_adjoin_singleton_of_squarefree 1 below · cited by 2 · depth 17
• Reduced special fibre of O[α] from squarefree reduced minimal polynomial IsDiscreteValuationRing.isReduced_adjoin_singleton_quotient_of_squarefree 0 below · cited by 1 · depth 17
• Lengths multiply along an injective map from a DVR IsDiscreteValuationRing.length_quotient_map_span_eq_length_mul_length 0 below · cited by 4 · depth 17
• Herbrand's theorem in the lower numbering for monogenic DVRs IsDiscreteValuationRing.map_lowerRamificationGroup_mk_eq_of_adjoin_singleton_eq_top 2 below · cited by 1 · depth 17
• Relative index of principal unit subgroups in a DVR IsDiscreteValuationRing.relIndex_principalUnits_add 2 below · cited by 2 · depth 17
• Characteristic polynomial of multiplication has a single slope IsDiscreteValuationRing.charpoly_mulLeft_single_slope_of_isAdicComplete 0 below · cited by 1 · depth 18
• Graded norm cokernels in a ramified layer of prime degree IsDiscreteValuationRing.exists_finset_card_le_forall_exists_sub_mul_finprod_smul_mem_pow_of_prime_card 8 below · cited by 1 · depth 18
• Tame inertia quotient embeds in residue field units IsDiscreteValuationRing.exists_monoidHom_lowerRamificationGroup_zero_residueField_units 0 below · cited by 2 · depth 18
• Norms are surjective on graded unit pieces when G₀=1 IsDiscreteValuationRing.exists_sub_finprod_smul_mem_pow_succ_of_lowerRamificationGroup_zero_eq_bot 3 below · cited by 1 · depth 18
• Norms of higher units via the Herbrand function, prime degree IsDiscreteValuationRing.finprod_smul_sub_one_mem_maximalIdeal_pow_of_sub_one_mem_pow_herbrand_of_prime_card 6 below · cited by 1 · depth 18
• Hasse–Arf condition for abelian lower ramification chains IsDiscreteValuationRing.hasseArfChain_lowerRamificationGroup_of_isMulCommutative 19 below · cited by 1 · depth 18
• Hasse–Arf condition from Sen's congruences, cyclic inertia IsDiscreteValuationRing.hasseArfChain_of_isCyclic_of_dvd_of_modEq 0 below · cited by 1 · depth 18
• Ramification function of a quotient: i_{G/H}(τ̄) via sum_{h∈ H} i_G(τ h) IsDiscreteValuationRing.iInf_addVal_smul_sub_eq_sum_ramificationDepth_of_adjoin_singleton_eq_top 0 below · cited by 1 · depth 18
• Herbrand's theorem for lower ramification groups IsDiscreteValuationRing.map_lowerRamificationGroup_mk_eq_of_iInf_addVal_smul_sub_eq_sum_ramificationDepth 0 below · cited by 1 · depth 18
• Normal Noetherian local domain of dimension one is a DVR IsDiscreteValuationRing.of_isIntegrallyClosed_of_ringKrullDim_eq_one 0 below · cited by 1 · depth 18
• Sen's congruence for ramification depths of p-power iterates IsDiscreteValuationRing.ramificationDepth_pow_prime_pow_modEq_of_mem_lowerRamificationGroup_one 0 below · cited by 1 · depth 18
• Lower jumps are divisible by [G₀:G₁] when G₀ is abelian IsDiscreteValuationRing.relIndex_dvd_of_lowerRamificationGroup_ne_succ_of_commute 1 below · cited by 1 · depth 18
• Index of consecutive principal unit groups in a DVR IsDiscreteValuationRing.relIndex_principalUnits_succ 1 below · cited by 1 · depth 18
• Uniqueness of the residual value of an element IsDiscreteValuationRing.eq_of_monic_aeval_eq_zero_map_residue_eq_pow 0 below · cited by 4 · depth 19
• Residual vanishing of roots of X²-aX+varpi IsDiscreteValuationRing.exists_monic_aeval_eq_zero_map_residue_eq_X_pow_of_sq_sub_mul_add_eq_zero 0 below · cited by 1 · depth 19
• Norm surjectivity above the ramification jump IsDiscreteValuationRing.exists_sub_one_mem_and_finprod_smul_sub_mem_of_jump_lt_of_prime_card 7 below · cited by 1 · depth 19
• Trace estimate in a one-jump ramification filtration IsDiscreteValuationRing.finsum_smul_mem_maximalIdeal_pow_of_lowerRamificationGroup_eq_top_of_eq_bot 4 below · cited by 3 · depth 19
• Hasse–Arf for abelian G from its cyclic quotients IsDiscreteValuationRing.hasseArfChain_lowerRamificationGroup_of_forall_isCyclic_quotient 10 below · cited by 1 · depth 19
• Cardinality of R/𝔪ⁿ for a discrete valuation ring IsDiscreteValuationRing.natCard_quotient_maximalIdeal_pow 0 below · cited by 5 · depth 19
• Trace surjectivity for a single lower ramification jump IsDiscreteValuationRing.exists_finsum_smul_eq_of_mem_maximalIdeal_pow_of_lowerRamificationGroup_eq_top_of_eq_bot 4 below · cited by 1 · depth 20
• Local unit index [R^×:(R^×)ⁿ]=#μₙ(R)·#(R/nR) IsDiscreteValuationRing.index_range_powMonoidHom_units_eq 8 below · cited by 1 · depth 21
• No n-torsion in higher principal units when v(n)<k IsDiscreteValuationRing.eq_one_of_pow_eq_one_of_mem_principalUnits 0 below · cited by 2 · depth 22
• p-th powers of principal units: (U^{(k)})ᵖ = U^{(k+e)} for k>e IsDiscreteValuationRing.map_powMonoidHom_principalUnits 2 below · cited by 1 · depth 22
• A discrete valuation ring is maximal among subrings of its fraction field IsDiscreteValuationRing.subalgebra_eq_bot_or_eq_top 0 below · cited by 1 · depth 22
• Adic completion of a DVR is a complete DVR IsDiscreteValuationRing.adicCompletion_isDomain_isDiscreteValuationRing_isAdicComplete 0 below · cited by 59 · depth 24
• Unramified extension of a complete DVR with prescribed residue field IsDiscreteValuationRing.exists_etale_dvr_residueField_equiv_card_algEquiv_eq_of_isAdicComplete 3 below · cited by 4 · depth 25
• Faithfully flat complete DVR extension with p a uniformiser IsDiscreteValuationRing.exists_faithfullyFlat_isAdicComplete_irreducible 1 below · cited by 1 · depth 25
• Unramified base change making Galois act abelian-by-p IsDiscreteValuationRing.exists_finite_etale_isGalois_isPGroup_commutator_le_of_etale 10 below · cited by 1 · depth 25
• A discrete valuation ring is a maximal subring of its fraction field IsDiscreteValuationRing.exists_algebraMap_eq_of_mem_subring_of_ne_top 0 below · cited by 1 · depth 26
• Unramified extension of a complete DVR with prescribed residue extension IsDiscreteValuationRing.exists_finite_etale_isAdicComplete_residueField_algHom 2 below · cited by 1 · depth 26
• Finite étale complete DVR extension carrying a Teichmüller character IsDiscreteValuationRing.exists_finite_etale_isAdicComplete_units_monoidHom_residue_eq 2 below · cited by 1 · depth 26
• A module-finite overring in κ with locally principal maximal ideals IsDiscreteValuationRing.exists_finite_locallyPrincipalOverring 0 below · cited by 5 · depth 26
• 1-ζ generates the maximal ideal of a DVR in ℚ(ζₚ) IsDiscreteValuationRing.maximalIdeal_eq_span_one_sub_of_isPrimitiveRoot 0 below · cited by 2 · depth 26
• Finite residue field of a DVR inside a number field IsDiscreteValuationRing.finite_quotient_maximalIdeal_of_isFractionRing 0 below · cited by 2 · depth 27
• A discrete valuation subring of A with fraction field K' IsDiscreteValuationRing.exists_isDiscreteValuationRing_ringHom_valuationSubring_of_finiteDimensional 0 below · cited by 1 · depth 28
• Existence of a residually trivial complete DVR extension IsDiscreteValuationRing.exists_isAdicComplete_map_maximalIdeal_eq_forall_sub_mem_maximalIdeal 1 below · cited by 3 · depth 29
• Adic completeness for a principal maximal ideal gives a DVR IsDiscreteValuationRing.of_isAdicComplete_span_singleton_of_isMaximal 0 below · cited by 2 · depth 29
• Uniqueness of a valuation ring over a DVR when residue degree exhausts the degree IsDiscreteValuationRing.valuationSubring_eq_of_finrank_le_finrank_residueField 2 below · cited by 1 · depth 29
• Tame rescaling of n-th roots in a discrete valuation ring IsDiscreteValuationRing.exists_mem_maximalIdeal_map_eq_mul_mul_one_add_of_pow_eq_of_pow_eq_mul 0 below · cited by 2 · depth 30
• Total ramification criterion over a discrete valuation ring IsDiscreteValuationRing.exists_primesOver_integralClosure_eq_singleton_of_forall_dvd_ramificationIdx 0 below · cited by 1 · depth 30
• Complete DVR with uniformiser and residues from A is widehatA IsDiscreteValuationRing.exists_ringEquiv_adicCompletion_apply_eq_algebraMap_of_maximalIdeal_eq_span_map_of_forall_exists_sub_mem 0 below · cited by 4 · depth 30
• Unique valuation ring over a totally ramified prime, and varpi = vπⁿ IsDiscreteValuationRing.forall_valuationSubring_eq_and_forall_exists_sub_mem_nonunits_of_primesOver_integralClosure_eq_singleton 1 below · cited by 2 · depth 30
• Unramified complete DVR extension as A₀[X]/(P) modulo all 𝔪ⁿ IsDiscreteValuationRing.exists_monic_aeval_eq_zero_forall_mem_pow_iff_of_maximalIdeal_eq_map_of_isSeparable 0 below · cited by 1 · depth 31
• Transport of complete coefficient DVRs reading the same constants IsDiscreteValuationRing.exists_ringEquiv_forall_apply_eq_comp_of_forall_exists_sub_mem_maximalIdeal 0 below · cited by 2 · depth 31
• Torsion length plus rank inequality for a dilated lattice IsDiscreteValuationRing.length_torsion_quotient_add_finrank_le_of_sq_smul_le_prod 0 below · cited by 1 · depth 31
• Cyclotomic action of an inertial automorphism of a DVR IsDiscreteValuationRing.ringEquiv_apply_eq_pow_of_isPrimitiveRoot_of_pow_sq_sub_one_eq_of_apply_eq_mul 0 below · cited by 2 · depth 31
• Faithfully flat DVR extension along a finite extension of fraction fields IsDiscreteValuationRing.exists_isDiscreteValuationRing_isFractionRing_faithfullyFlat_of_finiteDimensional 3 below · cited by 1 · depth 32
• Flat birational local extension of a DVR is an equality IsDiscreteValuationRing.bijective_algebraMap_of_flat_of_isLocalHom_of_isFractionRing 0 below · cited by 1 · depth 33
• Cyclotomic extension of a complete unramified DVR IsDiscreteValuationRing.exists_cyclotomic_dvr_of_maximalIdeal_eq_span_prime 0 below · cited by 1 · depth 33
• DVR extension containing an n-th root of π IsDiscreteValuationRing.exists_dvr_extension_pow_eq 0 below · cited by 1 · depth 34
• Uniqueness of local maps from an unramified coefficient ring IsDiscreteValuationRing.ringHom_eq_of_residue_comp_eq_of_maximalIdeal_eq_span_natCast 0 below · cited by 1 · depth 34
• Finite extensions of a complete DVR's fraction field come from a DVR IsDiscreteValuationRing.exists_isFractionRing_surjective_comp_of_finiteDimensional_of_isAdicComplete 3 below · cited by 1 · depth 35
• Unramified extension of a DVR with prescribed residue field IsDiscreteValuationRing.exists_finite_etale_dvr_map_maximalIdeal_eq_residueField_algEquiv 0 below · cited by 1 · depth 36