← all areas

Namespace IsLocalRing 181 theorems

— 178 · HasseForm 1 · IsCohenMacaulayOfDim 1 · ResidueField 1

directly in IsLocalRing 178

• Adic completeness passes to quotients of a complete local ring IsLocalRing.isAdicComplete_map_maximalIdeal_quotient 0 below · cited by 5 · depth 9
• Adic completeness of a module-finite local algebra IsLocalRing.isAdicComplete_of_module_finite 0 below · cited by 20 · depth 9
• A/𝔪^{m+1} is Artinian for Noetherian local A IsLocalRing.isArtinianRing_quotient_maximalIdeal_pow 0 below · cited by 4 · depth 9
• Complete noetherian local algebras are pro-Artinian for the adic topology IsLocalRing.isLocalProartinianAlgebra_adicTopology 0 below · cited by 1 · depth 9
• A domain module-finite over a complete local ring is local IsLocalRing.of_isDomain_of_moduleFinite_of_isAdicComplete 0 below · cited by 6 · depth 9
• A proper quotient of a local ring is local IsLocalRing.quotient_of_ne_top 0 below · cited by 4 · depth 9
• Points of a reduced finite local algebra into complete DVRs IsLocalRing.exists_fin_points_dvr_iInf_ker_eq_bot 1 below · cited by 17 · depth 10
• A minimal finite thickening detecting a family in 𝔪 IsLocalRing.exists_ideal_finite_quotient_forall_mem_span_singleton_of_mem_maximalIdeal 0 below · cited by 1 · depth 11
• Power-series presentation from generators of the relative cotangent space IsLocalRing.exists_mvPowerSeries_algHom_apply_X_eq_and_surjective_of_span 3 below · cited by 6 · depth 11
• Module-finite domains over complete local rings are local IsLocalRing.of_isDomain_of_module_finite_of_isAdicComplete 0 below · cited by 4 · depth 11
• Generators of mathfrak m_R counting 𝒪-algebra maps to k[ε] IsLocalRing.exists_generators_maximalIdeal_natCard_algHom_dualNumber_eq_pow 0 below · cited by 1 · depth 12
• Surjectivity of 𝒪 → A/J from relative cotangent generation IsLocalRing.mk_comp_algebraMap_surjective_of_maximalIdeal_le 0 below · cited by 1 · depth 12
• p-th powers in lower ramification groups IsLocalRing.pow_mem_lowerRamificationGroup_succ 0 below · cited by 2 · depth 12
• Nonzero elements divide powers of maximal-ideal elements IsLocalRing.exists_dvd_pow_of_krullDimLE_one 0 below · cited by 2 · depth 13
• Constancy of idempotents of a two-chart special fibre IsLocalRing.exists_sub_algebraMap_mem_map_maximalIdeal_of_mul_self_sub_mem_of_smul_eq_add 0 below · cited by 2 · depth 13
• Image of C lands in a full T-submodule IsLocalRing.map_mem_of_forall_generalized_eigenvector_mem_of_forall_exists_partner 0 below · cited by 1 · depth 13
• 𝒪-algebra points of local algebras preserve residues IsLocalRing.residue_algHom_apply_eq_of_residue_eq_map 0 below · cited by 3 · depth 13
• Residual values transfer along an injective intertwining map IsLocalRing.sub_algebraMap_mem_maximalIdeal_of_injective_of_intertwining 0 below · cited by 1 · depth 13
• Principal units have no n-torsion when n is invertible IsLocalRing.eq_one_of_pow_eq_one_of_sub_one_mem_maximalIdeal 0 below · cited by 1 · depth 14
• Extending a socle functional to ℤ/p^N IsLocalRing.exists_addMonoidHom_zmod_pow_apply_mul_eq_of_socle 0 below · cited by 1 · depth 14
• Regular parameter pair (varpi,t) when A/varpi A is a DVR IsLocalRing.exists_ofList_pair_eq_maximalIdeal_and_isRegular_of_isDiscreteValuationRing_quotient 0 below · cited by 5 · depth 14
• Fibral flatness criterion for a tower of local rings IsLocalRing.flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map_univ 1 below · cited by 1 · depth 14
• Base change O⊗_R A of a finite augmented local algebra is local IsLocalRing.tensorProduct_of_algHom_retraction_of_isLocalHom 0 below · cited by 2 · depth 14
• Fibrewise criterion of flatness for a tower of local rings IsLocalRing.flat_of_isScalarTower_of_flat_of_flat_quotient_maximalIdeal_map 1 below · cited by 2 · depth 15
• Finite étale local extensions with many distinct residues IsLocalRing.exists_finite_etale_faithfullyFlat_isLocalRing_sub_mem_maximalIdeal_imp_eq 0 below · cited by 2 · depth 16
• Reduced noetherian local ring embeds into its minimal-prime quotients IsLocalRing.exists_jointly_injective_isLocalHom_of_isReduced 0 below · cited by 1 · depth 16
• Residue maps of a local ring factor through images in fields IsLocalRing.exists_ringHom_range_comp_rangeRestrict_eq_of_surjective 0 below · cited by 1 · depth 16
• Character kills Γ^u iff its Swan sum is <u IsLocalRing.forall_mem_upperRamificationGroup_iff_finsum_indicator_lt 0 below · cited by 3 · depth 16
• Systems of parameters in Cohen–Macaulay local rings are regular IsLocalRing.isRegular_of_systemOfParameters 0 below · cited by 2 · depth 16
• Square roots of unity in a local ring with 2 invertible IsLocalRing.sq_eq_one_iff_of_isUnit_two 0 below · cited by 1 · depth 16
• Normal form for a pair cutting out a crossing UV = p^E IsLocalRing.eq_and_exists_isUnit_and_eq_mul_of_mul_eq_pow_of_span_pair_isPrime 0 below · cited by 3 · depth 17
• Non-maximal primes have height ≤ 1 when dim ̂ B ≤ 2 IsLocalRing.eq_bot_of_lt_of_ne_maximalIdeal_of_ringKrullDim_le_two 0 below · cited by 11 · depth 17
• Descent of a crossing presentation to a noetherian local ring IsLocalRing.exists_crossingPresentation_of_ringEquiv_adicCompletion_uvCrossingModel 30 below · cited by 4 · depth 17
• Local equation uv=varpi^e at a transversal crossing IsLocalRing.exists_mul_eq_pow_and_span_pair_eq_of_sup_eq_maximalIdeal 0 below · cited by 3 · depth 17
• Branch-adapted crossing presentation of a completed local ring IsLocalRing.exists_ringEquiv_adicCompletion_uvCrossingModel_of_mul_eq_pow_mul_unit 28 below · cited by 9 · depth 17
• Two generators modulo 𝔪 from a balanced involution IsLocalRing.exists_span_pair_sup_maximalIdeal_smul_top_eq_top_of_isCompl_of_involution 0 below · cited by 1 · depth 17
• Two-variable power series presentation of widehat R over O[[t]]/(t-varpi) IsLocalRing.exists_surjective_mvPowerSeries_adicCompletion_of_maximalIdeal_eq_span 1 below · cited by 7 · depth 17
• Index of the first principal units subgroup IsLocalRing.index_principalUnits_one 1 below · cited by 2 · depth 17
• Krull dimension ≥ 2 passes to the 𝔪-adic completion IsLocalRing.two_le_ringKrullDim_adicCompletion_of_two_le 1 below · cited by 9 · depth 17
• Herbrand's theorem in the upper numbering for quotients IsLocalRing.upperRamificationQuotientCompat_of_map_lowerRamificationGroup_mk_eq 1 below · cited by 2 · depth 17
• Contraction of an extended ideal along adic completion IsLocalRing.comap_map_adicCompletion_eq 0 below · cited by 12 · depth 18
• Powers of mathfrak m_R lie in pⁿR IsLocalRing.exists_maximalIdeal_pow_le_span_natCast_pow_of_module_finite 0 below · cited by 1 · depth 18
• Residual constancy passes to any 𝒪-algebra point IsLocalRing.exists_monic_aeval_eq_zero_map_residue_eq_pow_of_residue_eq 0 below · cited by 3 · depth 18
• Roots of unity of a polynomial reducing to (X-1)^{deg} have p-power order IsLocalRing.exists_pow_pow_eq_one_of_isRoot_map_of_map_residue_eq_X_sub_one_pow 0 below · cited by 1 · depth 18
• Adic completion of a noetherian local ring is faithfully flat IsLocalRing.faithfullyFlat_adicCompletion_maximalIdeal 0 below · cited by 15 · depth 18
• Transitivity of the Herbrand function: φ_G = φ_{G/H}∘φ_H IsLocalRing.herbrandPhi_eq_herbrandPhi_quotient_comp_of_map_lowerRamificationGroup_mk_eq 0 below · cited by 3 · depth 18
• Normality of a local domain with principal-ideal quotient IsLocalRing.isIntegrallyClosed_of_isPrincipalIdealRing_quotient 1 below · cited by 3 · depth 18
• The first ramification group is a p-group IsLocalRing.isPGroup_lowerRamificationGroup_one 1 below · cited by 1 · depth 18
• Principality descends from the 𝔪-adic completion IsLocalRing.isPrincipal_of_isPrincipal_map_adicCompletion 0 below · cited by 2 · depth 18
• Principal units of level one are the kernel of reduction IsLocalRing.principalUnits_one_eq_ker_map_residue 0 below · cited by 1 · depth 18
• Descent of a field-valued point to a finite complete DVR IsLocalRing.exists_isDiscreteValuationRing_moduleFinite_algHom_injective_comp_eq_of_moduleFinite 1 below · cited by 2 · depth 19
• Elements of 𝔪^k are u-1 for u in the k-th principal unit group IsLocalRing.exists_mem_principalUnits_coe_sub_one_eq 0 below · cited by 2 · depth 19
• Residual characterisation of x modulo mathfrak m_A by monic polynomials IsLocalRing.exists_monic_aeval_eq_zero_map_residue_eq_pow_iff_residue_eq_of_injective 0 below · cited by 1 · depth 19
• Integral closedness from a crossing presentation gh=varpi^ew IsLocalRing.isIntegrallyClosed_of_maximalIdeal_eq_span_of_mul_eq_pow_mul_unit 27 below · cited by 3 · depth 19
• Noetherian local domain with principal quotient is factorial IsLocalRing.uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient 0 below · cited by 3 · depth 19
• Element of 𝔪∖𝔪² avoiding all minimal primes IsLocalRing.exists_mem_maximalIdeal_notMem_sq_forall_minimalPrimes_notMem 0 below · cited by 1 · depth 20
• Uniqueness of Hensel lifts in a local ring IsLocalRing.hensel_lift_unique 0 below · cited by 1 · depth 20
• Integral closedness from a crossing presentation gh=varpi^e w IsLocalRing.isIntegrallyClosed_of_maximalIdeal_eq_span_of_mul_eq_pow_mul_isUnit 27 below · cited by 7 · depth 20
• An element dividing a unit of 𝒪 is not residually zero IsLocalRing.not_exists_monic_aeval_eq_zero_map_residue_eq_X_pow_of_mul_eq_algebraMap_of_isUnit 0 below · cited by 1 · depth 20
• Dimension drop for an element avoiding the minimal primes IsLocalRing.ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem 0 below · cited by 2 · depth 20
• Local extension is surjective from a cotangent condition on its completion IsLocalRing.surjective_algebraMap_of_ringEquiv_adicCompletion_of_maximalIdeal_le_map_sup_sq 1 below · cited by 1 · depth 20
• Residue characteristic p when p lies in the maximal ideal IsLocalRing.charP_residueField_of_natCast_mem_maximalIdeal 0 below · cited by 41 · depth 21
• Dimension count for Hom_Δ(N,F^×/q) IsLocalRing.finrank_invariants_linHom_fieldUnits_modPow_eq 10 below · cited by 1 · depth 21
• Units of a local ring: dimHom_Δ(N,R^×/(R^×)^q) IsLocalRing.finrank_invariants_linHom_units_modPow_eq 8 below · cited by 1 · depth 22
• Units lift along S → S/𝔪_R S for integral algebras IsLocalRing.isUnit_of_isUnit_mod_maximalIdeal_of_isIntegral 1 below · cited by 1 · depth 22
• Invariants of Hom(N,U^{(m)}/(U^{(m)})^q) under a coprime action IsLocalRing.finrank_invariants_linHom_principalUnits_modPow_eq_finrank 7 below · cited by 1 · depth 23
• 𝔪_R S lies in the Jacobson radical of an integral extension IsLocalRing.map_maximalIdeal_le_jacobson_bot_of_isIntegral 0 below · cited by 1 · depth 23
• Ring automorphisms preserve the principal unit filtration IsLocalRing.map_ringEquiv_mem_principalUnits_iff 0 below · cited by 2 · depth 23
• Wild step of the principal unit filtration IsLocalRing.pow_mem_principalUnits 0 below · cited by 1 · depth 23
• Tensor product of module-finite local algebras over a local ring with algebraically closed residue field IsLocalRing.tensorProduct_of_moduleFinite_of_isAlgClosed_residueField 0 below · cited by 1 · depth 23
• u ↦ u-1 is additive modulo 𝔪^{2k} IsLocalRing.coe_mul_sub_one_sub_mem_maximalIdeal_pow 0 below · cited by 1 · depth 24
• Chevalley's lemma on ideals with zero intersection IsLocalRing.exists_le_maximalIdeal_pow_of_iInf_eq_bot_of_isAdicComplete 0 below · cited by 1 · depth 24
• Transport of a crossing-model presentation along a ring isomorphism IsLocalRing.exists_ringHom_ringEquiv_adicCompletion_uvCrossingModel_of_ringEquiv 0 below · cited by 4 · depth 24
• Finite flat local algebra over a local ring with algebraically closed residue field IsLocalRing.free_and_forall_sub_mem_maximalIdeal_and_isLocalRing_tensorProduct 0 below · cited by 1 · depth 24
• Ring automorphisms preserve powers of the maximal ideal IsLocalRing.map_ringEquiv_mem_maximalIdeal_pow_iff 0 below · cited by 1 · depth 24
• Descent of a crossing presentation along an étale Galois coefficient extension IsLocalRing.exists_crossingPresentation_of_baseChange_of_forall_map_span_eq 2 below · cited by 2 · depth 25
• Unramified complete coefficient ring for a complete local A-algebra IsLocalRing.exists_isDiscreteValuationRing_ringHom_of_finite_residueField 8 below · cited by 5 · depth 25
• Formal node structure passes to a layer over a DVR extension IsLocalRing.exists_ringEquiv_adicCompletion_uvCrossingModel_of_isLocalHom_of_layer 36 below · cited by 3 · depth 25
• Height-one localisations of a ring with crossing-model completion IsLocalRing.isDiscreteValuationRing_localization_of_ringEquiv_adicCompletion_uvCrossingModel_of_mem_of_ne 37 below · cited by 5 · depth 25
• Base change of a regular fibre over a perfect field IsLocalRing.isDomain_localization_atPrime_tensorProduct_of_isRegularLocalRing_quotient_of_perfectField 7 below · cited by 1 · depth 25
• Normality of a local domain with crossing-model completion IsLocalRing.isIntegrallyClosed_of_ringEquiv_adicCompletion_uvCrossingModel 28 below · cited by 10 · depth 25
• S ∩ K = R for a flat local homomorphism of local domains IsLocalRing.mem_range_algebraMap_of_flat_of_isLocalHom 0 below · cited by 5 · depth 25
• Krull dimension is preserved by adic completion IsLocalRing.ringKrullDim_adicCompletion_maximalIdeal_eq 4 below · cited by 14 · depth 25
• Completion of a module-finite extension of Noetherian local rings IsLocalRing.exists_adicCompletion_ringHom_finite_of_moduleFinite 0 below · cited by 3 · depth 26
• The adic completion of a Noetherian local ring IsLocalRing.exists_isLocalRing_adicCompletion_isAdicComplete_map_maximalIdeal_eq 0 below · cited by 10 · depth 26
• Monic polynomial with lower coefficients in mathfrak m_A killing T modulo hS IsLocalRing.exists_monic_coeff_mem_maximalIdeal_aeval_mem_span_of_pow_mem 0 below · cited by 1 · depth 26
• Valuation subring meets FracB in B_P for nodal ̂ B IsLocalRing.exists_notMem_and_mul_eq_of_mem_valuationSubring_of_ringEquiv_adicCompletion_uvCrossingModel 35 below · cited by 14 · depth 26
• Complementary summands of a finite free module over a local ring IsLocalRing.free_and_finrank_add_eq_of_isCompl 0 below · cited by 1 · depth 26
• Normality from regularity at non-maximal primes and depth two IsLocalRing.isDomain_and_isIntegrallyClosed_and_isFractionRing_of_forall_not_isMaximal_isRegularLocalRing 5 below · cited by 3 · depth 26
• Reducedness of B/mathfrak pB from a locally principal finite overring IsLocalRing.isReduced_quotient_map_of_flat_of_locallyPrincipalOverring 0 below · cited by 4 · depth 26
• Chevalley's lemma on separated decreasing filtrations IsLocalRing.exists_le_maximalIdeal_pow_of_antitone_of_iInf_eq_bot 0 below · cited by 2 · depth 27
• Splitting S → A with kernel tS over a local ring IsLocalRing.exists_ringHom_comp_algebraMap_eq_and_ker_eq_span_of_injective_of_finite 0 below · cited by 1 · depth 27
• Descent of units along completion of a Noetherian local domain IsLocalRing.exists_units_eq_mul_of_algebraMap_adicCompletion_eq_mul_units 1 below · cited by 1 · depth 27
• Unit principle on a crossing model after completion IsLocalRing.exists_units_forall_mul_const_pow_eq_mul_monomial_of_ringEquiv_adicCompletion_uvCrossingModel_of_forall_prime_mem_localization 33 below · cited by 2 · depth 27
• Counting C-points of a one-dimensional local algebra in a valuation ring IsLocalRing.finite_and_natCard_ringHom_valuationSubring_eq_length_quotient_map_maximalIdeal 3 below · cited by 1 · depth 27
• Analytic normality of a normal two-dimensional local domain IsLocalRing.isDomain_and_isIntegrallyClosed_adicCompletion_of_moduleFinite_of_isUnramifiedAt 14 below · cited by 1 · depth 27
• Reduced Artinian algebras integrally closed over a local ring IsLocalRing.isField_of_isIntegrallyClosedIn_of_isArtinianRing_of_isReduced 0 below · cited by 1 · depth 27
• Essentially étale local algebras over A[T] at (varpi,T) are regular IsLocalRing.isRegularLocalRing_of_formallySmooth_of_formallyUnramified_polynomial_of_henselianLocalRing 7 below · cited by 1 · depth 27
• Flat local map with mathfrak m_RS=mathfrak m_S induces completion isomorphism IsLocalRing.exists_adicCompletion_ringEquiv_of_flat_of_map_maximalIdeal_eq_of_residue_surjective 4 below · cited by 2 · depth 28
• Powers of t generate S modulo (p,φvarpi) IsLocalRing.exists_forall_sub_sum_mem_span_pair_of_prime_of_not_associated 0 below · cited by 1 · depth 28
• Faithful residual G-action and Galois residue extension IsLocalRing.forall_smul_sub_mem_imp_eq_one_and_exists_sub_mem_and_isGalois_of_isSeparable_of_finrank_residueField_eq_card 0 below · cited by 3 · depth 28
• Fibre of an unramified A[X]-algebra at X is a DVR IsLocalRing.isDiscreteValuationRing_of_surjective_of_ker_eq_span_of_formallyUnramified_polynomial 0 below · cited by 3 · depth 28
• (ℓ_g-1)/2 is a unit when the residue field has characteristic 2 IsLocalRing.isUnit_natCast_guardPrime_sub_one_div_two_of_charP_two 0 below · cited by 1 · depth 28
• Units in a local ring: ℓ-1 when ℓ≡ 11 (mod 12) and residue characteristic 3 IsLocalRing.isUnit_natCast_guardPrime_sub_one_of_charP_three 0 below · cited by 1 · depth 28
• Length of the special fibre of D as sum ef IsLocalRing.length_quotient_map_maximalIdeal_eq_finsum_ramificationIdx_mul_inertiaDeg 1 below · cited by 1 · depth 28
• Étale by count for finite local extensions of local domains IsLocalRing.etale_of_finite_of_finrank_eq_finrank_residueField 14 below · cited by 1 · depth 29
• Maximal ideals over mathfrak m_A are κ-rational points IsLocalRing.exists_algHom_residueField_ker_eq_of_isMaximal_of_finiteType 0 below · cited by 6 · depth 29
• Isomorphic local rings have isomorphic maximal-adic completions IsLocalRing.exists_ringEquiv_adicCompletion_maximalIdeal_comp_algebraMap_of_ringEquiv 0 below · cited by 8 · depth 29
• Kernel of R → S/mathfrak m_S^k for flat local extensions IsLocalRing.ker_quotient_mk_comp_algebraMap_eq_maximalIdeal_pow_of_flat_of_map_maximalIdeal_eq 0 below · cited by 1 · depth 29
• Finiteness of S/mathfrak m_S^k over R under surjective residue map IsLocalRing.moduleFinite_quotient_maximalIdeal_pow_of_residueField_map_surjective 0 below · cited by 3 · depth 29
• Surjectivity of R → S/mathfrak m_S^k under mathfrak m_R S = mathfrak m_S IsLocalRing.quotient_mk_comp_algebraMap_surjective_of_map_maximalIdeal_eq_of_residueField_map_surjective 1 below · cited by 1 · depth 29
• Étaleness of widehat O⊗_O C over widehat O by degree count IsLocalRing.etale_adicCompletion_tensorProduct_of_finite_of_finrank_eq_finrank_residueField 12 below · cited by 1 · depth 30
• Branch primes and power-series readings of a crossing presentation IsLocalRing.exists_branchReadings_of_ringEquiv_adicCompletion_uvCrossingModel_pow 5 below · cited by 9 · depth 30
• Coheight-one prime avoiding a given non-zero element IsLocalRing.exists_isPrime_not_mem_ringKrullDim_quotient_eq_one 0 below · cited by 1 · depth 30
• Branch prime (t,y) at a crossing-model node IsLocalRing.exists_mul_eq_pow_mul_and_isPrime_span_pair_and_height_eq_one_of_ringEquiv_adicCompletion_uvCrossingModel 33 below · cited by 3 · depth 30
• Lifting an unramified complete DVR into an adic completion IsLocalRing.exists_ringHom_adicCompletion_of_isDiscreteValuationRing_of_maximalIdeal_eq_map_of_residueField 2 below · cited by 2 · depth 30
• Lifting a residue embedding into a square-zero thickening IsLocalRing.exists_ringHom_comp_eq_of_natCast_notMem_maximalIdeal_sq 0 below · cited by 1 · depth 30
• Noetherian local domains are dominated by discrete valuation rings IsLocalRing.exists_valuationSubring_isDiscreteValuationRing_dominates 2 below · cited by 3 · depth 30
• Perfect residue field of a local subring of ℚ̄ IsLocalRing.perfectField_residueField_of_isAlgebraic_rat 0 below · cited by 4 · depth 30
• Étaleness from equal degrees over a complete normal local base IsLocalRing.etale_of_finite_of_finrank_eq_finrank_residueField_of_isAdicComplete 7 below · cited by 1 · depth 31
• Hensel lifting of a simple residual root into the adic completion IsLocalRing.exists_aeval_eq_zero_sub_algebraMap_mem_adicCompletion_of_eval_derivative_ne_zero 0 below · cited by 1 · depth 31
• widehat O⊗_O C is complete local with residue field κ(C) IsLocalRing.exists_isLocalRing_adicCompletion_tensorProduct_residueField_equiv 2 below · cited by 1 · depth 31
• Completion of invariants equals stabiliser-invariants of the completion IsLocalRing.exists_ringHom_adicCompletion_inf_fixedPoints_range_eq_of_isLocalization 7 below · cited by 3 · depth 31
• Yoneda for pro-representable functors on Artinian local O-algebras IsLocalRing.exists_ringHom_forall_existsUnique_algHom_comp_eq_of_isAdicComplete 0 below · cited by 1 · depth 31
• Dominating DVR with finite residue field in a finite extension IsLocalRing.exists_valuationSubring_isDiscreteValuationRing_dominates_finite_residueField 4 below · cited by 1 · depth 31
• Generic degree is unchanged by base change to the completion IsLocalRing.finrank_fractionRing_adicCompletion_tensorProduct_eq 1 below · cited by 1 · depth 31
• Analytic irreducibility of a DVR branch in the completion IsLocalRing.isPrime_map_adicCompletion_and_eq_of_le_of_isDiscreteValuationRing_quotient 1 below · cited by 2 · depth 31
• Localising at n over a reduced Artinian fibre IsLocalRing.map_maximalIdeal_eq_maximalIdeal_localization_atPrime_of_isReduced_of_isArtinianRing 0 below · cited by 1 · depth 31
• Rigidity of unramified henselian local algebras IsLocalRing.ringHom_eq_of_forall_sub_mem_maximalIdeal_of_maximalIdeal_eq_map_of_isSeparable 0 below · cited by 1 · depth 31
• Pro-representability of a functor with bijective gluing IsLocalRing.exists_forall_algHom_bijective_of_forall_pullback_bijective_of_tangent_injective 11 below · cited by 1 · depth 32
• Ramified coefficient ring inside a complete local ring IsLocalRing.exists_isDiscreteValuationRing_ringHom_comp_eq_of_pow_sub_one_eq_mul_natCast 9 below · cited by 1 · depth 32
• Simple roots of the reduction lift in complete local rings IsLocalRing.exists_isRoot_residue_eq_of_isAdicComplete 0 below · cited by 1 · depth 32
• Completion of a flat local W-algebra of relative dimension one IsLocalRing.exists_ringEquiv_adicCompletion_powerSeries_of_flat_of_maximalIdeal_eq_sup_span 1 below · cited by 1 · depth 32
• Localising a Noetherian subalgebra of a local ring IsLocalRing.exists_subalgebra_coe_eq_isNoetherianRing_isLocalRing_isUnit_iff 0 below · cited by 1 · depth 32
• Noetherian local ring with completion k[[X]] is a DVR IsLocalRing.isDiscreteValuationRing_of_nonempty_adicCompletion_ringEquiv_powerSeries 2 below · cited by 1 · depth 32
• Descent of the DVR property from the adic completion IsLocalRing.isDiscreteValuationRing_quotient_of_map_ringEquiv_adicCompletion_eq 0 below · cited by 4 · depth 32
• Coprime naturals: one is a unit in a local ring IsLocalRing.isUnit_natCast_or_isUnit_natCast_of_coprime 0 below · cited by 1 · depth 32
• A solitary minimal prime over its contraction is extended IsLocalRing.map_comap_eq_of_minimalPrimes_span_of_ringEquiv_adicCompletion 0 below · cited by 4 · depth 32
• Recognition of 𝒪[[T]] among complete local 𝒪-algebras IsLocalRing.nonempty_algEquiv_powerSeries_of_maximalIdeal_eq_sup_span_singleton_sup_sq_of_two_le_ringKrullDim 0 below · cited by 1 · depth 32
• Recognition of O[[U,V]]/(UV-varpi) at a crossing point IsLocalRing.nonempty_algEquiv_uvCrossingModel_of_mul_eq_of_maximalIdeal_eq_sup_span_pair_sup_sq_of_two_le_ringKrullDim 36 below · cited by 1 · depth 32
• Universality of a hull under bijective gluing IsLocalRing.exists_forall_algHom_bijective_of_forall_pullback_bijective_of_hull 1 below · cited by 1 · depth 33
• Existence of a hull for a setoid-valued functor on Artinian algebras IsLocalRing.exists_hull_of_forall_pullback_surjective_of_tangent_injective 9 below · cited by 1 · depth 33
• Flat local extension realising a prescribed algebraic residue extension IsLocalRing.exists_isNoetherianRing_faithfullyFlat_map_maximalIdeal_eq_residueField_algEquiv_of_isAlgebraic 2 below · cited by 2 · depth 33
• Small kernels as finite residue-field vector spaces IsLocalRing.exists_module_residueField_linearMap_range_eq_ker_ringHom_of_mul_maximalIdeal_eq_bot 0 below · cited by 4 · depth 33
• Completion of a node ring is O[[U,V]]/(UV-varpi) IsLocalRing.exists_ringEquiv_adicCompletion_uvCrossingModel_of_mul_eq_of_span_pair 35 below · cited by 1 · depth 33
• Schlessinger comparison of fibre products for a flat algebra IsLocalRing.exists_ringEquiv_eqLocus_tensor_trivSqZeroExt_of_flat_of_mul_maximalIdeal_eq_bot 0 below · cited by 5 · depth 33
• Separability elements descend to the residue field IsLocalRing.exists_separabilityElement_residueField_tensor_of_separabilityElement 0 below · cited by 1 · depth 33
• Noetherian local ring with principal maximal ideal, generator non-nilpotent IsLocalRing.isDomain_and_isPrincipalIdealRing_of_maximalIdeal_eq_span_singleton 0 below · cited by 1 · depth 33
• Reducedness of κ(A)⊗_A R versus R/mathfrak m_A R IsLocalRing.isReduced_residueField_tensorProduct_iff 0 below · cited by 2 · depth 33
• Reducedness of κ(A)⊗_A R versus R/(a) for principal mathfrak m_A IsLocalRing.isReduced_residueField_tensorProduct_iff_of_maximalIdeal_eq_span 0 below · cited by 2 · depth 33
• Cotangent generation from separation of dual-number points IsLocalRing.maximalIdeal_eq_map_sup_span_sup_sq_of_forall_ringHom_dualNumber_eqOn 0 below · cited by 2 · depth 33
• Residually trivial endomorphism fixing κ(varpi) fixes κ IsLocalRing.ringHom_comp_eq_of_forall_sub_mem_maximalIdeal_of_apply_eq_of_maximalIdeal_eq_span 1 below · cited by 1 · depth 33
• A universal first-order class over k⊕ kᵈ (Schlessinger) IsLocalRing.exists_trivSqZeroExt_forall_exists_algHom_dualNumber_of_forall_pullback_surjective_of_tangent_injective 0 below · cited by 1 · depth 34
• Fibre products in Schlessinger's category of Artinian local O-algebras IsLocalRing.isLocalRing_and_isArtinianRing_equalizer_of_comp_algebraMap_eq_residue 0 below · cited by 2 · depth 34
• Surjectivity criterion for local maps of complete local rings IsLocalRing.surjective_of_isAdicComplete_of_maximalIdeal_le_map_sup_sq 0 below · cited by 2 · depth 34
• Small ideals of Artinian local rings as residue-field vector spaces IsLocalRing.exists_module_residueField_linearMap_range_eq_ker_of_mul_maximalIdeal_eq_bot 0 below · cited by 1 · depth 35
• Nonzero scalars act surjectively on the corner H(1-e) IsLocalRing.exists_smul_mul_one_sub_eq_of_map_maximalIdeal_eq_top 0 below · cited by 1 · depth 35
• Truncated monomial expansion modulo an ideal in a local ring IsLocalRing.exists_sub_sum_monomial_mem_of_maximalIdeal_eq_span_pair 0 below · cited by 1 · depth 35
• Completion of a formally smooth local algebra of dimension ≤ 1 IsLocalRing.isDomain_and_isIntegrallyClosed_adicCompletion_of_formallySmooth_of_ringKrullDim_le_one 3 below · cited by 2 · depth 35
• Unique lifting of residue embeddings into complete local algebras IsLocalRing.existsUnique_algHom_residue_eq_of_flat_of_map_maximalIdeal_eq_of_isSeparable_of_isAdicComplete 5 below · cited by 1 · depth 36
• Basis coordinates of a power series with coefficients in ι(V) IsLocalRing.existsUnique_forall_eq_sum_smul_of_forall_coeff_mem_range 0 below · cited by 3 · depth 36
• Lifting a finite separable residue extension to an étale local algebra IsLocalRing.exists_isLocalRing_etale_free_residueField_algEquiv 3 below · cited by 1 · depth 36
• Unique lifting to a local ring with nilpotent maximal ideal IsLocalRing.existsUnique_algHom_residue_eq_of_flat_of_map_maximalIdeal_eq_of_isNilpotent_maximalIdeal 4 below · cited by 1 · depth 37
• One-dimensional dual-number tangent space bounds the relative cotangent space IsLocalRing.exists_maximalIdeal_le_span_sup_sq_sup_map_of_forall_algHom_dualNumber 0 below · cited by 2 · depth 37
• Complete two-dimensional local domain over a DVR is W₀[[X]] IsLocalRing.exists_powerSeries_algEquiv_apply_X_eq_of_maximalIdeal_eq_span_pair_of_ringKrullDim_eq_two 3 below · cited by 2 · depth 37
• Regularity and dimension two from a two-generated maximal ideal IsLocalRing.isRegularLocalRing_and_ringKrullDim_eq_two_of_finite_of_maximalIdeal_le_span_pair_sup_sq 2 below · cited by 2 · depth 37
• Evaluation of power series at an element of the maximal ideal IsLocalRing.exists_algHom_powerSeries_map_X_eq_of_mem_maximalIdeal 0 below · cited by 1 · depth 38
• Power series ring from smoothness and one-dimensional tangent space IsLocalRing.exists_powerSeries_algEquiv_of_forall_exists_comp_eq_of_forall_algHom_dualNumber 6 below · cited by 2 · depth 38
• Nakayama criterion: 𝔪 = N when 𝔪 ≤ N + 𝔪² IsLocalRing.maximalIdeal_eq_of_le_sup_sq 0 below · cited by 1 · depth 38
• Pro-representing object determined by its functor on Artinian test algebras IsLocalRing.nonempty_algEquiv_of_forall_isArtinianRing_algHom_equiv 0 below · cited by 2 · depth 38
• Schlessinger's criterion in one variable: R ≅ Λ[[X]] IsLocalRing.exists_powerSeries_algEquiv_apply_X_eq_of_forall_exists_comp_eq_of_notMem_sq_sup_map 5 below · cited by 1 · depth 39
• Residue map to k on a local Λ-algebra reaching its residue field IsLocalRing.exists_residueMap_of_surjective_residue_comp_algebraMap 0 below · cited by 2 · depth 39
• Residue compatibility of Λ-algebra maps out of a local ring IsLocalRing.residueMap_comp_algHom_eq_of_surjective 0 below · cited by 8 · depth 39
• Embedding dimension at most two under the formal plane IsLocalRing.exists_card_le_two_and_span_image_eq_maximalIdeal_of_basis_mvPowerSeries 3 below · cited by 1 · depth 40
• Koszul relations force binom m2 generators of the relation module IsLocalRing.choose_two_le_of_basis_ker_linearCombination 0 below · cited by 1 · depth 41
• Residue field, units and square-zero kernel along a small surjection IsLocalRing.isAlgClosed_residueField_and_charP_and_isUnit_and_ker_mul_ker_of_surjective 0 below · cited by 1 · depth 41
• Derivation criterion for reducedness in characteristic zero IsLocalRing.isReduced_of_forall_exists_derivation_of_charZero 0 below · cited by 1 · depth 41
• Vanishing of r at every prime of a local ring IsLocalRing.mem_of_mul_sq_sub_intCast_mem_of_forall_charZero 0 below · cited by 1 · depth 41

IsLocalRing.HasseForm 1

• Unit binary forms on mathbb F_q-rational directions transfer along local maps IsLocalRing.HasseForm.isUnit_sum_map_mul_pow_of_forall_isUnit_sum_mul_pow 0 below · cited by 2 · depth 29

IsLocalRing.IsCohenMacaulayOfDim 1

• Dimension formula dim R/𝔭+ht𝔭=d in Cohen–Macaulay local rings IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_quotient_add_height 5 below · cited by 2 · depth 18

IsLocalRing.ResidueField 1

• Surjectivity onto the residue field passes to quotients IsLocalRing.ResidueField.algebraMap_surjective_quotient 0 below · cited by 4 · depth 9