Localizations of smooth and étale algebras

TheoremLocalizations of étale algebras are integrally closed domains#✓fully proved

The localization of an étale algebra at a prime is a domain and integrally closed.

theorem Algebra.Etale.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
    (P : Type u) [CommRing P] [IsDomain P] [IsIntegrallyClosed P]
    (A : Type u) [CommRing A] [Algebra P A] [Algebra.Etale P A]
    (q : Ideal A) [q.IsPrime] (A_q : Type u) [CommRing A_q] [Algebra A A_q]
    [IsLocalization.AtPrime A_q q] :
    IsDomain A_q ∧ IsIntegrallyClosed A_q

Used by 1

Used byLocalizations of smooth algebras are integrally closed domains

TheoremLocalizations of smooth algebras are integrally closed domains#✓fully proved

The localization of a smooth algebra at a prime is a domain and integrally closed.

theorem Algebra.Smooth.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
    (R : Type u) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.Smooth R S]
    (p : Ideal S) [p.IsPrime] (Sₚ : Type u) [CommRing Sₚ] [Algebra S Sₚ]
    [IsLocalization.AtPrime Sₚ p] :
    IsDomain Sₚ ∧ IsIntegrallyClosed Sₚ

Uses 1

Proof usesLocalizations of étale algebras are integrally closed domains

TheoremLocal rings with principal regular maximal ideal are domains#✓fully proved

A Noetherian local ring whose maximal ideal is generated by a single regular element is a domain.

theorem isDomain_of_maximalIdeal_eq_span {L : Type*} [CommRing L] [IsLocalRing L]
    [IsNoetherianRing L] {ϖ : L} (hreg : IsSMulRegular L ϖ)
    (hmax : maximalIdeal L = Ideal.span {ϖ}) : IsDomain L

Used by 1

Used bySmooth curves have discrete valuation rings as local rings

TheoremSmooth curves have discrete valuation rings as local rings#✓fully proved

The localization at a maximal ideal of a standard smooth algebra of relative dimension 1 over a field is a discrete valuation ring.

theorem isDiscreteValuationRing_localization_atPrime
    {k : Type*} [Field k] {A : Type*} [CommRing A] [Algebra k A]
    [Algebra.IsStandardSmoothOfRelativeDimension 1 k A]
    (p : Ideal A) [p.IsMaximal] :
    ∃ _ : IsDomain (Localization.AtPrime p), IsDiscreteValuationRing (Localization.AtPrime p)

Uses 1

Proof usesLocal rings with principal regular maximal ideal are domains

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.