Topology

📁 Source: Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

Statistics

Metric	Count
Definitions ProjectiveSpectrum, asHomogeneousIdeal, basicOpen, instPartialOrder, top, vanishingIdeal, zariskiTopology, zeroLocus	8
Theorems as_ideal_le_as_ideal, as_ideal_lt_as_ideal, basicOpen_eq_union_of_projection, basicOpen_eq_zeroLocus_compl, basicOpen_mul, basicOpen_mul_le_left, basicOpen_mul_le_right, basicOpen_one, basicOpen_pow, basicOpen_zero, coe_vanishingIdeal, ext, ext_iff, gc_homogeneousIdeal, gc_ideal, gc_set, homogeneousIdeal_le_vanishingIdeal_zeroLocus, ideal_le_vanishingIdeal_zeroLocus, instIsPrimeToIdealNatAsHomogeneousIdeal, isClosed_iff_zeroLocus, isClosed_zeroLocus, isOpen_basicOpen, isOpen_iff, isPrime, isTopologicalBasis_basic_opens, le_iff_mem_closure, mem_basicOpen, mem_coe_basicOpen, mem_compl_zeroLocus_iff_notMem, mem_vanishingIdeal, mem_zeroLocus, not_irrelevant_le, subset_vanishingIdeal_zeroLocus, subset_zeroLocus_iff_le_vanishingIdeal, subset_zeroLocus_iff_subset_vanishingIdeal, subset_zeroLocus_vanishingIdeal, sup_vanishingIdeal_le, union_zeroLocus, vanishingIdeal_anti_mono, vanishingIdeal_closure, vanishingIdeal_iUnion, vanishingIdeal_singleton, vanishingIdeal_union, vanishingIdeal_univ, zeroLocus_anti_mono, zeroLocus_anti_mono_homogeneousIdeal, zeroLocus_anti_mono_ideal, zeroLocus_bUnion, zeroLocus_bot, zeroLocus_empty, zeroLocus_empty_of_one_mem, zeroLocus_iSup_homogeneousIdeal, zeroLocus_iSup_ideal, zeroLocus_iUnion, zeroLocus_inf, zeroLocus_mul_homogeneousIdeal, zeroLocus_mul_ideal, zeroLocus_singleton_mul, zeroLocus_singleton_one, zeroLocus_singleton_pow, zeroLocus_singleton_zero, zeroLocus_span, zeroLocus_sup_homogeneousIdeal, zeroLocus_sup_ideal, zeroLocus_union, zeroLocus_univ, zeroLocus_vanishingIdeal_eq_closure	67
Total	75

ProjectiveSpectrum

Definitions

Name	Category	Theorems
asHomogeneousIdeal 📖	CompOp	39 math math: mem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, ext_iff, vanishingIdeal_singleton, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.Proj.pow_apply, AlgebraicGeometry.Proj.mul_apply, mem_vanishingIdeal, AlgebraicGeometry.Proj.one_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.Proj.sub_apply, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, AlgebraicGeometry.Proj.mem_basicOpen, not_irrelevant_le, isPrime, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, as_ideal_le_as_ideal, as_ideal_lt_as_ideal, mem_zeroLocus, AlgebraicGeometry.Proj.zero_apply, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Proj.ext_iff, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, instIsPrimeToIdealNatAsHomogeneousIdeal, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.Proj.stalkIso'_germ, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, mem_compl_zeroLocus_iff_notMem, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.mem_basicOpen_den, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', mem_coe_basicOpen, AlgebraicGeometry.Proj.res_apply, AlgebraicGeometry.Proj.stalkIso'_symm_mk, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom
basicOpen 📖	CompOp	39 math math: AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, mem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, basicOpen_mul_le_left, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, basicOpen_mul, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, isTopologicalBasis_basic_opens, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, basicOpen_zero, basicOpen_eq_zeroLocus_compl, isOpen_basicOpen, basicOpen_eq_union_of_projection, basicOpen_pow, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.mem_basicOpen_den, mem_coe_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, basicOpen_one, basicOpen_mul_le_right, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Proj.stalkIso'_symm_mk, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective
instPartialOrder 📖	CompOp	3 math math: as_ideal_le_as_ideal, as_ideal_lt_as_ideal, le_iff_mem_closure
top 📖	CompOp	18 math math: AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Proj.pow_apply, AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier, AlgebraicGeometry.Proj.one_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.Proj.sub_apply, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, AlgebraicGeometry.Proj.zero_apply, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', AlgebraicGeometry.Proj.ext_iff, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.mem_basicOpen_den, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', AlgebraicGeometry.Proj.res_apply, AlgebraicGeometry.Proj.stalkIso'_symm_mk, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom
vanishingIdeal 📖	CompOp	19 math math: vanishingIdeal_singleton, subset_zeroLocus_vanishingIdeal, gc_homogeneousIdeal, vanishingIdeal_closure, vanishingIdeal_iUnion, sup_vanishingIdeal_le, mem_vanishingIdeal, subset_zeroLocus_iff_le_vanishingIdeal, subset_zeroLocus_iff_subset_vanishingIdeal, gc_set, vanishingIdeal_anti_mono, homogeneousIdeal_le_vanishingIdeal_zeroLocus, gc_ideal, zeroLocus_vanishingIdeal_eq_closure, ideal_le_vanishingIdeal_zeroLocus, subset_vanishingIdeal_zeroLocus, coe_vanishingIdeal, vanishingIdeal_union, vanishingIdeal_univ
zariskiTopology 📖	CompOp	25 math math: mem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, vanishingIdeal_closure, basicOpen_mul_le_left, isClosed_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, isOpen_iff, basicOpen_mul, isTopologicalBasis_basic_opens, isClosed_iff_zeroLocus, zeroLocus_vanishingIdeal_eq_closure, basicOpen_zero, basicOpen_eq_zeroLocus_compl, isOpen_basicOpen, basicOpen_eq_union_of_projection, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.mem_basicOpen_den, mem_coe_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, basicOpen_one, basicOpen_mul_le_right, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, le_iff_mem_closure, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen
zeroLocus 📖	CompOp	39 math math: zeroLocus_mul_ideal, subset_zeroLocus_vanishingIdeal, gc_homogeneousIdeal, zeroLocus_mul_homogeneousIdeal, zeroLocus_univ, zeroLocus_empty_of_one_mem, zeroLocus_anti_mono, subset_zeroLocus_iff_le_vanishingIdeal, union_zeroLocus, subset_zeroLocus_iff_subset_vanishingIdeal, isClosed_zeroLocus, mem_zeroLocus, gc_set, isOpen_iff, zeroLocus_singleton_pow, zeroLocus_singleton_one, zeroLocus_singleton_zero, homogeneousIdeal_le_vanishingIdeal_zeroLocus, zeroLocus_bot, zeroLocus_iUnion, zeroLocus_bUnion, gc_ideal, isClosed_iff_zeroLocus, zeroLocus_vanishingIdeal_eq_closure, zeroLocus_anti_mono_ideal, basicOpen_eq_zeroLocus_compl, ideal_le_vanishingIdeal_zeroLocus, zeroLocus_anti_mono_homogeneousIdeal, zeroLocus_sup_homogeneousIdeal, zeroLocus_empty, zeroLocus_iSup_homogeneousIdeal, mem_compl_zeroLocus_iff_notMem, zeroLocus_sup_ideal, subset_vanishingIdeal_zeroLocus, zeroLocus_union, zeroLocus_singleton_mul, zeroLocus_span, zeroLocus_iSup_ideal, zeroLocus_inf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
as_ideal_le_as_ideal 📖	mathematical	—	HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrderHomogeneousIdeal asHomogeneousIdeal ProjectiveSpectrum instPartialOrder	—	—
as_ideal_lt_as_ideal 📖	mathematical	—	HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid Preorder.toLT PartialOrder.toPreorder instPartialOrderHomogeneousIdeal asHomogeneousIdeal ProjectiveSpectrum instPartialOrder	—	—
basicOpen_eq_union_of_projection 📖	mathematical	—	basicOpen iSup TopologicalSpace.Opens ProjectiveSpectrum zariskiTopology ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing AddMonoidHom.instFunLike GradedRing.proj Nat.instAddMonoid	—	TopologicalSpace.Opens.ext Set.ext mem_coe_basicOpen SetLike.mem_coe iSup.eq_1 TopologicalSpace.Opens.mem_sSup Mathlib.Tactic.Contrapose.contrapose₂ AddSubmonoidClass.toZeroMemClass DirectSum.sum_support_decompose Ideal.sum_mem mem_basicOpen HomogeneousSubmodule.is_homogeneous'
basicOpen_eq_zeroLocus_compl 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens ProjectiveSpectrum zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen Compl.compl Set Set.instCompl zeroLocus Set.instSingletonSet	—	Set.ext
basicOpen_mul 📖	mathematical	—	basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TopologicalSpace.Opens ProjectiveSpectrum zariskiTopology SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_mul Set.compl_union
basicOpen_mul_le_left 📖	mathematical	—	TopologicalSpace.Opens ProjectiveSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	basicOpen_mul inf_le_left
basicOpen_mul_le_right 📖	mathematical	—	TopologicalSpace.Opens ProjectiveSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	basicOpen_mul inf_le_right
basicOpen_one 📖	mathematical	—	basicOpen AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Top.top TopologicalSpace.Opens ProjectiveSpectrum zariskiTopology OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_one Set.compl_empty
basicOpen_pow 📖	mathematical	—	basicOpen Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_pow
basicOpen_zero 📖	mathematical	—	basicOpen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Bot.bot TopologicalSpace.Opens ProjectiveSpectrum zariskiTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_zero Set.compl_univ
coe_vanishingIdeal 📖	mathematical	—	SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike vanishingIdeal setOf	—	Set.ext vanishingIdeal.eq_1 SetLike.mem_coe HomogeneousIdeal.mem_iff HomogeneousIdeal.toIdeal_iInf Submodule.mem_iInf
ext 📖	—	asHomogeneousIdeal	—	—	Nat.instCanonicallyOrderedAdd
ext_iff 📖	mathematical	—	asHomogeneousIdeal	—	ext
gc_homogeneousIdeal 📖	mathematical	—	GaloisConnection HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid OrderDual Set ProjectiveSpectrum PartialOrder.toPreorder instPartialOrderHomogeneousIdeal OrderDual.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra zeroLocus SetLike.coe HomogeneousIdeal.setLike vanishingIdeal	—	subset_zeroLocus_iff_le_vanishingIdeal
gc_ideal 📖	mathematical	—	GaloisConnection Ideal CommSemiring.toSemiring CommRing.toCommSemiring OrderDual Set ProjectiveSpectrum PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule OrderDual.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra zeroLocus SetLike.coe Submodule.setLike HomogeneousIdeal.toIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid vanishingIdeal	—	subset_zeroLocus_iff_le_vanishingIdeal
gc_set 📖	mathematical	—	GaloisConnection Set OrderDual ProjectiveSpectrum PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder zeroLocus SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike vanishingIdeal	—	GaloisInsertion.gc zeroLocus_span GaloisConnection.compose gc_ideal
homogeneousIdeal_le_vanishingIdeal_zeroLocus 📖	mathematical	—	HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrderHomogeneousIdeal vanishingIdeal zeroLocus SetLike.coe HomogeneousIdeal.setLike	—	GaloisConnection.le_u_l gc_homogeneousIdeal
ideal_le_vanishingIdeal_zeroLocus 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule HomogeneousIdeal.toIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid vanishingIdeal zeroLocus SetLike.coe Submodule.setLike	—	GaloisConnection.le_u_l gc_ideal
instIsPrimeToIdealNatAsHomogeneousIdeal 📖	mathematical	—	Ideal.IsPrime Ring.toSemiring CommRing.toRing HomogeneousIdeal.toIdeal Nat.instAddMonoid asHomogeneousIdeal	—	isPrime
isClosed_iff_zeroLocus 📖	mathematical	—	IsClosed ProjectiveSpectrum zariskiTopology zeroLocus	—	isOpen_compl_iff isOpen_iff compl_compl
isClosed_zeroLocus 📖	mathematical	—	IsClosed ProjectiveSpectrum zariskiTopology zeroLocus	—	isClosed_iff_zeroLocus
isOpen_basicOpen 📖	mathematical	—	IsOpen ProjectiveSpectrum zariskiTopology SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	TopologicalSpace.Opens.isOpen
isOpen_iff 📖	mathematical	—	IsOpen ProjectiveSpectrum zariskiTopology Compl.compl Set Set.instCompl zeroLocus	—	—
isPrime 📖	mathematical	—	Ideal.IsPrime Ring.toSemiring CommRing.toRing HomogeneousIdeal.toIdeal Nat.instAddMonoid asHomogeneousIdeal	—	—
isTopologicalBasis_basic_opens 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis ProjectiveSpectrum zariskiTopology Set.range Set SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_basicOpen Set.not_subset mem_zeroLocus Set.mem_compl_iff compl_compl Set.compl_subset_compl basicOpen_eq_zeroLocus_compl zeroLocus_anti_mono Set.singleton_subset_iff
le_iff_mem_closure 📖	mathematical	—	ProjectiveSpectrum Preorder.toLE PartialOrder.toPreorder instPartialOrder Set Set.instMembership closure zariskiTopology Set.instSingletonSet	—	as_ideal_le_as_ideal zeroLocus_vanishingIdeal_eq_closure mem_zeroLocus vanishingIdeal_singleton instIsConcreteLE
mem_basicOpen 📖	mathematical	—	ProjectiveSpectrum TopologicalSpace.Opens zariskiTopology SetLike.instMembership TopologicalSpace.Opens.instSetLike basicOpen HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike asHomogeneousIdeal	—	—
mem_coe_basicOpen 📖	mathematical	—	ProjectiveSpectrum Set Set.instMembership SetLike.coe TopologicalSpace.Opens zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid SetLike.instMembership HomogeneousIdeal.setLike asHomogeneousIdeal	—	—
mem_compl_zeroLocus_iff_notMem 📖	mathematical	—	ProjectiveSpectrum Set Set.instMembership Compl.compl Set.instCompl zeroLocus Set.instSingletonSet HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid SetLike.instMembership HomogeneousIdeal.setLike asHomogeneousIdeal	—	Set.mem_compl_iff mem_zeroLocus Set.singleton_subset_iff
mem_vanishingIdeal 📖	mathematical	—	HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid SetLike.instMembership HomogeneousIdeal.setLike vanishingIdeal asHomogeneousIdeal	—	SetLike.mem_coe coe_vanishingIdeal Set.mem_setOf_eq
mem_zeroLocus 📖	mathematical	—	ProjectiveSpectrum Set Set.instMembership zeroLocus Set.instHasSubset SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike asHomogeneousIdeal	—	—
not_irrelevant_le 📖	mathematical	—	HomogeneousIdeal Ring.toSemiring CommRing.toRing AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrderHomogeneousIdeal HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd asHomogeneousIdeal	—	—
subset_vanishingIdeal_zeroLocus 📖	mathematical	—	Set Set.instHasSubset SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike vanishingIdeal zeroLocus	—	GaloisConnection.le_u_l gc_set
subset_zeroLocus_iff_le_vanishingIdeal 📖	mathematical	—	Set ProjectiveSpectrum Set.instHasSubset zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder HomogeneousIdeal.toIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid vanishingIdeal	—	mem_vanishingIdeal mem_zeroLocus le_trans
subset_zeroLocus_iff_subset_vanishingIdeal 📖	mathematical	—	Set ProjectiveSpectrum Set.instHasSubset zeroLocus SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike vanishingIdeal	—	gc_set
subset_zeroLocus_vanishingIdeal 📖	mathematical	—	Set ProjectiveSpectrum Set.instHasSubset zeroLocus SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike vanishingIdeal	—	GaloisConnection.l_u_le gc_ideal
sup_vanishingIdeal_le 📖	mathematical	—	HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrderHomogeneousIdeal HomogeneousIdeal.instMax vanishingIdeal Set ProjectiveSpectrum Set.instInter	—	HomogeneousIdeal.mem_iff HomogeneousIdeal.toIdeal_sup mem_vanishingIdeal Submodule.mem_sup Submodule.add_mem
union_zeroLocus 📖	mathematical	—	Set ProjectiveSpectrum Set.instUnion zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instMin Ideal.span	—	zeroLocus_inf zeroLocus_span
vanishingIdeal_anti_mono 📖	mathematical	Set ProjectiveSpectrum Set.instHasSubset	HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrderHomogeneousIdeal vanishingIdeal	—	GaloisConnection.monotone_u gc_ideal
vanishingIdeal_closure 📖	mathematical	—	vanishingIdeal closure ProjectiveSpectrum zariskiTopology	—	GaloisConnection.u_l_u_eq_u gc_ideal HomogeneousIdeal.ext zeroLocus_vanishingIdeal_eq_closure
vanishingIdeal_iUnion 📖	mathematical	—	vanishingIdeal Set.iUnion ProjectiveSpectrum iInf HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.instInfSet	—	HomogeneousIdeal.toIdeal_injective HomogeneousIdeal.toIdeal_iInf GaloisConnection.u_iInf gc_ideal
vanishingIdeal_singleton 📖	mathematical	—	vanishingIdeal ProjectiveSpectrum Set Set.instSingletonSet asHomogeneousIdeal	—	iInf_congr_Prop iInf_iInf_eq_left
vanishingIdeal_union 📖	mathematical	—	vanishingIdeal Set ProjectiveSpectrum Set.instUnion HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.instMin	—	HomogeneousIdeal.ext GaloisConnection.u_inf gc_ideal
vanishingIdeal_univ 📖	mathematical	—	vanishingIdeal Set ProjectiveSpectrum Set.instEmptyCollection Top.top HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.instTop	—	GaloisConnection.u_top gc_ideal
zeroLocus_anti_mono 📖	mathematical	Set Set.instHasSubset	ProjectiveSpectrum zeroLocus	—	GaloisConnection.monotone_l gc_set
zeroLocus_anti_mono_homogeneousIdeal 📖	mathematical	HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrderHomogeneousIdeal	Set ProjectiveSpectrum Set.instHasSubset zeroLocus SetLike.coe HomogeneousIdeal.setLike	—	GaloisConnection.monotone_l gc_homogeneousIdeal
zeroLocus_anti_mono_ideal 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Set ProjectiveSpectrum Set.instHasSubset zeroLocus SetLike.coe Submodule.setLike	—	GaloisConnection.monotone_l gc_ideal
zeroLocus_bUnion 📖	mathematical	—	zeroLocus Set.iUnion Set Set.instMembership Set.iInter ProjectiveSpectrum	—	zeroLocus_iUnion
zeroLocus_bot 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Bot.bot Submodule.instBot Set.univ ProjectiveSpectrum	—	GaloisConnection.l_bot gc_ideal
zeroLocus_empty 📖	mathematical	—	zeroLocus Set Set.instEmptyCollection Set.univ ProjectiveSpectrum	—	GaloisConnection.l_bot gc_set
zeroLocus_empty_of_one_mem 📖	mathematical	Set Set.instMembership AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	zeroLocus ProjectiveSpectrum Set.instEmptyCollection	—	Set.eq_empty_iff_forall_notMem Ideal.IsPrime.ne_top instIsPrimeToIdealNatAsHomogeneousIdeal Ideal.eq_top_iff_one
zeroLocus_iSup_homogeneousIdeal 📖	mathematical	—	zeroLocus SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike iSup HomogeneousIdeal.instSupSet Set.iInter ProjectiveSpectrum	—	GaloisConnection.l_iSup gc_homogeneousIdeal
zeroLocus_iSup_ideal 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.iInter ProjectiveSpectrum	—	GaloisConnection.l_iSup gc_ideal
zeroLocus_iUnion 📖	mathematical	—	zeroLocus Set.iUnion Set.iInter ProjectiveSpectrum	—	GaloisConnection.l_iSup gc_set
zeroLocus_inf 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instMin Set ProjectiveSpectrum Set.instUnion	—	Set.ext Ideal.IsPrime.inf_le isPrime
zeroLocus_mul_homogeneousIdeal 📖	mathematical	—	zeroLocus SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike instMulHomogeneousIdeal CommRing.toCommSemiring Set ProjectiveSpectrum Set.instUnion	—	Set.ext Ideal.IsPrime.mul_le isPrime
zeroLocus_mul_ideal 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.mul IsScalarTower.right Algebra.id Set ProjectiveSpectrum Set.instUnion	—	Set.ext IsScalarTower.right Ideal.IsPrime.mul_le isPrime
zeroLocus_singleton_mul 📖	mathematical	—	zeroLocus Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ProjectiveSpectrum Set.instUnion	—	Set.ext Ideal.IsPrime.mul_mem_iff_mem_or_mem Ideal.instIsTwoSided_1 isPrime
zeroLocus_singleton_one 📖	mathematical	—	zeroLocus Set Set.instSingletonSet AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ProjectiveSpectrum Set.instEmptyCollection	—	zeroLocus_empty_of_one_mem Set.mem_singleton
zeroLocus_singleton_pow 📖	mathematical	—	zeroLocus Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	Set.ext Ideal.IsPrime.pow_mem_iff_mem isPrime
zeroLocus_singleton_zero 📖	mathematical	—	zeroLocus Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Set.univ ProjectiveSpectrum	—	zeroLocus_bot
zeroLocus_span 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span	—	Set.ext GaloisInsertion.gc
zeroLocus_sup_homogeneousIdeal 📖	mathematical	—	zeroLocus SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike HomogeneousIdeal.instMax Set ProjectiveSpectrum Set.instInter	—	GaloisConnection.l_sup gc_homogeneousIdeal
zeroLocus_sup_ideal 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id Set ProjectiveSpectrum Set.instInter	—	GaloisConnection.l_sup gc_ideal
zeroLocus_union 📖	mathematical	—	zeroLocus Set Set.instUnion ProjectiveSpectrum Set.instInter	—	GaloisConnection.l_sup gc_set
zeroLocus_univ 📖	mathematical	—	zeroLocus Set.univ Set ProjectiveSpectrum Set.instEmptyCollection	—	zeroLocus_empty_of_one_mem Set.mem_univ
zeroLocus_vanishingIdeal_eq_closure 📖	mathematical	—	zeroLocus SetLike.coe HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike vanishingIdeal closure ProjectiveSpectrum zariskiTopology	—	Set.Subset.antisymm isClosed_iff_zeroLocus Set.Subset.trans subset_zeroLocus_iff_subset_vanishingIdeal IsClosed.closure_subset_iff isClosed_zeroLocus subset_zeroLocus_vanishingIdeal

(root)

Definitions

Name	Category	Theorems
ProjectiveSpectrum 📖	CompData	61 math math: ProjectiveSpectrum.mem_basicOpen, ProjectiveSpectrum.vanishingIdeal_singleton, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, ProjectiveSpectrum.zeroLocus_mul_ideal, ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal, ProjectiveSpectrum.gc_homogeneousIdeal, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal, ProjectiveSpectrum.vanishingIdeal_closure, ProjectiveSpectrum.zeroLocus_univ, ProjectiveSpectrum.vanishingIdeal_iUnion, ProjectiveSpectrum.zeroLocus_empty_of_one_mem, ProjectiveSpectrum.sup_vanishingIdeal_le, ProjectiveSpectrum.zeroLocus_anti_mono, ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, ProjectiveSpectrum.basicOpen_mul_le_left, ProjectiveSpectrum.union_zeroLocus, ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal, ProjectiveSpectrum.isClosed_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, ProjectiveSpectrum.as_ideal_le_as_ideal, ProjectiveSpectrum.as_ideal_lt_as_ideal, ProjectiveSpectrum.mem_zeroLocus, ProjectiveSpectrum.gc_set, ProjectiveSpectrum.isOpen_iff, ProjectiveSpectrum.zeroLocus_singleton_one, ProjectiveSpectrum.zeroLocus_singleton_zero, ProjectiveSpectrum.basicOpen_mul, ProjectiveSpectrum.zeroLocus_bot, ProjectiveSpectrum.zeroLocus_iUnion, ProjectiveSpectrum.zeroLocus_bUnion, ProjectiveSpectrum.isTopologicalBasis_basic_opens, ProjectiveSpectrum.gc_ideal, ProjectiveSpectrum.isClosed_iff_zeroLocus, ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure, ProjectiveSpectrum.zeroLocus_anti_mono_ideal, ProjectiveSpectrum.basicOpen_zero, ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl, ProjectiveSpectrum.isOpen_basicOpen, ProjectiveSpectrum.basicOpen_eq_union_of_projection, ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal, ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal, ProjectiveSpectrum.zeroLocus_empty, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal, ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem, AlgebraicGeometry.mem_basicOpen_den, ProjectiveSpectrum.zeroLocus_sup_ideal, ProjectiveSpectrum.mem_coe_basicOpen, ProjectiveSpectrum.zeroLocus_union, ProjectiveSpectrum.zeroLocus_singleton_mul, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, ProjectiveSpectrum.basicOpen_one, ProjectiveSpectrum.zeroLocus_iSup_ideal, ProjectiveSpectrum.basicOpen_mul_le_right, ProjectiveSpectrum.zeroLocus_inf, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, ProjectiveSpectrum.le_iff_mem_closure, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, ProjectiveSpectrum.vanishingIdeal_union, ProjectiveSpectrum.vanishingIdeal_univ

---

← Back to Index