Module

RegularLocalDepth.lean

Nyll.SchemeTheory.RingTheory.RegularLocalDepth

146 declarations indexed from sourceView source ↗

Module documentation

Depth of a regular local ring

The depth of a regular local ring equals its Krull dimension. Regular sequences and quotients by regular parameters supply the supporting induction and lifting arguments.

Imports16

Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.PowerSeries.Ideal
Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.PowerSeries.Inverse
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.Tactic.Choose
Mathlib.Tactic.Conv
Mathlib.Tactic.CrossRefAttribute
Mathlib.Tactic.Ext
Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.SimpRw
Mathlib.Tactic.TermCongr
Nyll.SchemeTheory.RingTheory.CohenMacaulay
Nyll.SchemeTheory.RingTheory.LocalAlgebra

Imported by5

instance

instSubsingletonQuotientOfSubsingleton

L68 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.Ws14Port.instSubsingletonQuotientOfSubsingleton

Source context 16 commands

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

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

L215 ↗

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

Source context 16 commands

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

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

L260 ↗

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

Source context 16 commands

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

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

L551 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L568 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L573 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L582 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L589 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L604 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L659 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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'

L670 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L679 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L690 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L703 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L749 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L779 ↗

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

Documentation

Identify successive quotients by two scalar multiples with the quotient by the sum of their 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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L799 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L839 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L859 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L884 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L951 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1123 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1135 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1141 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1158 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1163 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1169 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1175 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1182 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1246 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1255 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1260 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1265 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1278 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1288 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1305 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1309 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1323 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1347 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1361 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1366 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1385 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1423 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1468 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1496 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1534 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1541 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1556 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1574 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1584 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1606 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1618 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1747 ↗

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

Source context 18 commands

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

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

L1765 ↗

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

Source context 18 commands

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

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

L1856 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1895 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1904 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1910 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1916 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1926 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1943 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1951 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L1968 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2033 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2143 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2209 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2229 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2235 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2274 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2291 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2342 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2352 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2368 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2447 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2501 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2509 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

regularPositiveDepth_holds

L2518 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.Ws14Port.No4PatchingCore.regularPositiveDepth_holds

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_depth_self_eq_ringKrullDim
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 regularPositiveDepth_holds : RegularPositiveDepth.{u}

theorem

jointRegularElementSelection_holds

L2526 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

L2529 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.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 IsRegularLocalRing_depth_self_eq_ringKrullDim
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

theorem

regCM_aux

L2549 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_depth_self_eq_ringKrullDim.regCM_aux

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_depth_self_eq_ringKrullDim
open IsLocalRing RingTheory
open Ws14Port
open Ws14Port.No4PatchingCore
open _root_.IsLocalRing
open scoped Pointwise

Lean source · statement

theorem regCM_aux :
    ∀ (d : ℕ) (R : Type*) [CommRing R] [IsRegularLocalRing R],
      (maximalIdeal R).spanFinrank = d → Module.depth R R = (d : ℕ∞)

theorem

depth_self_eq_ringKrullDim

L2591 ↗

IsRegularLocalRing.depth_self_eq_ringKrullDim

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_depth_self_eq_ringKrullDim
open IsLocalRing RingTheory
open Ws14Port
open Ws14Port.No4PatchingCore
open _root_.IsLocalRing
open scoped Pointwise

Lean source · statement

theorem _root_.IsRegularLocalRing.depth_self_eq_ringKrullDim
    (R : Type*) [CommRing R] [IsRegularLocalRing R] :
    (Module.depth R R : WithBot ℕ∞) = ringKrullDim R

Module documentation

Depth of a regular local ring

Declarations