Module

ModuleDepthRegularQuotient.lean

Nyll.SchemeTheory.RingTheory.ModuleDepthRegularQuotient

100 declarations indexed from sourceView source ↗

Module documentation

Depth after quotienting by a regular scalar

For a finite module over a Noetherian local ring, quotienting by a scalar in the maximal ideal that is regular on the module lowers its depth by one. The supporting arguments compare regular sequences, associated primes, and power-series quotients.

Imports17

Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.PowerSeries.Ideal
Lean.Elab.Command
Batteries.Tactic.Alias
Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Mathlib.RingTheory.KrullDimension.Field
Mathlib.RingTheory.KrullDimension.PID
Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.PowerSeries.Inverse
Mathlib.Tactic.Conv
Mathlib.Tactic.CrossRefAttribute
Mathlib.Tactic.Ext
Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.TermCongr
Nyll.SchemeTheory.RingTheory.CohenMacaulay
Nyll.SchemeTheory.RingTheory.LocalAlgebra

Imported by4

instance

instSubsingletonQuotientOfSubsingleton

L60 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.instSubsingletonQuotientOfSubsingleton

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
noncomputable section

Lean source · statement

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

lemma

length_le_depth

L64 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.length_le_depth

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module 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

L69 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_of_subsingleton

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.depth_of_subsingleton [Subsingleton M] :
    Module.depth R M = ⊤

lemma

depth_of_isScalarTower

L81 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_of_isScalarTower

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module 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

L90 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_le_krullDim_support

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module 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

L180 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_le_dim_annihilator

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module 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

L186 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_le_dim

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module 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

L190 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.isSMulRegular_iff_of_free

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module 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

L207 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_subsingleton

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module 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

L215 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_free_aux

Source context 11 commands

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

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

L238 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_free

Source context 10 commands

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

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

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

L246 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_le_of_free

Source context 10 commands

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

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

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

L253 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.faithfulSMul_of_depth_eq_ringKrullDim

Source context 10 commands

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

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

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

L301 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.isSMulRegular_X

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L307 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.ker_constantCoeff

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L313 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.quotSpanXEquiv

Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L318 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.quotSpanXEquiv_mk

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L323 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.smul_top_eq_span_X

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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'

L332 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L335 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.mem_maximalIdeal_iff

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L340 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.X_mem_maximalIdeal

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L344 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.C_mem_maximalIdeal

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L352 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.quotXSMulTopAddEquiv

Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L357 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L364 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_smul

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L370 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.isWeaklyRegular_X_cons_map_C

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L383 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.le_depth_of_isWeaklyRegular

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L395 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.natCast_succ_le_depth

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L420 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.ringKrullDim_powerSeries

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.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

L440 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_lt_top

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.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

L444 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.patching_hypotheses

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.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

L452 ↗

Module.depth_le_depth_of_ringEquiv

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing
variable (R : Type*) [CommRing R] [IsLocalRing R]
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim
variable {R} {d : ℕ}

Lean source · statement

lemma _root_.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

L470 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_ringEquiv

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.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

L476 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_field

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.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

L482 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_isDiscreteValuationRing

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.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

L517 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.PowerSeries.isCohenMacaulayOfDim_succ

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
noncomputable section
open Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing
namespace PowerSeries
open PowerSeries
open _root_.Module.IsLocalRing
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

L541 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_isSMulRegular_of_depth_pos

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

depth_pos_of_isSMulRegular

L551 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_pos_of_isSMulRegular

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

depth_pos_iff_exists_isSMulRegular

L558 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_pos_iff_exists_isSMulRegular

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

maximalIdeal_ne_bot_of_depth_pos

L563 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.maximalIdeal_ne_bot_of_depth_pos

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

maximalIdeal_ne_bot_of_ringKrullDim_pos

L572 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.maximalIdeal_ne_bot_of_ringKrullDim_pos

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

maximalIdeal_notMem_associatedPrimes_of_depth_pos

L579 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.maximalIdeal_notMem_associatedPrimes_of_depth_pos

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
section DepthCharacterization
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes

L594 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
section PrimeAvoidance
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos

L649 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos'

L660 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos'

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular

L669 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.exists_isSMulRegular_and_isSMulRegular

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain

L680 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing

L693 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing

Lean source · statement

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

lemma

depth_eq_of_linearEquiv

L726 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_eq_of_linearEquiv

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L736 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_isWeaklyRegular_of_le_depth

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L756 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_lt_top

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L766 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.quotSMulTopQuotSMulTopEquivSup

Documentation

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

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L774 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.quotSMulTopQuotSMulTopComm

Documentation

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

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L786 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.eq_zero_of_maximalIdeal_smul_eq_zero

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L826 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.not_isAssociatedPrime_maximalIdeal_of_isSMulRegular

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L846 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.not_isAssociatedPrime_maximalIdeal_quotSMulTop

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L871 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L914 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_quotSMulTop_succ_le

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L938 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.le_depth_quotSMulTop_of_succ_le_depth

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1021 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_quotSMulTop_succ_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1052 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_quotSMulTop_eq_sub_one

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1062 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_mem_maximalIdeal_mk_eq

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1070 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_quotient_eq_depth

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1110 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.isLocalRing_quotient_span_singleton

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1122 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_quotient_quotSMulTop_succ_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1128 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_quotient_quotSMulTop_eq_sub_one

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1134 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_quotient_self_succ_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1145 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1150 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ_of_ne_zero

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1156 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ_of_regular_parameter

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1162 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.ringKrullDim_eq_succ_of_quotient_span_singleton_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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

L1169 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.ringKrullDim_quotient_span_singleton_of_ringKrullDim_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
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)

L1209 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
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

L1229 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.exists_isSMulRegular_of_notMem_associatedPrimes

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

lemma

depth_pos_of_maximalIdeal_notMem_associatedPrimes

L1238 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_pos_of_maximalIdeal_notMem_associatedPrimes

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_pos_iff_maximalIdeal_notMem_associatedPrimes

L1243 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_pos_iff_maximalIdeal_notMem_associatedPrimes

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes

L1248 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_pos_iff_not_isAssociatedPrime_maximalIdeal

L1261 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_pos_iff_not_isAssociatedPrime_maximalIdeal

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_eq_zero_iff_isAssociatedPrime_maximalIdeal

L1271 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_eq_zero_iff_isAssociatedPrime_maximalIdeal

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_eq_top_and_associatedPrimes_eq_empty_of_subsingleton

L1288 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_eq_top_and_associatedPrimes_eq_empty_of_subsingleton

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Degeneration
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

theorem

depth_pos_and_maximalIdeal_notMem_associatedPrimes_of_subsingleton

L1292 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_pos_and_maximalIdeal_notMem_associatedPrimes_of_subsingleton

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
section Degeneration
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

theorem

gate_dvr_maximalIdeal_notMem_associatedPrimes

L1306 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.DepthZeroAssociatedPrime.gate_dvr_maximalIdeal_notMem_associatedPrimes

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_dvr_depth_pos

L1320 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.DepthZeroAssociatedPrime.gate_dvr_depth_pos

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
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

L1330 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.DepthZeroAssociatedPrime.gate_field_maximalIdeal_mem_associatedPrimes

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_field_depth_eq_zero

L1337 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.DepthZeroAssociatedPrime.gate_field_depth_eq_zero

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
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

L1344 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.DepthZeroAssociatedPrime.gate_field_maximalIdeal_mem_associatedPrimes_via_depth

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_rat_depth_eq_zero_and_mem

L1349 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.DepthZeroAssociatedPrime.gate_rat_depth_eq_zero_and_mem

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

lemma

ringKrullDim_quotient_succ_le_of_lt

L1364 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.ringKrullDim_quotient_succ_le_of_lt

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section DimensionDrop
variable {R : Type*} [CommRing R]

Lean source · statement

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

def

pTorsion

L1380 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.pTorsion

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
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

L1402 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsAssociatedPrime.exists_forall_smul_eq_zero_notMem_smul_top

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section NakayamaStep
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

exists_isAssociatedPrime_quotSMulTop_le

L1447 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsAssociatedPrime.exists_isAssociatedPrime_quotSMulTop_le

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section NakayamaStep
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

depth_le_ringKrullDim_quotient_aux

L1477 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.depth_le_ringKrullDim_quotient_aux

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
universe u v
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

L1515 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.natCast_le_ringKrullDim_quotient_of_le_depth

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
universe u v
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

L1522 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_le_ringKrullDim_quotient_of_mem_associatedPrimes

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
universe u v
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

L1537 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.Module.depth_le_ringKrullDim_quotient_of_isAssociatedPrime

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
universe u v
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

L1555 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_quotient_eq_of_mem_associatedPrimes

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim

Lean source · statement

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

theorem

mem_minimalPrimes_of_mem_associatedPrimes

L1565 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.mem_minimalPrimes_of_mem_associatedPrimes

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim

Lean source · statement

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

lemma

isCohenMacaulayOfDim_of_depth_eq_ringKrullDim

L1587 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.isCohenMacaulayOfDim_of_depth_eq_ringKrullDim

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

mem_minimalPrimes_of_mem_associatedPrimes_of_depth_eq_ringKrullDim

L1599 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq.Ws14Port.IsLocalRing.mem_minimalPrimes_of_mem_associatedPrimes_of_depth_eq_ringKrullDim

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory
namespace Ws14Port
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 IsLocalRing RingTheory Module RingTheory.Sequence
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.PowerSeries
open scoped Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
open _root_.Module.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

depth_quotSMulTop_succ_eq

L1649 ↗

Module.depth_quotSMulTop_succ_eq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotSMulTop_succ_eq
open IsLocalRing RingTheory

Lean source · statement

theorem _root_.Module.depth_quotSMulTop_succ_eq
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (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

Module documentation

Depth after quotienting by a regular scalar

Declarations