Intersection subring definitions

Defines the subrings A_i = R[x_i, y_j^{-1}] of a Noetherian local domain T and their intersection, used in the Krull domain construction of Anderson--Jensen.

def adjoinLocSetY {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (y : ↥R.carrier) : Set T

The set A = R[x, y⁻¹] inside T: elements t such that t·yⁿ = f(x) for some f ∈ R[X] and n ∈ ℕ. This is the image of the localization of R[x] at the powers of y, embedded in T via evaluation.

Equations

• adjoinLocSetY R x y = {t : T | ∃ (f : Polynomial ↥R.carrier) (n : ℕ), t * ↑y ^ n = (Polynomial.aeval x) f}

theorem R_le_adjoinLocSetY {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (y r : ↥R.carrier) : ↑r ∈ adjoinLocSetY R x y

R ⊆ R[x, y⁻¹].

theorem x_mem_adjoinLocSetY {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (y : ↥R.carrier) : x ∈ adjoinLocSetY R x y

x ∈ R[x, y⁻¹].

def intersectionSet {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ : ↥R.carrier) : Set T

The intersection Rbar = A₁ ∩ A₂ as a set in T.

Equations

• intersectionSet R x₁ x₂ y₁ y₂ = adjoinLocSetY R x₁ y₂ ∩ adjoinLocSetY R x₂ y₁

theorem R_le_intersectionSet {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x₁ x₂ : T) (y₁ y₂ r : ↥R.carrier) : ↑r ∈ intersectionSet R x₁ x₂ y₁ y₂

R ⊆ Rbar.