Properties

📁 Source: Mathlib/AlgebraicGeometry/Properties.lean

Statistics

Metric	Count
Definitions IsReduced, instOrderTopCarrierCarrierCommRingCatOfIsIntegral	2
Theorems component_integral, nonempty, of_isIso, component_reduced, of_openCover, component_nontrivial, affine_isIntegral_iff, affine_isReduced_iff, basicOpen_eq_bot_iff, eq_zero_of_basicOpen_eq_bot, instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, instIsIntegralSpecOfIsDomainCarrier, instIsReducedSpecOfIsReducedCarrier, instIsReducedToScheme, instPrespectralSpaceCarrierCarrierCommRingCat, instQuasiSoberCarrierCarrierCommRingCat, instT0SpaceCarrierCarrierCommRingCat, irreducibleSpace_of_isIntegral, isField_of_isIntegral_of_subsingleton, isField_stalk_of_closure_mem_irreducibleComponents, isIntegral_iff_irreducibleSpace_and_isReduced, isIntegral_of_irreducibleSpace_of_isReduced, isIntegral_of_isAffine_of_isDomain, isIntegral_of_isOpenImmersion, isReduced_of_isAffine_isReduced, isReduced_of_isIntegral, isReduced_of_isOpenImmersion, isReduced_of_isReduced_stalk, isReduced_stalk_of_isReduced, map_injective_of_isIntegral, reduce_to_affine_global, reduce_to_affine_nbhd	34
Total	36

AlgebraicGeometry

Definitions

Name	Category	Theorems
IsReduced 📖	CompData	20 math math: instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian, IsSchemeTheoreticallyDominant.isReduced, GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents, instIsReducedFiberOfGeometricallyReduced, instIsReducedSpecOfIsReducedCarrier, geometricallyReduced_iff, GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian, isReduced_of_isIntegral, Scheme.PartialMap.instIsReducedToScheme, isIntegral_iff_irreducibleSpace_and_isReduced, instIsReducedToScheme, isReduced_of_isOpenImmersion, GeometricallyReduced.geometrically_isReduced, isReduced_of_isReduced_stalk, isReduced_of_isAffine_isReduced, instIsReducedToScheme_1, Scheme.Hom.instIsReducedNormalization, instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1, GeometricallyReduced.eq_geometrically, affine_isReduced_iff
instOrderTopCarrierCarrierCommRingCatOfIsIntegral 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affine_isIntegral_iff 📖	mathematical	—	IsIntegral Spec IsDomain CommRingCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing	—	MulEquiv.isDomain instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral instIsIntegralSpecOfIsDomainCarrier
affine_isReduced_iff 📖	mathematical	—	IsReduced Spec IsReduced CommRingCat.carrier MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	isReduced_of_injective RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingEquiv.injective IsReduced.component_reduced instIsReducedSpecOfIsReducedCarrier
basicOpen_eq_bot_iff 📖	mathematical	—	Scheme.basicOpen Bot.bot Scheme.Opens OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier HeytingAlgebra.toOrderBot CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing	—	eq_zero_of_basicOpen_eq_bot Scheme.basicOpen_zero
eq_zero_of_basicOpen_eq_bot 📖	mathematical	Scheme.basicOpen Bot.bot Scheme.Opens OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier HeytingAlgebra.toOrderBot	CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing	—	TopCat.Presheaf.section_ext CommRingCat.Colimits.hasColimits_commRingCat CommRingCat.FilteredColimits.forget_preservesFilteredColimits CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass reduce_to_affine_global TopCat.Presheaf.germ_res_apply Scheme.basicOpen_res inf_bot_eq Scheme.Hom.preimage_opensRange isReduced_of_isOpenImmersion Scheme.preimage_basicOpen TopologicalSpace.Opens.ext TopologicalSpace.Opens.is_open' IsOpenImmersion.instIsIsoCommRingCatStalkMap CategoryTheory.IsIso.hom_inv_id CommRingCat.comp_apply Scheme.Hom.germ_stalkMap_apply IsNilpotent.eq_zero IsReduced.component_reduced IsNilpotent.map PrimeSpectrum.basicOpen_eq_bot_iff basicOpen_eq_of_affine' CommRingCat.id_apply CategoryTheory.Iso.hom_inv_id
instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier 📖	mathematical	—	IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec SheafedSpace.instTopologicalSpaceCarrierCarrier	—	PrimeSpectrum.irreducibleSpace
instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms Scheme Scheme.instCategory IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	—	Homeomorph.irreducibleSpace_iff CategoryTheory.Iso.isIso_hom
instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral 📖	mathematical	—	IsDomain 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	—	IsIntegral.component_integral IsIntegral.nonempty
instIsIntegralSpecOfIsDomainCarrier 📖	mathematical	—	IsIntegral Spec	—	isIntegral_of_irreducibleSpace_of_isReduced instIsReducedSpecOfIsReducedCarrier isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier
instIsReducedSpecOfIsReducedCarrier 📖	mathematical	—	IsReduced Spec	—	isReduced_of_isReduced_stalk CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime instIsReducedLocalization isReduced_of_injective RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingEquiv.injective
instIsReducedToScheme 📖	mathematical	—	IsReduced Scheme.Opens.toScheme	—	isReduced_of_isOpenImmersion Scheme.Opens.instIsOpenImmersionι
instPrespectralSpaceCarrierCarrierCommRingCat 📖	mathematical	—	PrespectralSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	—	PrespectralSpace.of_isClosedEmbedding PrimeSpectrum.instPrespectralSpace CategoryTheory.Iso.isIso_hom Homeomorph.isClosedEmbedding Scheme.instIsOpenImmersionF isAffineOpen_opensRange Scheme.isAffine_affineCover PrespectralSpace.of_isOpenCover Scheme.OpenCover.isOpenCover_opensRange
instQuasiSoberCarrierCarrierCommRingCat 📖	mathematical	—	QuasiSober TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	—	quasiSober_of_open_cover Topology.IsOpenEmbedding.isOpen_range Scheme.Hom.isOpenEmbedding Scheme.instIsOpenImmersionF Topology.IsOpenEmbedding.quasiSober Topology.IsOpenEmbedding.isEmbedding Homeomorph.isOpenEmbedding PrimeSpectrum.quasiSober Scheme.local_affine Set.top_eq_univ Set.sUnion_range Set.eq_univ_iff_forall Scheme.instJointlySurjectivePrecoverage Scheme.Cover.covers
instT0SpaceCarrierCarrierCommRingCat 📖	mathematical	—	T0Space TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	—	T0Space.of_open_cover Scheme.instJointlySurjectivePrecoverage Scheme.Cover.covers TopologicalSpace.Opens.is_open' Scheme.instIsOpenImmersionF Topology.IsEmbedding.t0Space PrimeSpectrum.instT0Space isAffineOpen_opensRange Scheme.isAffine_affineCover Homeomorph.isEmbedding
irreducibleSpace_of_isIntegral 📖	mathematical	—	IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	—	IsIntegral.nonempty IsClosed.isOpen_compl le_sup_left le_sup_right TopologicalSpace.Opens.ext Set.ext instIsEmptyFalse MulEquiv.isDomain IsIntegral.component_integral Set.not_top_subset false_of_nontrivial_of_product_domain Scheme.component_nontrivial
isField_of_isIntegral_of_subsingleton 📖	mathematical	—	IsField 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	—	PrimeSpectrum.t1Space_iff_isField instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral Homeomorph.t1Space T2Space.t1Space DiscreteTopology.toT2Space Subsingleton.discreteTopology instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat Finite.of_subsingleton CategoryTheory.Iso.isIso_hom
isField_stalk_of_closure_mem_irreducibleComponents 📖	mathematical	Set TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Set.instMembership irreducibleComponents SheafedSpace.instTopologicalSpaceCarrierCarrier closure Set.instSingletonSet	IsField CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.vanishingIdeal_singleton PrimeSpectrum.vanishingIdeal_mem_minimalPrimes PrimeSpectrum.subsingleton_iff_isField_of_isReduced isReduced_stalk_of_isReduced IsLocalRing.toNontrivial LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes StructureSheaf.IsLocalization.to_stalk Scheme.Cover.exists_eq Scheme.instJointlySurjectivePrecoverage isReduced_of_isOpenImmersion Scheme.instIsOpenImmersionF MulEquiv.isField Topology.IsEmbedding.closure_eq_preimage_closure_image Topology.IsOpenEmbedding.toIsEmbedding Scheme.Hom.isOpenEmbedding Set.image_singleton preimage_mem_irreducibleComponents subset_closure Scheme.local_affine IsOpenImmersion.instIsIsoCommRingCatStalkMap
isIntegral_iff_irreducibleSpace_and_isReduced 📖	mathematical	—	IsIntegral IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier IsReduced	—	irreducibleSpace_of_isIntegral isReduced_of_isIntegral isIntegral_of_irreducibleSpace_of_isReduced
isIntegral_of_irreducibleSpace_of_isReduced 📖	mathematical	—	IsIntegral	—	ConnectedSpace.toNonempty IrreducibleSpace.connectedSpace nonempty_preirreducible_inter IrreducibleSpace.toPreirreducibleSpace TopologicalSpace.Opens.is_open' CommRingCat.Colimits.hasColimits_commRingCat zero_ne_one' NeZero.one IsLocalRing.toNontrivial LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf isUnit_zero_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass IsUnit.mul NoZeroDivisors.to_isDomain Scheme.component_nontrivial
isIntegral_of_isAffine_of_isDomain 📖	mathematical	—	IsIntegral	—	isIntegral_of_isOpenImmersion IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom instIsIntegralSpecOfIsDomainCarrier
isIntegral_of_isOpenImmersion 📖	mathematical	—	IsIntegral	—	Scheme.Hom.preimage_image_eq IsIntegral.component_integral Subtype.prop MulEquiv.isDomain Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor
isReduced_of_isAffine_isReduced 📖	mathematical	—	IsReduced	—	isReduced_of_isOpenImmersion IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom instIsReducedSpecOfIsReducedCarrier
isReduced_of_isIntegral 📖	mathematical	—	IsReduced	—	Set.eq_empty_or_nonempty SetLike.ext' isReduced_of_noZeroDivisors IsRightCancelMulZero.to_noZeroDivisors IsCancelMulZero.toIsRightCancelMulZero Subsingleton.to_isCancelMulZero CommRingCat.subsingleton_of_isTerminal IsDomain.to_noZeroDivisors IsIntegral.component_integral
isReduced_of_isOpenImmersion 📖	mathematical	—	IsReduced	—	Scheme.Hom.preimage_image_eq isReduced_of_injective RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor RingEquiv.injective IsReduced.component_reduced
isReduced_of_isReduced_stalk 📖	mathematical	IsReduced CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	IsReduced	—	CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.section_ext CommRingCat.FilteredColimits.forget_preservesFilteredColimits CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsNilpotent.eq_zero IsNilpotent.map
isReduced_stalk_of_isReduced 📖	mathematical	—	IsReduced CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ_exist CommRingCat.FilteredColimits.forget_preservesFilteredColimits TopCat.Presheaf.germ_eq map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass IsNilpotent.eq_zero IsReduced.component_reduced TopCat.Presheaf.germ_res CommRingCat.comp_apply
map_injective_of_isIntegral 📖	mathematical	—	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 DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SheafedSpace.instTopologicalSpaceCarrierCarrier	—	injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass basicOpen_eq_bot_iff isReduced_of_isIntegral Mathlib.Tactic.Contrapose.contrapose₁ nonempty_preirreducible_inter IrreducibleSpace.toPreirreducibleSpace irreducibleSpace_of_isIntegral TopologicalSpace.Opens.isOpen Scheme.basicOpen_res
reduce_to_affine_global 📖	—	Top.top Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Scheme.Hom.opensRange Spec	—	—	TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open Scheme.affineBasisCover_is_basis SetLike.mem_coe Subtype.prop TopologicalSpace.Opens.isOpen Topology.IsOpenEmbedding.isOpen_range Scheme.Hom.isOpenEmbedding Scheme.instIsOpenImmersionF Scheme.local_affine
reduce_to_affine_nbhd 📖	—	Spec DFunLike.coe PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	—	—	Scheme.instJointlySurjectivePrecoverage Scheme.Cover.covers Scheme.instIsOpenImmersionF Scheme.local_affine

AlgebraicGeometry.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
component_integral 📖	mathematical	—	IsDomain 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 CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing	—	—
nonempty 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace	—	—
of_isIso 📖	mathematical	—	AlgebraicGeometry.IsIntegral	—	Nonempty.map nonempty AlgebraicGeometry.isIntegral_of_isOpenImmersion AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.inv_isIso

AlgebraicGeometry.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
component_reduced 📖	mathematical	—	IsReduced 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
of_openCover 📖	—	AlgebraicGeometry.IsReduced CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion	—	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Scheme.Cover.exists_eq AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage isReduced_of_injective RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap AlgebraicGeometry.Scheme.instIsOpenImmersionF RingEquiv.injective AlgebraicGeometry.isReduced_stalk_of_isReduced AlgebraicGeometry.isReduced_of_isReduced_stalk

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
component_nontrivial 📖	mathematical	—	Nontrivial CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens	—	AlgebraicGeometry.LocallyRingedSpace.component_nontrivial

---

← Back to Index