Defs

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

Statistics

Metric	Count
Definitions PrimeSpectrum, asIdeal, equivSubtype, instPartialOrder	4
Theorems asIdeal_le_asIdeal, asIdeal_lt_asIdeal, equivSubtype_apply_coe, equivSubtype_symm_apply_asIdeal, ext, ext_iff, isPrime	7
Total	11

PrimeSpectrum

Definitions

Name	Category	Theorems
asIdeal 📖	CompOp	134 math math: mapPiLocalization_id, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Polynomial.mem_image_comap_C_basicOpen, preimageEquivFiber_symm_apply_coe, asIdeal_bot, residueField_specComap, localization_specComap_range, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, equivSubtype_apply_coe, Module.rankAtStalk_eq, equivSubtype_symm_apply_asIdeal, IsArtinianRing.primeSpectrum_asIdeal_range_eq, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, Module.mem_support_iff_of_finite, primeSpectrumProd_symm_inr_asIdeal, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.structureSheafInType.mul_apply, AlgebraicGeometry.StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, isPrime, coe_preimageHomeomorphFiber_apply_asIdeal, toPiLocalization_surjective_of_discreteTopology, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal, coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton, AlgebraicGeometry.StructureSheaf.comap_apply, isMax_iff, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt, mapPiLocalization_bijective, toPiLocalization_not_surjective_of_infinite, specComap_asIdeal, mem_compl_zeroLocus_iff_notMem, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, isMin_iff, mapPiLocalization_comp, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, preimageEquivFiber_apply_asIdeal, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, mem_image_comap_basicOpen, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, iInf_localization_eq_bot, AlgebraicGeometry.AffineSpace.spec_le_iff, mem_zeroLocus, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, mapPiLocalization_naturality, Module.rankAtStalk_eq_finrank_tensorProduct, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber, Module.mem_support_iff_exists_annihilator, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal, isClosed_singleton_iff_isMaximal, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal, toPiLocalization_bijective, residueField_comap, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, Algebra.QuasiFiniteAt.of_isOpen_singleton, sigmaToPi_asIdeal, Algebra.QuasiFiniteAt.of_isOpen_singleton_fiber, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, discreteTopology_iff_toPiLocalization_surjective, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, mem_range_comap_iff, exists_primeSpectrum_prod_le, IsLocalRing.PrimeSpectrum.asIdeal_top, piLocalizationToMaximal_comp_toPiLocalization, piLocalizationToMaximal_surjective, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.structureSheafInType.add_apply, vanishingIdeal_singleton, closure_singleton, coe_primesOverOrderIsoFiber_apply_asIdeal, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.Scheme.default_asIdeal, stableUnderSpecialization_singleton, nilradical_eq_iInf, ext_iff, coe_preimageOrderIsoFiber_apply_asIdeal, Module.mem_support_iff_nontrivial_residueField_tensorProduct, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk, Module.notMem_support_iff, Algebra.mem_etaleLocus_iff, stableUnderGeneralization_singleton, comap_asIdeal, Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, Module.mem_support_iff, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun_asIdeal, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal, mem_basicOpen, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, exist_mem_one_of_mem_maximal_ideal, coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk', exists_multiset_prod_cons_le_and_prod_not_le, mem_vanishingIdeal, instLiesOverAsIdealComapAlgebraMap, coe_primesOverOrderIsoFiber_symm_apply_coe, piLocalizationToMaximal_bijective, primeSpectrumProd_symm_inl_asIdeal, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal, toPiLocalization_injective, asIdeal_lt_asIdeal, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, mem_image_comap_zeroLocus_sdiff, Module.mem_freeLocus, localization_comap_range, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, Module.mem_support_iff_of_span_eq_top, AlgebraicGeometry.structureSheafInType.smul_apply, exists_primeSpectrum_prod_le_and_ne_bot_of_domain, AlgebraicGeometry.localRingHom_comp_stalkIso, ValuationSubring.primeSpectrumEquiv_apply, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, Module.annihilator_le_of_mem_support, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, nontrivial_iff_mem_rangeComap, discreteTopology_iff_toPiLocalization_bijective, MvPolynomial.mem_image_comap_C_basicOpen, range_asIdeal, asIdeal_le_asIdeal, Module.notMem_support_iff'
equivSubtype 📖	CompOp	2 math math: equivSubtype_apply_coe, equivSubtype_symm_apply_asIdeal
instPartialOrder 📖	CompOp	33 math math: IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, asIdeal_bot, equivSubtype_apply_coe, equivSubtype_symm_apply_asIdeal, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, ringKrullDim_quotient, RingHom.strictMono_comap_of_surjective, Ideal.exists_ltSeries_length_eq_height, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal, coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, isMax_iff, isMin_iff, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux, le_iff_mem_closure, IsLocalRing.PrimeSpectrum.asIdeal_top, RingHom.strictMono_specComap_of_surjective, finite_setOf_isMin, comapEquiv_apply, Ideal.exists_ltSeries_of_hasGoingDown, nhdsOrderEmbedding_apply, le_iff_specializes, coe_primesOverOrderIsoFiber_apply_asIdeal, IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top, comapEquiv_symm, coe_preimageOrderIsoFiber_apply_asIdeal, Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support, coe_primesOverOrderIsoFiber_symm_apply_coe, asIdeal_lt_asIdeal, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, AlgebraicGeometry.genericPoint_eq_bot_of_affine, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, asIdeal_le_asIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asIdeal_le_asIdeal 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal PrimeSpectrum instPartialOrder	—	—
asIdeal_lt_asIdeal 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal PrimeSpectrum instPartialOrder	—	—
equivSubtype_apply_coe 📖	mathematical	—	Ideal CommSemiring.toSemiring Ideal.IsPrime DFunLike.coe RelIso PrimeSpectrum Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RelIso.instFunLike equivSubtype asIdeal	—	—
equivSubtype_symm_apply_asIdeal 📖	mathematical	—	asIdeal DFunLike.coe RelIso Ideal CommSemiring.toSemiring Ideal.IsPrime PrimeSpectrum Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instPartialOrder RelIso.instFunLike RelIso.symm equivSubtype	—	—
ext 📖	—	asIdeal	—	—	—
ext_iff 📖	mathematical	—	asIdeal	—	ext
isPrime 📖	mathematical	—	Ideal.IsPrime CommSemiring.toSemiring asIdeal	—	—

(root)

Definitions

Name	Category	Theorems
PrimeSpectrum 📖	CompData	395 math math: PrimeSpectrum.mapPiLocalization_id, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, PrimeSpectrum.zeroLocus_anti_mono, PrimeSpectrum.closure_range_comap, PrimeSpectrum.isClopen_iff_mul_add, PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible, Module.support_quotient, Polynomial.mem_image_comap_C_basicOpen, PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation, PrimeSpectrum.sigmaToPi_bijective, LocalizedModule.subsingleton_iff_disjoint, PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.asIdeal_bot, PrimeSpectrum.residueField_specComap, AlgebraicGeometry.Polynomial.isOpenMap_comap_C, PrimeSpectrum.localization_specComap_range, AlgebraicGeometry.coprodSpec_apply, PrimeSpectrum.isClosedEmbedding_comap_snd, MvPolynomial.isOpenMap_comap_C, Ring.KrullDimLE.subsingleton_primeSpectrum, PrimeSpectrum.isClosed_zeroLocus, PrimeSpectrum.zeroLocus_nilradical, PrimeSpectrum.iUnion_range_specComap_comp_evalRingHom, PrimeSpectrum.isClopen_iff_mul_add_zeroLocus, PrimeSpectrum.zeroLocus_eq_univ_iff, PrimeSpectrum.zeroLocus_empty, PrimeSpectrum.primeSpectrumProd_symm_inl, PrimeSpectrum.equivSubtype_apply_coe, ChevalleyThm.chevalley_polynomialC, Module.rankAtStalk_eq_zero_iff_notMem_support, PrimeSpectrum.localization_comap_isInducing, PrimeSpectrum.isHomeomorph_comap, range_comap_of_surjective, PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg, PrimeSpectrum.equivSubtype_symm_apply_asIdeal, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, IsArtinianRing.primeSpectrum_asIdeal_range_eq, PrimeSpectrum.basicOpen_injOn_isIdempotentElem, PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, PrimeSpectrum.gc, MvPolynomial.image_comap_C_basicOpen, PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff, PrimeSpectrum.instDiscreteTopology, Module.freeLocus_localization, PrimeSpectrum.isClosed_iff_zeroLocus, chevalley_mvPolynomial_mvPolynomial, Algebra.basicOpen_subset_etaleLocus_iff_etale, range_specComap_of_surjective, Module.mem_support_iff_of_finite, IsLocalRing.closedPoint_mem_iff, PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add, PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal, Module.support_eq_empty, Module.freeLocus_eq_univ, Module.basicOpen_subset_freeLocus_iff, PrimeSpectrum.instQuasiSoberElemZeroLocus, PrimeSpectrum.localization_away_isOpenEmbedding, AlgebraicGeometry.StructureSheaf.exists_const, PrimeSpectrum.denseRange_comap_iff_minimalPrimes, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Algebra.basicOpen_subset_unramifiedLocus_iff, RingHom.Flat.generalizingMap_comap, PrimeSpectrum.instT0Space, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, ringKrullDim_quotient, Algebra.QuasiFiniteAt.isClopen_singleton, PrimeSpectrum.vanishingIdeal_range_comap, PrimeSpectrum.vanishingIdeal_irreducibleComponents, PrimeSpectrum.isCompact_isOpen_iff, Algebra.smoothLocus_eq_univ_iff, PrimeSpectrum.specComap_injective_of_surjective, PrimeSpectrum.vanishingIdeal_anti_mono_iff, PrimeSpectrum.comap_surjective_of_faithfullyFlat, IsLocalRing.isClosed_singleton_closedPoint, PrimeSpectrum.union_zeroLocus, RingHom.strictMono_comap_of_surjective, PrimeSpectrum.instQuasiSeparatedSpace, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, PrimeSpectrum.le_basicOpen_pow, PrimeSpectrum.iSup_basicOpen_eq_top_iff, Algebra.QuasiFinite.isDiscrete_comap_preimage_singleton, PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks, PrimeSpectrum.zeroLocus_subset_zeroLocus_iff, Ideal.exists_ltSeries_length_eq_height, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, PrimeSpectrum.isConstructible_basicOpen, PrimeSpectrum.basicOpen_mul, PrimeSpectrum.isMax_iff, PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal, PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem, Module.comap_freeLocus_le, PrimeSpectrum.quasiSober, PrimeSpectrum.comap_quotientMk_bijective_of_le_nilradical, PrimeSpectrum.instSpectralSpace, Algebra.etaleLocus_eq_univ_iff_etale, PrimeSpectrum.mapPiLocalization_bijective, PrimeSpectrum.t1Space_iff_isField, PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem, PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, ChevalleyThm.chevalley_mvPolynomialC, PrimeSpectrum.vanishingIdeal_eq_top_iff, PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, PrimeSpectrum.toPiLocalization_not_surjective_of_infinite, PrimeSpectrum.preimage_comap_zeroLocus, PrimeSpectrum.instIsEmptyOfSubsingleton, MvPolynomial.vanishingIdeal_pointToPoint, PrimeSpectrum.sup_vanishingIdeal_le, PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field, PrimeSpectrum.isIdempotentElemEquivClopens_one_sub, PrimeSpectrum.basicOpen_le_basicOpen_iff_algebraMap_isUnit, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, PrimeSpectrum.mem_compl_zeroLocus_iff_notMem, PrimeSpectrum.zeroLocus_minimalPrimes, PrimeSpectrum.isIrreducible_zeroLocus_iff, Polynomial.exists_image_comap_of_monic, AlgebraicGeometry.IsPreimmersion.Spec_map_iff, Algebra.basicOpen_subset_smoothLocus_iff_smooth, PrimeSpectrum.isMin_iff, PrimeSpectrum.mapPiLocalization_comp, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, RingHom.IsIntegral.comap_surjective, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous, PrimeSpectrum.mem_image_comap_basicOpen, PrimeSpectrum.isClosedEmbedding_comap_fst, PrimeSpectrum.instNonemptyOfNontrivial, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, PrimeSpectrum.basicOpen_zero, PrimeSpectrum.isClopen_iff, Polynomial.isOpen_image_comap_of_monic, PrimeSpectrum.isClosedMap_comap_of_isIntegral, Algebra.etaleLocus_eq_univ_iff, PrimeSpectrum.iUnion_range_comap_comp_evalRingHom, PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf, Module.support_subset_preimage_comap, AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus, Module.rankAtStalk_eq_zero_iff_subsingleton, MaximalSpectrum.toPrimeSpectrum_continuous, PrimeSpectrum.iInf_localization_eq_bot, IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes, AlgebraicGeometry.formallySmooth_stalkMap_iff, PrimeSpectrum.continuous_comap, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, PrimeSpectrum.mem_zeroLocus, PrimeSpectrum.preimage_specComap_zeroLocus, PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff, Algebra.isOpen_etaleLocus, PrimeSpectrum.zeroLocus_union, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton, PrimeSpectrum.ConstructibleSetData.isConstructible_toSet, PrimeSpectrum.vanishingIdeal_isIrreducible, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, PrimeSpectrum.zeroLocus_bUnion, Polynomial.isOpenMap_comap_C, Algebra.unramifiedLocus_eq_compl_support, PrimeSpectrum.mapPiLocalization_naturality, PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents, Module.freeLocus_eq_univ_iff, Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber, PrimeSpectrum.specComap_surjective_of_faithfullyFlat, PrimeSpectrum.zeroLocus_iSup, Module.mem_support_iff_exists_annihilator, Module.mem_support_iff', Module.support_of_exact, Algebra.smoothLocus_comap_of_isLocalization, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal, image_comap_zeroLocus_eq_zeroLocus_comap, PrimeSpectrum.isClosed_singleton_iff_isMaximal, Algebra.QuasiFinite.finite_comap_preimage, PrimeSpectrum.isOpen_iff, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal, IsLocalRing.specializes_closedPoint, PrimeSpectrum.toPiLocalization_bijective, PrimeSpectrum.residueField_comap, Algebra.smoothLocus_eq_univ, Algebra.isOpen_smoothLocus, Module.isOpen_freeLocus, PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux, IsLocalRing.closedPoint_mem_support, PrimeSpectrum.primeSpectrumProd_symm_inr, MvPolynomial.pointToPoint_zeroLocus_le, Module.rankAtStalk_tensorProduct, PrimeSpectrum.sigmaToPi_asIdeal, PrimeSpectrum.vanishingIdeal_union, Algebra.basicOpen_subset_etaleLocus_iff, PrimeSpectrum.exists_constructibleSetData_iff, PrimeSpectrum.le_iff_mem_closure, PrimeSpectrum.compactSpace, PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, PrimeSpectrum.isClosed_iff_zeroLocus_ideal, Polynomial.isCompact_image_comap_of_monic, PrimeSpectrum.isOpen_basicOpen, PrimeSpectrum.instPrespectralSpace, Module.isLocallyConstant_rankAtStalk_freeLocus, PrimeSpectrum.isTopologicalBasis_basic_opens, PrimeSpectrum.basicOpen_mul_le_left, PrimeSpectrum.mem_range_comap_iff, PrimeSpectrum.exists_primeSpectrum_prod_le, IsLocalRing.PrimeSpectrum.asIdeal_top, RingHom.strictMono_specComap_of_surjective, Module.mem_freeLocus_iff_tensor, PrimeSpectrum.finite_setOf_isMin, AlgebraicGeometry.coprodSpec_coprodMk, PrimeSpectrum.vanishingIdeal_empty, PrimeSpectrum.zeroLocus_bot, Module.support_eq_empty_iff, AlgebraicGeometry.Spec_carrier, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization, Module.rankAtStalk_pos_iff_mem_support, PrimeSpectrum.comapEquiv_apply, Ideal.exists_ltSeries_of_hasGoingDown, PrimeSpectrum.range_comap_snd, PrimeSpectrum.nonempty_iff_nontrivial, PrimeSpectrum.piLocalizationToMaximal_surjective, PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.zeroLocus_mul, PrimeSpectrum.preimage_comap_zeroLocus_aux, PrimeSpectrum.nhdsOrderEmbedding_apply, PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable, MvPolynomial.comap_C_surjective, PrimeSpectrum.stableUnderSpecialization_range_iff, PrimeSpectrum.closure_image_comap_zeroLocus, Module.rankAtStalk_prod, Algebra.unramifiedLocus_eq_univ_iff, IsLocalRing.closed_point_mem_iff, PrimeSpectrum.le_iff_specializes, PrimeSpectrum.instNoetherianSpace, PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.closure_singleton, PrimeSpectrum.isClopen_basicOpen_of_mul_add, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens, PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm, IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top, Module.nonempty_support_of_nontrivial, PrimeSpectrum.localization_comap_injective, PrimeSpectrum.stableUnderSpecialization_singleton, MaximalSpectrum.toPrimeSpectrum_injective, Polynomial.image_comap_C_basicOpen, PrimeSpectrum.gc_set, Module.support_quotSMulTop, PrimeSpectrum.comapEquiv_symm, PrimeSpectrum.vanishingIdeal_univ, PrimeSpectrum.isRetrocompact_zeroLocus_compl, LocalizedModule.subsingleton_iff_support_subset, PrimeSpectrum.nilradical_eq_iInf, PrimeSpectrum.comap_basicOpen, Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, AlgebraicGeometry.IsPreimmersion.SpecMap_iff, Algebra.isOpen_unramifiedLocus, Module.mem_support_iff_nontrivial_residueField_tensorProduct, MaximalSpectrum.toPrimeSpectrum_range, Algebra.QuasiFinite.finite_comap_preimage_singleton, PrimeSpectrum.zeroLocus_univ, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim, Module.isLocallyConstant_rankAtStalk, Module.notMem_support_iff, Module.support_of_noZeroSMulDivisors, PrimeSpectrum.zeroLocus_iUnion₂, Algebra.mem_etaleLocus_iff, PrimeSpectrum.isIdempotentElemEquivClopens_symm_top, PrimeSpectrum.comap_injective_of_surjective, RingHom.FaithfullyFlat.iff_flat_and_comap_surjective, PrimeSpectrum.stableUnderGeneralization_singleton, Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support, PrimeSpectrum.comap_singleton_isClosed_of_surjective, Module.support_subset_of_injective, PrimeSpectrum.irreducibleSpace, image_specComap_zeroLocus_eq_zeroLocus_comap, Module.mem_support_iff, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Module.nonempty_support_iff, PrimeSpectrum.isCompact_basicOpen, PrimeSpectrum.basicOpen_mul_le_right, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, PrimeSpectrum.zeroLocus_empty_of_one_mem, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, PrimeSpectrum.basicOpen_le_basicOpen_iff, IsArtinianRing.instFinitePrimeSpectrum, Algebra.QuasiFinite.discreteTopology_primeSpectrum, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal, PrimeSpectrum.mem_basicOpen, PrimeSpectrum.continuous_tensorProductTo, PrimeSpectrum.zeroLocus_singleton_one, PrimeSpectrum.subset_zeroLocus_vanishingIdeal, AlgebraicGeometry.Spec.map_base, PrimeSpectrum.zeroLocus_singleton_mul, Module.mem_freeLocus_of_isLocalization, PrimeSpectrum.ConstructibleSetData.toSet_map, PrimeSpectrum.isClopen_iff_zeroLocus, PrimeSpectrum.isEmbedding_comap_of_surjective, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, Module.stableUnderSpecialization_support, PrimeSpectrum.isEmpty_iff_subsingleton, exists_multiset_prod_cons_le_and_prod_not_le, PrimeSpectrum.zeroLocus_inf, PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime, AlgebraicGeometry.StructureSheaf.comap_basicOpen, PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite, AlgebraicGeometry.Spec.topObj_forget, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, AlgebraicGeometry.Scheme.affineBasisCover_map_range, PrimeSpectrum.piLocalizationToMaximal_bijective, PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal, PrimeSpectrum.exists_image_comap_of_finite_of_free, PrimeSpectrum.isClosed_range_comap_of_surjective, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal, PrimeSpectrum.toPiLocalization_injective, PrimeSpectrum.asIdeal_lt_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, PrimeSpectrum.localization_specComap_injective, PrimeSpectrum.subsingleton_iff_isField_of_isReduced, PrimeSpectrum.zeroLocus_eq_basicOpen_of_mul_add, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, AlgebraicGeometry.genericPoint_eq_bot_of_affine, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, Module.rankAtStalk_eq_zero_of_subsingleton, AlgebraicGeometry.Polynomial.isOpen_imageOfDf, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, PrimeSpectrum.sigmaToPi_not_surjective_of_infinite, PrimeSpectrum.zeroLocus_sup, PrimeSpectrum.sigmaToPi_injective, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, PrimeSpectrum.instJacobsonSpaceOfIsJacobsonRing, Module.mem_freeLocus, PrimeSpectrum.localization_comap_range, Algebra.smoothLocus_eq_compl_support_inter, PrimeSpectrum.range_comap_fst, PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, PrimeSpectrum.zeroLocus_empty_iff_eq_top, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, PrimeSpectrum.specComap_comp, Module.isClosed_support, PrimeSpectrum.localization_comap_isEmbedding, PrimeSpectrum.zeroLocus_anti_mono_ideal, PrimeSpectrum.basicOpen_one, RingHom.FaithfullyFlat.eq_and, Module.rankAtStalk_self, PrimeSpectrum.iSup_basicOpen_eq_top_iff', PrimeSpectrum.isClosed_comap_singleton_of_isIntegral, Algebra.basicOpen_subset_smoothLocus_iff, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, PrimeSpectrum.vanishingIdeal_closure, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, PrimeSpectrum.BasicConstructibleSetData.toSet_map, PrimeSpectrum.zeroLocus_singleton_zero, Module.mem_support_iff_of_span_eq_top, PrimeSpectrum.isClosedEmbedding_comap_of_surjective, PrimeSpectrum.isIdempotentElemEquivClopens_mul, RingHom.IsIntegral.specComap_surjective, PrimeSpectrum.localization_away_comap_range, PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain, PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal, PrimeSpectrum.isRetrocompact_basicOpen, PrimeSpectrum.vanishingIdeal_iUnion, PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply, PrimeSpectrum.isCompact_isOpen_iff_ideal, AlgebraicGeometry.Spec.toTop_obj_carrier, ValuationSubring.primeSpectrumEquiv_apply, PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl, PrimeSpectrum.isBasis_basic_opens, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, Polynomial.comap_C_surjective, PrimeSpectrum.nontrivial_iff_mem_rangeComap, Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocus, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, Module.support_subset_of_surjective, PrimeSpectrum.comap_isInducing_of_surjective, PrimeSpectrum.comap_comp, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective, PrimeSpectrum.isHomeomorph_comap_of_bijective, MvPolynomial.mem_image_comap_C_basicOpen, Algebra.etaleLocus_eq_compl_support, Algebra.QuasiFinite.finite_primeSpectrum, PrimeSpectrum.stableUnderSpecialization_image_iff, PrimeSpectrum.basicOpen_eq_bot_iff, PrimeSpectrum.isConstructible_range_comap, Module.rankAtStalk_eq_finrank_of_free, PrimeSpectrum.range_asIdeal, PrimeSpectrum.asIdeal_le_asIdeal, PrimeSpectrum.zeroLocus_eq_singleton, Module.notMem_support_iff'

---

← Back to Index