Module

SymbolicPowerErrorArtinian.lean

Nyll.EtaleFundamentalGroups.Purity.SymbolicPowerErrorArtinian

3 declarations indexed from sourceView source ↗

Module documentation

Artinian coefficient rings for symbolic-power errors

If R / P has dimension at most one, adjoining an element outside P to an ordinary power of P gives an Artinian quotient. This supplies the coefficient ring for a finite symbolic-power error killed by that element.

Imports4

Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Imported by2

theorem

prime_eq_maximalIdeal_of_pow_sup_span_singleton_le

L30 ↗

EtaleFundamentalGroups.Purity.prime_eq_maximalIdeal_of_pow_sup_span_singleton_le

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem prime_eq_maximalIdeal_of_pow_sup_span_singleton_le
    (P : Ideal R) [P.IsPrime]
    (hdim : ringKrullDim (R ⧸ P) ≤ (1 : WithBot ℕ∞))
    (n : ℕ) (s : R) (hs : s ∉ P)
    (Q : Ideal R) [Q.IsPrime]
    (hQ : P ^ n ⊔ Ideal.span {s} ≤ Q) :
    Q = maximalIdeal R

theorem

radical_pow_sup_span_singleton_eq_maximalIdeal

L61 ↗

EtaleFundamentalGroups.Purity.radical_pow_sup_span_singleton_eq_maximalIdeal

Documentation

Adjoining an element outside a prime with one-dimensional quotient to an ordinary prime power gives maximal radical whenever the ideal is proper.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem radical_pow_sup_span_singleton_eq_maximalIdeal
    (P : Ideal R) [P.IsPrime]
    (hdim : ringKrullDim (R ⧸ P) ≤ (1 : WithBot ℕ∞))
    (n : ℕ) (s : R) (hs : s ∉ P)
    (hproper : P ^ n ⊔ Ideal.span {s} ≠ ⊤) :
    (P ^ n ⊔ Ideal.span {s}).radical = maximalIdeal R

theorem

isArtinianRing_quotient_pow_sup_span_singleton

L79 ↗

EtaleFundamentalGroups.Purity.isArtinianRing_quotient_pow_sup_span_singleton

Documentation

An element outside a prime with one-dimensional quotient kills the positive-dimensional part of the quotient by any ordinary prime power.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem isArtinianRing_quotient_pow_sup_span_singleton
    [IsNoetherianRing R]
    (P : Ideal R) [P.IsPrime]
    (hdim : ringKrullDim (R ⧸ P) ≤ (1 : WithBot ℕ∞))
    (n : ℕ) (s : R) (hs : s ∉ P) :
    IsArtinianRing (R ⧸ (P ^ n ⊔ Ideal.span {s}))

Module documentation

Artinian coefficient rings for symbolic-power errors

Declarations

prime_eq_maximalIdeal_of_pow_sup_span_singleton_le

radical_pow_sup_span_singleton_eq_maximalIdeal

isArtinianRing_quotient_pow_sup_span_singleton