Constructible sets in the prime spectrum

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

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

theorem PrimeSpectrum.BasicConstructibleSetData.ext_iff {R : Type u_1} {x y : BasicConstructibleSetData R} : x = y ↔ x.f = y.f ∧ x.n = y.n ∧ HEq x.g y.g

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_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_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_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

theorem PrimeSpectrum.ConstructibleSetData.isConstructible_toSet {R : Type u_1} [CommSemiring R] (S : ConstructibleSetData R) : Topology.IsConstructible S.toSet

theorem PrimeSpectrum.exists_constructibleSetData_iff {R : Type u_1} [CommSemiring R] {s : Set (PrimeSpectrum R)} : (∃ (S : ConstructibleSetData R), S.toSet = s) ↔ Topology.IsConstructible s

theorem PrimeSpectrum.exists_range_eq_of_isConstructible {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} (hs : Topology.IsConstructible s) : ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range ⇑(comap f) = s

Stacks Tag 00F8 (without the finite presentation part)

theorem PrimeSpectrum.isClosed_of_stableUnderSpecialization_of_isConstructible {R : Type u_4} [CommRing R] {s : Set (PrimeSpectrum R)} (hs : StableUnderSpecialization s) (hs' : Topology.IsConstructible s) : IsClosed s

Stacks Tag 00I0 ((1))

theorem PrimeSpectrum.isOpen_of_stableUnderGeneralization_of_isConstructible {R : Type u_4} [CommRing R] {s : Set (PrimeSpectrum R)} (hs : StableUnderGeneralization s) (hs' : Topology.IsConstructible s) : IsOpen s

Stacks Tag 00I0 ((1))