Module

RegularLocalDomain.lean

Nyll.SchemeTheory.RingTheory.RegularLocalDomain

13 declarations indexed from sourceView source ↗

Module documentation

Regular local rings are domains

Avoiding minimal primes produces regular elements that lower the dimension. Induction on the dimension then proves the domain property for regular local rings.

Imports8

Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.Tactic.Choose
Mathlib.Tactic.Ring.RingNF
Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by26

theorem

maximalIdeal_ne_bot_of_ringKrullDim_pos

L40 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.maximalIdeal_ne_bot_of_ringKrullDim_pos

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v

Lean source · statement

theorem maximalIdeal_ne_bot_of_ringKrullDim_pos (R : Type u) [CommRing R] [IsLocalRing R]
    (hdim : 0 < ringKrullDim R) :
    maximalIdeal R ≠ ⊥

theorem

isLocalRing_quotient_span_singleton

L53 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.isLocalRing_quotient_span_singleton

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section FromABFreeness
variable {R : Type u} [CommRing R]

Lean source · statement

theorem isLocalRing_quotient_span_singleton [IsLocalRing R] {x : R}
    (hx : x ∈ maximalIdeal R) : IsLocalRing (R ⧸ Ideal.span {x})

theorem

exists_ringKrullDim_eq_natCast

L62 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.exists_ringKrullDim_eq_natCast

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section FromABFreeness
variable {R : Type u} [CommRing R]

Lean source · statement

theorem exists_ringKrullDim_eq_natCast (R : Type u) [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] : ∃ d : ℕ, ringKrullDim R = (d : WithBot ℕ∞)

theorem

exists_finite_span_eq_maximalIdeal_mem

L78 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.exists_finite_span_eq_maximalIdeal_mem

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section Exchange0
variable (R : Type u) [CommRing R]

Lean source · statement

theorem exists_finite_span_eq_maximalIdeal_mem [IsLocalRing R] [IsNoetherianRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    ∃ S : Set R, x ∈ S ∧ S.Finite ∧ S.ncard ≤ (maximalIdeal R).spanFinrank ∧
      Ideal.span S = maximalIdeal R

theorem

maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos

L145 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section PrimeAvoidance

Lean source · statement

theorem maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos
    (R : Type u) [CommRing R] [IsLocalRing R] (hdim : 0 < ringKrullDim R) :
    maximalIdeal R ∉ minimalPrimes R

theorem

exists_parameter_notMem_minimalPrimes

L162 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.exists_parameter_notMem_minimalPrimes

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section PrimeAvoidance

Lean source · statement

theorem exists_parameter_notMem_minimalPrimes
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdim : 0 < ringKrullDim R) :
    ∃ x ∈ maximalIdeal R, x ∉ (maximalIdeal R) ^ 2 ∧ ∀ p ∈ minimalPrimes R, x ∉ p

theorem

annihilator_self_eq_bot

L208 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.annihilator_self_eq_bot

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section DimensionDrop
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem annihilator_self_eq_bot (R : Type u) [CommRing R] : Module.annihilator R R = ⊥

theorem

ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes

L213 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section DimensionDrop
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes
    {x : R} (hx : x ∈ maximalIdeal R) (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) :
    ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R

theorem

ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes

L223 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section DimensionDrop
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes
    {x : R} (hx : x ∈ maximalIdeal R) (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes

L239 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section QuotientRegularity
variable (R : Type u) [CommRing R] [IsRegularLocalRing R]

Lean source · statement

theorem isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2)
    (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) [IsLocalRing (R ⧸ Ideal.span {x})] :
    IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧
      (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1 =
        (maximalIdeal R).spanFinrank

theorem

isDomain_of_isRegularLocalRing_aux

L318 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.isDomain_of_isRegularLocalRing_aux

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section MatsumuraDomain

Lean source · statement

theorem isDomain_of_isRegularLocalRing_aux :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R],
      (maximalIdeal R).spanFinrank = n → IsDomain R

theorem

isDomain_of_isRegularLocalRing

L372 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain.W2RLR.No4PatchingCore.isDomain_of_isRegularLocalRing

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
namespace W2RLR
universe u v
namespace No4PatchingCore
section MatsumuraDomain

Lean source · statement

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

theorem

isDomain

L384 ↗

IsRegularLocalRing.isDomain

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_isDomain
open IsLocalRing RingTheory
open scoped Pointwise
open IsLocalRing

Lean source · statement

theorem _root_.IsRegularLocalRing.isDomain (R : Type*) [CommRing R] [IsRegularLocalRing R] :
    IsDomain R

Module documentation

Regular local rings are domains

Declarations