Constructible sets in the prime spectrum

This file provides tooling for manipulating constructible sets in the prime spectrum of a ring.

TODO

Link to constructible sets in a topological space.

structure PrimeSpectrum.BasicConstructibleSetData (R : Type u_1) : Type u_1

The data of a basic constructible set s is a tuple (f, g₁, ..., gₙ)

• f : R

  Given the data of a basic constructible set s = V(g₁, ..., gₙ) \ V(f), return f.

• n : ℕ

  Given the data of a basic constructible set s = V(g₁, ..., gₙ) \ V(f), return n.

• g : Fin self.n → R

  Given the data of a basic constructible set s = V(g₁, ..., gₙ) \ V(f), return g.

theorem PrimeSpectrum.BasicConstructibleSetData.ext {R : Type u_1} {x y : BasicConstructibleSetData R} (f : x.f = y.f) (n : x.n = y.n) (g : HEq x.g y.g) : x = y

noncomputable instance PrimeSpectrum.BasicConstructibleSetData.instDecidableEq {R : Type u_1} : DecidableEq (BasicConstructibleSetData R)

Equations

• PrimeSpectrum.BasicConstructibleSetData.instDecidableEq = Classical.decEq (PrimeSpectrum.BasicConstructibleSetData R)

noncomputable def PrimeSpectrum.BasicConstructibleSetData.map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (C : BasicConstructibleSetData R) : BasicConstructibleSetData S

Given the data of the constructible set s, build the data of the constructible set {I | {x | φ x ∈ I} ∈ s}.

Equations

• PrimeSpectrum.BasicConstructibleSetData.map φ C = { f := φ C.f, n := C.n, g := ⇑φ ∘ C.g }

@[simp]

theorem PrimeSpectrum.BasicConstructibleSetData.map_n {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (C : BasicConstructibleSetData R) : (map φ C).n = C.n

@[simp]

theorem PrimeSpectrum.BasicConstructibleSetData.map_f {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (C : BasicConstructibleSetData R) : (map φ C).f = φ C.f

@[simp]

theorem PrimeSpectrum.BasicConstructibleSetData.map_g {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (C : BasicConstructibleSetData R) (a✝ : Fin C.n) : (map φ C).g a✝ = (⇑φ ∘ C.g) a✝

@[simp]

theorem PrimeSpectrum.BasicConstructibleSetData.map_id {R : Type u_1} [CommSemiring R] (C : BasicConstructibleSetData R) : map (RingHom.id R) C = C

@[simp]

theorem PrimeSpectrum.BasicConstructibleSetData.map_id' {R : Type u_1} [CommSemiring R] : map (RingHom.id R) = id

theorem PrimeSpectrum.BasicConstructibleSetData.map_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [CommSemiring T] (φ : S →+* T) (ψ : R →+* S) (C : BasicConstructibleSetData R) : map (φ.comp ψ) C = map φ (map ψ C)

theorem PrimeSpectrum.BasicConstructibleSetData.map_comp' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [CommSemiring T] (φ : S →+* T) (ψ : R →+* S) : map (φ.comp ψ) = map φ ∘ map ψ

def PrimeSpectrum.BasicConstructibleSetData.toSet {R : Type u_1} [CommSemiring R] (C : BasicConstructibleSetData R) : Set (PrimeSpectrum R)

Given the data of a basic constructible set s, namely a tuple (f, g₁, ..., gₙ) such that s = V(g₁, ..., gₙ) \ V(f), return s.

Equations

• C.toSet = PrimeSpectrum.zeroLocus (Set.range C.g) \ PrimeSpectrum.zeroLocus {C.f}

@[simp]

theorem PrimeSpectrum.BasicConstructibleSetData.toSet_map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (C : BasicConstructibleSetData R) : (map φ C).toSet = ⇑(comap φ) ⁻¹' C.toSet

@[reducible, inline]

abbrev PrimeSpectrum.ConstructibleSetData (R : Type u_1) : Type u_1

The data of a constructible set s in the prime spectrum of a ring is finitely many tuples (f, g₁, ..., gₙ) such that s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f).

To obtain s from its data, use PrimeSpectrum.ConstructibleSetData.toSet.

Equations

• PrimeSpectrum.ConstructibleSetData R = Finset (PrimeSpectrum.BasicConstructibleSetData R)

noncomputable def PrimeSpectrum.ConstructibleSetData.map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (s : ConstructibleSetData R) : ConstructibleSetData S

Given the data of the constructible set s, build the data of the constructible set {I | {x | f x ∈ I} ∈ s}.

Equations

• PrimeSpectrum.ConstructibleSetData.map φ s = Finset.image (PrimeSpectrum.BasicConstructibleSetData.map φ) s

@[simp]

theorem PrimeSpectrum.ConstructibleSetData.map_id {R : Type u_1} [CommSemiring R] (s : ConstructibleSetData R) : map (RingHom.id R) s = s

theorem PrimeSpectrum.ConstructibleSetData.map_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [CommSemiring T] (f : S →+* T) (g : R →+* S) (s : ConstructibleSetData R) : map (f.comp g) s = map f (map g s)

def PrimeSpectrum.ConstructibleSetData.toSet {R : Type u_1} [CommSemiring R] (S : ConstructibleSetData R) : Set (PrimeSpectrum R)

Given the data of a constructible set s, namely finitely many tuples (f, g₁, ..., gₙ) such that s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f), return s.

Equations

• S.toSet = ⋃ C ∈ S, C.toSet

@[simp]

theorem PrimeSpectrum.ConstructibleSetData.toSet_map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : ConstructibleSetData R) : (map f s).toSet = ⇑(comap f) ⁻¹' s.toSet

def PrimeSpectrum.ConstructibleSetData.degBound {R : Type u_1} [CommSemiring R] (S : ConstructibleSetData (Polynomial R)) : ℕ

The degree bound on a constructible set for Chevalley's theorem for the inclusion R ↪ R[X].

Equations

• S.degBound = Finset.sup S fun (C : PrimeSpectrum.BasicConstructibleSetData (Polynomial R)) => ∑ i : Fin C.n, (C.g i).degree.succ