Module

IsLocalRing_isRegular_of_systemOfParameters.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isRegular_of_systemOfParameters

179 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring is Regular of system Of Parameters

Imports159

Lean.Elab.Command
Mathlib.Algebra.Algebra.Basic
Mathlib.Algebra.Algebra.Defs
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.Field.Defs
Mathlib.Algebra.Field.IsField
Mathlib.Algebra.Field.Rat
Mathlib.Algebra.Group.Action.Defs
Mathlib.Algebra.Group.Action.Faithful
Mathlib.Algebra.Group.Defs
Mathlib.Algebra.Group.Equiv.Defs
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Algebra.Group.Monoid
Mathlib.Algebra.Group.Semigroup
Mathlib.Algebra.Group.Units.Hom
Mathlib.Algebra.GroupWithZero.Action.Defs
Mathlib.Algebra.GroupWithZero.Defs
Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Mathlib.Algebra.Module.Defs
Mathlib.Algebra.Module.Equiv.Defs
Mathlib.Algebra.Module.LinearMap.Defs
Mathlib.Algebra.Module.SpanRank
Mathlib.Algebra.Module.SpanRankOperations
Mathlib.Algebra.Module.Submodule.Defs
Mathlib.Algebra.Module.Submodule.Equiv
Mathlib.Algebra.Module.Submodule.Ker
Mathlib.Algebra.Module.Submodule.Lattice
Mathlib.Algebra.Module.Submodule.LinearMap
Mathlib.Algebra.Module.Submodule.Pointwise
Mathlib.Algebra.Module.Submodule.Range
Mathlib.Algebra.Module.Submodule.RestrictScalars
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.Algebra.Module.Torsion.Free
Mathlib.Algebra.Notation.Pi.Defs
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Mathlib.Algebra.Order.Ring.Cast
Mathlib.Algebra.Order.Sub.Defs
Mathlib.Algebra.Order.SuccPred
Mathlib.Algebra.Order.ZeroLEOne
Mathlib.Algebra.Prime.Defs
Mathlib.Algebra.Regular.SMul
Mathlib.Algebra.Ring.Defs
Mathlib.Algebra.Ring.Equiv
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.Basic.Finite.Defs
Mathlib.Basic.Logic.Basic
Mathlib.Basic.Nonempty
Mathlib.Basic.Nontrivial.Defs
Mathlib.Basic.Unique
Mathlib.Data.ENat.Basic
Mathlib.Data.ENat.Lattice
Mathlib.Data.ENat.SuccOrder
Mathlib.Data.Finset.Card
Mathlib.Data.Finset.Dedup
Mathlib.Data.Fintype.Defs
Mathlib.Data.Fintype.EquivFin
Mathlib.Data.List.Basic
Mathlib.Data.List.Forall2
Mathlib.Data.Nat.Cast.Defs
Mathlib.Data.Nat.Init
Mathlib.Data.Set.Basic
Mathlib.Data.Set.Card
Mathlib.Data.Set.Finite.Basic
Mathlib.Data.Set.Image
Mathlib.Data.Set.Insert
Mathlib.Data.Set.Lattice.Bounded
Mathlib.Data.Set.Operations
Mathlib.Data.SetLike.Basic
Mathlib.LinearAlgebra.Basis.Basic
Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.LinearAlgebra.FreeModule.Basic
Mathlib.LinearAlgebra.FreeModule.Finite.Basic
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.LinearAlgebra.LinearIndependent.Defs
Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.LinearAlgebra.Quotient.Defs
Mathlib.LinearAlgebra.Span.Basic
Mathlib.LinearAlgebra.Span.Defs
Mathlib.LinearAlgebra.TensorProduct.Basis
Mathlib.Logic.Function.Basic
Mathlib.Order.BooleanAlgebra.Set
Mathlib.Order.BoundedOrder.Basic
Mathlib.Order.CompleteLattice.Basic
Mathlib.Order.CompleteLattice.Defs
Mathlib.Order.Defs.LinearOrder
Mathlib.Order.Defs.PartialOrder
Mathlib.Order.KrullDimension
Mathlib.Order.Lattice
Mathlib.Order.RelSeries
Mathlib.Order.SetNotation
Mathlib.Order.WithBot
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Finiteness.Cardinality
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Mathlib.RingTheory.Ideal.Colon
Mathlib.RingTheory.Ideal.Cotangent
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Maximal
Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Mathlib.RingTheory.Ideal.Nonunits
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Prime
Mathlib.RingTheory.Ideal.Quotient.Basic
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.Ideal.Quotient.Noetherian
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.Jacobson.Ideal
Mathlib.RingTheory.Jacobson.Radical
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.KrullDimension.Field
Mathlib.RingTheory.KrullDimension.Module
Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Mathlib.RingTheory.KrullDimension.PID
Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.KrullDimension.Zero
Mathlib.RingTheory.LocalRing.Basic
Mathlib.RingTheory.LocalRing.Defs
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
Mathlib.RingTheory.LocalRing.ResidueField.Defs
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.MvPowerSeries.Basic
Mathlib.RingTheory.MvPowerSeries.Inverse
Mathlib.RingTheory.Nakayama
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Noetherian.Defs
Mathlib.RingTheory.PowerSeries.Basic
Mathlib.RingTheory.PowerSeries.Ideal
Mathlib.RingTheory.PowerSeries.Inverse
Mathlib.RingTheory.QuotSMulTop
Mathlib.RingTheory.Regular.IsSMulRegular
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.RingTheory.Spectrum.Prime.Defs
Mathlib.RingTheory.Spectrum.Prime.RingHom
Mathlib.RingTheory.Support
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Tactic.Choose
Mathlib.Tactic.Conv
Mathlib.Tactic.CrossRefAttribute
Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.Set
Mathlib.Tactic.SimpRw
Mathlib.Tactic.Simproc.ExistsAndEq
Mathlib.Tactic.TermCongr
Nyll.SchemeTheory.RingTheory.CohenMacaulay
Nyll.SchemeTheory.RingTheory.LocalAlgebra

Imported by2

instance

instSubsingletonQuotientOfSubsingleton

L209 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.instSubsingletonQuotientOfSubsingleton

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

instance instSubsingletonQuotientOfSubsingleton [Subsingleton M] (N : Submodule R M) :
  Subsingleton (M ⧸ N)

lemma

isWeaklyRegular_of_subsingleton

L346 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_subsingleton

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma RingTheory.Sequence.isWeaklyRegular_of_subsingleton
    {R : Type*} (M : Type*) [CommRing R] [AddCommGroup M] [Module R M]
    [Subsingleton R] (s : List R) : Sequence.IsWeaklyRegular M s

lemma

faithfulSMul_of_depth_eq_ringKrullDim

L391 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.faithfulSMul_of_depth_eq_ringKrullDim

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.faithfulSMul_of_depth_eq_ringKrullDim [IsDomain R] [Nontrivial M] [Module.Finite R M]
    (H : ringKrullDim R < ⊤) (H' : .some (Module.depth R M) = ringKrullDim R) :
    FaithfulSMul R M

lemma

exists_isSMulRegular_of_depth_pos

L684 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.exists_isSMulRegular_of_depth_pos

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

lemma Module.exists_isSMulRegular_of_depth_pos (h : 0 < Module.depth R M) :
    ∃ x ∈ maximalIdeal R, IsSMulRegular M x

lemma

depth_pos_iff_exists_isSMulRegular

L701 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_pos_iff_exists_isSMulRegular

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

lemma Module.depth_pos_iff_exists_isSMulRegular :
    0 < Module.depth R M ↔ ∃ x ∈ maximalIdeal R, IsSMulRegular M x

lemma

maximalIdeal_ne_bot_of_depth_pos

L706 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.maximalIdeal_ne_bot_of_depth_pos

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

lemma Module.maximalIdeal_ne_bot_of_depth_pos [Nontrivial M] (h : 0 < Module.depth R M) :
    maximalIdeal R ≠ ⊥

lemma

maximalIdeal_ne_bot_of_ringKrullDim_pos

L715 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.maximalIdeal_ne_bot_of_ringKrullDim_pos

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

lemma IsLocalRing.maximalIdeal_ne_bot_of_ringKrullDim_pos (hdim : 0 < ringKrullDim R) :
    maximalIdeal R ≠ ⊥

lemma

maximalIdeal_notMem_associatedPrimes_of_depth_pos

L722 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.maximalIdeal_notMem_associatedPrimes_of_depth_pos

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

lemma Module.maximalIdeal_notMem_associatedPrimes_of_depth_pos [IsNoetherianRing R]
    (h : 0 < Module.depth R M) : maximalIdeal R ∉ associatedPrimes R M

theorem

exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes

L737 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section PrimeAvoidance
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes
    (hR : maximalIdeal R ∉ associatedPrimes R R)
    (hM : maximalIdeal R ∉ associatedPrimes R M)
    (hbot : maximalIdeal R ≠ ⊥) :
    ∃ x ∈ maximalIdeal R,
      x ∉ (maximalIdeal R) ^ 2 ∧ IsSMulRegular R x ∧ IsSMulRegular M x

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos

L792 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

theorem Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos
    (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hR : 0 < Module.depth R R) (hM : 0 < Module.depth R M) :
    ∃ x ∈ maximalIdeal R,
      x ∉ (maximalIdeal R) ^ 2 ∧ IsSMulRegular R x ∧ IsSMulRegular M x

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos'

L803 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

theorem Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos'
    (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hR : 0 < Module.depth R R) (hM : 0 < Module.depth R M)
    (_hdim : 0 < ringKrullDim R) :
    ∃ x ∈ maximalIdeal R,
      x ∉ (maximalIdeal R) ^ 2 ∧ IsSMulRegular R x ∧ IsSMulRegular M x

theorem

exists_isSMulRegular_and_isSMulRegular

L812 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.exists_isSMulRegular_and_isSMulRegular

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

theorem IsLocalRing.IsCohenMacaulayOfDim.exists_isSMulRegular_and_isSMulRegular
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {d : ℕ}
    (hCM : IsCohenMacaulayOfDim R d)
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hd : 0 < d) (hM : 0 < Module.depth R M) :
    ∃ x ∈ maximalIdeal R,
      x ∉ (maximalIdeal R) ^ 2 ∧ IsSMulRegular R x ∧ IsSMulRegular M x

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain

L823 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

theorem Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain
    (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hM : 0 < Module.depth R M) (hdim : 0 < ringKrullDim R) :
    ∃ x ∈ maximalIdeal R,
      x ∉ (maximalIdeal R) ^ 2 ∧ IsSMulRegular R x ∧ IsSMulRegular M x

theorem

exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing

L836 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

theorem IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing
    (𝓞 : Type*) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞]
    (M : Type*) [AddCommGroup M] [Module 𝓞 M] [Module.Finite 𝓞 M]
    (hM : 0 < Module.depth 𝓞 M) :
    ∃ x ∈ maximalIdeal 𝓞,
      x ∉ (maximalIdeal 𝓞) ^ 2 ∧ IsSMulRegular 𝓞 x ∧ IsSMulRegular M x

lemma

exists_isWeaklyRegular_of_le_depth

L885 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.exists_isWeaklyRegular_of_le_depth

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Transport
variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

lemma exists_isWeaklyRegular_of_le_depth (M : Type*) [AddCommGroup M] [Module R M]
    (n : ℕ) (hn : (n : ℕ∞) ≤ Module.depth R M) :
    ∃ s : List R, Sequence.IsWeaklyRegular M s ∧ (∀ r ∈ s, r ∈ maximalIdeal R) ∧
      s.length = n

lemma

quotSMulTopQuotSMulTopEquivSup

L915 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.quotSMulTopQuotSMulTopEquivSup

Documentation

Identify successive scalar quotients with the quotient by the sum of the two scalar-multiple submodules.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Transport
variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
variable (M) in

Lean source · statement

def quotSMulTopQuotSMulTopEquivSup (M : Type*) [AddCommGroup M] [Module R M] (z x : R) :
    QuotSMulTop x (QuotSMulTop z M) ≃ₗ[R]
      M ⧸ (z • (⊤ : Submodule R M) ⊔ x • (⊤ : Submodule R M))

def

eq_zero_of_maximalIdeal_smul_eq_zero

L936 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.eq_zero_of_maximalIdeal_smul_eq_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Elementary
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

lemma eq_zero_of_maximalIdeal_smul_eq_zero {x y₁ y₂ : R} (hxreg : IsSMulRegular M x)
    (hy : Sequence.IsWeaklyRegular M [y₁, y₂])
    (hy₁ : y₁ ∈ maximalIdeal R) (hy₂ : y₂ ∈ maximalIdeal R)
    (m₀ : QuotSMulTop x M) (hm₀ : ∀ a ∈ maximalIdeal R, a • m₀ = 0) : m₀ = 0

lemma

not_isAssociatedPrime_maximalIdeal_of_isSMulRegular

L976 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.not_isAssociatedPrime_maximalIdeal_of_isSMulRegular

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section AssociatedPrimes
variable [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

lemma not_isAssociatedPrime_maximalIdeal_of_isSMulRegular {x : R}
    (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    ¬ IsAssociatedPrime (maximalIdeal R) M

lemma

not_isAssociatedPrime_maximalIdeal_quotSMulTop

L996 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.not_isAssociatedPrime_maximalIdeal_quotSMulTop

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section AssociatedPrimes
variable [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable (M) in

Lean source · statement

lemma not_isAssociatedPrime_maximalIdeal_quotSMulTop {x : R} (hxreg : IsSMulRegular M x)
    (hdepth : (2 : ℕ∞) ≤ Module.depth R M) :
    ¬ IsAssociatedPrime (maximalIdeal R) (QuotSMulTop x M)

lemma

exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

L1021 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section AssociatedPrimes
variable [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable (M) in

Lean source · statement

lemma exists_mem_maximalIdeal_isSMulRegular_isSMulRegular
    (N₁ N₂ : Type*) [AddCommGroup N₁] [Module R N₁] [Module.Finite R N₁]
    [AddCommGroup N₂] [Module R N₂] [Module.Finite R N₂]
    (h₁ : ¬ IsAssociatedPrime (maximalIdeal R) N₁)
    (h₂ : ¬ IsAssociatedPrime (maximalIdeal R) N₂) :
    ∃ z ∈ maximalIdeal R, IsSMulRegular N₁ z ∧ IsSMulRegular N₂ z

lemma

le_depth_quotSMulTop_of_succ_le_depth

L1088 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.le_depth_quotSMulTop_of_succ_le_depth

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section DepthDrop
variable [IsNoetherianRing R]

Lean source · statement

lemma le_depth_quotSMulTop_of_succ_le_depth
    (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {x : R} (hx : x ∈ maximalIdeal R) (n : ℕ) (hxreg : IsSMulRegular M x)
    (hd : ((n + 1 : ℕ) : ℕ∞) ≤ Module.depth R M) :
    (n : ℕ∞) ≤ Module.depth R (QuotSMulTop x M)

theorem

isLocalRing_quotient_span_singleton

L1260 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.isLocalRing_quotient_span_singleton

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section QuotientCurrency

Lean source · statement

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

theorem

depth_quotient_quotSMulTop_succ_eq

L1272 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_quotient_quotSMulTop_succ_eq

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section QuotientCurrency
variable [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem depth_quotient_quotSMulTop_succ_eq {x : R} [IsLocalRing (R ⧸ Ideal.span {x})]
    (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    Module.depth (R ⧸ Ideal.span {x}) (QuotSMulTop x M) + 1 = Module.depth R M

theorem

depth_quotient_quotSMulTop_eq_sub_one

L1278 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_quotient_quotSMulTop_eq_sub_one

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section QuotientCurrency
variable [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem depth_quotient_quotSMulTop_eq_sub_one {x : R} [IsLocalRing (R ⧸ Ideal.span {x})]
    (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    Module.depth (R ⧸ Ideal.span {x}) (QuotSMulTop x M) = Module.depth R M - 1

theorem

ringKrullDim_quotient_span_singleton_succ

L1295 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section KrullDim
variable (R) [IsNoetherianRing R]

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ {x : R}
    (hxreg : IsSMulRegular R x) (hx : x ∈ maximalIdeal R) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

ringKrullDim_quotient_span_singleton_succ_of_ne_zero

L1300 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ_of_ne_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section KrullDim
variable (R) [IsNoetherianRing R]

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ_of_ne_zero [IsDomain R] {x : R}
    (hx0 : x ≠ 0) (hx : x ∈ maximalIdeal R) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

ringKrullDim_quotient_span_singleton_succ_of_regular_parameter

L1306 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ_of_regular_parameter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section KrullDim
variable (R) [IsNoetherianRing R]

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ_of_regular_parameter [IsDomain R] {x : R}
    (hx : x ∈ maximalIdeal R) (hx2 : x ∉ (maximalIdeal R) ^ 2) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

ringKrullDim_eq_succ_of_quotient_span_singleton_eq

L1312 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.ringKrullDim_eq_succ_of_quotient_span_singleton_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section KrullDim
variable (R) [IsNoetherianRing R]

Lean source · statement

theorem ringKrullDim_eq_succ_of_quotient_span_singleton_eq {x : R}
    (hxreg : IsSMulRegular R x) (hx : x ∈ maximalIdeal R) {d : ℕ}
    (hd : ringKrullDim (R ⧸ Ideal.span {x}) = ((d : ℕ) : WithBot ℕ∞)) :
    ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞)

theorem

ringKrullDim_quotient_span_singleton_of_ringKrullDim_eq

L1319 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.ringKrullDim_quotient_span_singleton_of_ringKrullDim_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section KrullDim
variable (R) [IsNoetherianRing R]

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_of_ringKrullDim_eq {x : R}
    (hxreg : IsSMulRegular R x) (hx : x ∈ maximalIdeal R) {d : ℕ}
    (hd : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞)) :
    ringKrullDim (R ⧸ Ideal.span {x}) = ((d : ℕ) : WithBot ℕ∞)

instance

exists_isSMulRegular_of_notMem_associatedPrimes

L1383 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.exists_isSMulRegular_of_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

lemma Module.exists_isSMulRegular_of_notMem_associatedPrimes
    (h : maximalIdeal R ∉ associatedPrimes R M) :
    ∃ x ∈ maximalIdeal R, IsSMulRegular M x

lemma

depth_pos_of_maximalIdeal_notMem_associatedPrimes

L1392 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_pos_of_maximalIdeal_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

lemma Module.depth_pos_of_maximalIdeal_notMem_associatedPrimes
    (h : maximalIdeal R ∉ associatedPrimes R M) : 0 < Module.depth R M

theorem

depth_pos_iff_maximalIdeal_notMem_associatedPrimes

L1397 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_pos_iff_maximalIdeal_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem Module.depth_pos_iff_maximalIdeal_notMem_associatedPrimes :
    0 < Module.depth R M ↔ maximalIdeal R ∉ associatedPrimes R M

theorem

depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes

L1402 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem Module.depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes :
    Module.depth R M = 0 ↔ maximalIdeal R ∈ associatedPrimes R M

theorem

depth_pos_iff_not_isAssociatedPrime_maximalIdeal

L1415 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_pos_iff_not_isAssociatedPrime_maximalIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem Module.depth_pos_iff_not_isAssociatedPrime_maximalIdeal :
    0 < Module.depth R M ↔ ¬ IsAssociatedPrime (maximalIdeal R) M

theorem

depth_eq_zero_iff_isAssociatedPrime_maximalIdeal

L1425 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_eq_zero_iff_isAssociatedPrime_maximalIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

theorem Module.depth_eq_zero_iff_isAssociatedPrime_maximalIdeal :
    Module.depth R M = 0 ↔ IsAssociatedPrime (maximalIdeal R) M

theorem

depth_eq_top_and_associatedPrimes_eq_empty_of_subsingleton

L1442 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_eq_top_and_associatedPrimes_eq_empty_of_subsingleton

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Degeneration
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

theorem Module.depth_eq_top_and_associatedPrimes_eq_empty_of_subsingleton [Subsingleton M] :
    Module.depth R M = ⊤ ∧ associatedPrimes R M = ∅

theorem

depth_pos_and_maximalIdeal_notMem_associatedPrimes_of_subsingleton

L1446 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_pos_and_maximalIdeal_notMem_associatedPrimes_of_subsingleton

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Degeneration
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

theorem Module.depth_pos_and_maximalIdeal_notMem_associatedPrimes_of_subsingleton
    [Subsingleton M] :
    0 < Module.depth R M ∧ maximalIdeal R ∉ associatedPrimes R M

theorem

gate_dvr_maximalIdeal_notMem_associatedPrimes

L1460 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.DepthZeroAssociatedPrime.gate_dvr_maximalIdeal_notMem_associatedPrimes

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

theorem gate_dvr_maximalIdeal_notMem_associatedPrimes
    (𝓞 : Type*) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞] :
    maximalIdeal 𝓞 ∉ associatedPrimes 𝓞 𝓞

theorem

gate_field_maximalIdeal_mem_associatedPrimes

L1484 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.DepthZeroAssociatedPrime.gate_field_maximalIdeal_mem_associatedPrimes

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

theorem gate_field_maximalIdeal_mem_associatedPrimes (K : Type*) [Field K] :
    maximalIdeal K ∈ associatedPrimes K K

theorem

gate_field_maximalIdeal_mem_associatedPrimes_via_depth

L1498 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.DepthZeroAssociatedPrime.gate_field_maximalIdeal_mem_associatedPrimes_via_depth

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

theorem gate_field_maximalIdeal_mem_associatedPrimes_via_depth (K : Type*) [Field K] :
    maximalIdeal K ∈ associatedPrimes K K

theorem

gate_rat_depth_eq_zero_and_mem

L1503 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.DepthZeroAssociatedPrime.gate_rat_depth_eq_zero_and_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

theorem gate_rat_depth_eq_zero_and_mem :
    Module.depth ℚ ℚ = 0 ∧ maximalIdeal ℚ ∈ associatedPrimes ℚ ℚ

lemma

ringKrullDim_quotient_succ_le_of_lt

L1522 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.ringKrullDim_quotient_succ_le_of_lt

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section DimensionDrop
variable {R : Type*} [CommRing R]

Lean source · statement

lemma ringKrullDim_quotient_succ_le_of_lt {p q : Ideal R} [p.IsPrime] (hpq : p < q) :
    ringKrullDim (R ⧸ q) + 1 ≤ ringKrullDim (R ⧸ p)

def

exists_forall_smul_eq_zero_notMem_smul_top

L1560 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsAssociatedPrime.exists_forall_smul_eq_zero_notMem_smul_top

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section NakayamaStep
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

lemma IsAssociatedPrime.exists_forall_smul_eq_zero_notMem_smul_top
    [Module.Finite R M] {p : Ideal R} (hp : IsAssociatedPrime p M)
    {x : R} (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    ∃ k : M, (∀ a ∈ p, a • k = 0) ∧ k ∉ x • (⊤ : Submodule R M)

lemma

exists_isAssociatedPrime_quotSMulTop_le

L1605 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsAssociatedPrime.exists_isAssociatedPrime_quotSMulTop_le

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section NakayamaStep
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

lemma IsAssociatedPrime.exists_isAssociatedPrime_quotSMulTop_le
    [Module.Finite R M] {p : Ideal R} (hp : IsAssociatedPrime p M)
    {x : R} (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    ∃ q : Ideal R, IsAssociatedPrime q (QuotSMulTop x M) ∧ p ≤ q ∧ x ∈ q

lemma

depth_le_ringKrullDim_quotient_aux

L1633 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.depth_le_ringKrullDim_quotient_aux

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

lemma depth_le_ringKrullDim_quotient_aux (n : ℕ) :
    ∀ (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] (p : Ideal R),
      IsAssociatedPrime p M → (n : ℕ∞) ≤ Module.depth R M →
      ((n : ℕ) : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ p)

lemma

natCast_le_ringKrullDim_quotient_of_le_depth

L1671 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.natCast_le_ringKrullDim_quotient_of_le_depth

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

lemma Module.natCast_le_ringKrullDim_quotient_of_le_depth (n : ℕ)
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {p : Ideal R} (hp : p ∈ associatedPrimes R M)
    (hn : (n : ℕ∞) ≤ Module.depth R M) :
    ((n : ℕ) : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ p)

theorem

depth_le_ringKrullDim_quotient_of_mem_associatedPrimes

L1678 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_le_ringKrullDim_quotient_of_mem_associatedPrimes

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem Module.depth_le_ringKrullDim_quotient_of_mem_associatedPrimes
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {p : Ideal R} (hp : p ∈ associatedPrimes R M) :
    .some (Module.depth R M) ≤ ringKrullDim (R ⧸ p)

theorem

depth_le_ringKrullDim_quotient_of_isAssociatedPrime

L1693 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.depth_le_ringKrullDim_quotient_of_isAssociatedPrime

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem Module.depth_le_ringKrullDim_quotient_of_isAssociatedPrime
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {p : Ideal R} (hp : IsAssociatedPrime p M) :
    .some (Module.depth R M) ≤ ringKrullDim (R ⧸ p)

theorem

ringKrullDim_quotient_eq_of_mem_associatedPrimes

L1711 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_quotient_eq_of_mem_associatedPrimes

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim

Lean source · statement

theorem ringKrullDim_quotient_eq_of_mem_associatedPrimes {d : ℕ}
    (hCM : IsCohenMacaulayOfDim R d) {p : Ideal R}
    (hp : p ∈ associatedPrimes R R) :
    ringKrullDim (R ⧸ p) = ringKrullDim R

theorem

mem_minimalPrimes_of_mem_associatedPrimes

L1721 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.mem_minimalPrimes_of_mem_associatedPrimes

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim

Lean source · statement

theorem mem_minimalPrimes_of_mem_associatedPrimes {d : ℕ}
    (hCM : IsCohenMacaulayOfDim R d) {p : Ideal R}
    (hp : p ∈ associatedPrimes R R) :
    p ∈ minimalPrimes R

lemma

isCohenMacaulayOfDim_of_depth_eq_ringKrullDim

L1742 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.isCohenMacaulayOfDim_of_depth_eq_ringKrullDim

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

lemma isCohenMacaulayOfDim_of_depth_eq_ringKrullDim
    (h : .some (Module.depth R R) = ringKrullDim R) :
    ∃ d : ℕ, IsCohenMacaulayOfDim R d

theorem

mem_minimalPrimes_of_mem_associatedPrimes_of_depth_eq_ringKrullDim

L1754 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.mem_minimalPrimes_of_mem_associatedPrimes_of_depth_eq_ringKrullDim

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem mem_minimalPrimes_of_mem_associatedPrimes_of_depth_eq_ringKrullDim
    (h : .some (Module.depth R R) = ringKrullDim R)
    {p : Ideal R} (hp : p ∈ associatedPrimes R R) :
    p ∈ minimalPrimes R

theorem

span_eq_top_of_span_quotientMk_eq_top

L1884 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.QuotSMulTop.span_eq_top_of_span_quotientMk_eq_top

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
open IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.QuotSMulTop
section Engines
variable [IsLocalRing R] (x : R)

Lean source · full declaration

theorem span_eq_top_of_span_quotientMk_eq_top [Module.Finite R M]
    (hx : x ∈ maximalIdeal R) {ι : Type*} (m : ι → M)
    (hspan : Submodule.span (R ⧸ Ideal.span {x})
      (Set.range fun i => (Submodule.Quotient.mk (m i) : QuotSMulTop x M)) = ⊤) :
    Submodule.span R (Set.range m) = ⊤ := by
  have h1 : Submodule.span R
      (Set.range fun i => (Submodule.Quotient.mk (m i) : QuotSMulTop x M)) = ⊤ := by
    rw [← Submodule.restrictScalars_span R (R ⧸ Ideal.span {x}) Ideal.Quotient.mk_surjective,
      hspan, Submodule.restrictScalars_top]
  have h2 : (Submodule.span R (Set.range m)).map
      (Submodule.mkQ (x • ⊤ : Submodule R M)) = ⊤ := by
    rw [Submodule.map_span, ← Set.range_comp]
    exact h1
  rw [Submodule.map_mkQ_eq_top] at h2
  refine top_le_iff.mp (Submodule.le_of_le_smul_of_le_jacobson_bot Module.Finite.fg_top
    (span_le_jacobson_bot x hx) ?_)
  rw [Submodule.ideal_span_singleton_smul, sup_comm, h2]

theorem

linearIndependent_of_quotientMk_linearIndependent

L1902 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.QuotSMulTop.linearIndependent_of_quotientMk_linearIndependent

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
open IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.QuotSMulTop
section Engines
variable [IsLocalRing R] (x : R)

Lean source · full declaration

theorem linearIndependent_of_quotientMk_linearIndependent [IsNoetherianRing R]
    (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular M x) {ι : Type*} [Finite ι] (m : ι → M)
    (hli : LinearIndependent (R ⧸ Ideal.span {x})
      (fun i => (Submodule.Quotient.mk (m i) : QuotSMulTop x M))) :
    LinearIndependent R m := by
  classical
  let : Fintype ι := Fintype.ofFinite ι
  have hker_le : LinearMap.ker (Fintype.linearCombination R m) ≤
      Ideal.span {x} • LinearMap.ker (Fintype.linearCombination R m) := by
    intro a ha
    rw [LinearMap.mem_ker, Fintype.linearCombination_apply] at ha
    have hcoeff : ∀ i, Ideal.Quotient.mk (Ideal.span {x}) (a i) = 0 := by
      have h0 : ∑ i, (Ideal.Quotient.mk (Ideal.span {x}) (a i)) •
          (Submodule.Quotient.mk (m i) : QuotSMulTop x M) = 0 := by
        have hterm : ∀ i, (Ideal.Quotient.mk (Ideal.span {x}) (a i)) •
            (Submodule.Quotient.mk (m i) : QuotSMulTop x M)
            = (Submodule.mkQ (x • ⊤ : Submodule R M)) (a i • m i) := fun i => rfl
        simp_rw [hterm, ← map_sum, ha, map_zero]
      exact Fintype.linearIndependent_iff.mp hli _ h0
    have hdvd : ∀ i, x ∣ a i := fun i =>
      Ideal.mem_span_singleton.mp (Ideal.Quotient.eq_zero_iff_mem.mp (hcoeff i))
    choose c hc using hdvd
    have ha_eq : a = x • c := funext fun i => by
      rw [Pi.smul_apply, smul_eq_mul]; exact hc i
    have hc_ker : c ∈ LinearMap.ker (Fintype.linearCombination R m) := by
      rw [LinearMap.mem_ker]
      apply hreg
      change x • Fintype.linearCombination R m c = x • (0 : M)
      rw [smul_zero, ← map_smul, ← ha_eq]
      exact ha
    rw [ha_eq]
    exact Submodule.smul_mem_smul (Ideal.mem_span_singleton_self x) hc_ker
  have hker : LinearMap.ker (Fintype.linearCombination R m) = ⊥ :=
    Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (Ideal.span {x}) _
      (IsNoetherian.noetherian _) hker_le (span_le_jacobson_bot x hx)
  rw [Fintype.linearIndependent_iff]
  intro g hg i
  have hg_ker : g ∈ LinearMap.ker (Fintype.linearCombination R m) := by
    rw [LinearMap.mem_ker, Fintype.linearCombination_apply]
    exact hg
  rw [hker, Submodule.mem_bot] at hg_ker
  exact congrFun hg_ker i

theorem

free_of_quotSMulTop_free_of_regular_param

L1993 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.Module.free_of_quotSMulTop_free_of_regular_param

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
section MainTheorems
variable [IsLocalRing R] [IsNoetherianRing R] [Module.Finite R M]

Lean source · statement

theorem Module.free_of_quotSMulTop_free_of_regular_param (x : R)
    (hx : x ∈ IsLocalRing.maximalIdeal R) (_hx2 : x ∉ (IsLocalRing.maximalIdeal R) ^ 2)
    (_hregR : IsSMulRegular R x) (hregM : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    Module.Free R M

theorem

isLocalRing_quotient_span_singleton

L2032 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.isLocalRing_quotient_span_singleton

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
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

isScalarTower_quotient_span_singleton

L2041 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.isScalarTower_quotient_span_singleton

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

theorem isScalarTower_quotient_span_singleton {M : Type v} [AddCommGroup M] [Module R M]
    (x : R) : IsScalarTower R (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

theorem

moduleFinite_quotient_span_singleton

L2047 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.moduleFinite_quotient_span_singleton

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

theorem moduleFinite_quotient_span_singleton {M : Type v} [AddCommGroup M] [Module R M]
    [Module.Finite R M] (x : R) :
    Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

theorem

nontrivial_quotSMulTop_of_mem_maximalIdeal

L2053 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.nontrivial_quotSMulTop_of_mem_maximalIdeal

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

theorem nontrivial_quotSMulTop_of_mem_maximalIdeal [IsLocalRing R] {M : Type v}
    [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] {x : R}
    (hx : x ∈ maximalIdeal R) : Nontrivial (QuotSMulTop x M)

theorem

exists_ringKrullDim_eq_natCast

L2063 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.exists_ringKrullDim_eq_natCast

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
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

isField_of_spanFinrank_maximalIdeal_eq_zero

L2080 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.isField_of_spanFinrank_maximalIdeal_eq_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section BaseCase
variable (R : Type u) [CommRing R] [IsRegularLocalRing R]

Lean source · statement

theorem isField_of_spanFinrank_maximalIdeal_eq_zero
    (hn : (maximalIdeal R).spanFinrank = 0) : IsField R

theorem

free_of_spanFinrank_maximalIdeal_eq_zero

L2088 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.free_of_spanFinrank_maximalIdeal_eq_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section BaseCase
variable (R : Type u) [CommRing R] [IsRegularLocalRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]

Lean source · statement

theorem free_of_spanFinrank_maximalIdeal_eq_zero
    (hn : (maximalIdeal R).spanFinrank = 0) : Module.Free R M

theorem

exists_finite_span_eq_maximalIdeal_mem

L2105 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.exists_finite_span_eq_maximalIdeal_mem

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Exchange
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

isRegularLocalRing_quotient_span_singleton

L2170 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.isRegularLocalRing_quotient_span_singleton

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Exchange
variable (R : Type u) [CommRing R]
variable [IsRegularLocalRing R]

Lean source · statement

theorem isRegularLocalRing_quotient_span_singleton
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2)
    (hxreg : IsSMulRegular R x) [IsLocalRing (R ⧸ Ideal.span {x})] :
    IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧
      (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1 =
        (maximalIdeal R).spanFinrank

def

free_of_depth_eq_ringKrullDim_aux

L2280 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_aux

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Assembly

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_aux
    (hsel : JointRegularElementSelection.{u, v})
    (hdrop : DepthDropQuotient.{u, v})
    (hstep : QuotientInductionStep.{u, v}) :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R]
      (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M],
      (maximalIdeal R).spanFinrank = n →
      .some (Module.depth R M) = ringKrullDim R → Module.Free R M

theorem

free_of_depth_eq_ringKrullDim_of_dim_zero

L2346 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_of_dim_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Assembly

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_of_dim_zero
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (hdim : ringKrullDim R = 0) : Module.Free R M

theorem

jointRegularElementSelection_of_regularPositiveDepth

L2366 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.jointRegularElementSelection_of_regularPositiveDepth

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section SiblingWiring

Lean source · statement

theorem jointRegularElementSelection_of_regularPositiveDepth
    (hbridge : RegularPositiveDepth.{u}) : JointRegularElementSelection.{u, v}

theorem

free_of_depth_eq_ringKrullDim_of_landed_siblings

L2372 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_of_landed_siblings

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section SiblingWiring

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_of_landed_siblings
    (hbridge : RegularPositiveDepth.{u})
    (hdrop : DepthDropQuotient.{u, v})
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (H : .some (Module.depth R M) = ringKrullDim R) : Module.Free R M

theorem

maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos

L2411 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open 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

L2428 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.exists_parameter_notMem_minimalPrimes

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open 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

ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes

L2479 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open 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

L2489 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open 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

L2505 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open 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

L2584 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.isDomain_of_isRegularLocalRing_aux

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open 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

L2638 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.isDomain_of_isRegularLocalRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section MatsumuraDomain

Lean source · statement

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

theorem

depth_self_pos_of_isRegularLocalRing

L2646 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.depth_self_pos_of_isRegularLocalRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section PositiveDepth

Lean source · statement

theorem depth_self_pos_of_isRegularLocalRing (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (hdim : 0 < ringKrullDim R) : 0 < Module.depth R R

theorem

jointRegularElementSelection_holds

L2663 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.jointRegularElementSelection_holds

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Unconditional

Lean source · statement

theorem jointRegularElementSelection_holds : JointRegularElementSelection.{u, v}

theorem

free_of_depth_eq_ringKrullDim_unconditional

L2666 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_unconditional

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Unconditional

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_unconditional
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (H : .some (Module.depth R M) = ringKrullDim R) : Module.Free R M

def

cmUnmixednessHypothesis_of_depth_le_dim

L2697 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.cmUnmixednessHypothesis_of_depth_le_dim

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem cmUnmixednessHypothesis_of_depth_le_dim
    (h : ∀ (S : Type u) [CommRing S] [IsLocalRing S] [IsNoetherianRing S],
      ∀ p ∈ associatedPrimes S S,
        (.some (Module.depth S S) : WithBot ℕ∞) ≤ ringKrullDim (S ⧸ p)) :
    CMUnmixednessHypothesis.{u}

theorem

isAssociatedPrime_eq_bot_of_isDomain

L2707 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.isAssociatedPrime_eq_bot_of_isDomain

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isAssociatedPrime_eq_bot_of_isDomain {S : Type u} [CommRing S] [IsDomain S]
    [IsNoetherianRing S] {p : Ideal S} (hp : IsAssociatedPrime p S) : p = ⊥

theorem

depth_le_ringKrullDim_quotient_of_isDomain

L2732 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.depth_le_ringKrullDim_quotient_of_isDomain

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem depth_le_ringKrullDim_quotient_of_isDomain (S : Type u) [CommRing S] [IsLocalRing S]
    [IsNoetherianRing S] [IsDomain S] :
    ∀ p ∈ associatedPrimes S S,
      (.some (Module.depth S S) : WithBot ℕ∞) ≤ ringKrullDim (S ⧸ p)

theorem

exists_ringKrullDim_eq_natCast

L2741 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.exists_ringKrullDim_eq_natCast

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

eq_maximalIdeal_of_ringKrullDim_quotient_le_zero

L2751 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.eq_maximalIdeal_of_ringKrullDim_quotient_le_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem eq_maximalIdeal_of_ringKrullDim_quotient_le_zero {R : Type u} [CommRing R]
    [IsLocalRing R] {p : Ideal R} [p.IsPrime]
    (h : ringKrullDim (R ⧸ p) ≤ 0) : p = maximalIdeal R

theorem

notMem_of_ringKrullDim_quotient_cons_le_zero

L2761 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.notMem_of_ringKrullDim_quotient_cons_le_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem notMem_of_ringKrullDim_quotient_cons_le_zero {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] {x : R} {rest : List R}
    (hmem : ∀ y ∈ x :: rest, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList (x :: rest)) ≤ 0)
    {p : Ideal R} (hp : p.IsPrime)
    (hpdim : ringKrullDim (R ⧸ p) = ringKrullDim R)
    (hlen : ((rest.length : ℕ) : WithBot ℕ∞) < ringKrullDim R) :
    x ∉ p

theorem

isRegular_of_sop_of_cmUnmixedness

L2820 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.isRegular_of_sop_of_cmUnmixedness

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isRegular_of_sop_of_cmUnmixedness (hunmix : CMUnmixednessHypothesis.{u}) :
    ∀ (d : ℕ) (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R],
      (.some (Module.depth R R) : WithBot ℕ∞) = ringKrullDim R →
      ringKrullDim R = (d : WithBot ℕ∞) →
      ∀ xs : List R, xs.length = d →
        (∀ y ∈ xs, y ∈ maximalIdeal R) →
        ringKrullDim (R ⧸ Ideal.ofList xs) = 0 →
        Sequence.IsRegular R xs

theorem

isRegular_of_sop_of_ringKrullDim_eq_zero

L2931 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.isRegular_of_sop_of_ringKrullDim_eq_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isRegular_of_sop_of_ringKrullDim_eq_zero {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R]
    (_hdim : ringKrullDim R = (0 : WithBot ℕ∞))
    (xs : List R) (hlen : xs.length = 0) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop_of_ringKrullDim_eq_one

L2940 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.isRegular_of_sop_of_ringKrullDim_eq_one

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isRegular_of_sop_of_ringKrullDim_eq_one {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R]
    (hCM : (.some (Module.depth R R) : WithBot ℕ∞) = ringKrullDim R)
    (hdim : ringKrullDim R = ((1 : ℕ) : WithBot ℕ∞))
    (xs : List R) (hlen : xs.length = 1)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList xs) = 0) :
    Sequence.IsRegular R xs

theorem

ne_top_of_radical_eq_maximalIdeal

L3020 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.ne_top_of_radical_eq_maximalIdeal

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem ne_top_of_radical_eq_maximalIdeal {I : Ideal R}
    (hrad : I.radical = maximalIdeal R) : I ≠ ⊤

theorem

isPrime_quotient_eq_map_maximalIdeal_of_radical_eq_maximalIdeal

L3027 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.isPrime_quotient_eq_map_maximalIdeal_of_radical_eq_maximalIdeal

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem isPrime_quotient_eq_map_maximalIdeal_of_radical_eq_maximalIdeal {I : Ideal R}
    (hrad : I.radical = maximalIdeal R) (P : Ideal (R ⧸ I)) (hP : P.IsPrime) :
    P = Ideal.map (Ideal.Quotient.mk I) (maximalIdeal R)

theorem

ringKrullDim_quotient_eq_zero_of_radical_eq_maximalIdeal

L3045 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.ringKrullDim_quotient_eq_zero_of_radical_eq_maximalIdeal

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem ringKrullDim_quotient_eq_zero_of_radical_eq_maximalIdeal {I : Ideal R}
    (hrad : I.radical = maximalIdeal R) :
    ringKrullDim (R ⧸ I) = 0

theorem

eq_maximalIdeal_of_isPrime_of_le_of_ringKrullDim_quotient_le_zero

L3061 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.eq_maximalIdeal_of_isPrime_of_le_of_ringKrullDim_quotient_le_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem eq_maximalIdeal_of_isPrime_of_le_of_ringKrullDim_quotient_le_zero {I p : Ideal R}
    (hdim : ringKrullDim (R ⧸ I) ≤ 0) (hp : p.IsPrime) (hIp : I ≤ p) :
    p = maximalIdeal R

theorem

radical_eq_maximalIdeal_of_ringKrullDim_quotient_eq_zero

L3072 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.radical_eq_maximalIdeal_of_ringKrullDim_quotient_eq_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem radical_eq_maximalIdeal_of_ringKrullDim_quotient_eq_zero {I : Ideal R}
    (hne : I ≠ ⊤) (hdim : ringKrullDim (R ⧸ I) = 0) :
    I.radical = maximalIdeal R

theorem

radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero

L3083 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero (I : Ideal R) :
    I.radical = maximalIdeal R ↔ (I ≠ ⊤ ∧ ringKrullDim (R ⧸ I) = 0)

theorem

radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero_of_noetherian

L3089 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero_of_noetherian

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero_of_noetherian
    [IsNoetherianRing R] (I : Ideal R) :
    I.radical = IsLocalRing.maximalIdeal R ↔ (I ≠ ⊤ ∧ ringKrullDim (R ⧸ I) = 0)

theorem

ofList_ne_top_of_forall_mem_maximalIdeal

L3094 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.ofList_ne_top_of_forall_mem_maximalIdeal

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem ofList_ne_top_of_forall_mem_maximalIdeal {xs : List R}
    (hmem : ∀ x ∈ xs, x ∈ maximalIdeal R) :
    Ideal.ofList xs ≠ ⊤

theorem

ofList_radical_eq_maximalIdeal_iff_ringKrullDim_quotient_eq_zero

L3100 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.ofList_radical_eq_maximalIdeal_iff_ringKrullDim_quotient_eq_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem ofList_radical_eq_maximalIdeal_iff_ringKrullDim_quotient_eq_zero {xs : List R}
    (hmem : ∀ x ∈ xs, x ∈ maximalIdeal R) :
    (Ideal.ofList xs).radical = maximalIdeal R ↔
      ringKrullDim (R ⧸ Ideal.ofList xs) = 0

def

matsumuraThm174iiiSopRegularRowRadicalForm

L3109 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowRadicalForm

Documentation

The regular-sequence assertion for a parameter list of the Cohen-Macaulay dimension whose generated ideal has maximal-ideal radical.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

def matsumuraThm174iiiSopRegularRowRadicalForm (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] : Prop

def

matsumuraThm174iiiSopRegularRowQuotientDimForm

L3120 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowQuotientDimForm

Documentation

The regular-sequence assertion for a parameter list of the Cohen-Macaulay dimension whose generated ideal gives a zero-dimensional quotient.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

def matsumuraThm174iiiSopRegularRowQuotientDimForm (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] : Prop

theorem

matsumuraThm174iiiSopRegularRow_radicalForm_iff_quotientDimForm

L3129 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRow_radicalForm_iff_quotientDimForm

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem matsumuraThm174iiiSopRegularRow_radicalForm_iff_quotientDimForm
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowRadicalForm R ↔
      matsumuraThm174iiiSopRegularRowQuotientDimForm R

theorem

matsumuraThm174iiiSopRegularRowQuotientDimForm_of_cmUnmixedness

L3141 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowQuotientDimForm_of_cmUnmixedness

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowQuotientDimForm_of_cmUnmixedness
    (hunmix : CMUnmixednessHypothesis.{u}) (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowQuotientDimForm R

theorem

matsumuraThm174iiiSopRegularRowRadicalForm_of_cmUnmixedness

L3147 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowRadicalForm_of_cmUnmixedness

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowRadicalForm_of_cmUnmixedness
    (hunmix : CMUnmixednessHypothesis.{u}) (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowRadicalForm R

theorem

isRegular_of_sop_radical

L3154 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.isRegular_of_sop_radical

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem IsCohenMacaulayOfDim.isRegular_of_sop_radical {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] {d : ℕ} (hCM : IsCohenMacaulayOfDim R d)
    (hunmix : CMUnmixednessHypothesis.{u})
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hrad : (Ideal.ofList xs).radical = maximalIdeal R) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop_radical_of_ringKrullDim_eq_one

L3164 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.isRegular_of_sop_radical_of_ringKrullDim_eq_one

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem isRegular_of_sop_radical_of_ringKrullDim_eq_one {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R]
    (hCM : (.some (Module.depth R R) : WithBot ℕ∞) = ringKrullDim R)
    (hdim : ringKrullDim R = ((1 : ℕ) : WithBot ℕ∞))
    (xs : List R) (hlen : xs.length = 1)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hrad : (Ideal.ofList xs).radical = maximalIdeal R) :
    Sequence.IsRegular R xs

theorem

cmUnmixednessHypothesis_holds

L3175 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.cmUnmixednessHypothesis_holds

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem cmUnmixednessHypothesis_holds : CMUnmixednessHypothesis.{u}

theorem

matsumuraThm174iiiSopRegularRowQuotientDimForm_holds

L3180 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowQuotientDimForm_holds

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowQuotientDimForm_holds (R : Type u) [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowQuotientDimForm R

theorem

matsumuraThm174iiiSopRegularRowRadicalForm_holds

L3186 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowRadicalForm_holds

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowRadicalForm_holds (R : Type u) [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowRadicalForm R

theorem

isRegular_of_sop_unconditional

L3191 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.isRegular_of_sop_unconditional

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem IsCohenMacaulayOfDim.isRegular_of_sop_unconditional {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] {d : ℕ} (hCM : IsCohenMacaulayOfDim R d)
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList xs) = 0) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop_radical_unconditional

L3199 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isRegular_of_systemOfParameters.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.isRegular_of_sop_radical_unconditional

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem IsCohenMacaulayOfDim.isRegular_of_sop_radical_unconditional {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] {d : ℕ} (hCM : IsCohenMacaulayOfDim R d)
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hrad : (Ideal.ofList xs).radical = maximalIdeal R) :
    Sequence.IsRegular R xs

theorem

isRegular_of_systemOfParameters

L3214 ↗

IsLocalRing.isRegular_of_systemOfParameters

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isRegular_of_systemOfParameters
open IsLocalRing RingTheory

Lean source · statement

theorem _root_.IsLocalRing.isRegular_of_systemOfParameters
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hCM : (Module.depth R R : WithBot ℕ∞) = ringKrullDim R)
    {d : ℕ} (hdim : ringKrullDim R = d)
    (xs : List R) (hlen : xs.length = d) (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList xs) = 0) :
    RingTheory.Sequence.IsRegular R xs

Module documentation

Is Local Ring is Regular of system Of Parameters

Declarations