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.

@[reducible, inline]

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

The data of a constructible set s 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 (R × (n : ℕ) × (Fin n → R))

def PrimeSpectrum.ConstructibleSetData.map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [DecidableEq S] (f : 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 f s = Finset.image (fun (x : R × (n : ℕ) × (Fin n → R)) => match x with | (r, ⟨n, g⟩) => (f r, ⟨n, ⇑f ∘ g⟩)) s

@[simp]

theorem PrimeSpectrum.ConstructibleSetData.map_id {R : Type u_1} [CommSemiring R] [DecidableEq 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] [DecidableEq S] [DecidableEq 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 = ⋃ x ∈ S, PrimeSpectrum.zeroLocus (Set.range x.2.snd) \ PrimeSpectrum.zeroLocus {x.1}

@[simp]

theorem PrimeSpectrum.ConstructibleSetData.toSet_map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [DecidableEq 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 (e : Polynomial R × (n : ℕ) × (Fin n → Polynomial R)) => ∑ i : Fin e.2.fst, (e.2.snd i).degree.succ