Module

IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem

13 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring ring Krull Dim quotient span singleton add one of forall minimal Primes not

Mem

Imports4

Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.Tactic.Choose
Mathlib.Tactic.Ring.RingNF

Imported by2

theorem

maximalIdeal_ne_bot_of_ringKrullDim_pos

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem.W2RLR.maximalIdeal_ne_bot_of_ringKrullDim_pos

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L48 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L57 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L73 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L140 ↗

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L157 ↗

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L203 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L208 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L218 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L234 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L313 ↗

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

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

L367 ↗

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

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
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

ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem

L379 ↗

IsLocalRing.ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem

Source context 6 commands

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

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

Lean source · statement

theorem
  _root_.IsLocalRing.ringKrullDim_quotient_span_singleton_add_one_of_forall_minimalPrimes_notMem
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {x : R}
    (hx : x ∈ maximalIdeal R) (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

Module documentation

Is Local Ring ring Krull Dim quotient span singleton add one of forall minimal Primes not

Declarations