Module

MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.lean

Nyll.AlgebraicCurves.Valuations.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing

209 declarations indexed from sourceView source ↗

Module documentation

Mv Power Series ring Krull Dim fin eq of is Discrete Valuation Ring

Imports30

Lean.Elab.Tactic.Omega
Lean.Elab.Tactic.NormCast
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Mathlib.RingTheory.KrullDimension.Regular
Mathlib.RingTheory.KrullDimension.Module
Mathlib.RingTheory.KrullDimension.LocalRing
Mathlib.RingTheory.KrullDimension.PID
Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.QuotSMulTop
Mathlib.RingTheory.Ideal.Cotangent
Mathlib.RingTheory.Finiteness.Nakayama
Mathlib.RingTheory.Support
Mathlib.RingTheory.MvPowerSeries.Equiv
Mathlib.RingTheory.MvPowerSeries.PiTopology
Mathlib.RingTheory.MvPowerSeries.Ideal
Mathlib.RingTheory.PowerSeries.Ideal
Mathlib.RingTheory.PowerSeries.NoZeroDivisors
Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.Tactic.Linarith
Mathlib.Tactic.Ext
Mathlib.Tactic.Push
Mathlib.Tactic.ByContra
Nyll.SchemeTheory.RingTheory.CohenMacaulay

Imported by1

Nyll.AlgebraicCurves.Valuations.All

instance

instSubsingletonQuotientOfSubsingleton

L80 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.instSubsingletonQuotientOfSubsingleton

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

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

lemma

length_le_depth

L84 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.length_le_depth

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.length_le_depth (s : List R)
    (hs : Sequence.IsWeaklyRegular M s) (hs' : ∀ r ∈ s, r ∈ maximalIdeal R) :
    s.length ≤ Module.depth R M

lemma

depth_of_subsingleton

L89 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_of_subsingleton

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

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

lemma

depth_of_isScalarTower

L101 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_of_isScalarTower

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.depth_of_isScalarTower :
    Module.depth R M ≤ Module.depth S M

lemma

depth_le_krullDim_support

L108 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_le_krullDim_support

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.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

L189 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_le_dim_annihilator

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.depth_le_dim_annihilator
    [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ ringKrullDim (R ⧸ Module.annihilator R M)

lemma

depth_le_dim

L195 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_le_dim

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.depth_le_dim [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ ringKrullDim R

lemma

isSMulRegular_iff_of_free

L199 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.isSMulRegular_iff_of_free

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma isSMulRegular_iff_of_free {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Nontrivial M] {r : R} :
    IsSMulRegular M r ↔ IsSMulRegular R r

lemma

isWeaklyRegular_of_subsingleton

L216 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_subsingleton

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma RingTheory.Sequence.isWeaklyRegular_of_subsingleton
    {R : Type*} (M : Type*) [CommRing R] [AddCommGroup M] [Module R M]
    [Subsingleton R] (s : List R) : Sequence.IsWeaklyRegular M s

lemma

isWeaklyRegular_of_free_aux

L223 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_free_aux

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section
open scoped Pointwise TensorProduct in

Lean source · statement

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

lemma

isWeaklyRegular_of_free

L246 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.RingTheory.Sequence.isWeaklyRegular_of_free

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma RingTheory.Sequence.isWeaklyRegular_of_free
    {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Nontrivial M] {s : List R} :
      Sequence.IsWeaklyRegular M s ↔ Sequence.IsWeaklyRegular R s

lemma

depth_le_of_free

L254 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_le_of_free

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.depth_le_of_free [Module.Free R M] : Module.depth R R ≤ Module.depth R M

lemma

faithfulSMul_of_depth_eq_ringKrullDim

L261 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.faithfulSMul_of_depth_eq_ringKrullDim

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
variable (R S M : Type*) [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
variable [AddCommGroup M] [Module R M] [Module S M] [Algebra R S] [IsScalarTower R S M]
variable [IsLocalHom (algebraMap R S)]
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.RingTheory
open _root_.Module
open _root_.RingTheory.Sequence
noncomputable section

Lean source · statement

lemma Module.faithfulSMul_of_depth_eq_ringKrullDim [IsDomain R] [Nontrivial M] [Module.Finite R M]
    (H : ringKrullDim R < ⊤) (H' : .some (Module.depth R M) = ringKrullDim R) :
    FaithfulSMul R M

lemma

isSMulRegular_X

L313 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.isSMulRegular_X

Source context 16 commands

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

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

Lean source · statement

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

lemma

ker_constantCoeff

L319 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.ker_constantCoeff

Source context 16 commands

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

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

Lean source · statement

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

def

quotSpanXEquiv

L324 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.quotSpanXEquiv

Documentation

The quotient by the power series variable is the coefficient ring.

Source context 16 commands

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

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

Lean source · statement

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

lemma

quotSpanXEquiv_mk

L328 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.quotSpanXEquiv_mk

Source context 16 commands

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

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

Lean source · statement

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

lemma

smul_top_eq_span_X

L333 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.smul_top_eq_span_X

Source context 16 commands

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

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

Lean source · statement

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

instance

instIsLocalRingPowerSeries'

L342 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.instIsLocalRingPowerSeries'

Source context 18 commands

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

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

Lean source · statement

instance instIsLocalRingPowerSeries' : IsLocalRing R⟦X⟧

lemma

mem_maximalIdeal_iff

L345 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.mem_maximalIdeal_iff

Source context 18 commands

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

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

Lean source · statement

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

lemma

X_mem_maximalIdeal

L350 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.X_mem_maximalIdeal

Source context 18 commands

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

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

Lean source · statement

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

lemma

C_mem_maximalIdeal

L354 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.C_mem_maximalIdeal

Source context 18 commands

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

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

Lean source · statement

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

def

quotXSMulTopAddEquiv

L361 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.quotXSMulTopAddEquiv

Documentation

The additive equivalence from quotienting by multiplication by the variable.

Source context 16 commands

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

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

Lean source · statement

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

lemma

quotXSMulTopAddEquiv_mk

L364 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_mk

Source context 16 commands

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

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

Lean source · statement

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

lemma

quotXSMulTopAddEquiv_smul

L372 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.quotXSMulTopAddEquiv_smul

Source context 16 commands

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

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

Lean source · statement

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

lemma

isWeaklyRegular_X_cons_map_C

L378 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.isWeaklyRegular_X_cons_map_C

Source context 16 commands

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

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

Lean source · statement

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

lemma

le_depth_of_isWeaklyRegular

L391 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.le_depth_of_isWeaklyRegular

Source context 18 commands

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

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

Lean source · statement

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

lemma

natCast_succ_le_depth

L403 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.natCast_succ_le_depth

Source context 18 commands

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

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

Lean source · statement

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

lemma

ringKrullDim_powerSeries

L428 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.ringKrullDim_powerSeries

Source context 18 commands

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

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

Lean source · statement

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

lemma

ringKrullDim_lt_top

L448 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_lt_top

Source context 19 commands

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

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

Lean source · statement

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

lemma

patching_hypotheses

L452 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.patching_hypotheses

Source context 19 commands

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

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

Lean source · statement

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

lemma

depth_le_depth_of_ringEquiv

L460 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.Module.depth_le_depth_of_ringEquiv

Source context 19 commands

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

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

Lean source · statement

lemma 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

L476 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_ringEquiv

Source context 19 commands

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

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

Lean source · statement

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

lemma

of_field

L482 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_field

Source context 19 commands

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

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

Lean source · statement

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

lemma

of_isDiscreteValuationRing

L488 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.of_isDiscreteValuationRing

Source context 19 commands

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

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

Lean source · statement

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

theorem

isCohenMacaulayOfDim_succ

L521 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.PowerSeries.isCohenMacaulayOfDim_succ

Source context 17 commands

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

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

Lean source · statement

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

lemma

exists_isSMulRegular_of_depth_pos

L548 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_isSMulRegular_of_depth_pos

Source context 12 commands

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

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

Lean source · statement

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

lemma

depth_pos_of_isSMulRegular

L558 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_pos_of_isSMulRegular

Source context 12 commands

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

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

Lean source · statement

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

lemma

depth_pos_iff_exists_isSMulRegular

L565 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_pos_iff_exists_isSMulRegular

Source context 12 commands

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

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

Lean source · statement

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

lemma

maximalIdeal_ne_bot_of_depth_pos

L570 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.maximalIdeal_ne_bot_of_depth_pos

Source context 12 commands

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

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

Lean source · statement

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

lemma

maximalIdeal_ne_bot_of_ringKrullDim_pos

L579 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.maximalIdeal_ne_bot_of_ringKrullDim_pos

Source context 12 commands

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

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

Lean source · statement

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

lemma

maximalIdeal_notMem_associatedPrimes_of_depth_pos

L586 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.maximalIdeal_notMem_associatedPrimes_of_depth_pos

Source context 12 commands

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

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

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes

L601 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section PrimeAvoidance
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos

L656 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos'

L667 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular

L676 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.exists_isSMulRegular_and_isSMulRegular

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain

L687 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_isSMulRegular_and_isSMulRegular_of_depth_pos_of_isDomain

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing

L700 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.exists_isSMulRegular_and_isSMulRegular_of_isDiscreteValuationRing

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing

Lean source · statement

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

lemma

depth_eq_of_linearEquiv

L736 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_eq_of_linearEquiv

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Transport
variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

lemma depth_eq_of_linearEquiv (e : M ≃ₗ[R] N) : Module.depth R M = Module.depth R N

lemma

exists_isWeaklyRegular_of_le_depth

L746 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_isWeaklyRegular_of_le_depth

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Transport
variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

lemma exists_isWeaklyRegular_of_le_depth (M : Type*) [AddCommGroup M] [Module R M]
    (n : ℕ) (hn : (n : ℕ∞) ≤ Module.depth R M) :
    ∃ s : List R, Sequence.IsWeaklyRegular M s ∧ (∀ r ∈ s, r ∈ maximalIdeal R) ∧
      s.length = n

lemma

depth_lt_top

L766 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_lt_top

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Transport
variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
variable (M) in

Lean source · statement

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

def

quotSMulTopQuotSMulTopEquivSup

L775 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.quotSMulTopQuotSMulTopEquivSup

Documentation

Identify the iterated scalar quotient with the quotient by the sum of scalar images.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Transport
variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
variable (M) in

Lean source · statement

def quotSMulTopQuotSMulTopEquivSup (M : Type*) [AddCommGroup M] [Module R M] (z x : R) :
    QuotSMulTop x (QuotSMulTop z M) ≃ₗ[R]
      M ⧸ (z • (⊤ : Submodule R M) ⊔ x • (⊤ : Submodule R M))

def

quotSMulTopQuotSMulTopComm

L783 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.quotSMulTopQuotSMulTopComm

Documentation

Interchange the order of the two scalar quotients.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Transport
variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
variable (M) in

Lean source · statement

def 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

L795 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.eq_zero_of_maximalIdeal_smul_eq_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section Elementary
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

lemma eq_zero_of_maximalIdeal_smul_eq_zero {x y₁ y₂ : R} (hxreg : IsSMulRegular M x)
    (hy : Sequence.IsWeaklyRegular M [y₁, y₂])
    (hy₁ : y₁ ∈ maximalIdeal R) (hy₂ : y₂ ∈ maximalIdeal R)
    (m₀ : QuotSMulTop x M) (hm₀ : ∀ a ∈ maximalIdeal R, a • m₀ = 0) : m₀ = 0

lemma

not_isAssociatedPrime_maximalIdeal_of_isSMulRegular

L835 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.not_isAssociatedPrime_maximalIdeal_of_isSMulRegular

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section AssociatedPrimes
variable [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

lemma not_isAssociatedPrime_maximalIdeal_of_isSMulRegular {x : R}
    (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    ¬ IsAssociatedPrime (maximalIdeal R) M

lemma

not_isAssociatedPrime_maximalIdeal_quotSMulTop

L855 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.not_isAssociatedPrime_maximalIdeal_quotSMulTop

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section AssociatedPrimes
variable [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable (M) in

Lean source · statement

lemma not_isAssociatedPrime_maximalIdeal_quotSMulTop {x : R} (hxreg : IsSMulRegular M x)
    (hdepth : (2 : ℕ∞) ≤ Module.depth R M) :
    ¬ IsAssociatedPrime (maximalIdeal R) (QuotSMulTop x M)

lemma

exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

L880 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_mem_maximalIdeal_isSMulRegular_isSMulRegular

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section AssociatedPrimes
variable [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable (M) in

Lean source · statement

lemma exists_mem_maximalIdeal_isSMulRegular_isSMulRegular
    (N₁ N₂ : Type*) [AddCommGroup N₁] [Module R N₁] [Module.Finite R N₁]
    [AddCommGroup N₂] [Module R N₂] [Module.Finite R N₂]
    (h₁ : ¬ IsAssociatedPrime (maximalIdeal R) N₁)
    (h₂ : ¬ IsAssociatedPrime (maximalIdeal R) N₂) :
    ∃ z ∈ maximalIdeal R, IsSMulRegular N₁ z ∧ IsSMulRegular N₂ z

lemma

depth_quotSMulTop_succ_le

L923 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_quotSMulTop_succ_le

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section DepthDrop
variable [IsNoetherianRing R]

Lean source · statement

lemma 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

L947 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.le_depth_quotSMulTop_of_succ_le_depth

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace Module
open Module
variable {R : Type*} [CommRing R] [IsLocalRing R]
section DepthDrop
variable [IsNoetherianRing R]

Lean source · statement

lemma le_depth_quotSMulTop_of_succ_le_depth
    (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {x : R} (hx : x ∈ maximalIdeal R) (n : ℕ) (hxreg : IsSMulRegular M x)
    (hd : ((n + 1 : ℕ) : ℕ∞) ≤ Module.depth R M) :
    (n : ℕ∞) ≤ Module.depth R (QuotSMulTop x M)

theorem

depth_quotSMulTop_succ_eq

L1030 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_quotSMulTop_succ_eq

Source context 18 commands

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

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

L1061 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_quotSMulTop_eq_sub_one

Source context 18 commands

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

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

L1071 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_mem_maximalIdeal_mk_eq

Source context 16 commands

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

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

Lean source · statement

lemma 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

L1079 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_quotient_eq_depth

Source context 16 commands

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

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

Lean source · statement

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

L1119 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.isLocalRing_quotient_span_singleton

Source context 16 commands

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

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

Lean source · statement

lemma isLocalRing_quotient_span_singleton {x : R} (hx : x ∈ maximalIdeal R) :
    IsLocalRing (R ⧸ Ideal.span {x})

theorem

depth_quotient_quotSMulTop_succ_eq

L1131 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_quotient_quotSMulTop_succ_eq

Source context 18 commands

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

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

Lean source · statement

theorem depth_quotient_quotSMulTop_succ_eq {x : R} [IsLocalRing (R ⧸ Ideal.span {x})]
    (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    Module.depth (R ⧸ Ideal.span {x}) (QuotSMulTop x M) + 1 = Module.depth R M

theorem

depth_quotient_quotSMulTop_eq_sub_one

L1137 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_quotient_quotSMulTop_eq_sub_one

Source context 18 commands

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

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

Lean source · statement

theorem depth_quotient_quotSMulTop_eq_sub_one {x : R} [IsLocalRing (R ⧸ Ideal.span {x})]
    (hx : x ∈ maximalIdeal R) (hxreg : IsSMulRegular M x) :
    Module.depth (R ⧸ Ideal.span {x}) (QuotSMulTop x M) = Module.depth R M - 1

theorem

depth_quotient_self_succ_eq

L1143 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_quotient_self_succ_eq

Source context 18 commands

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

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

Lean source · statement

theorem depth_quotient_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

L1154 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ

Source context 17 commands

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

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

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ {x : R}
    (hxreg : IsSMulRegular R x) (hx : x ∈ maximalIdeal R) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

ringKrullDim_quotient_span_singleton_succ_of_ne_zero

L1159 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ_of_ne_zero

Source context 17 commands

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

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

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ_of_ne_zero [IsDomain R] {x : R}
    (hx0 : x ≠ 0) (hx : x ∈ maximalIdeal R) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

ringKrullDim_quotient_span_singleton_succ_of_regular_parameter

L1165 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.ringKrullDim_quotient_span_singleton_succ_of_regular_parameter

Source context 17 commands

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

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

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ_of_regular_parameter [IsDomain R] {x : R}
    (hx : x ∈ maximalIdeal R) (hx2 : x ∉ (maximalIdeal R) ^ 2) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

ringKrullDim_eq_succ_of_quotient_span_singleton_eq

L1171 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.ringKrullDim_eq_succ_of_quotient_span_singleton_eq

Source context 17 commands

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

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

Lean source · statement

theorem ringKrullDim_eq_succ_of_quotient_span_singleton_eq {x : R}
    (hxreg : IsSMulRegular R x) (hx : x ∈ maximalIdeal R) {d : ℕ}
    (hd : ringKrullDim (R ⧸ Ideal.span {x}) = ((d : ℕ) : WithBot ℕ∞)) :
    ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞)

theorem

ringKrullDim_quotient_span_singleton_of_ringKrullDim_eq

L1178 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.ringKrullDim_quotient_span_singleton_of_ringKrullDim_eq

Source context 17 commands

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

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

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_of_ringKrullDim_eq {x : R}
    (hxreg : IsSMulRegular R x) (hx : x ∈ maximalIdeal R) {d : ℕ}
    (hd : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞)) :
    ringKrullDim (R ⧸ Ideal.span {x}) = ((d : ℕ) : WithBot ℕ∞)

instance

(anonymous instance)

L1218 ↗

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
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

L1242 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.exists_isSMulRegular_of_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

lemma

depth_pos_of_maximalIdeal_notMem_associatedPrimes

L1251 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_pos_of_maximalIdeal_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_pos_iff_maximalIdeal_notMem_associatedPrimes

L1256 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_pos_iff_maximalIdeal_notMem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes

L1261 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_pos_iff_not_isAssociatedPrime_maximalIdeal

L1274 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_pos_iff_not_isAssociatedPrime_maximalIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_eq_zero_iff_isAssociatedPrime_maximalIdeal

L1284 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_eq_zero_iff_isAssociatedPrime_maximalIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Characterization
variable (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]

Lean source · statement

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

theorem

depth_eq_top_and_associatedPrimes_eq_empty_of_subsingleton

L1301 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_eq_top_and_associatedPrimes_eq_empty_of_subsingleton

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Degeneration
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

theorem

depth_pos_and_maximalIdeal_notMem_associatedPrimes_of_subsingleton

L1305 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_pos_and_maximalIdeal_notMem_associatedPrimes_of_subsingleton

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
section Degeneration
variable (R : Type*) [CommRing R] [IsLocalRing R]
variable (M : Type*) [AddCommGroup M] [Module R M]

Lean source · statement

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

theorem

gate_dvr_maximalIdeal_notMem_associatedPrimes

L1319 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.DepthZeroAssociatedPrime.gate_dvr_maximalIdeal_notMem_associatedPrimes

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_dvr_depth_pos

L1333 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.DepthZeroAssociatedPrime.gate_dvr_depth_pos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_field_maximalIdeal_mem_associatedPrimes

L1343 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.DepthZeroAssociatedPrime.gate_field_maximalIdeal_mem_associatedPrimes

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_field_depth_eq_zero

L1350 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.DepthZeroAssociatedPrime.gate_field_depth_eq_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_field_maximalIdeal_mem_associatedPrimes_via_depth

L1357 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.DepthZeroAssociatedPrime.gate_field_maximalIdeal_mem_associatedPrimes_via_depth

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

theorem

gate_rat_depth_eq_zero_and_mem

L1362 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.DepthZeroAssociatedPrime.gate_rat_depth_eq_zero_and_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace DepthZeroAssociatedPrime
open DepthZeroAssociatedPrime

Lean source · statement

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

lemma

ringKrullDim_quotient_succ_le_of_lt

L1381 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.ringKrullDim_quotient_succ_le_of_lt

Source context 13 commands

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

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

Lean source · statement

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

def

pTorsion

L1397 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.pTorsion

Source context 13 commands

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

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

Lean source · full declaration

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

lemma

exists_forall_smul_eq_zero_notMem_smul_top

L1419 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsAssociatedPrime.exists_forall_smul_eq_zero_notMem_smul_top

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section NakayamaStep
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

exists_isAssociatedPrime_quotSMulTop_le

L1464 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsAssociatedPrime.exists_isAssociatedPrime_quotSMulTop_le

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section NakayamaStep
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

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

lemma

depth_le_ringKrullDim_quotient_aux

L1492 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.depth_le_ringKrullDim_quotient_aux

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

lemma depth_le_ringKrullDim_quotient_aux (n : ℕ) :
    ∀ (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] (p : Ideal R),
      IsAssociatedPrime p M → (n : ℕ∞) ≤ Module.depth R M →
      ((n : ℕ) : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ p)

lemma

natCast_le_ringKrullDim_quotient_of_le_depth

L1530 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.natCast_le_ringKrullDim_quotient_of_le_depth

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

lemma Module.natCast_le_ringKrullDim_quotient_of_le_depth (n : ℕ)
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {p : Ideal R} (hp : p ∈ associatedPrimes R M)
    (hn : (n : ℕ∞) ≤ Module.depth R M) :
    ((n : ℕ) : WithBot ℕ∞) ≤ ringKrullDim (R ⧸ p)

theorem

depth_le_ringKrullDim_quotient_of_mem_associatedPrimes

L1537 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_le_ringKrullDim_quotient_of_mem_associatedPrimes

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem Module.depth_le_ringKrullDim_quotient_of_mem_associatedPrimes
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {p : Ideal R} (hp : p ∈ associatedPrimes R M) :
    .some (Module.depth R M) ≤ ringKrullDim (R ⧸ p)

theorem

depth_le_ringKrullDim_quotient_of_isAssociatedPrime

L1552 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.depth_le_ringKrullDim_quotient_of_isAssociatedPrime

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section MainTheorem
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]

Lean source · statement

theorem Module.depth_le_ringKrullDim_quotient_of_isAssociatedPrime
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    {p : Ideal R} (hp : IsAssociatedPrime p M) :
    .some (Module.depth R M) ≤ ringKrullDim (R ⧸ p)

theorem

ringKrullDim_quotient_eq_of_mem_associatedPrimes

L1570 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.ringKrullDim_quotient_eq_of_mem_associatedPrimes

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim

Lean source · statement

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

theorem

mem_minimalPrimes_of_mem_associatedPrimes

L1580 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.mem_minimalPrimes_of_mem_associatedPrimes

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing
namespace IsCohenMacaulayOfDim
open IsCohenMacaulayOfDim

Lean source · statement

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

lemma

isCohenMacaulayOfDim_of_depth_eq_ringKrullDim

L1602 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isCohenMacaulayOfDim_of_depth_eq_ringKrullDim

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

mem_minimalPrimes_of_mem_associatedPrimes_of_depth_eq_ringKrullDim

L1614 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.mem_minimalPrimes_of_mem_associatedPrimes_of_depth_eq_ringKrullDim

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Pointwise
noncomputable section
section Unmixedness
variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

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

theorem

mk_smul_mk

L1684 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.mk_smul_mk

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

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

theorem

quotientMk_smul

L1690 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.quotientMk_smul

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

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

instance

instModuleFiniteQuotient

L1695 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.instModuleFiniteQuotient

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

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

theorem

nontrivial_quotientRing

L1699 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.nontrivial_quotientRing

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

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

theorem

span_le_jacobson_bot

L1707 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.span_le_jacobson_bot

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Bookkeeping
variable (x : R)

Lean source · statement

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

theorem

free_self

L1718 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.free_self

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section RankOne
variable (x : R)

Lean source · statement

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

theorem

span_eq_top_of_span_quotientMk_eq_top

L1746 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.span_eq_top_of_span_quotientMk_eq_top

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Engines
variable [IsLocalRing R] (x : R)

Lean source · full declaration

theorem span_eq_top_of_span_quotientMk_eq_top [Module.Finite R M]
    (hx : x ∈ maximalIdeal R) {ι : Type*} (m : ι → M)
    (hspan : Submodule.span (R ⧸ Ideal.span {x})
      (Set.range fun i => (Submodule.Quotient.mk (m i) : QuotSMulTop x M)) = ⊤) :
    Submodule.span R (Set.range m) = ⊤ := by
  have h1 : Submodule.span R
      (Set.range fun i => (Submodule.Quotient.mk (m i) : QuotSMulTop x M)) = ⊤ := by
    rw [← Submodule.restrictScalars_span R (R ⧸ Ideal.span {x}) Ideal.Quotient.mk_surjective,
      hspan, Submodule.restrictScalars_top]
  have h2 : (Submodule.span R (Set.range m)).map
      (Submodule.mkQ (x • ⊤ : Submodule R M)) = ⊤ := by
    rw [Submodule.map_span, ← Set.range_comp]
    exact h1
  rw [Submodule.map_mkQ_eq_top] at h2
  refine top_le_iff.mp (Submodule.le_of_le_smul_of_le_jacobson_bot Module.Finite.fg_top
    (span_le_jacobson_bot x hx) ?_)
  rw [Submodule.ideal_span_singleton_smul, sup_comm, h2]

theorem

linearIndependent_of_quotientMk_linearIndependent

L1764 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.linearIndependent_of_quotientMk_linearIndependent

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Engines
variable [IsLocalRing R] (x : R)

Lean source · full declaration

theorem linearIndependent_of_quotientMk_linearIndependent [IsNoetherianRing R]
    (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular M x) {ι : Type*} [Finite ι] (m : ι → M)
    (hli : LinearIndependent (R ⧸ Ideal.span {x})
      (fun i => (Submodule.Quotient.mk (m i) : QuotSMulTop x M))) :
    LinearIndependent R m := by
  classical
  let : Fintype ι := Fintype.ofFinite ι
  have hker_le : LinearMap.ker (Fintype.linearCombination R m) ≤
      Ideal.span {x} • LinearMap.ker (Fintype.linearCombination R m) := by
    intro a ha
    rw [LinearMap.mem_ker, Fintype.linearCombination_apply] at ha
    have hcoeff : ∀ i, Ideal.Quotient.mk (Ideal.span {x}) (a i) = 0 := by
      have h0 : ∑ i, (Ideal.Quotient.mk (Ideal.span {x}) (a i)) •
          (Submodule.Quotient.mk (m i) : QuotSMulTop x M) = 0 := by
        have hterm : ∀ i, (Ideal.Quotient.mk (Ideal.span {x}) (a i)) •
            (Submodule.Quotient.mk (m i) : QuotSMulTop x M)
            = (Submodule.mkQ (x • ⊤ : Submodule R M)) (a i • m i) := fun i => rfl
        simp_rw [hterm, ← map_sum, ha, map_zero]
      exact Fintype.linearIndependent_iff.mp hli _ h0
    have hdvd : ∀ i, x ∣ a i := fun i =>
      Ideal.mem_span_singleton.mp (Ideal.Quotient.eq_zero_iff_mem.mp (hcoeff i))
    choose c hc using hdvd
    have ha_eq : a = x • c := funext fun i => by
      rw [Pi.smul_apply, smul_eq_mul]; exact hc i
    have hc_ker : c ∈ LinearMap.ker (Fintype.linearCombination R m) := by
      rw [LinearMap.mem_ker]
      apply hreg
      change x • Fintype.linearCombination R m c = x • (0 : M)
      rw [smul_zero, ← map_smul, ← ha_eq]
      exact ha
    rw [ha_eq]
    exact Submodule.smul_mem_smul (Ideal.mem_span_singleton_self x) hc_ker
  have hker : LinearMap.ker (Fintype.linearCombination R m) = ⊥ :=
    Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (Ideal.span {x}) _
      (IsNoetherian.noetherian _) hker_le (span_le_jacobson_bot x hx)
  rw [Fintype.linearIndependent_iff]
  intro g hg i
  have hg_ker : g ∈ LinearMap.ker (Fintype.linearCombination R m) := by
    rw [LinearMap.mem_ker, Fintype.linearCombination_apply]
    exact hg
  rw [hker, Submodule.mem_bot] at hg_ker
  exact congrFun hg_ker i

theorem

exists_basis_lift

L1813 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.QuotSMulTop.exists_basis_lift

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
namespace QuotSMulTop
open _root_.QuotSMulTop
section Main
variable [IsLocalRing R] [IsNoetherianRing R] [Module.Finite R M] (x : R)

Lean source · statement

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

theorem

free_of_quotSMulTop_free

L1846 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.free_of_quotSMulTop_free

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
open scoped Ws14Port.QuotSMulTop
section MainTheorems
variable [IsLocalRing R] [IsNoetherianRing R] [Module.Finite R M]

Lean source · statement

theorem Module.free_of_quotSMulTop_free (x : R) (hx : x ∈ IsLocalRing.maximalIdeal R)
    (hreg : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    Module.Free R M

theorem

free_of_quotSMulTop_free_of_regular_param

L1857 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.free_of_quotSMulTop_free_of_regular_param

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
open scoped Ws14Port.QuotSMulTop
section MainTheorems
variable [IsLocalRing R] [IsNoetherianRing R] [Module.Finite R M]

Lean source · statement

theorem Module.free_of_quotSMulTop_free_of_regular_param (x : R)
    (hx : x ∈ IsLocalRing.maximalIdeal R) (_hx2 : x ∉ (IsLocalRing.maximalIdeal R) ^ 2)
    (_hregR : IsSMulRegular R x) (hregM : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    Module.Free R M

theorem

finrank_quotSMulTop_eq

L1864 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.Module.finrank_quotSMulTop_eq

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Function
open scoped Pointwise
open Ws14Port.Module
open scoped Ws14Port.Module
noncomputable section
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
open scoped Ws14Port.QuotSMulTop
section MainTheorems
variable [IsLocalRing R] [IsNoetherianRing R] [Module.Finite R M]

Lean source · statement

theorem Module.finrank_quotSMulTop_eq (x : R) (hx : x ∈ IsLocalRing.maximalIdeal R)
    (hreg : IsSMulRegular M x)
    (hfree : Module.Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) :
    Module.finrank (R ⧸ Ideal.span {x}) (QuotSMulTop x M) = Module.finrank R M

theorem

isLocalRing_quotient_span_singleton

L1895 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.isLocalRing_quotient_span_singleton

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

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

theorem

isScalarTower_quotient_span_singleton

L1904 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.isScalarTower_quotient_span_singleton

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

theorem isScalarTower_quotient_span_singleton {M : Type v} [AddCommGroup M] [Module R M]
    (x : R) : IsScalarTower R (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

theorem

moduleFinite_quotient_span_singleton

L1910 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.moduleFinite_quotient_span_singleton

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

theorem moduleFinite_quotient_span_singleton {M : Type v} [AddCommGroup M] [Module R M]
    [Module.Finite R M] (x : R) :
    Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)

theorem

nontrivial_quotSMulTop_of_mem_maximalIdeal

L1916 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.nontrivial_quotSMulTop_of_mem_maximalIdeal

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

theorem nontrivial_quotSMulTop_of_mem_maximalIdeal [IsLocalRing R] {M : Type v}
    [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] {x : R}
    (hx : x ∈ maximalIdeal R) : Nontrivial (QuotSMulTop x M)

theorem

exists_ringKrullDim_eq_natCast

L1926 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.exists_ringKrullDim_eq_natCast

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientInfrastructure
variable {R : Type u} [CommRing R]

Lean source · statement

theorem exists_ringKrullDim_eq_natCast (R : Type u) [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] : ∃ d : ℕ, ringKrullDim R = (d : WithBot ℕ∞)

theorem

isField_of_spanFinrank_maximalIdeal_eq_zero

L1943 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.isField_of_spanFinrank_maximalIdeal_eq_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section BaseCase
variable (R : Type u) [CommRing R] [IsRegularLocalRing R]

Lean source · statement

theorem isField_of_spanFinrank_maximalIdeal_eq_zero
    (hn : (maximalIdeal R).spanFinrank = 0) : IsField R

theorem

free_of_spanFinrank_maximalIdeal_eq_zero

L1951 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.free_of_spanFinrank_maximalIdeal_eq_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section BaseCase
variable (R : Type u) [CommRing R] [IsRegularLocalRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]

Lean source · statement

theorem free_of_spanFinrank_maximalIdeal_eq_zero
    (hn : (maximalIdeal R).spanFinrank = 0) : Module.Free R M

theorem

free_of_ringKrullDim_eq_zero

L1956 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.free_of_ringKrullDim_eq_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section BaseCase
variable (R : Type u) [CommRing R] [IsRegularLocalRing R]
variable (M : Type v) [AddCommGroup M] [Module R M]

Lean source · statement

theorem free_of_ringKrullDim_eq_zero (hdim : ringKrullDim R = 0) : Module.Free R M

theorem

exists_finite_span_eq_maximalIdeal_mem

L1968 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.exists_finite_span_eq_maximalIdeal_mem

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Exchange
variable (R : Type u) [CommRing R]

Lean source · statement

theorem exists_finite_span_eq_maximalIdeal_mem [IsLocalRing R] [IsNoetherianRing R]
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2) :
    ∃ S : Set R, x ∈ S ∧ S.Finite ∧ S.ncard ≤ (maximalIdeal R).spanFinrank ∧
      Ideal.span S = maximalIdeal R

theorem

isRegularLocalRing_quotient_span_singleton

L2033 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.isRegularLocalRing_quotient_span_singleton

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Exchange
variable (R : Type u) [CommRing R]
variable [IsRegularLocalRing R]

Lean source · statement

theorem isRegularLocalRing_quotient_span_singleton
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2)
    (hxreg : IsSMulRegular R x) [IsLocalRing (R ⧸ Ideal.span {x})] :
    IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧
      (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1 =
        (maximalIdeal R).spanFinrank

def

JointRegularElementSelection

L2113 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.JointRegularElementSelection

Documentation

Existence of a common regular element outside the square of the maximal ideal.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Carriers

Lean source · statement

def JointRegularElementSelection : Prop

def

DepthDropQuotient

L2120 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.DepthDropQuotient

Documentation

Depth drops by one after quotienting by a common regular element.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Carriers

Lean source · statement

def DepthDropQuotient : Prop

def

QuotientInductionStep

L2128 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.QuotientInductionStep

Documentation

The quotient step for induction on regular local rings and finite modules.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Carriers

Lean source · statement

def QuotientInductionStep : Prop

theorem

free_of_depth_eq_ringKrullDim_aux

L2140 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_aux

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Assembly

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_aux
    (hsel : JointRegularElementSelection.{u, v})
    (hdrop : DepthDropQuotient.{u, v})
    (hstep : QuotientInductionStep.{u, v}) :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R]
      (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M],
      (maximalIdeal R).spanFinrank = n →
      .some (Module.depth R M) = ringKrullDim R → Module.Free R M

theorem

free_of_depth_eq_ringKrullDim

L2196 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Assembly

Lean source · statement

theorem free_of_depth_eq_ringKrullDim
    (hsel : JointRegularElementSelection.{u, v})
    (hdrop : DepthDropQuotient.{u, v})
    (hstep : QuotientInductionStep.{u, v})
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (H : .some (Module.depth R M) = ringKrullDim R) : Module.Free R M

theorem

free_of_depth_eq_ringKrullDim_of_dim_zero

L2206 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_of_dim_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Assembly

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_of_dim_zero
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (hdim : ringKrullDim R = 0) : Module.Free R M

theorem

quotientInductionStep_holds

L2216 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.quotientInductionStep_holds

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section SiblingWiring

Lean source · statement

theorem quotientInductionStep_holds : QuotientInductionStep.{u, v}

def

RegularPositiveDepth

L2221 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.RegularPositiveDepth

Documentation

A regular local ring of positive dimension has positive depth.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section SiblingWiring

Lean source · statement

def RegularPositiveDepth : Prop

theorem

jointRegularElementSelection_of_regularPositiveDepth

L2225 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.jointRegularElementSelection_of_regularPositiveDepth

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section SiblingWiring

Lean source · statement

theorem jointRegularElementSelection_of_regularPositiveDepth
    (hbridge : RegularPositiveDepth.{u}) : JointRegularElementSelection.{u, v}

theorem

free_of_depth_eq_ringKrullDim_of_landed_siblings

L2231 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_of_landed_siblings

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section SiblingWiring

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_of_landed_siblings
    (hbridge : RegularPositiveDepth.{u})
    (hdrop : DepthDropQuotient.{u, v})
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (H : .some (Module.depth R M) = ringKrullDim R) : Module.Free R M

theorem

depthDropQuotient_holds

L2253 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.depthDropQuotient_holds

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace No4PatchingCore
open No4PatchingCore

Lean source · statement

theorem depthDropQuotient_holds : DepthDropQuotient.{u, v}

theorem

maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos

L2270 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section PrimeAvoidance

Lean source · statement

theorem maximalIdeal_notMem_minimalPrimes_of_ringKrullDim_pos
    (R : Type u) [CommRing R] [IsLocalRing R] (hdim : 0 < ringKrullDim R) :
    maximalIdeal R ∉ minimalPrimes R

theorem

exists_parameter_notMem_minimalPrimes

L2287 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.exists_parameter_notMem_minimalPrimes

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section PrimeAvoidance

Lean source · statement

theorem exists_parameter_notMem_minimalPrimes
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdim : 0 < ringKrullDim R) :
    ∃ x ∈ maximalIdeal R, x ∉ (maximalIdeal R) ^ 2 ∧ ∀ p ∈ minimalPrimes R, x ∉ p

theorem

annihilator_self_eq_bot

L2333 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.annihilator_self_eq_bot

Source context 14 commands

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

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

Lean source · statement

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

theorem

ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes

L2338 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes

Source context 14 commands

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

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

Lean source · statement

theorem ringKrullDim_quotSMulTop_succ_eq_of_forall_notMem_minimalPrimes
    {x : R} (hx : x ∈ maximalIdeal R) (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) :
    ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R

theorem

ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes

L2348 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes

Source context 14 commands

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

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

Lean source · statement

theorem ringKrullDim_quotient_span_singleton_succ_eq_of_forall_notMem_minimalPrimes
    {x : R} (hx : x ∈ maximalIdeal R) (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) :
    ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem

isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes

L2364 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section QuotientRegularity
variable (R : Type u) [CommRing R] [IsRegularLocalRing R]

Lean source · statement

theorem isRegularLocalRing_quotient_span_singleton_of_forall_notMem_minimalPrimes
    {x : R} (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2)
    (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) [IsLocalRing (R ⧸ Ideal.span {x})] :
    IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧
      (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1 =
        (maximalIdeal R).spanFinrank

theorem

isDomain_of_isRegularLocalRing_aux

L2443 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.isDomain_of_isRegularLocalRing_aux

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section MatsumuraDomain

Lean source · statement

theorem isDomain_of_isRegularLocalRing_aux :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R],
      (maximalIdeal R).spanFinrank = n → IsDomain R

theorem

isDomain_of_isRegularLocalRing

L2497 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.isDomain_of_isRegularLocalRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section MatsumuraDomain

Lean source · statement

theorem isDomain_of_isRegularLocalRing (R : Type u) [CommRing R] [IsRegularLocalRing R] :
    IsDomain R

theorem

depth_self_pos_of_isRegularLocalRing

L2505 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.depth_self_pos_of_isRegularLocalRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section PositiveDepth

Lean source · statement

theorem depth_self_pos_of_isRegularLocalRing (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (hdim : 0 < ringKrullDim R) : 0 < Module.depth R R

theorem

regularPositiveDepth_holds

L2514 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.regularPositiveDepth_holds

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section PositiveDepth

Lean source · statement

theorem regularPositiveDepth_holds : RegularPositiveDepth.{u}

theorem

jointRegularElementSelection_holds

L2522 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.jointRegularElementSelection_holds

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Unconditional

Lean source · statement

theorem jointRegularElementSelection_holds : JointRegularElementSelection.{u, v}

theorem

free_of_depth_eq_ringKrullDim_unconditional

L2525 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.No4PatchingCore.free_of_depth_eq_ringKrullDim_unconditional

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open scoped Pointwise
namespace No4PatchingCore
open No4PatchingCore
section Unconditional

Lean source · statement

theorem free_of_depth_eq_ringKrullDim_unconditional
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (H : .some (Module.depth R M) = ringKrullDim R) : Module.Free R M

def

CMUnmixednessHypothesis

L2550 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.CMUnmixednessHypothesis

Documentation

Associated prime quotients of a Cohen-Macaulay local ring have the same dimension.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

def CMUnmixednessHypothesis : Prop

theorem

cmUnmixednessHypothesis_of_depth_le_dim

L2555 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.cmUnmixednessHypothesis_of_depth_le_dim

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem cmUnmixednessHypothesis_of_depth_le_dim
    (h : ∀ (S : Type u) [CommRing S] [IsLocalRing S] [IsNoetherianRing S],
      ∀ p ∈ associatedPrimes S S,
        (.some (Module.depth S S) : WithBot ℕ∞) ≤ ringKrullDim (S ⧸ p)) :
    CMUnmixednessHypothesis.{u}

theorem

isAssociatedPrime_eq_bot_of_isDomain

L2565 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isAssociatedPrime_eq_bot_of_isDomain

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isAssociatedPrime_eq_bot_of_isDomain {S : Type u} [CommRing S] [IsDomain S]
    [IsNoetherianRing S] {p : Ideal S} (hp : IsAssociatedPrime p S) : p = ⊥

theorem

unmixedness_of_isDomain

L2583 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.unmixedness_of_isDomain

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem unmixedness_of_isDomain (S : Type u) [CommRing S] [IsLocalRing S] [IsNoetherianRing S]
    [IsDomain S] :
    ∀ p ∈ associatedPrimes S S, ringKrullDim (S ⧸ p) = ringKrullDim S

theorem

depth_le_ringKrullDim_quotient_of_isDomain

L2590 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.depth_le_ringKrullDim_quotient_of_isDomain

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem depth_le_ringKrullDim_quotient_of_isDomain (S : Type u) [CommRing S] [IsLocalRing S]
    [IsNoetherianRing S] [IsDomain S] :
    ∀ p ∈ associatedPrimes S S,
      (.some (Module.depth S S) : WithBot ℕ∞) ≤ ringKrullDim (S ⧸ p)

theorem

exists_ringKrullDim_eq_natCast

L2599 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.exists_ringKrullDim_eq_natCast

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem exists_ringKrullDim_eq_natCast (S : Type u) [CommRing S] [IsLocalRing S]
    [IsNoetherianRing S] :
    ∃ m : ℕ, ringKrullDim S = (m : WithBot ℕ∞)

theorem

eq_maximalIdeal_of_ringKrullDim_quotient_le_zero

L2609 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.eq_maximalIdeal_of_ringKrullDim_quotient_le_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem eq_maximalIdeal_of_ringKrullDim_quotient_le_zero {R : Type u} [CommRing R]
    [IsLocalRing R] {p : Ideal R} [p.IsPrime]
    (h : ringKrullDim (R ⧸ p) ≤ 0) : p = maximalIdeal R

theorem

notMem_of_ringKrullDim_quotient_cons_le_zero

L2619 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.notMem_of_ringKrullDim_quotient_cons_le_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem notMem_of_ringKrullDim_quotient_cons_le_zero {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] {x : R} {rest : List R}
    (hmem : ∀ y ∈ x :: rest, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList (x :: rest)) ≤ 0)
    {p : Ideal R} (hp : p.IsPrime)
    (hpdim : ringKrullDim (R ⧸ p) = ringKrullDim R)
    (hlen : ((rest.length : ℕ) : WithBot ℕ∞) < ringKrullDim R) :
    x ∉ p

theorem

isRegular_of_sop_of_cmUnmixedness

L2678 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isRegular_of_sop_of_cmUnmixedness

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isRegular_of_sop_of_cmUnmixedness (hunmix : CMUnmixednessHypothesis.{u}) :
    ∀ (d : ℕ) (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R],
      (.some (Module.depth R R) : WithBot ℕ∞) = ringKrullDim R →
      ringKrullDim R = (d : WithBot ℕ∞) →
      ∀ xs : List R, xs.length = d →
        (∀ y ∈ xs, y ∈ maximalIdeal R) →
        ringKrullDim (R ⧸ Ideal.ofList xs) = 0 →
        Sequence.IsRegular R xs

theorem

isRegular_of_sop

L2768 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isRegular_of_sop

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isRegular_of_sop {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hunmix : CMUnmixednessHypothesis.{u}) {d : ℕ}
    (hCM : (.some (Module.depth R R) : WithBot ℕ∞) = ringKrullDim R)
    (hdim : ringKrullDim R = (d : WithBot ℕ∞))
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList xs) = 0) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop

L2778 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.isRegular_of_sop

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem IsCohenMacaulayOfDim.isRegular_of_sop {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] {d : ℕ} (hCM : IsCohenMacaulayOfDim R d)
    (hunmix : CMUnmixednessHypothesis.{u})
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList xs) = 0) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop_of_ringKrullDim_eq_zero

L2789 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isRegular_of_sop_of_ringKrullDim_eq_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isRegular_of_sop_of_ringKrullDim_eq_zero {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R]
    (_hdim : ringKrullDim R = (0 : WithBot ℕ∞))
    (xs : List R) (hlen : xs.length = 0) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop_of_ringKrullDim_eq_one

L2798 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isRegular_of_sop_of_ringKrullDim_eq_one

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
open _root_.Submodule
open _root_.Pointwise
noncomputable section
namespace IsLocalRing
open _root_.Module.IsLocalRing

Lean source · statement

theorem isRegular_of_sop_of_ringKrullDim_eq_one {R : Type u} [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R]
    (hCM : (.some (Module.depth R R) : WithBot ℕ∞) = ringKrullDim R)
    (hdim : ringKrullDim R = ((1 : ℕ) : WithBot ℕ∞))
    (xs : List R) (hlen : xs.length = 1)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList xs) = 0) :
    Sequence.IsRegular R xs

theorem

ne_top_of_radical_eq_maximalIdeal

L2878 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.ne_top_of_radical_eq_maximalIdeal

Source context 15 commands

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

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

Lean source · statement

theorem ne_top_of_radical_eq_maximalIdeal {I : Ideal R}
    (hrad : I.radical = maximalIdeal R) : I ≠ ⊤

theorem

isPrime_quotient_eq_map_maximalIdeal_of_radical_eq_maximalIdeal

L2885 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isPrime_quotient_eq_map_maximalIdeal_of_radical_eq_maximalIdeal

Source context 15 commands

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

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

Lean source · statement

theorem isPrime_quotient_eq_map_maximalIdeal_of_radical_eq_maximalIdeal {I : Ideal R}
    (hrad : I.radical = maximalIdeal R) (P : Ideal (R ⧸ I)) (hP : P.IsPrime) :
    P = Ideal.map (Ideal.Quotient.mk I) (maximalIdeal R)

theorem

ringKrullDim_quotient_eq_zero_of_radical_eq_maximalIdeal

L2903 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.ringKrullDim_quotient_eq_zero_of_radical_eq_maximalIdeal

Source context 15 commands

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

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

Lean source · statement

theorem ringKrullDim_quotient_eq_zero_of_radical_eq_maximalIdeal {I : Ideal R}
    (hrad : I.radical = maximalIdeal R) :
    ringKrullDim (R ⧸ I) = 0

theorem

eq_maximalIdeal_of_isPrime_of_le_of_ringKrullDim_quotient_le_zero

L2919 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.eq_maximalIdeal_of_isPrime_of_le_of_ringKrullDim_quotient_le_zero

Source context 15 commands

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

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

Lean source · statement

theorem eq_maximalIdeal_of_isPrime_of_le_of_ringKrullDim_quotient_le_zero {I p : Ideal R}
    (hdim : ringKrullDim (R ⧸ I) ≤ 0) (hp : p.IsPrime) (hIp : I ≤ p) :
    p = maximalIdeal R

theorem

radical_eq_maximalIdeal_of_ringKrullDim_quotient_eq_zero

L2930 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.radical_eq_maximalIdeal_of_ringKrullDim_quotient_eq_zero

Source context 15 commands

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

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

Lean source · statement

theorem radical_eq_maximalIdeal_of_ringKrullDim_quotient_eq_zero {I : Ideal R}
    (hne : I ≠ ⊤) (hdim : ringKrullDim (R ⧸ I) = 0) :
    I.radical = maximalIdeal R

theorem

radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero

L2941 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero

Source context 15 commands

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

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

Lean source · statement

theorem radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero (I : Ideal R) :
    I.radical = maximalIdeal R ↔ (I ≠ ⊤ ∧ ringKrullDim (R ⧸ I) = 0)

theorem

radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero_of_noetherian

L2947 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero_of_noetherian

Source context 15 commands

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

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

Lean source · statement

theorem radical_eq_maximalIdeal_iff_ne_top_and_ringKrullDim_quotient_eq_zero_of_noetherian
    [IsNoetherianRing R] (I : Ideal R) :
    I.radical = IsLocalRing.maximalIdeal R ↔ (I ≠ ⊤ ∧ ringKrullDim (R ⧸ I) = 0)

theorem

ofList_ne_top_of_forall_mem_maximalIdeal

L2952 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.ofList_ne_top_of_forall_mem_maximalIdeal

Source context 15 commands

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

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

Lean source · statement

theorem ofList_ne_top_of_forall_mem_maximalIdeal {xs : List R}
    (hmem : ∀ x ∈ xs, x ∈ maximalIdeal R) :
    Ideal.ofList xs ≠ ⊤

theorem

ofList_radical_eq_maximalIdeal_iff_ringKrullDim_quotient_eq_zero

L2958 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.ofList_radical_eq_maximalIdeal_iff_ringKrullDim_quotient_eq_zero

Source context 15 commands

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

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

Lean source · statement

theorem ofList_radical_eq_maximalIdeal_iff_ringKrullDim_quotient_eq_zero {xs : List R}
    (hmem : ∀ x ∈ xs, x ∈ maximalIdeal R) :
    (Ideal.ofList xs).radical = maximalIdeal R ↔
      ringKrullDim (R ⧸ Ideal.ofList xs) = 0

def

matsumuraThm174iiiSopRegularRowRadicalForm

L2966 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowRadicalForm

Documentation

The radical criterion for a system of parameters to form a regular row.

Source context 15 commands

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

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

Lean source · statement

def matsumuraThm174iiiSopRegularRowRadicalForm (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] : Prop

def

matsumuraThm174iiiSopRegularRowQuotientDimForm

L2976 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowQuotientDimForm

Documentation

The quotient dimension criterion for a system of parameters to form a regular row.

Source context 15 commands

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

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

Lean source · statement

def matsumuraThm174iiiSopRegularRowQuotientDimForm (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] : Prop

theorem

matsumuraThm174iiiSopRegularRow_radicalForm_iff_quotientDimForm

L2985 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRow_radicalForm_iff_quotientDimForm

Source context 15 commands

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

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

Lean source · statement

theorem matsumuraThm174iiiSopRegularRow_radicalForm_iff_quotientDimForm
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowRadicalForm R ↔
      matsumuraThm174iiiSopRegularRowQuotientDimForm R

theorem

matsumuraThm174iiiSopRegularRowQuotientDimForm_of_cmUnmixedness

L2997 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowQuotientDimForm_of_cmUnmixedness

Source context 15 commands

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

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

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowQuotientDimForm_of_cmUnmixedness
    (hunmix : CMUnmixednessHypothesis.{u}) (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowQuotientDimForm R

theorem

matsumuraThm174iiiSopRegularRowRadicalForm_of_cmUnmixedness

L3003 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowRadicalForm_of_cmUnmixedness

Source context 15 commands

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

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

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowRadicalForm_of_cmUnmixedness
    (hunmix : CMUnmixednessHypothesis.{u}) (R : Type u) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowRadicalForm R

theorem

isRegular_of_sop_radical

L3010 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.isRegular_of_sop_radical

Source context 15 commands

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

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

Lean source · statement

theorem IsCohenMacaulayOfDim.isRegular_of_sop_radical {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] {d : ℕ} (hCM : IsCohenMacaulayOfDim R d)
    (hunmix : CMUnmixednessHypothesis.{u})
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hrad : (Ideal.ofList xs).radical = maximalIdeal R) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop_radical_of_ringKrullDim_eq_one

L3020 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.isRegular_of_sop_radical_of_ringKrullDim_eq_one

Source context 15 commands

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

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

Lean source · statement

theorem isRegular_of_sop_radical_of_ringKrullDim_eq_one {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R]
    (hCM : (.some (Module.depth R R) : WithBot ℕ∞) = ringKrullDim R)
    (hdim : ringKrullDim R = ((1 : ℕ) : WithBot ℕ∞))
    (xs : List R) (hlen : xs.length = 1)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hrad : (Ideal.ofList xs).radical = maximalIdeal R) :
    Sequence.IsRegular R xs

theorem

cmUnmixednessHypothesis_holds

L3031 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.cmUnmixednessHypothesis_holds

Source context 15 commands

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

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

Lean source · statement

theorem cmUnmixednessHypothesis_holds : CMUnmixednessHypothesis.{u}

theorem

matsumuraThm174iiiSopRegularRowQuotientDimForm_holds

L3036 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowQuotientDimForm_holds

Source context 15 commands

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

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

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowQuotientDimForm_holds (R : Type u) [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowQuotientDimForm R

theorem

matsumuraThm174iiiSopRegularRowRadicalForm_holds

L3042 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.matsumuraThm174iiiSopRegularRowRadicalForm_holds

Source context 15 commands

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

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

Lean source · statement

theorem matsumuraThm174iiiSopRegularRowRadicalForm_holds (R : Type u) [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] :
    matsumuraThm174iiiSopRegularRowRadicalForm R

theorem

isRegular_of_sop_unconditional

L3047 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.isRegular_of_sop_unconditional

Source context 15 commands

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

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

Lean source · statement

theorem IsCohenMacaulayOfDim.isRegular_of_sop_unconditional {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] {d : ℕ} (hCM : IsCohenMacaulayOfDim R d)
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hsop : ringKrullDim (R ⧸ Ideal.ofList xs) = 0) :
    Sequence.IsRegular R xs

theorem

isRegular_of_sop_radical_unconditional

L3055 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.IsLocalRing.IsCohenMacaulayOfDim.isRegular_of_sop_radical_unconditional

Source context 15 commands

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

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

Lean source · statement

theorem IsCohenMacaulayOfDim.isRegular_of_sop_radical_unconditional {R : Type u} [CommRing R]
    [IsLocalRing R] [IsNoetherianRing R] {d : ℕ} (hCM : IsCohenMacaulayOfDim R d)
    (xs : List R) (hlen : xs.length = d)
    (hmem : ∀ y ∈ xs, y ∈ maximalIdeal R)
    (hrad : (Ideal.ofList xs).radical = maximalIdeal R) :
    Sequence.IsRegular R xs

theorem

sumElim_injective2

L3082 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.Finsupp.sumElim_injective2

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section IndexBijection
variable {α β : Type*}

Lean source · statement

theorem Finsupp.sumElim_injective2 :
    Function.Injective2 (Finsupp.sumElim : (α →₀ ℕ) → (β →₀ ℕ) → (α ⊕ β →₀ ℕ))

theorem

sumElim_eq_zero_iff

L3091 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.Finsupp.sumElim_eq_zero_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section IndexBijection
variable {α β : Type*}

Lean source · statement

theorem Finsupp.sumElim_eq_zero_iff {a : α →₀ ℕ} {b : β →₀ ℕ} :
    a.sumElim b = 0 ↔ a = 0 ∧ b = 0

theorem

sumElim_eq_single_inl_iff

L3100 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.Finsupp.sumElim_eq_single_inl_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section IndexBijection
variable {α β : Type*}

Lean source · statement

theorem Finsupp.sumElim_eq_single_inl_iff {a : α →₀ ℕ} {b : β →₀ ℕ} {s : α} {c : ℕ} :
    a.sumElim b = Finsupp.single (Sum.inl s) c ↔ a = Finsupp.single s c ∧ b = 0

theorem

sumElim_eq_single_inr_iff

L3109 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.Finsupp.sumElim_eq_single_inr_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section IndexBijection
variable {α β : Type*}

Lean source · statement

theorem Finsupp.sumElim_eq_single_inr_iff {a : α →₀ ℕ} {b : β →₀ ℕ} {t : β} {c : ℕ} :
    a.sumElim b = Finsupp.single (Sum.inr t) c ↔ a = 0 ∧ b = Finsupp.single t c

def

sumToFun

L3125 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.sumToFun

Documentation

Separate the variables of a power series indexed by a disjoint union.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]

Lean source · statement

def sumToFun (f : MvPowerSeries (α ⊕ β) R) : MvPowerSeries α (MvPowerSeries β R)

def

sumInvFun

L3129 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.sumInvFun

Documentation

Combine the two sets of variables in an iterated power series.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]

Lean source · statement

def sumInvFun (g : MvPowerSeries α (MvPowerSeries β R)) : MvPowerSeries (α ⊕ β) R

theorem

coeff_sumToFun

L3136 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.coeff_sumToFun

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}

Lean source · statement

theorem coeff_sumToFun (f : MvPowerSeries (α ⊕ β) R) (a : α →₀ ℕ) (b : β →₀ ℕ) :
    coeff b (coeff a (sumToFun α β f)) = coeff (a.sumElim b) f

theorem

coeff_sumInvFun

L3140 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.coeff_sumInvFun

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}

Lean source · statement

theorem coeff_sumInvFun (g : MvPowerSeries α (MvPowerSeries β R)) (d : α ⊕ β →₀ ℕ) :
    coeff d (sumInvFun α β g) =
      coeff (d.comapDomain Sum.inr Sum.inr_injective.injOn)
        (coeff (d.comapDomain Sum.inl Sum.inl_injective.injOn) g)

theorem

coeff_mul_sumElim

L3146 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.coeff_mul_sumElim

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}

Lean source · statement

theorem coeff_mul_sumElim [DecidableEq α] [DecidableEq β]
    (f g : MvPowerSeries (α ⊕ β) R) (a : α →₀ ℕ) (b : β →₀ ℕ) :
    coeff (a.sumElim b) (f * g) =
      ∑ q ∈ antidiagonal a, ∑ r ∈ antidiagonal b,
        coeff (q.1.sumElim r.1) f * coeff (q.2.sumElim r.2) g

def

sumRingEquiv

L3163 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.sumRingEquiv

Documentation

The ring equivalence separating variables indexed by a disjoint union.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in

Lean source · full declaration

def sumRingEquiv : MvPowerSeries (α ⊕ β) R ≃+* MvPowerSeries α (MvPowerSeries β R) where
  toFun := sumToFun α β
  invFun := sumInvFun α β
  left_inv f := by
    ext d
    rw [show coeff d (sumInvFun α β (sumToFun α β f)) =
        coeff ((d.comapDomain Sum.inl Sum.inl_injective.injOn).sumElim
          (d.comapDomain Sum.inr Sum.inr_injective.injOn)) f from rfl,
      Finsupp.comapDomain_sumElim_comapDomain]
  right_inv g := by
    ext a b
    rw [show coeff b (coeff a (sumToFun α β (sumInvFun α β g))) =
        coeff ((a.sumElim b).comapDomain Sum.inr Sum.inr_injective.injOn)
          (coeff ((a.sumElim b).comapDomain Sum.inl Sum.inl_injective.injOn) g) from rfl,
      Finsupp.comapDomain_inl_sumElim, Finsupp.comapDomain_inr_sumElim]
  map_add' f g := by
    ext a b
    simp only [map_add, coeff_sumToFun]
  map_mul' f g := by
    classical
    ext a b
    rw [coeff_sumToFun, coeff_mul_sumElim]
    rw [show coeff a (sumToFun α β f * sumToFun α β g) =
        ∑ q ∈ antidiagonal a, coeff q.1 (sumToFun α β f) * coeff q.2 (sumToFun α β g) from
      coeff_mul (φ := sumToFun α β f) (ψ := sumToFun α β g) (n := a), map_sum]
    refine Finset.sum_congr rfl fun q _ => ?_
    rw [show coeff b (coeff q.1 (sumToFun α β f) * coeff q.2 (sumToFun α β g)) =
        ∑ r ∈ antidiagonal b, coeff r.1 (coeff q.1 (sumToFun α β f)) *
          coeff r.2 (coeff q.2 (sumToFun α β g)) from coeff_mul ..]
    exact Finset.sum_congr rfl fun r _ => by rw [coeff_sumToFun, coeff_sumToFun]

theorem

coeff_sumRingEquiv

L3194 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.coeff_sumRingEquiv

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in

Lean source · statement

theorem coeff_sumRingEquiv (f : MvPowerSeries (α ⊕ β) R) (a : α →₀ ℕ) (b : β →₀ ℕ) :
    coeff b (coeff a (sumRingEquiv α β R f)) = coeff (a.sumElim b) f

theorem

sumRingEquiv_X_inl

L3198 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.sumRingEquiv_X_inl

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in

Lean source · statement

theorem sumRingEquiv_X_inl (s : α) :
    sumRingEquiv α β R (X (Sum.inl s)) = X s

theorem

sumRingEquiv_X_inr

L3208 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.sumRingEquiv_X_inr

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in

Lean source · statement

theorem sumRingEquiv_X_inr (t : β) :
    sumRingEquiv α β R (X (Sum.inr t)) = C (X t)

theorem

sumRingEquiv_C

L3217 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.sumRingEquiv_C

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section SumRingEquiv
variable (α β : Type*) {R : Type*} [CommSemiring R]
variable {α β}
variable (α β) (R) in

Lean source · statement

theorem sumRingEquiv_C (r : R) :
    sumRingEquiv α β R (C r) = C (C r)

def

finSuccSumEquiv

L3232 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccSumEquiv

Documentation

Separate the first finite index from the remaining indices.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]

Lean source · full declaration

def finSuccSumEquiv (n : ℕ) : Fin (n + 1) ≃ Unit ⊕ Fin n where
  toFun := Fin.cases (Sum.inl ()) (fun i => Sum.inr i)
  invFun := Sum.elim (fun _ => 0) Fin.succ
  left_inv i := by
    induction i using Fin.cases <;> simp
  right_inv x := by
    rcases x with ⟨⟩ | i <;> simp

theorem

finSuccSumEquiv_zero

L3240 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccSumEquiv_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]

Lean source · statement

theorem finSuccSumEquiv_zero (n : ℕ) : finSuccSumEquiv n 0 = Sum.inl ()

theorem

finSuccSumEquiv_succ

L3242 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccSumEquiv_succ

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]

Lean source · statement

theorem finSuccSumEquiv_succ (n : ℕ) (i : Fin n) :
    finSuccSumEquiv n i.succ = Sum.inr i

def

finSuccRingEquiv

L3248 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccRingEquiv

Documentation

Express power series in finitely many variables as an iterated power series ring.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in

Lean source · statement

def finSuccRingEquiv (n : ℕ) :
    MvPowerSeries (Fin (n + 1)) R ≃+* PowerSeries (MvPowerSeries (Fin n) R)

theorem

finSuccRingEquiv_apply

L3252 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccRingEquiv_apply

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in

Lean source · statement

theorem finSuccRingEquiv_apply (n : ℕ) (f : MvPowerSeries (Fin (n + 1)) R) :
    finSuccRingEquiv R n f =
      sumRingEquiv Unit (Fin n) R (rename (finSuccSumEquiv n) f)

theorem

finSuccRingEquiv_X_zero

L3257 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccRingEquiv_X_zero

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in

Lean source · statement

theorem finSuccRingEquiv_X_zero (n : ℕ) :
    finSuccRingEquiv R n (X 0) = PowerSeries.X

theorem

finSuccRingEquiv_X_succ

L3262 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccRingEquiv_X_succ

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in

Lean source · statement

theorem finSuccRingEquiv_X_succ (n : ℕ) (i : Fin n) :
    finSuccRingEquiv R n (X i.succ) = PowerSeries.C (X i)

theorem

finSuccRingEquiv_C

L3267 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.finSuccRingEquiv_C

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section FinSucc
variable {R : Type*} [CommSemiring R]
variable (R) in

Lean source · statement

theorem finSuccRingEquiv_C (n : ℕ) (r : R) :
    finSuccRingEquiv R n (C r) = PowerSeries.C (C r)

def

isEmptyRingEquiv

L3279 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.isEmptyRingEquiv

Documentation

Power series with no variables form the coefficient ring.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section IsEmpty
variable (σ : Type*) [IsEmpty σ] (R : Type*) [CommSemiring R]

Lean source · statement

def isEmptyRingEquiv : MvPowerSeries σ R ≃+* R

theorem

isEmptyRingEquiv_apply

L3287 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.isEmptyRingEquiv_apply

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section IsEmpty
variable (σ : Type*) [IsEmpty σ] (R : Type*) [CommSemiring R]

Lean source · statement

theorem isEmptyRingEquiv_apply (f : MvPowerSeries σ R) :
    isEmptyRingEquiv σ R f = constantCoeff f

theorem

isEmptyRingEquiv_symm_apply

L3290 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.isEmptyRingEquiv_symm_apply

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section IsEmpty
variable (σ : Type*) [IsEmpty σ] (R : Type*) [CommSemiring R]

Lean source · statement

theorem isEmptyRingEquiv_symm_apply (r : R) :
    (isEmptyRingEquiv σ R).symm r = C r

instance

instIsNoetherianRingMvPowerSeriesFin

L3297 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.instIsNoetherianRingMvPowerSeriesFin

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.MvPowerSeries
open Finset.HasAntidiagonal (antidiagonal mem_antidiagonal)
noncomputable section
namespace MvPowerSeries
open _root_.MvPowerSeries
section Noetherian

Lean source · statement

instance instIsNoetherianRingMvPowerSeriesFin (R : Type*) [CommRing R] [IsNoetherianRing R]
  (n : ℕ) :
    IsNoetherianRing (MvPowerSeries (Fin n) R)

theorem

isCohenMacaulayOfDim_fin

L3320 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.isCohenMacaulayOfDim_fin

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace MvPowerSeries
open _root_.MvPowerSeries
variable (𝓞 : Type u) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞]
  [IsNoetherianRing 𝓞]

Lean source · statement

theorem isCohenMacaulayOfDim_fin (n : ℕ) :
    IsLocalRing.IsCohenMacaulayOfDim (MvPowerSeries (Fin n) 𝓞) (n + 1)

theorem

ringKrullDim_fin

L3330 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.ringKrullDim_fin

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace MvPowerSeries
open _root_.MvPowerSeries
variable (𝓞 : Type u) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞]
  [IsNoetherianRing 𝓞]

Lean source · statement

theorem ringKrullDim_fin (n : ℕ) :
    ringKrullDim (MvPowerSeries (Fin n) 𝓞) = ((n + 1 : ℕ) : WithBot ℕ∞)

theorem

depth_fin

L3334 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.depth_fin

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace MvPowerSeries
open _root_.MvPowerSeries
variable (𝓞 : Type u) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞]
  [IsNoetherianRing 𝓞]

Lean source · statement

theorem depth_fin (n : ℕ) :
    Module.depth (MvPowerSeries (Fin n) 𝓞) (MvPowerSeries (Fin n) 𝓞) = ((n + 1 : ℕ) : ℕ∞)

theorem

ringKrullDim_fin_lt_top

L3338 ↗

AlgebraicCurves.Valuations.Proofs.MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing.Ws14Port.MvPowerSeries.ringKrullDim_fin_lt_top

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory
namespace Ws14Port
universe u v
open IsLocalRing RingTheory RingTheory.Sequence Module
section
open _root_.Module.IsLocalRing
namespace MvPowerSeries
open _root_.MvPowerSeries
variable (𝓞 : Type u) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞]
  [IsNoetherianRing 𝓞]

Lean source · statement

theorem ringKrullDim_fin_lt_top (n : ℕ) :
    ringKrullDim (MvPowerSeries (Fin n) 𝓞) < ⊤

theorem

ringKrullDim_fin_eq_of_isDiscreteValuationRing

L3348 ↗

MvPowerSeries.ringKrullDim_fin_eq_of_isDiscreteValuationRing

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace MvPowerSeries_ringKrullDim_fin_eq_of_isDiscreteValuationRing
open IsLocalRing RingTheory

Lean source · statement

theorem _root_.MvPowerSeries.ringKrullDim_fin_eq_of_isDiscreteValuationRing
    (𝓞 : Type*) [CommRing 𝓞] [IsDomain 𝓞] [IsDiscreteValuationRing 𝓞] (n : ℕ) :
    ringKrullDim (MvPowerSeries (Fin n) 𝓞) = ((n + 1 : ℕ) : WithBot ℕ∞)

Module documentation

Mv Power Series ring Krull Dim fin eq of is Discrete Valuation Ring

Declarations