symbolic power of a prime ideal

Stream: Is there code for X?

[张守信(Shouxin Zhang)]

Is there any api has existed in lib or some PR for the following code?

import Mathlib

open Ideal

variable {R : Type*} [CommSemiring R]

/-- The n-th symbolic power of a prime ideal p -/
def Ideal.symPow (p : Ideal R) [p.IsPrime] (n : ℕ) : Ideal R where
  carrier := {x : R | ∃ s ∈ p.primeCompl, s * x ∈ p ^ n}
  zero_mem' := by use 1; simp [p.primeCompl.one_mem]
  add_mem' := by
    rintro x y ⟨sx, hsx, hx'⟩ ⟨sy, hsy, hy'⟩
    use sx * sy, p.primeCompl.mul_mem hsx hsy
    rw [show sx * sy * (x + y) = (sx * x) * sy + sx * (sy * y) by ring_nf]
    apply Ideal.add_mem
    . exact Ideal.mul_mem_right _ _ hx'
    . exact Ideal.mul_mem_left _ _ hy'
  smul_mem' := by
    rintro r x ⟨s, hs, hx'⟩
    use s, hs
    rw [smul_eq_mul, mul_comm r, ← mul_assoc]
    exact Ideal.mul_mem_right _ _ hx'

[Andrew Yang]

You probably just pullback IsLocalRing.maximalIdeal (Localization.AtPrime p) ^ n.

[Junyan Xu]

This is the way it's defined when used in the proof of Krull principal ideal theorem.