Documentation Verification Report

Artinian

📁 Source: Mathlib/AlgebraicGeometry/Artinian.lean

Statistics

Metric	Count
Definitions `IsArtinianScheme`, `IsLocallyArtinian`	2
Theorems `finite`, `iff_isNoetherian_and_discreteTopology`, `isNoetherianScheme`, `toCompactSpace`, `toIsLocallyArtinian`, `discreteTopology`, `discreteTopology_of_isAffine`, `iff_isLocallyNoetherian_and_discreteTopology`, `isArtinianRing_of_isAffine`, `isArtinianRing_presheaf_obj`, `isLocallyNoetherian`, `of_isImmersion`, `of_isLocallyNoetherian_of_discreteTopology`, `of_topologicalKrullDim_le_zero`, `isArtinianScheme_Spec`, `isLocallyArtinianScheme_Spec`, `instIsArtinianSchemeOfSubsingletonCarrierCarrierCommRingCatOfIsReduced`, `instIsArtinianSchemeSpecOfIsArtinianRingCarrier`, `instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced`, `instIsLocallyArtinianOfIsEmptyCarrierCarrierCommRingCat`, `instIsLocallyArtinianToScheme`, `instIsLocallyArtinianXScheme`, `isArtinianScheme_iff`, `isLocallyArtinian_iff_of_isOpenCover`, `isLocallyArtinian_iff_openCover`	25
Total	27

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsArtinianScheme` 📖	CompData	6 math math: `instIsArtinianSchemeSpecOfIsArtinianRingCarrier`, `instIsArtinianSchemeFiberOfLocallyQuasiFiniteOfQuasiCompact`, `instIsArtinianSchemeOfSubsingletonCarrierCarrierCommRingCatOfIsReduced`, `isArtinianScheme_iff`, `IsArtinianScheme.iff_isNoetherian_and_discreteTopology`, `Scheme.isArtinianScheme_Spec`
`IsLocallyArtinian` 📖	CompData	15 math math: `instIsLocallyArtinianXScheme`, `instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced`, `isLocallyArtinian_iff_of_isOpenCover`, `instIsLocallyArtinianOfIsEmptyCarrierCarrierCommRingCat`, `IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology`, `IsLocallyArtinian.of_isImmersion`, `isArtinianScheme_iff`, `IsLocallyArtinian.of_topologicalKrullDim_le_zero`, `instIsLocallyArtinianFiberOfLocallyQuasiFinite`, `IsLocallyArtinian.of_locallyQuasiFinite`, `IsLocallyArtinian.of_isLocallyNoetherian_of_discreteTopology`, `isLocallyArtinian_iff_openCover`, `instIsLocallyArtinianToScheme`, `IsArtinianScheme.toIsLocallyArtinian`, `Scheme.isLocallyArtinianScheme_Spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsArtinianSchemeOfSubsingletonCarrierCarrierCommRingCatOfIsReduced` 📖	mathematical	—	`IsArtinianScheme`	—	`instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced` `Subsingleton.discreteTopology` `Scheme.compactSpace_of_isAffine` `instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat` `Finite.of_subsingleton`
`instIsArtinianSchemeSpecOfIsArtinianRingCarrier` 📖	mathematical	—	`IsArtinianScheme` `Spec`	—	`IsArtinianScheme.iff_isNoetherian_and_discreteTopology` `instIsNoetherianSpecOfIsNoetherianRingCarrier` `instIsNoetherianRingOfIsArtinianRing` `PrimeSpectrum.instDiscreteTopology`
`instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced` 📖	mathematical	—	`IsLocallyArtinian`	—	`isEmpty_or_nonempty` `instIsLocallyArtinianOfIsEmptyCarrierCarrierCommRingCat` `isIntegral_iff_irreducibleSpace_and_isReduced` `instPreirreducibleSpaceOfSubsingleton` `isField_of_isIntegral_of_subsingleton` `Scheme.isLocallyArtinianScheme_Spec` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `FiniteDimensional.finiteDimensional_self` `IsLocallyArtinian.of_isImmersion` `instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat` `Finite.of_subsingleton` `IsImmersion.instOfIsClosedImmersion` `IsClosedImmersion.instOfIsIsoScheme` `CategoryTheory.Iso.isIso_hom` `isOpen_discrete` `TopologicalSpace.Opens.ext` `Set.ext` `isOpen_iUnion` `Topology.IsEmbedding.discreteTopology` `Topology.IsOpenEmbedding.toIsEmbedding` `Scheme.Hom.isOpenEmbedding` `Scheme.instIsOpenImmersionF` `isReduced_of_isOpenImmersion` `isLocallyArtinian_iff_openCover` `Unique.instSubsingleton`
`instIsLocallyArtinianOfIsEmptyCarrierCarrierCommRingCat` 📖	mathematical	—	`IsLocallyArtinian`	—	`instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleRingOfSubsingleton` `instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty` `Module.Finite.self`
`instIsLocallyArtinianToScheme` 📖	mathematical	—	`IsLocallyArtinian` `Scheme.Opens.toScheme`	—	`Scheme.Opens.instIsOpenImmersionι`
`instIsLocallyArtinianXScheme` 📖	mathematical	—	`IsLocallyArtinian` `CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion`	—	`Scheme.instIsOpenImmersionF`
`isArtinianScheme_iff` 📖	mathematical	—	`IsArtinianScheme` `IsLocallyArtinian` `CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	—
`isLocallyArtinian_iff_of_isOpenCover` 📖	mathematical	`TopologicalSpace.IsOpenCover` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsAffineOpen`	`IsLocallyArtinian` `IsArtinianRing` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`IsLocallyArtinian.isArtinianRing_presheaf_obj` `isLocallyArtinian_iff_openCover` `IsLocallyArtinian.of_isImmersion` `IsImmersion.instOfIsClosedImmersion` `IsClosedImmersion.instOfIsIsoScheme` `CategoryTheory.Iso.isIso_hom`
`isLocallyArtinian_iff_openCover` 📖	mathematical	—	`IsLocallyArtinian` `CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion`	—	`instIsLocallyArtinianXScheme` `IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology` `isLocallyNoetherian_iff_openCover` `IsLocallyArtinian.isLocallyNoetherian` `discreteTopology_iff_isOpen_singleton` `Scheme.Cover.exists_eq` `Scheme.instJointlySurjectivePrecoverage` `Set.image_congr` `Set.image_singleton` `Topology.IsOpenEmbedding.isOpenMap` `Scheme.Hom.isOpenEmbedding` `Scheme.instIsOpenImmersionF` `isOpen_discrete` `IsLocallyArtinian.discreteTopology`

AlgebraicGeometry.IsArtinianScheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace`	—	`finite_of_compact_of_discrete` `toCompactSpace` `AlgebraicGeometry.IsLocallyArtinian.discreteTopology` `toIsLocallyArtinian`
`iff_isNoetherian_and_discreteTopology` 📖	mathematical	—	`AlgebraicGeometry.IsArtinianScheme` `AlgebraicGeometry.IsNoetherian` `DiscreteTopology` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	—
`isNoetherianScheme` 📖	mathematical	—	`AlgebraicGeometry.IsNoetherian`	—	`AlgebraicGeometry.IsLocallyArtinian.isLocallyNoetherian` `toIsLocallyArtinian` `toCompactSpace`
`toCompactSpace` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	—
`toIsLocallyArtinian` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyArtinian`	—	—

AlgebraicGeometry.IsLocallyArtinian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discreteTopology` 📖	mathematical	—	`DiscreteTopology` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`discreteTopology_iff_isOpen_singleton` `AlgebraicGeometry.exists_isAffineOpen_mem_and_subset` `TopologicalSpace.Opens.mem_top` `isArtinianRing_presheaf_obj` `PrimeSpectrum.instDiscreteTopology` `Homeomorph.discreteTopology` `CategoryTheory.Iso.isIso_hom` `Set.image_singleton` `IsOpen.trans` `isOpen_discrete` `TopologicalSpace.Opens.is_open'`
`discreteTopology_of_isAffine` 📖	mathematical	—	`DiscreteTopology` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`discreteTopology`
`iff_isLocallyNoetherian_and_discreteTopology` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyArtinian` `AlgebraicGeometry.IsLocallyNoetherian` `DiscreteTopology` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`isLocallyNoetherian` `discreteTopology` `of_isLocallyNoetherian_of_discreteTopology`
`isArtinianRing_of_isAffine` 📖	mathematical	—	`IsArtinianRing` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`isArtinianRing_presheaf_obj` `AlgebraicGeometry.isAffineOpen_top`
`isArtinianRing_presheaf_obj` 📖	mathematical	—	`IsArtinianRing` `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`	—	—
`isLocallyNoetherian` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyNoetherian`	—	`instIsNoetherianRingOfIsArtinianRing` `isArtinianRing_presheaf_obj`
`of_isImmersion` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyArtinian`	—	`iff_isLocallyNoetherian_and_discreteTopology` `AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian` `AlgebraicGeometry.IsImmersion.instLocallyOfFiniteType` `isLocallyNoetherian` `Topology.IsEmbedding.discreteTopology` `discreteTopology` `AlgebraicGeometry.Scheme.Hom.isEmbedding` `AlgebraicGeometry.IsImmersion.toIsPreimmersion`
`of_isLocallyNoetherian_of_discreteTopology` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyArtinian`	—	`of_topologicalKrullDim_le_zero` `topologicalKrullDim_zero_of_discreteTopology`
`of_topologicalKrullDim_le_zero` 📖	mathematical	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `topologicalKrullDim` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `WithBot.zero` `instZeroENat`	`AlgebraicGeometry.IsLocallyArtinian`	—	`AlgebraicGeometry.IsLocallyNoetherian.component_noetherian` `isArtinianRing_iff_krullDimLE_zero` `Ring.KrullDimLE.eq_1` `Order.krullDimLE_iff` `ringKrullDim.eq_1` `Nat.cast_zero` `PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim` `IsHomeomorph.topologicalKrullDim_eq` `CategoryTheory.Iso.isIso_hom` `Homeomorph.isHomeomorph` `LE.le.trans` `topologicalKrullDim_subspace_le`

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isArtinianScheme_Spec` 📖	mathematical	—	`AlgebraicGeometry.IsArtinianScheme` `AlgebraicGeometry.Spec` `IsArtinianRing` `CommRingCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`compactSpace_of_isAffine` `AlgebraicGeometry.isAffine_Spec`
`isLocallyArtinianScheme_Spec` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyArtinian` `AlgebraicGeometry.Spec` `IsArtinianRing` `CommRingCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`RingEquiv.isArtinianRing` `AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine` `AlgebraicGeometry.isAffine_Spec` `AlgebraicGeometry.IsLocallyArtinian.of_topologicalKrullDim_le_zero` `AlgebraicGeometry.instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier` `instIsNoetherianRingOfIsArtinianRing` `topologicalKrullDim_zero_of_discreteTopology` `PrimeSpectrum.instDiscreteTopology`

---

← Back to Index