QuasiCompact

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

Statistics

Metric	Count
Definitions	0
Theorems `compactSpace_of_compactSpace`, `isCompact_preimage`, `isCompact_preimage`, `isSpectralMap`, `isNilpotent_iff_basicOpen_eq_bot`, `isNilpotent_iff_basicOpen_eq_bot_of_isCompact`, `zeroLocus_eq_univ_iff_subset_nilradical`, `zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact`, `compactSpace_iff_exists`, `compactSpace_iff_quasiCompact`, `compact_open_induction_on`, `exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen`, `exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact`, `instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact`, `instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1`, `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat`, `instIsMultiplicativeSchemeQuasiCompact`, `instQuasiCompactFstScheme`, `instQuasiCompactMorphismRestrict`, `instQuasiCompactSndScheme`, `instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat`, `isClosedMap_iff_specializingMap`, `isCompactOpen_iff_eq_basicOpen_union`, `isCompactOpen_iff_eq_finset_affine_union`, `isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens`, `isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen`, `isCompact_basicOpen`, `isCompact_iff_exists`, `isCompact_iff_finite_and_eq_biUnion_affineOpens`, `quasiCompact_comp`, `quasiCompact_iff`, `quasiCompact_iff_forall_affine`, `quasiCompact_iff_forall_isAffineOpen`, `quasiCompact_iff_isSpectralMap`, `quasiCompact_iff_spectral`, `quasiCompact_isStableUnderBaseChange`, `quasiCompact_isStableUnderComposition`, `quasiCompact_of_isIso`	38
Total	38

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_iff_exists` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Spec` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `instIsAffineSigmaObjScheme` `Finite.of_fintype` `instIsAffineXSchemeFiniteSubcover` `Scheme.isAffine_affineCover` `Scheme.instJointlySurjectivePrecoverage` `Scheme.Cover.covers` `Scheme.Hom.comp_apply` `CategoryTheory.Limits.Sigma.ι_desc` `Scheme.Hom.surjective` `instSurjectiveOfIsIsoScheme` `CategoryTheory.Iso.isIso_inv` `isCompact_range` `Scheme.compactSpace_of_isAffine` `isAffine_Spec` `Scheme.Hom.continuous` `Function.Surjective.range_eq`
`compactSpace_iff_quasiCompact` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `QuasiCompact` `CategoryTheory.Limits.terminal` `Scheme` `Scheme.instCategory` `instHasTerminalScheme` `CategoryTheory.Limits.terminal.from`	—	`instHasTerminalScheme` `HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `instIsAffineTerminalScheme`
`compact_open_induction_on` 📖	—	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame` `HeytingAlgebra.toOrderBot` `SemilatticeSup.toMax` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `Set` `Set.instMembership` `Scheme.affineOpens`	—	—	`isCompact_iff_finite_and_eq_biUnion_affineOpens` `Set.Finite.induction_on` `iSup_congr_Prop` `iSup_neg` `iSup_bot` `iSup_insert` `sup_comm` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `Set.iUnion_congr_Prop` `Set.iUnion_coe_set`
`exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen` 📖	mathematical	`TopCat.Presheaf.restrictOpen` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `PresheafedSpace.presheaf` `Scheme.basicOpen` `CategoryTheory.ToType` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Scheme.Opens` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsLocalization.Away.exists_of_eq` `IsAffineOpen.isLocalization_basicOpen` `Scheme.basicOpen_le` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.mul_zero`
`exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact` 📖	mathematical	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.carrier` `TopCat.Presheaf.restrictOpen` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `PresheafedSpace.presheaf` `Scheme.basicOpen` `CategoryTheory.ToType` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Scheme.Opens` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens` `TopologicalSpace.Opens.is_open'` `TopologicalSpace.Opens.ext` `isOpen_iUnion` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `le_iSup` `exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen` `Scheme.basicOpen_res` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `nonempty_fintype` `Set.Finite.to_subtype` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Finset.le_sup` `Finset.mem_univ` `pow_add` `mul_assoc` `MulZeroClass.mul_zero` `MonoidWithZeroHomClass.toMonoidHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `TopCat.Sheaf.eq_of_locally_eq` `CommRingCat.hasLimits` `CommRingCat.forgetReflectIsos` `CommRingCat.forget_preservesLimits`
`instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`QuasiCompact.compactSpace_of_compactSpace` `Scheme.Pullback.instHasPullback` `instQuasiCompactSndScheme`
`instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`QuasiCompact.compactSpace_of_compactSpace` `Scheme.Pullback.instHasPullback` `instQuasiCompactFstScheme`
`instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` 📖	mathematical	—	`HasAffineProperty` `QuasiCompact` `CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`Homeomorph.compactSpace` `Scheme.Hom.isIso_base` `CategoryTheory.Iso.isIso_inv` `Scheme.preimage_basicOpen` `isCompact_iff_compactSpace` `isCompact_basicOpen` `isCompact_univ` `isCompact_univ_iff` `TopologicalSpace.Opens.coe_top` `Scheme.Hom.preimage_top` `IsAffineOpen.iSup_basicOpen_eq_self_iff` `isAffineOpen_top` `Scheme.Hom.preimage_iSup` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `isCompact_iUnion` `Finite.of_fintype` `CategoryTheory.MorphismProperty.ext`
`instIsMultiplicativeSchemeQuasiCompact` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `QuasiCompact`	—	`quasiCompact_of_isIso` `CategoryTheory.IsIso.id` `quasiCompact_isStableUnderComposition`
`instQuasiCompactFstScheme` 📖	mathematical	—	`QuasiCompact` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.MorphismProperty.pullback_fst` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `quasiCompact_isStableUnderBaseChange`
`instQuasiCompactMorphismRestrict` 📖	mathematical	—	`QuasiCompact` `Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `morphismRestrict`	—	`IsZariskiLocalAtTarget.restrict` `HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat`
`instQuasiCompactSndScheme` 📖	mathematical	—	`QuasiCompact` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.MorphismProperty.pullback_snd` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `quasiCompact_isStableUnderBaseChange`
`instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat` 📖	mathematical	—	`QuasiCompact` `Spec` `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` `Scheme.toSpecΓ`	—	`HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `isAffine_Spec`
`isClosedMap_iff_specializingMap` 📖	mathematical	—	`IsClosedMap` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `SpecializingMap`	—	`IsClosedMap.specializingMap` `StableUnderSpecialization.image` `IsClosed.stableUnderSpecialization` `Equiv.surjective` `PrimeSpectrum.isClosed_image_of_stableUnderSpecialization` `compactSpace_iff_exists` `QuasiCompact.compactSpace_of_compactSpace` `Scheme.compactSpace_of_isAffine` `isAffine_Spec` `HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `IsClosed.preimage` `Scheme.Hom.continuous` `Set.image_preimage_eq` `Set.image_congr` `Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `isOpenImmersion_stableUnderBaseChange` `Scheme.Pullback.instHasPullback` `IsZariskiLocalAtTarget.iff_of_openCover` `isClosedMap_isZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `quasiCompact_isStableUnderBaseChange` `IsZariskiLocalAtTarget.of_isPullback` `specializingMap_isZariskiLocalAtTarget` `Scheme.instIsOpenImmersionF` `CategoryTheory.IsPullback.of_hasPullback` `Scheme.local_affine`
`isCompactOpen_iff_eq_basicOpen_union` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsOpen` `Set.Finite` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Set.iUnion` `Set` `Set.instMembership` `SetLike.coe` `TopologicalSpace.Opens.instSetLike` `Scheme.basicOpen`	—	`isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen`
`isCompactOpen_iff_eq_finset_affine_union` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsOpen` `Set.Finite` `Set.Elem` `Scheme.Opens` `Scheme.affineOpens` `Set.iUnion` `Set` `Set.instMembership` `SetLike.coe` `TopologicalSpace.Opens.instSetLike`	—	`isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens`
`isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsOpen` `Set.Finite` `Set.Elem` `Scheme.Opens` `Scheme.affineOpens` `Set.iUnion` `Set` `Set.instMembership` `SetLike.coe` `TopologicalSpace.Opens.instSetLike`	—	`TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion` `Subtype.range_coe` `Scheme.isBasis_affineOpens` `IsAffineOpen.isCompact`
`isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsOpen` `Set.Finite` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Set.iUnion` `Set` `Set.instMembership` `SetLike.coe` `TopologicalSpace.Opens.instSetLike` `Scheme.basicOpen`	—	`TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion` `isBasis_basicOpen` `IsAffineOpen.isCompact` `IsAffineOpen.basicOpen` `isAffineOpen_top`
`isCompact_basicOpen` 📖	mathematical	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike`	`Scheme.basicOpen`	—	`isCompact_iff_finite_and_eq_biUnion_affineOpens` `LE.le.trans_eq` `le_iSup₂` `Scheme.basicOpen_res` `IsAffineOpen.basicOpen` `Set.finite_range` `Set.Finite.to_subtype` `iSup_range` `iSup_inf_eq` `iSup_subtype` `inf_eq_right` `Scheme.basicOpen_le`
`isCompact_iff_exists` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `Set.range` `Spec` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`isCompact_iff_compactSpace` `compactSpace_iff_exists` `Function.Surjective.range_comp` `Scheme.Opens.range_ι` `Scheme.Opens.instIsOpenImmersionι` `Set.instReflSubset` `Set.range_eq_univ` `Set.image_val_injective` `Set.image_congr` `Set.image_univ` `Set.range_comp` `TopCat.coe_comp` `Scheme.Hom.comp_base` `IsOpenImmersion.lift_fac`
`isCompact_iff_finite_and_eq_biUnion_affineOpens` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `Set.Finite` `Set.Elem` `Scheme.affineOpens` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `Set` `Set.instMembership`	—	`TopologicalSpace.Opens.isOpen` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `SetLike.coe_injective` `isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens`
`quasiCompact_comp` 📖	mathematical	—	`QuasiCompact` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`Scheme.Hom.comp_base` `TopCat.coe_comp` `Set.preimage_comp` `QuasiCompact.isCompact_preimage` `Continuous.isOpen_preimage` `Scheme.Hom.continuous`
`quasiCompact_iff` 📖	mathematical	—	`QuasiCompact` `IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	—
`quasiCompact_iff_forall_affine` 📖	mathematical	—	`QuasiCompact` `IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`quasiCompact_iff_forall_isAffineOpen`
`quasiCompact_iff_forall_isAffineOpen` 📖	mathematical	—	`QuasiCompact` `IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`quasiCompact_iff` `TopologicalSpace.Opens.isOpen` `IsAffineOpen.isCompact` `isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens` `Set.preimage_iUnion` `Set.Finite.isCompact_biUnion` `Subtype.prop`
`quasiCompact_iff_isSpectralMap` 📖	mathematical	—	`QuasiCompact` `IsSpectralMap` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`Scheme.Hom.continuous` `IsSpectralMap.isCompact_preimage_of_isOpen`
`quasiCompact_iff_spectral` 📖	mathematical	—	`QuasiCompact` `IsSpectralMap` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`quasiCompact_iff_isSpectralMap`
`quasiCompact_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `QuasiCompact`	—	`HasAffineProperty.isStableUnderBaseChange` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `AffineTargetMorphismProperty.IsLocal.respectsIso` `HasAffineProperty.isLocal_affineProperty` `Scheme.Pullback.instHasPullback` `Finite.of_fintype` `Scheme.instJointlySurjectivePrecoverage` `Scheme.compactSpace_of_isAffine` `Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine` `Scheme.isAffine_affineCover` `Scheme.OpenCover.compactSpace`
`quasiCompact_isStableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `QuasiCompact`	—	`quasiCompact_comp`
`quasiCompact_of_isIso` 📖	mathematical	—	`QuasiCompact`	—	`Scheme.Hom.isIso_base` `Set.image_eq_preimage_of_inverse` `CategoryTheory.IsIso.inv_hom_id_apply` `CategoryTheory.IsIso.hom_inv_id_apply` `IsCompact.image` `ContinuousMap.continuous_toFun`

AlgebraicGeometry.QuasiCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_of_compactSpace` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`Set.preimage_univ` `isCompact_preimage` `isOpen_univ` `CompactSpace.isCompact_univ`
`isCompact_preimage` 📖	mathematical	`IsOpen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsCompact`	`Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	—	—

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_iff_basicOpen_eq_bot` 📖	mathematical	—	`IsNilpotent` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `basicOpen` `Bot.bot` `OrderBot.toBot` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame` `HeytingAlgebra.toOrderBot`	—	`isNilpotent_iff_basicOpen_eq_bot_of_isCompact` `CompactSpace.isCompact_univ`
`isNilpotent_iff_basicOpen_eq_bot_of_isCompact` 📖	mathematical	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Opens` `TopologicalSpace.Opens.instSetLike`	`IsNilpotent` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `basicOpen` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame` `HeytingAlgebra.toOrderBot`	—	`AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent` `basicOpen_le` `le_refl` `bot_le` `TopCat.Presheaf.restrict_restrict` `Subsingleton.eq_zero` `instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact` `mul_one`
`zeroLocus_eq_univ_iff_subset_nilradical` 📖	mathematical	—	`zeroLocus` `Top.top` `Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Set.univ` `Set` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Set.instHasSubset` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `nilradical`	—	`zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact` `CompactSpace.isCompact_univ`
`zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact` 📖	mathematical	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Opens` `TopologicalSpace.Opens.instSetLike`	`zeroLocus` `Set.univ` `Set` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Set.instHasSubset` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `nilradical`	—	`Set.iInter_congr_Prop` `isNilpotent_iff_basicOpen_eq_bot_of_isCompact`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_preimage` 📖	mathematical	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike`	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`IsSpectralMap.isCompact_preimage_of_isOpen` `isSpectralMap` `TopologicalSpace.Opens.is_open'`
`isSpectralMap` 📖	mathematical	—	`IsSpectralMap` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`AlgebraicGeometry.quasiCompact_iff_isSpectralMap`

---

← Back to Index