Documentation Verification Report

Noetherian

πŸ“ Source: Mathlib/AlgebraicGeometry/Noetherian.lean

Statistics

MetricCount
DefinitionsIsLocallyNoetherian, IsNoetherian
2
Theoremscomponent_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
Total35

AlgebraicGeometry

Definitions

NameCategoryTheorems
IsLocallyNoetherian πŸ“–CompData
16 mathmath: 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 mathmath: 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

NameKindAssumesProvesValidatesDepends 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 πŸ“–mathematicalIsAffine
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 πŸ“–mathematicaliSup
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 πŸ“–mathematicaliSup
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 πŸ“–mathematicalIsAffine
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 πŸ“–mathematicaliSup
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

NameKindAssumesProvesValidatesDepends 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

NameKindAssumesProvesValidatesDepends 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

NameKindAssumesProvesValidatesDepends On
iff_locallyOfFiniteType πŸ“–mathematicalβ€”AlgebraicGeometry.LocallyOfFinitePresentation
AlgebraicGeometry.LocallyOfFiniteType
β€”AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation
AlgebraicGeometry.instLocallyOfFinitePresentationOfIsLocallyNoetherianOfLocallyOfFiniteType

AlgebraicGeometry.LocallyOfFiniteType

Theorems

NameKindAssumesProvesValidatesDepends 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