Module

RegularLocalDepthFreeness.lean

Nyll.SchemeTheory.RingTheory.RegularLocalDepthFreeness

145 declarations indexed from sourceView source ↗

Module documentation

Freeness from maximal depth over a regular local ring

A finite module over a regular local ring is free when its depth equals the Krull dimension of the ring. Regular parameters reduce the dimension, and bases lifted from regular quotients finish the induction.

Imports16

Mathlib.RingTheory.PowerSeries.Ideal
Lean.Elab.Command
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 by3

instance

instSubsingletonQuotientOfSubsingleton

L69 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.instSubsingletonQuotientOfSubsingleton

Source context 16 commands

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

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

length_le_depth

L73 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.length_le_depth

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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.length_le_depth (s : List R)
    (hs : Sequence.IsWeaklyRegular M s) (hs' : ∀ r ∈ s, r ∈ maximalIdeal R) :
    s.length ≤ Module.depth R M

lemma

depth_of_subsingleton

L78 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_of_subsingleton

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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.depth_of_subsingleton [Subsingleton M] :
    Module.depth R M = ⊤

lemma

depth_of_isScalarTower

L90 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_of_isScalarTower

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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.depth_of_isScalarTower :
    Module.depth R M ≤ Module.depth S M

lemma

depth_le_krullDim_support

L99 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_le_krullDim_support

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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
open scoped Pointwise in

Lean source · statement

lemma Module.depth_le_krullDim_support [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ Order.krullDim (Module.support R M)

lemma

depth_le_dim_annihilator

L189 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_le_dim_annihilator

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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.depth_le_dim_annihilator
    [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ ringKrullDim (R ⧸ Module.annihilator R M)

lemma

depth_le_dim

L195 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_le_dim

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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.depth_le_dim [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ ringKrullDim R

lemma

isSMulRegular_iff_of_free

L199 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.isSMulRegular_iff_of_free

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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 isSMulRegular_iff_of_free {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Nontrivial M] {r : R} :
    IsSMulRegular M r ↔ IsSMulRegular R r

lemma

isWeaklyRegular_of_subsingleton

L216 ↗

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

isWeaklyRegular_of_free_aux

L223 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_free_aux

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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
open scoped Pointwise TensorProduct in

Lean source · statement

lemma RingTheory.Sequence.isWeaklyRegular_of_free_aux
    {R : Type u} {M : Type max u v} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Nontrivial M] {s : List R} :
      Sequence.IsWeaklyRegular M s ↔ Sequence.IsWeaklyRegular R s

lemma

isWeaklyRegular_of_free

L246 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_free

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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_free
    {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Nontrivial M] {s : List R} :
      Sequence.IsWeaklyRegular M s ↔ Sequence.IsWeaklyRegular R s

lemma

depth_le_of_free

L254 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_le_of_free

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
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.depth_le_of_free [Module.Free R M] : Module.depth R R ≤ Module.depth R M

lemma

faithfulSMul_of_depth_eq_ringKrullDim

L261 ↗

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

isSMulRegular_X

L312 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.isSMulRegular_X

Source context 15 commands

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

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

Lean source · statement

lemma isSMulRegular_X : IsSMulRegular R⟦X⟧ (X : R⟦X⟧)

lemma

ker_constantCoeff

L318 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.ker_constantCoeff

Source context 15 commands

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

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

Lean source · statement

lemma ker_constantCoeff : RingHom.ker (constantCoeff (R := R)) = Ideal.span {(X : R⟦X⟧)}

def

quotSpanXEquiv

L324 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.quotSpanXEquiv

Documentation

Identify the power-series ring modulo its variable with the coefficient ring using the constant coefficient.

Source context 15 commands

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

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

Lean source · statement

def quotSpanXEquiv : (R⟦X⟧ ⧸ Ideal.span {(X : R⟦X⟧)}) ≃+* R

lemma

quotSpanXEquiv_mk

L329 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.quotSpanXEquiv_mk

Source context 15 commands

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

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

Lean source · statement

lemma quotSpanXEquiv_mk (f : R⟦X⟧) :
    quotSpanXEquiv (Ideal.Quotient.mk _ f) = constantCoeff f

lemma

smul_top_eq_span_X

L334 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.smul_top_eq_span_X

Source context 15 commands

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

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

Lean source · statement

lemma smul_top_eq_span_X :
    (X : R⟦X⟧) • (⊤ : Ideal R⟦X⟧) = Ideal.span {(X : R⟦X⟧)}

instance

instIsLocalRingPowerSeries'

L343 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'

Source context 17 commands

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

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

Lean source · statement

instance instIsLocalRingPowerSeries' : IsLocalRing R⟦X⟧

lemma

mem_maximalIdeal_iff

L346 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.mem_maximalIdeal_iff

Source context 17 commands

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

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

Lean source · statement

lemma mem_maximalIdeal_iff {f : R⟦X⟧} :
    f ∈ maximalIdeal R⟦X⟧ ↔ constantCoeff f ∈ maximalIdeal R

lemma

X_mem_maximalIdeal

L351 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.X_mem_maximalIdeal

Source context 17 commands

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

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

Lean source · statement

lemma X_mem_maximalIdeal : (X : R⟦X⟧) ∈ maximalIdeal R⟦X⟧

lemma

C_mem_maximalIdeal

L355 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.C_mem_maximalIdeal

Source context 17 commands

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

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

Lean source · statement

lemma C_mem_maximalIdeal {r : R} (hr : r ∈ maximalIdeal R) :
    (C r : R⟦X⟧) ∈ maximalIdeal R⟦X⟧

def

quotXSMulTopAddEquiv

L363 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.quotXSMulTopAddEquiv

Documentation

The additive identification of power series modulo multiplication by the variable with the coefficient ring.

Source context 15 commands

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

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

Lean source · statement

def quotXSMulTopAddEquiv : QuotSMulTop (X : R⟦X⟧) R⟦X⟧ ≃+ R

lemma

quotXSMulTopAddEquiv_mk

L368 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk

Source context 15 commands

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

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

Lean source · statement

lemma quotXSMulTopAddEquiv_mk (f : R⟦X⟧) :
    quotXSMulTopAddEquiv (Submodule.Quotient.mk f) = constantCoeff f

lemma

quotXSMulTopAddEquiv_smul

L375 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_smul

Source context 15 commands

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

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

Lean source · statement

lemma quotXSMulTopAddEquiv_smul (r : R) (m : QuotSMulTop (X : R⟦X⟧) R⟦X⟧) :
    quotXSMulTopAddEquiv ((C r : R⟦X⟧) • m) = r • quotXSMulTopAddEquiv m

lemma

isWeaklyRegular_X_cons_map_C

L381 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.isWeaklyRegular_X_cons_map_C

Source context 15 commands

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

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

Lean source · statement

lemma isWeaklyRegular_X_cons_map_C {s : List R} (hs : Sequence.IsWeaklyRegular R s) :
    Sequence.IsWeaklyRegular R⟦X⟧ ((X : R⟦X⟧) :: s.map C)

lemma

le_depth_of_isWeaklyRegular

L394 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.le_depth_of_isWeaklyRegular

Source context 17 commands

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

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

Lean source · statement

lemma le_depth_of_isWeaklyRegular {s : List R} (hs : Sequence.IsWeaklyRegular R s)
    (hs' : ∀ r ∈ s, r ∈ maximalIdeal R) :
    (s.length : ℕ∞) + 1 ≤ Module.depth R⟦X⟧ R⟦X⟧

lemma

natCast_succ_le_depth

L406 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.natCast_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace PowerSeries
open PowerSeries
variable {R : Type*} [CommRing R]
section Depth
variable (R) [IsLocalRing R]

Lean source · statement

lemma natCast_succ_le_depth {d : ℕ} (hd : (d : ℕ∞) ≤ Module.depth R R) :
    ((d + 1 : ℕ) : ℕ∞) ≤ Module.depth R⟦X⟧ R⟦X⟧

lemma

ringKrullDim_powerSeries

L431 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.ringKrullDim_powerSeries

Source context 17 commands

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

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

Lean source · statement

lemma ringKrullDim_powerSeries : ringKrullDim R⟦X⟧ = ringKrullDim R + 1

lemma

ringKrullDim_lt_top

L450 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_lt_top

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim
variable {R} {d : ℕ}

Lean source · statement

lemma ringKrullDim_lt_top [IsNoetherianRing R] (_ : IsCohenMacaulayOfDim R d) :
    ringKrullDim R < ⊤

lemma

patching_hypotheses

L454 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.patching_hypotheses

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim
variable {R} {d : ℕ}

Lean source · statement

lemma patching_hypotheses {Λ Rₒₒ : Type*} [CommRing Λ] [IsLocalRing Λ] [CommRing Rₒₒ]
    [IsLocalRing Rₒₒ] [IsNoetherianRing Rₒₒ]
    (hΛ : IsCohenMacaulayOfDim Λ d) (hR : IsCohenMacaulayOfDim Rₒₒ d) :
    ringKrullDim Rₒₒ < ⊤ ∧ .some (Module.depth Λ Λ) = ringKrullDim Rₒₒ

lemma

depth_le_depth_of_ringEquiv

L462 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.Module.depth_le_depth_of_ringEquiv

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim
variable {R} {d : ℕ}

Lean source · statement

lemma Module.depth_le_depth_of_ringEquiv {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) :
    Module.depth R R ≤ Module.depth S S

lemma

of_ringEquiv

L478 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_ringEquiv

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim
variable {R} {d : ℕ}

Lean source · statement

lemma of_ringEquiv {S : Type*} [CommRing S] [IsLocalRing S] (e : R ≃+* S)
    (h : IsCohenMacaulayOfDim R d) : IsCohenMacaulayOfDim S d

lemma

of_field

L484 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_field

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim
variable {R} {d : ℕ}

Lean source · statement

lemma of_field (K : Type*) [Field K] : IsCohenMacaulayOfDim K 0

lemma

of_isDiscreteValuationRing

L490 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_isDiscreteValuationRing

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim
variable {R} {d : ℕ}

Lean source · statement

lemma of_isDiscreteValuationRing (𝓞 : Type*) [CommRing 𝓞] [IsDomain 𝓞]
    [IsDiscreteValuationRing 𝓞] : IsCohenMacaulayOfDim 𝓞 1

theorem

isCohenMacaulayOfDim_succ

L524 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.PowerSeries.isCohenMacaulayOfDim_succ

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
open Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing
namespace PowerSeries
open PowerSeries
variable (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]

Lean source · statement

theorem isCohenMacaulayOfDim_succ {d : ℕ}
    (h : _root_.IsLocalRing.IsCohenMacaulayOfDim R d) :
    _root_.IsLocalRing.IsCohenMacaulayOfDim R⟦X⟧ (d + 1)

lemma

exists_isSMulRegular_of_depth_pos

L551 ↗

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

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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_of_isSMulRegular

L561 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_pos_of_isSMulRegular

Source context 11 commands

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

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

Lean source · statement

lemma Module.depth_pos_of_isSMulRegular {x : R} (hx : x ∈ maximalIdeal R)
    (hreg : IsSMulRegular M x) : 0 < Module.depth R M

lemma

depth_pos_iff_exists_isSMulRegular

L568 ↗

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

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.maximalIdeal_ne_bot_of_depth_pos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.maximalIdeal_ne_bot_of_ringKrullDim_pos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.maximalIdeal_notMem_associatedPrimes_of_depth_pos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos

Source context 8 commands

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

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

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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos'

Source context 8 commands

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

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

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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.exists_isSMulRegular_and_isSMulRegular

Source context 8 commands

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

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

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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain

Source context 8 commands

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

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

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.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing

Source context 8 commands

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

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

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

depth_eq_of_linearEquiv

L737 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_eq_of_linearEquiv

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 depth_eq_of_linearEquiv (e : M ≃ₗ[R] N) : Module.depth R M = Module.depth R N

lemma

exists_isWeaklyRegular_of_le_depth

L747 ↗

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

Source context 16 commands

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

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

depth_lt_top

L767 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_lt_top

Source context 17 commands

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

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

lemma depth_lt_top [IsNoetherianRing R] [Module.Finite R M] [Nontrivial M] :
    Module.depth R M < ⊤

def

quotSMulTopQuotSMulTopEquivSup

L777 ↗

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

Documentation

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

Source context 17 commands

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

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

quotSMulTopQuotSMulTopComm

L785 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.quotSMulTopQuotSMulTopComm

Documentation

Interchange the order of quotienting a module by two scalar multiples.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 quotSMulTopQuotSMulTopComm (M : Type*) [AddCommGroup M] [Module R M] (x z : R) :
    QuotSMulTop x (QuotSMulTop z M) ≃ₗ[R] QuotSMulTop z (QuotSMulTop x M)

lemma

eq_zero_of_maximalIdeal_smul_eq_zero

L797 ↗

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

Source context 16 commands

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

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

L837 ↗

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

Source context 17 commands

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

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

L857 ↗

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

Source context 18 commands

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

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

L882 ↗

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

Source context 18 commands

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

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

depth_quotSMulTop_succ_le

L925 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_quotSMulTop_succ_le

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 depth_quotSMulTop_succ_le (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {x : R} (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    Module.depth R (QuotSMulTop x M) + 1 ≤ Module.depth R M

lemma

le_depth_quotSMulTop_of_succ_le_depth

L949 ↗

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

Source context 16 commands

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

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

depth_quotSMulTop_succ_eq

L1032 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_quotSMulTop_succ_eq

Source context 17 commands

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

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

Lean source · statement

theorem depth_quotSMulTop_succ_eq {x : R} (hx : x ∈ maximalIdeal R)
    (hxreg : IsSMulRegular M x) :
    Module.depth R (QuotSMulTop x M) + 1 = Module.depth R M

theorem

depth_quotSMulTop_eq_sub_one

L1063 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_quotSMulTop_eq_sub_one

Source context 17 commands

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

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

Lean source · statement

theorem depth_quotSMulTop_eq_sub_one {x : R} (hx : x ∈ maximalIdeal R)
    (hxreg : IsSMulRegular M x) :
    Module.depth R (QuotSMulTop x M) = Module.depth R M - 1

lemma

exists_mem_maximalIdeal_mk_eq

L1073 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.exists_mem_maximalIdeal_mk_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 exists_mem_maximalIdeal_mk_eq {I : Ideal R} [IsLocalRing (R ⧸ I)]
    (a : R ⧸ I) (ha : a ∈ maximalIdeal (R ⧸ I)) :
    ∃ y ∈ maximalIdeal R, Ideal.Quotient.mk I y = a

theorem

depth_quotient_eq_depth

L1081 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_quotient_eq_depth

Source context 15 commands

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

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

Lean source · statement

theorem depth_quotient_eq_depth (I : Ideal R) [IsLocalRing (R ⧸ I)]
    (N : Type*) [AddCommGroup N] [Module R N] [Module (R ⧸ I) N] [IsScalarTower R (R ⧸ I) N] :
    Module.depth (R ⧸ I) N = Module.depth R N

lemma

isLocalRing_quotient_span_singleton

L1121 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.isLocalRing_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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

L1133 ↗

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

Source context 17 commands

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

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

L1139 ↗

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

Source context 17 commands

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

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

depth_quotient_self_succ_eq

L1145 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_quotient_self_succ_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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_self_succ_eq {x : R} [IsLocalRing (R ⧸ Ideal.span {x})]
    (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular R x) :
    Module.depth (R ⧸ Ideal.span {x}) (QuotSMulTop x R) + 1 = Module.depth R R

theorem

ringKrullDim_quotient_span_singleton_succ

L1156 ↗

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

Source context 16 commands

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

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

L1161 ↗

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

Source context 16 commands

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

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

L1167 ↗

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

Source context 16 commands

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

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

L1173 ↗

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

Source context 16 commands

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

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

L1180 ↗

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

Source context 16 commands

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

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

(anonymous instance)

L1220 ↗

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Submodule
open _root_.Pointwise
noncomputable section
section SATGates
variable (K : Type) [Field K]

Lean source · statement

instance : IsLocalRing ((PowerSeries K) ⧸ Ideal.span {(PowerSeries.X : PowerSeries K)})

lemma

exists_isSMulRegular_of_notMem_associatedPrimes

L1243 ↗

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

Source context 11 commands

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

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

L1252 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_pos_of_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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

L1257 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_pos_iff_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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

L1262 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.depth_eq_zero_iff_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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

L1275 ↗

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

Source context 11 commands

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

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

L1285 ↗

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

Source context 11 commands

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

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

L1302 ↗

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

Source context 11 commands

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

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

L1306 ↗

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

Source context 11 commands

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

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

L1320 ↗

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

Source context 10 commands

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

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

Lean source · statement

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

theorem

gate_dvr_depth_pos

L1334 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.DepthZeroAssociatedPrime.gate_dvr_depth_pos

Source context 10 commands

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

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

Lean source · statement

theorem gate_dvr_depth_pos
    (𝓞 : Type*) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞] :
    0 < Module.depth 𝓞 𝓞

theorem

gate_field_maximalIdeal_mem_associatedPrimes

L1344 ↗

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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_depth_eq_zero

L1351 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.DepthZeroAssociatedPrime.gate_field_depth_eq_zero

Source context 10 commands

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

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

Lean source · statement

theorem gate_field_depth_eq_zero (K : Type*) [Field K] : Module.depth K K = 0

theorem

gate_field_maximalIdeal_mem_associatedPrimes_via_depth

L1358 ↗

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

Source context 10 commands

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

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

L1363 ↗

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

Source context 10 commands

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

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

L1381 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.ringKrullDim_quotient_succ_le_of_lt

Source context 12 commands

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

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

pTorsion

L1397 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.pTorsion

Source context 12 commands

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

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

Lean source · full declaration

def pTorsion (p : Ideal R) (M : Type*) [AddCommGroup M] [Module R M] :
    Submodule R M where
  carrier := {m : M | ∀ a ∈ p, a • m = 0}
  zero_mem' := fun a _ => smul_zero a
  add_mem' := by
    intro m₁ m₂ h₁ h₂
    change ∀ a ∈ p, a • (m₁ + m₂) = 0
    intro a ha
    rw [smul_add, h₁ a ha, h₂ a ha, add_zero]
  smul_mem' := by
    intro c m hm
    change ∀ a ∈ p, a • (c • m) = 0
    intro a ha
    rw [smul_comm, hm a ha, smul_zero]

lemma

exists_forall_smul_eq_zero_notMem_smul_top

L1419 ↗

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

Source context 13 commands

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

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

L1464 ↗

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

Source context 13 commands

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

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

L1492 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.depth_le_ringKrullDim_quotient_aux

Source context 12 commands

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

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

L1530 ↗

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

Source context 12 commands

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

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

L1537 ↗

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

Source context 12 commands

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

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

L1552 ↗

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

Source context 12 commands

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

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

L1569 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace 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

L1579 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace 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

L1601 ↗

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace 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

L1613 ↗

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace 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

mk_smul_mk

L1679 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop.mk_smul_mk

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

theorem mk_smul_mk (r : R) (m : M) :
    (Ideal.Quotient.mk (Ideal.span {x}) r) •
        (Submodule.Quotient.mk m : QuotSMulTop x M) =
      (Submodule.Quotient.mk (r • m) : QuotSMulTop x M)

theorem

quotientMk_smul

L1685 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop.quotientMk_smul

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

theorem quotientMk_smul (r : R) (q : QuotSMulTop x M) :
    (Ideal.Quotient.mk (Ideal.span {x}) r) • q = r • q

instance

instModuleFiniteQuotient

L1690 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop.instModuleFiniteQuotient

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

instance instModuleFiniteQuotient [Module.Finite R M] :
    Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

theorem

nontrivial_quotientRing

L1694 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop.nontrivial_quotientRing

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

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

theorem

span_le_jacobson_bot

L1702 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop.span_le_jacobson_bot

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

theorem span_le_jacobson_bot [IsLocalRing R] (hx : x ∈ maximalIdeal R) :
    Ideal.span {x} ≤ Ideal.jacobson ⊥

theorem

free_self

L1713 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop.free_self

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop
section RankOne
variable (x : R)

Lean source · statement

theorem free_self : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x R)

theorem

span_eq_top_of_span_quotientMk_eq_top

L1741 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.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

L1759 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.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.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

exists_basis_lift

L1808 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop.exists_basis_lift

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.QuotSMulTop
section Main
variable [IsLocalRing R] [IsNoetherianRing R] [Module.Finite R M] (x : R)

Lean source · statement

theorem exists_basis_lift (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular M x)
    {ι : Type*} [Finite ι]
    (b : Module.Basis ι (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    ∃ b' : Module.Basis ι R M,
      ∀ i, (Submodule.Quotient.mk (b' i) : QuotSMulTop x M) = b i

theorem

free_of_quotSMulTop_free

L1838 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.free_of_quotSMulTop_free

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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 (x : R) (hx : x ∈ IsLocalRing.maximalIdeal R)
    (hreg : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    Module.Free R M

theorem

free_of_quotSMulTop_free_of_regular_param

L1850 ↗

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

Source context 16 commands

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

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

finrank_quotSMulTop_eq

L1857 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.Module.finrank_quotSMulTop_eq

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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.finrank_quotSMulTop_eq (x : R) (hx : x ∈ IsLocalRing.maximalIdeal R)
    (hreg : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    Module.finrank (R ⧸ Ideal.span {x}) (QuotSMulTop x M) = Module.finrank R M

theorem

isLocalRing_quotient_span_singleton

L1888 ↗

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

Source context 13 commands

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

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

L1897 ↗

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

Source context 13 commands

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

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

L1903 ↗

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

Source context 13 commands

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

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

L1909 ↗

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

Source context 13 commands

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

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

L1919 ↗

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

Source context 13 commands

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

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

L1936 ↗

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

Source context 13 commands

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

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

L1944 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.free_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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

free_of_ringKrullDim_eq_zero

L1949 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.free_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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_ringKrullDim_eq_zero (hdim : ringKrullDim R = 0) : Module.Free R M

theorem

exists_finite_span_eq_maximalIdeal_mem

L1961 ↗

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

Source context 13 commands

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

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

L2026 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.isRegularLocalRing_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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

JointRegularElementSelection

L2107 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.JointRegularElementSelection

Documentation

The assertion that a finite nontrivial module of positive depth over a positive-dimensional regular local ring admits a parameter regular on both the ring and the module.

Source context 12 commands

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

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

Lean source · statement

def JointRegularElementSelection : Prop

def

DepthDropQuotient

L2115 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.DepthDropQuotient

Documentation

The assertion that quotienting by an element regular on both a Noetherian local ring and a finite nontrivial module lowers the module depth by one over the quotient ring.

Source context 12 commands

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

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

Lean source · statement

def DepthDropQuotient : Prop

def

QuotientInductionStep

L2124 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.QuotientInductionStep

Documentation

The assertion that freeness of the quotient module over the quotient ring lifts to freeness of the original finite module along a regular parameter.

Source context 12 commands

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

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

Lean source · statement

def QuotientInductionStep : Prop

theorem

free_of_depth_eq_ringKrullDim_aux

L2136 ↗

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

Source context 12 commands

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

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

L2192 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim

Source context 12 commands

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

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

Lean source · statement

theorem free_of_depth_eq_ringKrullDim
    (hsel : JointRegularElementSelection.{u, v})
    (hdrop : DepthDropQuotient.{u, v})
    (hstep : QuotientInductionStep.{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

free_of_depth_eq_ringKrullDim_of_dim_zero

L2202 ↗

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

Source context 12 commands

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

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

quotientInductionStep_holds

L2212 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.quotientInductionStep_holds

Source context 12 commands

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

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

Lean source · statement

theorem quotientInductionStep_holds : QuotientInductionStep.{u, v}

def

RegularPositiveDepth

L2218 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.RegularPositiveDepth

Documentation

The assertion that every positive-dimensional regular local ring has positive depth as a module over itself.

Source context 12 commands

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

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

Lean source · statement

def RegularPositiveDepth : Prop

theorem

jointRegularElementSelection_of_regularPositiveDepth

L2222 ↗

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

Source context 12 commands

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

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

L2228 ↗

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

Source context 12 commands

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

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

depthDropQuotient_holds

L2249 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.depthDropQuotient_holds

Source context 10 commands

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

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

Lean source · statement

theorem depthDropQuotient_holds : DepthDropQuotient.{u, v}

theorem

maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos

L2265 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.maximalIdeal_notMem_minimalPrimes_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 Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
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

L2282 ↗

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

Source context 12 commands

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

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

annihilator_self_eq_bot

L2328 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_free_of_depth_eq_ringKrullDim_of_isRegularLocalRing.Ws14Port.No4PatchingCore.annihilator_self_eq_bot

Source context 13 commands

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

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

Lean source · statement

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

theorem

ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes

L2333 ↗

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

Source context 13 commands

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

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

L2343 ↗

Source context 13 commands

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

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

L2359 ↗

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

Source context 13 commands

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

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

L2438 ↗

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

Source context 12 commands

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

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

L2492 ↗

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

Source context 12 commands

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

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

L2500 ↗

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

Source context 12 commands

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

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

L2509 ↗

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

Source context 12 commands

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

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

Lean source · statement

theorem regularPositiveDepth_holds : RegularPositiveDepth.{u}

theorem

jointRegularElementSelection_holds

L2517 ↗

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

Source context 12 commands

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

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

L2520 ↗

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

Source context 12 commands

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

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

free_of_depth_eq_ringKrullDim_of_isRegularLocalRing

L2535 ↗

Module.free_of_depth_eq_ringKrullDim_of_isRegularLocalRing

Source context 4 commands

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

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

Lean source · statement

theorem _root_.Module.free_of_depth_eq_ringKrullDim_of_isRegularLocalRing
    (R : Type*) [CommRing R] [IsRegularLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (H : (Module.depth R M : WithBot ℕ∞) = ringKrullDim R) : Module.Free R M

Module documentation

Freeness from maximal depth over a regular local ring

Declarations