Documentation Verification Report

ConstructibleSet

📁 Source: Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean

Statistics

Metric	Count
Definitions `BasicConstructibleSetData`, `f`, `g`, `instDecidableEq`, `map`, `n`, `toSet`, `ConstructibleSetData`, `degBound`, `map`, `toSet`	11
Theorems `ext`, `ext_iff`, `map_comp`, `map_comp'`, `map_f`, `map_g`, `map_id`, `map_id'`, `map_n`, `toSet_map`, `isConstructible_toSet`, `map_comp`, `map_id`, `toSet_map`, `exists_constructibleSetData_iff`, `exists_range_eq_of_isConstructible`, `isClosed_of_stableUnderSpecialization_of_isConstructible`, `isOpen_of_stableUnderGeneralization_of_isConstructible`	18
Total	29

PrimeSpectrum

Definitions

Name	Category	Theorems
`BasicConstructibleSetData` 📖	CompData	2 math math: `BasicConstructibleSetData.map_comp'`, `BasicConstructibleSetData.map_id'`
`ConstructibleSetData` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_constructibleSetData_iff` 📖	mathematical	—	`ConstructibleSetData.toSet` `Topology.IsConstructible` `PrimeSpectrum` `zariskiTopology`	—	`ConstructibleSetData.isConstructible_toSet` `Topology.IsConstructible.induction_of_isTopologicalBasis` `compactSpace` `instQuasiSeparatedSpace` `Zero.instNonempty` `isTopologicalBasis_basic_opens` `isCompact_basicOpen` `Set.iUnion_congr_Prop` `Set.iUnion_iUnion_eq_left` `basicOpen_eq_zeroLocus_compl` `Set.biUnion_of_singleton` `compl_sdiff_compl` `Set.ext` `Equiv.exists_congr_right` `Equiv.symm_apply_apply` `Finset.coe_union` `Set.biUnion_union`
`exists_range_eq_of_isConstructible` 📖	mathematical	`Topology.IsConstructible` `PrimeSpectrum` `CommRing.toCommSemiring` `zariskiTopology`	`Set.range` `comap`	—	`exists_constructibleSetData_iff` `Ideal.instIsTwoSided_1` `iUnion_range_comap_comp_evalRingHom` `Finite.of_fintype` `ConstructibleSetData.toSet.eq_1` `Set.iUnion_congr_Prop` `Set.biUnion_eq_iUnion` `Set.range_comp` `localization_away_comap_range` `Localization.isLocalization` `continuous_comap` `comap_basicOpen` `TopologicalSpace.Opens.coe_comap` `Set.image_preimage_eq_inter_range` `RingHom.instRingHomClass` `range_comap_of_surjective` `Ideal.Quotient.mk_surjective` `BasicConstructibleSetData.toSet.eq_1` `Set.diff_eq_compl_inter` `basicOpen_eq_zeroLocus_compl` `Ideal.mk_ker` `zeroLocus_span`
`isClosed_of_stableUnderSpecialization_of_isConstructible` 📖	mathematical	`StableUnderSpecialization` `PrimeSpectrum` `CommRing.toCommSemiring` `zariskiTopology` `Topology.IsConstructible`	`IsClosed`	—	`exists_range_eq_of_isConstructible` `isClosed_range_of_stableUnderSpecialization`
`isOpen_of_stableUnderGeneralization_of_isConstructible` 📖	mathematical	`StableUnderGeneralization` `PrimeSpectrum` `CommRing.toCommSemiring` `zariskiTopology` `Topology.IsConstructible`	`IsOpen`	—	`isClosed_compl_iff` `isClosed_of_stableUnderSpecialization_of_isConstructible` `StableUnderGeneralization.compl` `Topology.IsConstructible.compl`

PrimeSpectrum.BasicConstructibleSetData

Definitions

Name	Category	Theorems
`f` 📖	CompOp	2 math math: `map_f`, `ext_iff`
`g` 📖	CompOp	2 math math: `ext_iff`, `map_g`
`instDecidableEq` 📖	CompOp	—
`map` 📖	CompOp	8 math math: `map_comp'`, `map_id`, `map_n`, `map_f`, `map_comp`, `map_g`, `toSet_map`, `map_id'`
`n` 📖	CompOp	4 math math: `ChevalleyThm.chevalley_polynomialC`, `map_n`, `ext_iff`, `map_g`
`toSet` 📖	CompOp	1 math math: `toSet_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`f` `n` `g`	—	—	—
`ext_iff` 📖	mathematical	—	`f` `n` `g`	—	`ext`
`map_comp` 📖	mathematical	—	`map` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—
`map_comp'` 📖	mathematical	—	`map` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `PrimeSpectrum.BasicConstructibleSetData`	—	`map_comp`
`map_f` 📖	mathematical	—	`f` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	—	—
`map_g` 📖	mathematical	—	`g` `map` `n` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	—	—
`map_id` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`map_id'` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `PrimeSpectrum.BasicConstructibleSetData`	—	`map_id`
`map_n` 📖	mathematical	—	`n` `map`	—	—
`toSet_map` 📖	mathematical	—	`toSet` `map` `Set.preimage` `PrimeSpectrum` `PrimeSpectrum.comap`	—	`PrimeSpectrum.preimage_comap_zeroLocus` `Set.image_singleton`

PrimeSpectrum.ConstructibleSetData

Definitions

Name	Category	Theorems
`degBound` 📖	CompOp	1 math math: `ChevalleyThm.chevalley_polynomialC`
`map` 📖	CompOp	3 math math: `map_id`, `toSet_map`, `map_comp`
`toSet` 📖	CompOp	6 math math: `ChevalleyThm.chevalley_polynomialC`, `chevalley_mvPolynomial_mvPolynomial`, `ChevalleyThm.chevalley_mvPolynomialC`, `isConstructible_toSet`, `PrimeSpectrum.exists_constructibleSetData_iff`, `toSet_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConstructible_toSet` 📖	mathematical	—	`Topology.IsConstructible` `PrimeSpectrum` `PrimeSpectrum.zariskiTopology` `toSet`	—	`Topology.IsConstructible.biUnion` `Finset.finite_toSet` `Topology.IsConstructible.sdiff` `Topology.isConstructible_compl` `IsRetrocompact.isConstructible` `IsClosed.isOpen_compl` `PrimeSpectrum.isClosed_zeroLocus` `PrimeSpectrum.isRetrocompact_zeroLocus_compl` `Set.finite_range` `Finite.of_fintype` `Set.finite_singleton`
`map_comp` 📖	mathematical	—	`map` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`PrimeSpectrum.BasicConstructibleSetData.map_comp'` `Finset.image_image`
`map_id` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`PrimeSpectrum.BasicConstructibleSetData.map_id'` `Finset.image_id`
`toSet_map` 📖	mathematical	—	`toSet` `map` `Set.preimage` `PrimeSpectrum` `PrimeSpectrum.comap`	—	`Finset.set_biUnion_finset_image` `Set.iUnion_congr_Prop` `PrimeSpectrum.BasicConstructibleSetData.toSet_map` `Set.preimage_iUnion`

---

← Back to Index