Regular Local Ring is Domain

In this file, we prove that regular local ring is domain

Main definition and results

• isDomain_of_isRegularLocalRing : a regular local ring is domain

• isRegular_of_span_eq_maximalIdeal : for a regular local ring R, if a list of length equal to its dimension generates maximalIdeal R, it form a regular sequence.

theorem IsLocalRing.ResidueField.map_bijective_of_surjective {R : Type u_1} [CommRing R] [IsLocalRing R] {S : Type u_2} [CommRing S] [IsLocalRing S] (f : R →+* S) (surj : Function.Surjective ⇑f) [IsLocalHom f] : Function.Bijective ⇑(map f)

theorem IsLocalRing.spanFinrank_maximalIdeal_quotient {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (S : Finset R) (sub : ↑S ⊆ ↑(maximalIdeal R)) (li : LinearIndependent (ι := ↑↑S) (ResidueField R) (⇑(maximalIdeal R).toCotangent ∘ Set.inclusion sub)) : Submodule.spanFinrank (maximalIdeal (R ⧸ Ideal.span ↑S)) + S.card = Submodule.spanFinrank (maximalIdeal R)

theorem quotient_isRegularLocalRing_tfae (R : Type u_1) [CommRing R] [IsRegularLocalRing R] (S : Finset R) (sub : ↑S ⊆ ↑(IsLocalRing.maximalIdeal R)) : [∃ (T : Finset R), S ⊆ T ∧ ↑T.card = ringKrullDim R ∧ Ideal.span ↑T = IsLocalRing.maximalIdeal R, LinearIndependent (ι := ↑↑S) (IsLocalRing.ResidueField R) (⇑(IsLocalRing.maximalIdeal R).toCotangent ∘ Set.inclusion sub), IsRegularLocalRing (R ⧸ Ideal.span ↑S) ∧ ringKrullDim (R ⧸ Ideal.span ↑S) + ↑S.card = ringKrullDim R].TFAE

theorem quotient_span_singleton (R : Type u_1) [CommRing R] [IsRegularLocalRing R] {x : R} (mem : x ∈ IsLocalRing.maximalIdeal R) (nmem : x ∉ IsLocalRing.maximalIdeal R ^ 2) : IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧ ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem FiniteRingKrullDim.ringKrullDim_eq_nat (R : Type u_1) [CommRing R] [FiniteRingKrullDim R] : ∃ (n : ℕ), ringKrullDim R = ↑n

theorem Ideal.span_singleton_mul_eq_self_of_isPrime {R : Type u_1} [CommRing R] {p : Ideal R} [p.IsPrime] (x : R) (hx : x ∉ p) (hp : p ≤ span {x}) : span {x} * p = p

theorem isDomain_of_isRegularLocalRing (R : Type u_1) [CommRing R] [IsRegularLocalRing R] : IsDomain R

instance instIsDomainOfIsRegularLocalRing (R : Type u_1) [CommRing R] [IsRegularLocalRing R] : IsDomain R

theorem IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one (R : Type u_1) [CommRing R] [IsRegularLocalRing R] (dim : ringKrullDim R = 1) : IsDiscreteValuationRing R

Regular local ring of dimension one is discrete valuation ring. For iff version, should exist after making IsDiscreteValuationRing extend IsDomain.

theorem isRegular_of_span_eq_maximalIdeal (R : Type u_1) [CommRing R] [IsRegularLocalRing R] (rs : List R) (span : Ideal.ofList rs = IsLocalRing.maximalIdeal R) (len : ↑rs.length = ringKrullDim R) : RingTheory.Sequence.IsRegular R rs