IsOpenComapC

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

Statistics

Metric	Count
Definitions imageOfDf	1
Theorems comap_C_mem_imageOfDf, imageOfDf_eq_comap_C_compl_zeroLocus, isOpenMap_comap_C, isOpen_imageOfDf	4
Total	5

AlgebraicGeometry.Polynomial

Definitions

Name	Category	Theorems
imageOfDf 📖	CompOp	3 math math: comap_C_mem_imageOfDf, imageOfDf_eq_comap_C_compl_zeroLocus, isOpen_imageOfDf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_C_mem_imageOfDf 📖	mathematical	PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring Set Set.instMembership Compl.compl Set.instCompl PrimeSpectrum.zeroLocus Set.instSingletonSet	imageOfDf PrimeSpectrum.comap Polynomial.C	—	exists_C_coeff_notMem PrimeSpectrum.mem_compl_zeroLocus_iff_notMem
imageOfDf_eq_comap_C_compl_zeroLocus 📖	mathematical	—	imageOfDf Set.image PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring PrimeSpectrum.comap Polynomial.C Compl.compl Set Set.instCompl PrimeSpectrum.zeroLocus Set.instSingletonSet	—	Set.ext Ideal.isPrime_map_C_of_isPrime PrimeSpectrum.isPrime Set.mem_compl_iff PrimeSpectrum.mem_zeroLocus Set.singleton_subset_iff Ideal.mem_map_C_iff PrimeSpectrum.ext Ideal.ext Polynomial.coeff_C_zero Ideal.subset_span Set.mem_image_of_mem comap_C_mem_imageOfDf
isOpenMap_comap_C 📖	mathematical	—	IsOpenMap PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring PrimeSpectrum.zariskiTopology PrimeSpectrum.comap Polynomial.C	—	compl_compl Set.iUnion_of_singleton_coe PrimeSpectrum.zeroLocus_iUnion Set.compl_iInter Set.image_iUnion isOpen_iUnion isOpen_imageOfDf
isOpen_imageOfDf 📖	mathematical	—	IsOpen PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.zariskiTopology imageOfDf	—	imageOfDf.eq_1 Set.setOf_exists isOpen_iUnion PrimeSpectrum.isOpen_basicOpen

---

← Back to Index