NYLL
Module

SymbolicPowerErrorModule.lean

Nyll.EtaleFundamentalGroups.Purity.SymbolicPowerErrorModule
1 declaration indexed from sourceView source ↗

Module documentation

The Artinian error between symbolic and ordinary powers

For a prime P with dim (R / P) ≤ 1, the image of P^(n) in R / P^n is an Artinian R-module. A common denominator outside P annihilates this image, as does P^n. The image is therefore a finite module over the Artinian quotient by P^n + (s).

Imports5
Imported by2

Declarations

theorem

isArtinian_primeSymbolicPower_quotient_pow

L30 ↗
EtaleFundamentalGroups.Purity.isArtinian_primeSymbolicPower_quotient_pow
Documentation

The difference between a symbolic power and the ordinary power is an Artinian module when the prime quotient has dimension at most one.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
Lean source · statement
theorem isArtinian_primeSymbolicPower_quotient_pow
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (P : Ideal R) [P.IsPrime]
    (hdim : ringKrullDim (R ⧸ P) ≤ (1 : WithBot ℕ∞)) (n : ℕ) :
    IsArtinian R
      (Submodule.map (Submodule.mkQ (P ^ n))
        (primeSymbolicPower P n : Submodule R R))

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