Noetherian

📁 Source: Mathlib/AlgebraicGeometry/Noetherian.lean

Statistics

Metric	Count
Definitions `IsLocallyNoetherian`, `IsNoetherian`	2
Theorems `component_noetherian`, `quasiSeparatedSpace`, `noetherianSpace`, `toCompactSpace`, `toIsLocallyNoetherian`, `iff_locallyOfFiniteType`, `isLocallyNoetherian`, `finite_irreducibleComponents_of_isNoetherian`, `instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType`, `instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType_1`, `instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier`, `instIsLocallyNoetherianToScheme`, `instIsLocallyNoetherianXScheme`, `instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian`, `instIsNoetherianSpecOfIsNoetherianRingCarrier`, `instIsNoetherianSpecOfOfIsNoetherianRing`, `instLocallyOfFinitePresentationOfIsLocallyNoetherianOfLocallyOfFiniteType`, `instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier`, `instQuasiCompactOfIsLocallyNoetherianOfIsOpenImmersion`, `isLocallyNoetherian_Spec`, `isLocallyNoetherian_iff_of_affine_openCover`, `isLocallyNoetherian_iff_of_iSup_eq_top`, `isLocallyNoetherian_iff_openCover`, `isLocallyNoetherian_of_affine_cover`, `isLocallyNoetherian_of_isOpenImmersion`, `isNoetherianRing_of_away`, `isNoetherian_Spec`, `isNoetherian_iff`, `isNoetherian_iff_of_finite_affine_openCover`, `isNoetherian_iff_of_finite_iSup_eq_top`, `noetherianSpace_of_isAffine`, `noetherianSpace_of_isAffineOpen`, `quasiCompact_of_noetherianSpace_source`	33
Total	35

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsLocallyNoetherian` 📖	CompData	16 math math: `IsNoetherian.toIsLocallyNoetherian`, `isLocallyNoetherian_of_affine_cover`, `LocallyOfFiniteType.isLocallyNoetherian`, `instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier`, `isNoetherian_iff`, `isLocallyNoetherian_iff_of_affine_openCover`, `IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology`, `instIsLocallyNoetherianToScheme`, `instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType_1`, `isLocallyNoetherian_Spec`, `IsLocallyArtinian.isLocallyNoetherian`, `instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType`, `isLocallyNoetherian_iff_of_iSup_eq_top`, `instIsLocallyNoetherianXScheme`, `isLocallyNoetherian_of_isOpenImmersion`, `isLocallyNoetherian_iff_openCover`
`IsNoetherian` 📖	CompData	8 math math: `instIsNoetherianSpecOfIsNoetherianRingCarrier`, `isNoetherian_iff_of_finite_affine_openCover`, `isNoetherian_iff`, `isNoetherian_iff_of_finite_iSup_eq_top`, `IsArtinianScheme.iff_isNoetherian_and_discreteTopology`, `instIsNoetherianSpecOfOfIsNoetherianRing`, `IsArtinianScheme.isNoetherianScheme`, `isNoetherian_Spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_irreducibleComponents_of_isNoetherian` 📖	mathematical	—	`Set.Finite` `Set` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `irreducibleComponents` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`TopologicalSpace.NoetherianSpace.finite_irreducibleComponents` `IsNoetherian.noetherianSpace`
`instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType` 📖	mathematical	—	`IsLocallyNoetherian` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback`	—	`LocallyOfFiniteType.isLocallyNoetherian` `Scheme.Pullback.instHasPullback` `instLocallyOfFiniteTypeSndScheme`
`instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType_1` 📖	mathematical	—	`IsLocallyNoetherian` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback`	—	`LocallyOfFiniteType.isLocallyNoetherian` `Scheme.Pullback.instHasPullback` `instLocallyOfFiniteTypeFstScheme`
`instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier` 📖	mathematical	—	`IsLocallyNoetherian` `Spec`	—	`isLocallyNoetherian_of_affine_cover` `isAffineOpen_top` `isAffine_Spec` `ciSup_unique` `isNoetherianRing_of_ringEquiv`
`instIsLocallyNoetherianToScheme` 📖	mathematical	—	`IsLocallyNoetherian` `Scheme.Opens.toScheme`	—	`isLocallyNoetherian_of_isOpenImmersion` `Scheme.Opens.instIsOpenImmersionι`
`instIsLocallyNoetherianXScheme` 📖	mathematical	—	`IsLocallyNoetherian` `CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion`	—	`isLocallyNoetherian_of_isOpenImmersion` `Scheme.instIsOpenImmersionF`
`instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian` 📖	mathematical	—	`IsNoetherianRing` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `PresheafedSpace.carrier` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `PresheafedSpace.presheaf` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `exists_isAffineOpen_mem_and_subset` `PrimeSpectrum.isPrime` `IsAffineOpen.isLocalization_stalk` `IsLocalization.isNoetherianRing` `IsLocallyNoetherian.component_noetherian`
`instIsNoetherianSpecOfIsNoetherianRingCarrier` 📖	mathematical	—	`IsNoetherian` `Spec`	—	`instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier` `Scheme.compactSpace_of_isAffine` `isAffine_Spec`
`instIsNoetherianSpecOfOfIsNoetherianRing` 📖	mathematical	—	`IsNoetherian` `Spec` `CommRingCat.of`	—	`instIsNoetherianSpecOfIsNoetherianRingCarrier`
`instLocallyOfFinitePresentationOfIsLocallyNoetherianOfLocallyOfFiniteType` 📖	mathematical	—	`LocallyOfFinitePresentation`	—	`IsLocallyNoetherian.component_noetherian` `Algebra.FinitePresentation.of_finiteType` `Scheme.Hom.finiteType_appLE`
`instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier` 📖	mathematical	—	`TopologicalSpace.NoetherianSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`PrimeSpectrum.instNoetherianSpace`
`instQuasiCompactOfIsLocallyNoetherianOfIsOpenImmersion` 📖	mathematical	—	`QuasiCompact`	—	`quasiCompact_iff_forall_isAffineOpen` `TopologicalSpace.Opens.map_coe` `Set.preimage_inter_range` `Topology.IsInducing.isCompact_preimage'` `Topology.IsOpenEmbedding.isInducing` `Scheme.Hom.isOpenEmbedding` `TopologicalSpace.noetherianSpace_set_iff` `noetherianSpace_of_isAffineOpen` `IsLocallyNoetherian.component_noetherian` `Set.inter_subset_left` `Set.inter_subset_right`
`isLocallyNoetherian_Spec` 📖	mathematical	—	`IsLocallyNoetherian` `Spec` `IsNoetherianRing` `CommRingCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`isAffineOpen_top` `isAffine_Spec` `IsLocallyNoetherian.component_noetherian` `isNoetherianRing_of_ringEquiv` `instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier`
`isLocallyNoetherian_iff_of_affine_openCover` 📖	mathematical	`IsAffine` `CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion`	`IsLocallyNoetherian` `IsNoetherianRing` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`Scheme.instIsOpenImmersionF` `isAffineOpen_opensRange` `IsLocallyNoetherian.component_noetherian` `isNoetherianRing_of_ringEquiv` `isLocallyNoetherian_of_affine_cover` `Scheme.OpenCover.iSup_opensRange`
`isLocallyNoetherian_iff_of_iSup_eq_top` 📖	mathematical	`iSup` `Scheme.Opens` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `Scheme.affineOpens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`IsLocallyNoetherian` `IsNoetherianRing` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`IsLocallyNoetherian.component_noetherian` `isLocallyNoetherian_of_affine_cover`
`isLocallyNoetherian_iff_openCover` 📖	mathematical	—	`IsLocallyNoetherian` `CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion`	—	`instIsLocallyNoetherianXScheme` `isLocallyNoetherian_iff_of_affine_openCover` `Scheme.isAffine_affineOpenCover` `isNoetherianRing_of_ringEquiv` `Scheme.instIsOpenImmersionF` `IsLocallyNoetherian.component_noetherian` `isAffineOpen_opensRange` `Scheme.isAffine_affineCover`
`isLocallyNoetherian_of_affine_cover` 📖	mathematical	`iSup` `Scheme.Opens` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `Scheme.affineOpens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsNoetherianRing` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	`IsLocallyNoetherian`	—	`of_affine_open_cover` `IsAffineOpen.isLocalization_basicOpen` `Subtype.prop` `IsLocalization.isNoetherianRing` `isNoetherianRing_of_away` `Localization.isLocalization` `isNoetherianRing_of_ringEquiv`
`isLocallyNoetherian_of_isOpenImmersion` 📖	mathematical	—	`IsLocallyNoetherian`	—	`IsLocallyNoetherian.component_noetherian` `IsAffineOpen.image_of_isOpenImmersion` `isNoetherianRing_of_surjective` `RingEquiv.surjective`
`isNoetherianRing_of_away` 📖	—	`Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsNoetherianRing` `Localization.Away` `CommRing.toCommMonoid` `SetLike.instMembership` `OreLocalization.instSemiring` `Ring.toSemiring` `CommRing.toRing` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm`	—	—	`monotone_stabilizes_iff_noetherian` `Nat.sInf_mem` `Ideal.map_mono` `OrderHom.monotone` `Finset.le_sup` `Subtype.prop` `RingHom.instRingHomClass` `IsLocalization.ideal_eq_iInf_comap_map_away` `iInf_subtype'` `iInf_congr`
`isNoetherian_Spec` 📖	mathematical	—	`IsNoetherian` `Spec` `IsNoetherianRing` `CommRingCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`Scheme.compactSpace_of_isAffine` `isAffine_Spec`
`isNoetherian_iff` 📖	mathematical	—	`IsNoetherian` `IsLocallyNoetherian` `CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	—
`isNoetherian_iff_of_finite_affine_openCover` 📖	mathematical	`IsAffine` `CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion`	`IsNoetherian` `IsNoetherianRing` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`isLocallyNoetherian_iff_of_affine_openCover` `IsNoetherian.toIsLocallyNoetherian` `Scheme.OpenCover.compactSpace` `Scheme.compactSpace_of_isAffine`
`isNoetherian_iff_of_finite_iSup_eq_top` 📖	mathematical	`iSup` `Scheme.Opens` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `Scheme.affineOpens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`IsNoetherian` `IsNoetherianRing` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`isLocallyNoetherian_iff_of_iSup_eq_top` `IsNoetherian.toIsLocallyNoetherian` `isLocallyNoetherian_of_affine_cover` `TopologicalSpace.Opens.coe_top` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `isCompact_iUnion` `isCompact_iff_isCompact_univ` `CompactSpace.isCompact_univ` `noetherianSpace_of_isAffineOpen` `TopologicalSpace.NoetherianSpace.compactSpace`
`noetherianSpace_of_isAffine` 📖	mathematical	—	`TopologicalSpace.NoetherianSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`TopologicalSpace.noetherianSpace_iff_of_homeomorph` `CategoryTheory.Iso.isIso_inv` `instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier`
`noetherianSpace_of_isAffineOpen` 📖	mathematical	—	`TopologicalSpace.NoetherianSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens.toScheme` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`isNoetherianRing_of_ringEquiv` `noetherianSpace_of_isAffine`
`quasiCompact_of_noetherianSpace_source` 📖	mathematical	—	`QuasiCompact`	—	`TopologicalSpace.NoetherianSpace.isCompact`

AlgebraicGeometry.IsLocallyNoetherian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`component_noetherian` 📖	mathematical	—	`IsNoetherianRing` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `Set` `Set.instMembership` `AlgebraicGeometry.Scheme.affineOpens` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	—
`quasiSeparatedSpace` 📖	mathematical	—	`QuasiSeparatedSpace` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens` `Topology.IsOpenEmbedding.isInducing` `AlgebraicGeometry.Scheme.Hom.isOpenEmbedding` `AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec` `Topology.IsInducing.isCompact_preimage_iff` `AlgebraicGeometry.IsAffineOpen.range_fromSpec` `Set.inter_subset_left` `Set.preimage_inter_range` `Set.inter_comm` `Topology.IsInducing.isCompact_preimage'` `TopologicalSpace.noetherianSpace_set_iff` `AlgebraicGeometry.noetherianSpace_of_isAffineOpen` `component_noetherian`

AlgebraicGeometry.IsNoetherian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`noetherianSpace` 📖	mathematical	—	`TopologicalSpace.NoetherianSpace` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`TopologicalSpace.noetherian_univ_iff` `toCompactSpace` `AlgebraicGeometry.Scheme.Cover.iUnion_range` `AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X` `AlgebraicGeometry.Scheme.isAffine_affineCover` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.isAffineOpen_opensRange` `AlgebraicGeometry.noetherianSpace_of_isAffineOpen` `AlgebraicGeometry.IsLocallyNoetherian.component_noetherian` `toIsLocallyNoetherian` `TopologicalSpace.NoetherianSpace.iUnion` `Finite.of_fintype`
`toCompactSpace` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	—
`toIsLocallyNoetherian` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyNoetherian`	—	—

AlgebraicGeometry.LocallyOfFinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_locallyOfFiniteType` 📖	mathematical	—	`AlgebraicGeometry.LocallyOfFinitePresentation` `AlgebraicGeometry.LocallyOfFiniteType`	—	`AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.instLocallyOfFinitePresentationOfIsLocallyNoetherianOfLocallyOfFiniteType`

AlgebraicGeometry.LocallyOfFiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocallyNoetherian` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyNoetherian`	—	`AlgebraicGeometry.Spec.map_surjective` `AlgebraicGeometry.HasRingHomProperty.Spec_iff` `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType` `Algebra.FiniteType.isNoetherianRing` `Algebra.FiniteType.of_finitePresentation` `Algebra.FinitePresentation.self` `AlgebraicGeometry.isLocallyNoetherian_iff_openCover` `AlgebraicGeometry.locallyOfFiniteType_comp` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.Scheme.local_affine` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme` `AlgebraicGeometry.instIsLocallyNoetherianXScheme`

---

← Back to Index