Module

Module_depth_quotient_eq_depth.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_depth_quotient_eq_depth

100 declarations indexed from sourceView source ↗

Module documentation

Module depth quotient eq depth

Imports16

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

instance

instSubsingletonQuotientOfSubsingleton

L55 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L59 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L64 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L76 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L83 ↗

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

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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_krullDim_support [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ Order.krullDim (Module.support R M)

lemma

depth_le_dim_annihilator

L170 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L176 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L180 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L197 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L204 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L227 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L235 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L242 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.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_quotient_eq_depth
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

L293 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L299 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L305 ↗

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

Documentation

Identify a power-series ring modulo the variable with its coefficient ring by taking the constant coefficient.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L309 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L314 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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'

L323 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L326 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L331 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L335 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L343 ↗

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

Documentation

The additive identification of power series modulo multiples of the variable with their coefficient ring.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L347 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L354 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L360 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L373 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L385 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L410 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
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

L439 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L443 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L451 ↗

Module.depth_le_depth_of_ringEquiv

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L483 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L489 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L495 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L548 ↗

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

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace PowerSeries
open PowerSeries
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open IsLocalRing
open _root_.Module.IsLocalRing
variable (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]

Lean source · statement

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

lemma

exists_isSMulRegular_of_depth_pos

L585 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L595 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L602 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L607 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L616 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L623 ↗

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

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L643 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L703 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk

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'

L714 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk

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

L723 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk

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

L734 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk

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

L747 ↗

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

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk

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

L784 ↗

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

Source context 37 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L794 ↗

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

Source context 37 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L814 ↗

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

Source context 38 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L824 ↗

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

Documentation

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

Source context 38 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L833 ↗

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

Documentation

Swap the order of two scalar quotients by identifying both with the quotient by their summed submodules.

Source context 38 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L856 ↗

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

Source context 40 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L907 ↗

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

Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L927 ↗

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

Source context 45 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L952 ↗

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

Source context 45 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1006 ↗

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

Source context 46 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1030 ↗

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

Source context 46 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1113 ↗

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

Source context 47 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1144 ↗

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

Source context 47 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1165 ↗

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

Source context 48 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1173 ↗

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

Source context 48 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1213 ↗

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

Source context 48 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1225 ↗

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

Source context 50 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1231 ↗

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

Source context 50 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1237 ↗

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

Source context 50 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1259 ↗

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

Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1264 ↗

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

Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1270 ↗

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

Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1276 ↗

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

Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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

L1283 ↗

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

Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
universe u
variable {R : Type*} [CommRing R] [IsLocalRing R]
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
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)

L1339 ↗

Source context 36 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1373 ↗

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

Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L1382 ↗

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

Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L1387 ↗

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

Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L1392 ↗

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

Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L1405 ↗

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

Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L1415 ↗

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

Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L1437 ↗

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

Source context 42 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1441 ↗

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

Source context 42 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
section Degeneration
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

theorem

gate_dvr_maximalIdeal_notMem_associatedPrimes

L1460 ↗

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

Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_dvr_depth_pos

L1474 ↗

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

Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1484 ↗

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

Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1491 ↗

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

Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1498 ↗

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

Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_rat_depth_eq_zero_and_mem

L1503 ↗

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

Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1527 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.ringKrullDim_quotient_succ_le_of_lt

Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
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

L1548 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.pTorsion

Source context 55 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1575 ↗

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

Source context 59 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1620 ↗

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

Source context 59 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1655 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.depth_le_ringKrullDim_quotient_aux

Source context 62 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1693 ↗

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

Source context 62 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1700 ↗

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

Source context 62 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1715 ↗

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

Source context 62 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
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

L1742 ↗

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

Source context 70 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L1752 ↗

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

Source context 70 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open 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

L1784 ↗

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

Source context 71 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open IsLocalRing
open _root_.Module.IsLocalRing
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk

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

L1796 ↗

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

Source context 71 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
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 RingTheory
open scoped Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Submodule
open _root_.Pointwise
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
open IsLocalRing
open _root_.Module.IsLocalRing
open RingTheory
open _root_.Pointwise
noncomputable section
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local simp] PowerSeries.quotSpanXEquiv_mk
attribute [local instance] PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] PowerSeries.quotXSMulTopAddEquiv_mk
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port
open IsLocalRing
open _root_.Module.IsLocalRing
attribute [local simp]
  Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp]
  Algebra.Proofs.Module_depth_quotient_eq_depth.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk

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_quotient_eq_depth

L1872 ↗

Module.depth_quotient_eq_depth

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Module_depth_quotient_eq_depth
open IsLocalRing RingTheory
attribute [local simp] Ws14Port.PowerSeries.quotSpanXEquiv_mk
attribute [local instance] Ws14Port.PowerSeries.instIsLocalRingPowerSeries'
attribute [local simp] Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk
attribute [local instance] Ws14Port.instSubsingletonQuotientOfSubsingleton

Lean source · statement

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

Module documentation

Module depth quotient eq depth

Declarations