Theorems · Definition · algebraic geometry
PrimeSpectrum.ConstructibleSetData
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.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- PrimeSpectrum.BasicConstructibleSetDataproof · cited by 22
Cited by13
Results whose statement or proof uses this declaration.
- PrimeSpectrum.ConstructibleSetData.toSetstatement and proof · cited by 8
- PrimeSpectrum.ConstructibleSetData.mapstatement and proof · cited by 4
- PrimeSpectrum.ConstructibleSetData.degBoundstatement and proof · cited by 3
- PrimeSpectrum.ConstructibleSetData.isConstructible_toSetstatement and proof · cited by 2
- ChevalleyThm.chevalley_polynomialCstatement and proof · cited by 2
- PrimeSpectrum.exists_constructibleSetData_iffstatement and proof · cited by 2
- ChevalleyThm.chevalley_mvPolynomialCstatement and proof · cited by 1
- PrimeSpectrum.ConstructibleSetData.toSet_mapstatement and proof · cited by 1
- PrimeSpectrum.isConstructible_comap_Cproof · cited by 1
- PrimeSpectrum.exists_range_eq_of_isConstructibleproof · cited by 1
- chevalley_mvPolynomial_mvPolynomialstatement and proof · cited by 0
- PrimeSpectrum.ConstructibleSetData.map_compstatement and proof · cited by 0