NYLL
Module

IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
6 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring Is Cohen Macaulay Of Dim ring Krull Dim quotient add height

Imports10
Imported by2

Declarations

theorem

ringKrullDim_quotient_add_height_le

L39 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height.CMDimFormula.ringKrullDim_quotient_add_height_le
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
universe u
open IsLocalRing Pointwise
namespace CMDimFormula
Lean source · statement
theorem ringKrullDim_quotient_add_height_le {R : Type u} [CommRing R] (p : Ideal R) [p.IsPrime] :
    ringKrullDim (R ⧸ p) + p.height ≤ ringKrullDim R
theorem

depth_eq_of_linearEquiv

L56 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height.CMDimFormula.depth_eq_of_linearEquiv
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
universe u
open IsLocalRing Pointwise
namespace CMDimFormula
Lean source · statement
theorem depth_eq_of_linearEquiv {R : Type u} [CommRing R] [IsLocalRing R] {M N : Type u}
    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) :
    Module.depth R M = Module.depth R N
theorem

enat_eq_of_add_one_eq

L61 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height.CMDimFormula.enat_eq_of_add_one_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
universe u
open IsLocalRing Pointwise
namespace CMDimFormula
Lean source · statement
theorem enat_eq_of_add_one_eq {a : ℕ∞} {d : ℕ} (h : a + 1 = (d + 1 : ℕ)) : a = d
theorem

withBot_eq_of_add_one_eq

L65 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height.CMDimFormula.withBot_eq_of_add_one_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
universe u
open IsLocalRing Pointwise
namespace CMDimFormula
Lean source · statement
theorem withBot_eq_of_add_one_eq {a : WithBot ℕ∞} {d : ℕ} (h : a + 1 = ((d + 1 : ℕ) : WithBot ℕ∞))
  : a = d
theorem

le_ringKrullDim_quotient_add

L77 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height.CMDimFormula.le_ringKrullDim_quotient_add
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
universe u
open IsLocalRing Pointwise
namespace CMDimFormula
Lean source · statement
theorem le_ringKrullDim_quotient_add (n : ℕ) :
    ∀ {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {d : ℕ}
      (_h : IsCohenMacaulayOfDim R d) (p : Ideal R) [p.IsPrime], p.height = n →
      (d : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ p) + n
theorem

ringKrullDim_quotient_add_height

L182 ↗
IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_quotient_add_height
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_IsCohenMacaulayOfDim_ringKrullDim_quotient_add_height
universe u
open IsLocalRing Pointwise
open CMDimFormula in
Lean source · statement
theorem _root_.IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_quotient_add_height
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {d : ℕ}
    (h : IsCohenMacaulayOfDim R d) (p : Ideal R) [p.IsPrime] :
    ringKrullDim (R ⧸ p) + p.height = d

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.