NYLL
Module

IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem
13 declarations indexed from sourceView source ↗

Module documentation

Is Regular Local Ring quotient span singleton of not Mem sq of forall minimal Primes not

Mem

Imports4
  • Mathlib.RingTheory.KrullDimension.Regular
  • Mathlib.RingTheory.RegularLocalRing.Defs
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.Ring.RingNF
Imported by4

Declarations

theorem

maximalIdeal_ne_bot_of_ringKrullDim_pos

L35 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem.W2RLR.No4PatchingCore.maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem.W2RLR.No4PatchingCore.exists_parameter_notMem_minimalPrimes
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem.W2RLR.No4PatchingCore.ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem.W2RLR.No4PatchingCore.ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_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 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem.W2RLR.No4PatchingCore.isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes
Source context 10 commands

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

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

quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem

L379 ↗
IsRegularLocalRing.quotient_span_singleton_of_notMem_sq_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 IsRegularLocalRing_quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem
open IsLocalRing RingTheory
open scoped Pointwise
open IsLocalRing
Lean source · statement
theorem
  _root_.IsRegularLocalRing.quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem
    (R : Type*) [CommRing R] [IsRegularLocalRing R] {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

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.