← all areas

Namespace IsRegularLocalRing 39 theorems

• A regular local ring is a domain IsRegularLocalRing.isDomain 0 below · cited by 81 · depth 14
• Regular local rings are Cohen–Macaulay IsRegularLocalRing.depth_self_eq_ringKrullDim 0 below · cited by 5 · depth 16
• Regularity of k ⊗_{k_0} R at every prime IsRegularLocalRing.localization_atPrime_tensor_of_isAlgClosed 8 below · cited by 3 · depth 16
• Regularity of R/(x) for x ∈ 𝔪 ∖ 𝔪² IsRegularLocalRing.quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem 0 below · cited by 10 · depth 16
• Embedding dimensions in a surjection onto a regular local ring IsRegularLocalRing.spanFinrank_ker_add_finrank_cotangentSpace 1 below · cited by 1 · depth 16
• Normal Noetherian local domain of dimension one is regular IsRegularLocalRing.of_isIntegrallyClosed_of_ringKrullDim_eq_one 1 below · cited by 1 · depth 17
• Height-one primes are principal in regular local rings of dimension ≤ 2 IsRegularLocalRing.isPrincipal_of_isPrime_of_height_eq_one_of_ringKrullDim_le_two 5 below · cited by 6 · depth 18
• Minimal number of generators of the kernel of a surjection of regular local rings IsRegularLocalRing.spanFinrank_ker_add_ringKrullDim_eq 1 below · cited by 2 · depth 18
• Regular local rings of dimension ≤ 2 are factorial IsRegularLocalRing.uniqueFactorizationMonoid_of_ringKrullDim_le_two 4 below · cited by 27 · depth 19
• Regularity criterion for a two-dimensional local ring IsRegularLocalRing.of_maximalIdeal_eq_span_of_mem_sq_of_ringKrullDim_eq_two 0 below · cited by 1 · depth 22
• Regular local rings of dimension at most one are integrally closed domains IsRegularLocalRing.isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one 0 below · cited by 7 · depth 27
• Descent of regularity to the fibre ring S/(varpi) IsRegularLocalRing.quotient_span_algebraMap_of_flat_of_isLocalHom_of_ringKrullDim_le_one 1 below · cited by 1 · depth 27
• Transversal primes in a regular local ring of dimension ≤ 2 IsRegularLocalRing.exists_span_singleton_eq_and_span_singleton_eq_and_mul_eq_of_sup_eq_maximalIdeal_of_inf_eq_span_singleton 2 below · cited by 1 · depth 28
• Regularity of R/(ivarpi) for a retraction onto a DVR IsRegularLocalRing.quotient_span_singleton_map_of_leftInverse_of_irreducible 2 below · cited by 1 · depth 28
• 𝒪[[X₁,…,Xₙ]] over a discrete valuation ring is regular local IsRegularLocalRing.mvPowerSeries_fin 0 below · cited by 10 · depth 30
• Abhyankar's lemma at a tame point: completion of S_y IsRegularLocalRing.exists_ringEquiv_adicCompletion_of_isInvariant_of_isLocalization_atPrime_of_isUnramifiedAt_off 56 below · cited by 1 · depth 31
• Flat unramified ascent of regularity and of the parameters (varpi,s) IsRegularLocalRing.of_isUnramifiedAt_of_flat_of_maximalIdeal_eq_span_pair 2 below · cited by 1 · depth 31
• Regular one-dimensional fibre modulo varpi_S from the completion IsRegularLocalRing.quotient_span_of_ringEquiv_adicCompletion_of_maximalIdeal_eq_span_pair 1 below · cited by 1 · depth 31
• Abhyankar's lemma on completions at a regular surface point IsRegularLocalRing.exists_ringEquiv_adicCompletion_of_isInvariant_of_card_inertia_eq_of_isUnramifiedAt_off 55 below · cited by 1 · depth 32
• Drinfeld chart shape for a regular two-dimensional complete local ring IsRegularLocalRing.exists_ringEquiv_mvPowerSeries_quotient_drinfeldForm_of_eq_mul 8 below · cited by 3 · depth 32
• Completion of a two-dimensional regular local ring IsRegularLocalRing.isDomain_and_isIntegrallyClosed_adicCompletion_of_ringKrullDim_eq_two 10 below · cited by 4 · depth 32
• Regularity lifts along a non-zero-divisor in the maximal ideal IsRegularLocalRing.of_isRegularLocalRing_quotient_span_singleton_of_mem_nonZeroDivisors 0 below · cited by 4 · depth 32
• Adjoining an n-th root of a regular parameter preserves regularity IsRegularLocalRing.adjoinRoot_X_pow_sub_C_of_notMem_sq 2 below · cited by 3 · depth 33
• Abhyankar's lemma at a regular point of the branch divisor IsRegularLocalRing.exists_algEquiv_adjoinRoot_X_pow_sub_C_mul_of_isCyclic_of_isUnramifiedAt_of_residue 27 below · cited by 1 · depth 33
• Complete regular local W₀-algebras of dimension 2 as W₀[[X₀,X₁]]/(π-h) IsRegularLocalRing.exists_algEquiv_mvPowerSeries_quotient_span_C_sub_of_maximalIdeal_eq_span_pair 7 below · cited by 1 · depth 33
• Finite étale local extensions of complete regular two-dimensional local rings IsRegularLocalRing.of_etale_of_isLocalRing_of_maximalIdeal_eq_span_pair 1 below · cited by 3 · depth 33
• Regularity of S[X]/(g) for an Eisenstein polynomial g IsRegularLocalRing.adjoinRoot_of_monic_of_coeff_mem_maximalIdeal_of_coeff_zero_not_mem_sq 0 below · cited by 8 · depth 34
• Descent of a Kummer presentation along étale base change IsRegularLocalRing.exists_algEquiv_adjoinRoot_X_pow_sub_C_mul_of_baseChange_of_isIntegrallyClosed 15 below · cited by 1 · depth 34
• Abhyankar's lemma: cyclic covers unramified off s are Kummer IsRegularLocalRing.exists_algEquiv_adjoinRoot_X_pow_sub_C_mul_of_isCyclic_of_isUnramifiedAt_of_residue_of_isPrimitiveRoot 10 below · cited by 1 · depth 34
• Étale base change of tame cyclic cover data IsRegularLocalRing.exists_algEquiv_tensorProduct_isGalois_isCyclic_of_etale_of_isUnramifiedAt_of_forall_sub_mem 9 below · cited by 1 · depth 34
• Étale extension containing a primitive e-th root of unity IsRegularLocalRing.exists_etale_isLocalRing_isPrimitiveRoot_of_isUnit 6 below · cited by 1 · depth 34
• Kummer extensions: B ≅ R[T]/(T^e-t) for regular R IsRegularLocalRing.exists_algEquiv_adjoinRoot_X_pow_sub_C_apply_root_eq_of_isIntegrallyClosed_of_finrank_eq 6 below · cited by 2 · depth 35
• Descent of an e-th root along finite étale base change IsRegularLocalRing.exists_isUnit_pow_eq_mul_of_baseChange 13 below · cited by 1 · depth 35
• Regularity descends along a finite étale local extension IsRegularLocalRing.of_etale_of_moduleFinite 0 below · cited by 1 · depth 36
• Complete regular local ring of dimension ≤ 2 maps to a complete DVR IsRegularLocalRing.exists_isDiscreteValuationRing_ringHom_comp_eq_of_ringKrullDim_le_two_of_isAdicComplete_of_natCast_ne_zero 28 below · cited by 1 · depth 37
• Regular parameter with residually characteristic-zero quotient IsRegularLocalRing.exists_notMem_sq_charZero_quotient_span_singleton 13 below · cited by 1 · depth 38
• Regular local rings of Krull dimension ≤ 2 are regular IsRegularLocalRing.isRegularRing_of_ringKrullDim_le_two 6 below · cited by 2 · depth 38
• Quotient of a complete regular local domain by a regular parameter IsRegularLocalRing.quotient_span_singleton_isAdicComplete_of_notMem_sq 14 below · cited by 1 · depth 38
• Localisation at a regular parameter is a DVR IsRegularLocalRing.isPrime_span_singleton_and_isDiscreteValuationRing_localization_of_notMem_sq 13 below · cited by 1 · depth 39