Namespace IsIntegrallyClosed 32 theorems
- Reducedness of A/(x) for normal domains via minimal primes
IsIntegrallyClosed.isReduced_quotient_span_singleton_of_forall_mem_minimalPrimes6 below · cited by 2 · depth 14 - Directed unions of integrally closed subrings are integrally closed
IsIntegrallyClosed.of_directed_iUnion_subring0 below · cited by 2 · depth 14 - Associated primes of A/(x) are minimal over (x)
IsIntegrallyClosed.mem_minimalPrimes_of_mem_associatedPrimes4 below · cited by 3 · depth 15 - Integrally closed in an ambient field implies integrally closed
IsIntegrallyClosed.of_isIntegrallyClosedIn_of_faithfulSMul0 below · cited by 3 · depth 15 - Fibre k⊗_Λ A has Krull dimension one at each maximal ideal
IsIntegrallyClosed.ringKrullDim_localization_tensor_eq_one_of_irreducible8 below · cited by 1 · depth 15 - Algebraic Hartogs lemma for Noetherian normal domains
IsIntegrallyClosed.exists_algebraMap_eq_of_forall_height_eq_one4 below · cited by 13 · depth 16 - Valuation subring of a height-one prime of a normal Noetherian domain
IsIntegrallyClosed.exists_valuationSubring_mem_iff_and_nonunits_iff_of_height_eq_one0 below · cited by 16 · depth 16 - Associated primes of a nonzero principal ideal have height one
IsIntegrallyClosed.height_eq_one_of_mem_associatedPrimes3 below · cited by 7 · depth 16 - Associated primes of a principal ideal give discrete valuation rings
IsIntegrallyClosed.isDiscreteValuationRing_localization_of_mem_associatedPrimes1 below · cited by 4 · depth 16 - Reducedness of A/pA from a squarefree minimal polynomial
IsIntegrallyClosed.isReduced_quotient_span_singleton_of_squarefree_minpoly10 below · cited by 2 · depth 16 - Normal Noetherian domains are regular at height-one primes
IsIntegrallyClosed.isRegularLocalRing_localization_atPrime_of_ringKrullDim_eq_one2 below · cited by 4 · depth 16 - Torsion-freeness of A/pA over R/(p) for integral extensions
IsIntegrallyClosed.mem_span_singleton_of_mul_mem_of_isIntegral5 below · cited by 3 · depth 16 - Localisation at a height-one prime as a valuation subring of K
IsIntegrallyClosed.exists_valuationSubring_mem_iff_of_height_eq_one1 below · cited by 11 · depth 17 - Normal Noetherian local domain with depth one is a DVR
IsIntegrallyClosed.isDiscreteValuationRing_of_maximalIdeal_mem_associatedPrimes0 below · cited by 1 · depth 17 - Integral closedness descends from a localisation
IsIntegrallyClosed.of_isIntegrallyClosedIn_of_isLocalization0 below · cited by 1 · depth 17 - Rational function regular along a prime divisor and integral lies in R
IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow_mul0 below · cited by 3 · depth 18 - A second height-one prime over varpi from a factorisation GH=varpi^e u
IsIntegrallyClosed.exists_isPrime_height_eq_one_mem_ne_of_mul_eq_pow_mul5 below · cited by 1 · depth 18 - Normality descends along a flat local ring homomorphism
IsIntegrallyClosed.isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom0 below · cited by 5 · depth 24 - Regular pair extending a nonzero element in a normal local domain of dimension ≥ 2
IsIntegrallyClosed.exists_isRegular_pair_of_two_le_ringKrullDim0 below · cited by 3 · depth 26 - Normality in dimension ≤ 2 gives regularity off the closed point
IsIntegrallyClosed.isRegularLocalRing_localization_of_ne_maximalIdeal_of_ringKrullDim_le_two0 below · cited by 4 · depth 26 - Integral closedness descends along faithfully flat algebras
IsIntegrallyClosed.of_faithfullyFlat0 below · cited by 2 · depth 26 - Unmixedness of principal ideals in normal Noetherian domains, local form
IsIntegrallyClosed.exists_not_mem_and_mul_mem_span_singleton_of_forall_mem_minimalPrimes_not_mem5 below · cited by 1 · depth 27 - Algebraic Hartogs lemma via valuation rings of an algebraic extension
IsIntegrallyClosed.mem_range_algebraMap_of_forall_height_eq_one_exists_valuationSubring_ne_top7 below · cited by 3 · depth 27 - Denominators outside the centre of a valuation subring
IsIntegrallyClosed.exists_notMem_and_mul_eq_of_mem_valuationSubring_of_ringKrullDim_le_two2 below · cited by 3 · depth 28 - Integral closure in a Kummer extension F[X]/(X^k-vh^k)
IsIntegrallyClosed.integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow2 below · cited by 2 · depth 28 - Algebraic Hartogs: height-one local membership implies integrality
IsIntegrallyClosed.mem_range_algebraMap_of_forall_height_eq_one4 below · cited by 8 · depth 28 - Algebraic Hartogs lemma along a prime divisor
IsIntegrallyClosed.mem_range_of_isPrime_span_of_forall_height_eq_one_of_notMem5 below · cited by 1 · depth 28 - Integral closure in an étale Kummer algebra K[X]/(Xⁿ-u)
IsIntegrallyClosed.integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit1 below · cited by 1 · depth 29 - Finite free integrally closed subring of full generic rank
IsIntegrallyClosed.bijective_algebraMap_of_finrank_eq_finrank_fractionRing1 below · cited by 1 · depth 32 - Regularity at a cusp from a power series chart
IsIntegrallyClosed.isRegularLocalRing_of_isLocalization_atPrime_of_ringHom_powerSeries_of_forall_minimalPrimes_le7 below · cited by 4 · depth 32 - Principal ideal with unique minimal prime, uniformising at it, equals it
IsIntegrallyClosed.span_singleton_eq_of_minimalPrimes_eq_singleton_of_map_eq_maximalIdeal5 below · cited by 1 · depth 33 - Normality descends from the 𝔪-adic completion
IsIntegrallyClosed.localization_atPrime_of_adicCompletion0 below · cited by 1 · depth 35