QuasiSeparated

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

Statistics

Metric	Count
Definitions `QuasiSeparated`	1
Theorems `isQuasiSeparated`, `of_comp`, `diagonalQuasiCompact`, `of_comp`, `of_quasiSeparatedSpace`, `quasiCompact_diagonal`, `isQuasiSeparated_preimage`, `quasiSeparatedSpace_of_isOpenCover`, `exists_eq_pow_mul_of_isAffineOpen`, `exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated`, `exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux`, `exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux`, `exists_of_res_eq_of_qcqs`, `exists_of_res_eq_of_qcqs_of_top`, `exists_of_res_zero_of_qcqs`, `exists_of_res_zero_of_qcqs_of_top`, `instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace`, `instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat`, `instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated`, `instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty`, `instIsMultiplicativeSchemeQuasiSeparated`, `instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat`, `instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat`, `instQuasiSeparatedFstScheme`, `instQuasiSeparatedMorphismRestrict`, `instQuasiSeparatedOfMonoScheme`, `instQuasiSeparatedResLE`, `instQuasiSeparatedSndScheme`, `instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat`, `isIso_ΓSpec_adjunction_unit_app_basicOpen`, `isLocalization_basicOpen_of_qcqs`, `quasiCompact_affineProperty_iff_quasiSeparatedSpace`, `quasiCompact_iff_compactSpace`, `quasiCompact_of_compactSpace`, `quasiCompact_over_affine_iff`, `quasiSeparatedSpace_iff_affine`, `quasiSeparatedSpace_iff_forall_affineOpens`, `quasiSeparatedSpace_iff_quasiCompact_prod_lift`, `quasiSeparatedSpace_iff_quasiSeparated`, `quasiSeparatedSpace_of_isAffine`, `quasiSeparatedSpace_of_quasiSeparated`, `quasiSeparated_comp`, `quasiSeparated_eq_diagonal_is_quasiCompact`, `quasiSeparated_iff`, `quasiSeparated_iff_quasiSeparatedSpace`, `quasiSeparated_isStableUnderBaseChange`, `quasiSeparated_isStableUnderComposition`, `quasiSeparated_over_affine_iff`	48
Total	49

AlgebraicGeometry

Definitions

Name	Category	Theorems
`QuasiSeparated` 📖	CompData	24 math math: `quasiSeparated_comp`, `instQuasiSeparatedResLE`, `IsSeparated.eq_valuativeCriterion`, `instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat`, `quasiSeparated_eq_diagonal_is_quasiCompact`, `instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty`, `instIsMultiplicativeSchemeQuasiSeparated`, `QuasiSeparated.of_comp`, `instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated`, `instQuasiSeparatedSndScheme`, `instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat`, `quasiSeparated_iff_quasiSeparatedSpace`, `instQuasiSeparatedMorphismRestrict`, `IsProper.eq_valuativeCriterion`, `quasiSeparated_iff`, `Scheme.Hom.instQuasiSeparatedToNormalization`, `quasiSeparatedSpace_iff_quasiSeparated`, `instQuasiSeparatedOfMonoScheme`, `instQuasiSeparatedFstScheme`, `QuasiSeparated.of_quasiSeparatedSpace`, `IsSeparated.instQuasiSeparated`, `quasiSeparated_isStableUnderComposition`, `quasiSeparated_isStableUnderBaseChange`, `quasiSeparated_over_affine_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_pow_mul_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` `Scheme.Opens` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Submonoid.IsLocalizationMap.surj` `IsLocalization'.toIsLocalizationMap` `IsAffineOpen.isLocalization_basicOpen` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_comm`
`exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated` 📖	mathematical	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.carrier` `IsQuasiSeparated`	`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` `Scheme.Opens` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`compact_open_induction_on` `CommRingCat.subsingleton_of_isTerminal` `eq_bot_iff` `Scheme.basicOpen_le` `le_sup_left` `IsQuasiSeparated.of_subset` `Set.subset_union_left` `le_sup_right` `exists_eq_pow_mul_of_isAffineOpen` `isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens` `TopologicalSpace.Opens.is_open'` `Set.subset_union_right` `IsAffineOpen.isCompact` `nonempty_fintype` `Set.Finite.to_subtype` `TopologicalSpace.Opens.ext` `isOpen_iUnion` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `le_trans` `le_iSup` `inf_le_left` `inf_le_right` `exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux` `TopCat.Sheaf.eq_of_locally_eq'` `CommRingCat.hasLimits` `CommRingCat.forgetReflectIsos` `CommRingCat.forget_preservesLimits` `le_of_eq` `Finset.le_sup` `Finset.mem_univ` `Scheme.basicOpen_res` `TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff` `add_assoc` `add_comm` `LE.le.trans` `pow_add` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux` 📖	—	`Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instMembership` `Scheme.affineOpens` `TopCat.Presheaf.restrictOpen` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `PresheafedSpace.presheaf` `Scheme.basicOpen` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.ToType` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Opposite.op` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—	`le_trans` `le_sup_left` `le_sup_right` `IsLocalization.eq_iff_exists` `IsAffineOpen.isLocalization_basicOpen` `exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux` `Scheme.basicOpen_le` `Scheme.basicOpen_res` `inf_le_inf` `le_rfl` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LE.le.trans` `TopCat.Presheaf.restrictOpen.congr_simp` `pow_add` `mul_assoc` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux` 📖	—	`TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Presheaf.restrictOpen` `CommRingCat` `CommRingCat.instCategory` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.ToType` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Opposite.op` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	—	`LE.le.trans` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `CategoryTheory.Functor.map_comp` `mul_left_comm`
`exists_of_res_eq_of_qcqs` 📖	mathematical	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.carrier` `IsQuasiSeparated` `TopCat.Presheaf.restrictOpen` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `PresheafedSpace.presheaf` `Scheme.basicOpen`	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `Scheme.Opens` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsLocalization.Away.exists_of_eq` `isLocalization_basicOpen_of_qcqs`
`exists_of_res_eq_of_qcqs_of_top` 📖	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` `Top.top` `Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Scheme.basicOpen`	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`exists_of_res_eq_of_qcqs` `CompactSpace.isCompact_univ` `isQuasiSeparated_univ`
`exists_of_res_zero_of_qcqs` 📖	mathematical	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.carrier` `IsQuasiSeparated` `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`	—	`exists_of_res_eq_of_qcqs` `RingedSpace.res_zero` `MulZeroClass.mul_zero`
`exists_of_res_zero_of_qcqs_of_top` 📖	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` `Top.top` `Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Scheme.basicOpen` `CategoryTheory.ToType` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`exists_of_res_zero_of_qcqs` `CompactSpace.isCompact_univ` `isQuasiSeparated_univ`
`instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.equalizer` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `instHasFiniteLimitsScheme` `CategoryTheory.Limits.instFinCategoryWalkingParallelPair` `CategoryTheory.Limits.parallelPair` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `instHasFiniteLimitsScheme` `QuasiCompact.isCompact_preimage` `instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat` `isOpen_univ` `isCompact_univ`
`instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat` 📖	mathematical	—	`HasAffineProperty` `QuasiSeparated` `QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`HasAffineProperty.copy` `Scheme.Pullback.instHasPullbacks` `instHasAffinePropertyDiagonalSchemeDiagonal` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `quasiSeparated_eq_diagonal_is_quasiCompact` `AffineTargetMorphismProperty.ext` `quasiCompact_affineProperty_iff_quasiSeparatedSpace`
`instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `Scheme` `Scheme.instCategory` `QuasiCompact` `QuasiSeparated`	—	`Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal` `quasiCompact_isStableUnderBaseChange` `instIsMultiplicativeSchemeQuasiCompact` `quasiSeparated_isStableUnderBaseChange` `quasiSeparated_eq_diagonal_is_quasiCompact` `le_refl`
`instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `Scheme` `Scheme.instCategory` `QuasiSeparated` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`QuasiSeparated.of_comp`
`instIsMultiplicativeSchemeQuasiSeparated` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `QuasiSeparated`	—	`instQuasiSeparatedOfMonoScheme` `IsOpenImmersion.mono` `IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `quasiSeparated_isStableUnderComposition`
`instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat` 📖	mathematical	—	`QuasiCompact` `CategoryTheory.Limits.prod` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `instCartesianMonoidalCategoryScheme` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.pair` `CategoryTheory.Limits.prod.lift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `quasiSeparatedSpace_iff_quasiCompact_prod_lift`
`instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat` 📖	mathematical	—	`QuasiCompact` `CategoryTheory.Limits.equalizer` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `instHasFiniteLimitsScheme` `CategoryTheory.Limits.instFinCategoryWalkingParallelPair` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.equalizer.ι`	—	`CategoryTheory.MorphismProperty.of_isPullback` `quasiCompact_isStableUnderBaseChange` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `instHasFiniteLimitsScheme` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `CategoryTheory.IsPullback.flip` `CategoryTheory.Limits.isPullback_equalizer_prod` `instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat`
`instQuasiSeparatedFstScheme` 📖	mathematical	—	`QuasiSeparated` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.MorphismProperty.pullback_fst` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `quasiSeparated_isStableUnderBaseChange`
`instQuasiSeparatedMorphismRestrict` 📖	mathematical	—	`QuasiSeparated` `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` `instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat`
`instQuasiSeparatedOfMonoScheme` 📖	mathematical	—	`QuasiSeparated`	—	`Scheme.Pullback.instHasPullback` `quasiCompact_of_isIso` `CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono`
`instQuasiSeparatedResLE` 📖	mathematical	`Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	`QuasiSeparated` `Scheme.Opens.toScheme` `Scheme.Hom.resLE`	—	`quasiSeparated_comp` `instQuasiSeparatedOfMonoScheme` `IsOpenImmersion.mono` `instIsOpenImmersionHomOfLE` `instQuasiSeparatedMorphismRestrict`
`instQuasiSeparatedSndScheme` 📖	mathematical	—	`QuasiSeparated` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.MorphismProperty.pullback_snd` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `quasiSeparated_isStableUnderBaseChange`
`instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat` 📖	mathematical	—	`QuasiSeparated` `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` `instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat` `isAffine_Spec`
`isIso_ΓSpec_adjunction_unit_app_basicOpen` 📖	mathematical	—	`CategoryTheory.IsIso` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `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` `PrimeSpectrum.basicOpen` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `Scheme.toSpecΓ` `Scheme.Hom.app`	—	`CategoryTheory.IsIso.of_isIso_comp_right` `Scheme.toSpecΓ_preimage_basicOpen` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom` `CategoryTheory.ConcreteCategory.isIso_iff_bijective` `CommRingCat.forgetReflectIsos` `IsLocalization.bijective` `StructureSheaf.IsLocalization.to_basicOpen` `isLocalization_basicOpen_of_qcqs` `isCompact_univ` `isQuasiSeparated_univ` `Scheme.basicOpen_le` `LE.le.trans` `le_of_eq` `Opposite.op_injective` `le_top` `CategoryTheory.eqToHom_op` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality_assoc` `Scheme.toSpecΓ_appTop` `CategoryTheory.Iso.inv_hom_id_assoc`
`isLocalization_basicOpen_of_qcqs` 📖	mathematical	`IsCompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.carrier` `IsQuasiSeparated`	`IsLocalization.Away` `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` `CommRing.toCommSemiring` `CommRingCat.commRing` `Scheme.basicOpen` `Scheme.algebra_section_section_basicOpen`	—	`Scheme.basicOpen_le` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.pow` `RingedSpace.isUnit_res_basicOpen` `exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated` `mul_comm` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.algebraMap_toAlgebra` `exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact`
`quasiCompact_affineProperty_iff_quasiSeparatedSpace` 📖	mathematical	—	`AffineTargetMorphismProperty.diagonal` `CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `QuasiSeparatedSpace`	—	`Scheme.Pullback.instHasPullback` `quasiSeparatedSpace_iff_forall_affineOpens` `Topology.IsOpenEmbedding.isEmbedding` `Scheme.Hom.isOpenEmbedding` `IsOpenImmersion.comp` `IsOpenImmersion.instFstScheme` `Scheme.Opens.instIsOpenImmersionι` `isCompact_iff_compactSpace` `Homeomorph.compactSpace` `Subtype.range_coe` `IsOpenImmersion.hasPullback_of_left` `IsOpenImmersion.range_pullback_to_base_of_left` `isAffineOpen_opensRange`
`quasiCompact_iff_compactSpace` 📖	mathematical	—	`QuasiCompact` `CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`QuasiCompact.compactSpace_of_compactSpace` `quasiCompact_of_compactSpace`
`quasiCompact_of_compactSpace` 📖	mathematical	—	`QuasiCompact`	—	`HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `isAffine_Spec` `QuasiCompact.of_comp` `instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat`
`quasiCompact_over_affine_iff` 📖	mathematical	—	`QuasiCompact` `CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`quasiCompact_iff_compactSpace`
`quasiSeparatedSpace_iff_affine` 📖	mathematical	—	`QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsCompact` `Set` `Set.instInter` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `Set.instMembership` `Scheme.affineOpens`	—	`quasiSeparatedSpace_iff_forall_affineOpens`
`quasiSeparatedSpace_iff_forall_affineOpens` 📖	mathematical	—	`QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsCompact` `Set` `Set.instInter` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `Set.instMembership` `Scheme.affineOpens`	—	`quasiSeparatedSpace_iff` `TopologicalSpace.Opens.is_open'` `IsAffineOpen.isCompact` `compact_open_induction_on` `inf_of_le_right` `Set.inter_union_distrib_left` `IsCompact.union` `Set.empty_inter` `Set.union_inter_distrib_right`
`quasiSeparatedSpace_iff_quasiCompact_prod_lift` 📖	mathematical	—	`QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `QuasiCompact` `CategoryTheory.Limits.prod` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `instCartesianMonoidalCategoryScheme` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.pair` `CategoryTheory.Limits.prod.lift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `instHasTerminalScheme` `Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `Scheme.instHasPullbacksIsOpenImmersion` `HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `CategoryTheory.Iso.isIso_hom` `HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat` `instIsAffineTerminalScheme` `Scheme.Pullback.instHasPullback` `quasiSeparated_iff` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.pullback.diagonal_fst` `CategoryTheory.Category.assoc` `prodIsoPullback_hom_fst` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.pullback.diagonal_snd` `prodIsoPullback_hom_snd`
`quasiSeparatedSpace_iff_quasiSeparated` 📖	mathematical	—	`QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `QuasiSeparated` `CategoryTheory.Limits.terminal` `Scheme` `Scheme.instCategory` `instHasTerminalScheme` `CategoryTheory.Limits.terminal.from`	—	`instHasTerminalScheme` `HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat` `instIsAffineTerminalScheme`
`quasiSeparatedSpace_of_isAffine` 📖	mathematical	—	`QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`quasiSeparatedSpace_congr` `CategoryTheory.Iso.isIso_hom` `PrimeSpectrum.instQuasiSeparatedSpace`
`quasiSeparatedSpace_of_quasiSeparated` 📖	mathematical	—	`QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`instHasTerminalScheme` `quasiSeparatedSpace_iff_quasiSeparated` `CategoryTheory.Limits.IsTerminal.hom_ext` `quasiSeparated_comp`
`quasiSeparated_comp` 📖	mathematical	—	`QuasiSeparated` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.comp_mem` `quasiSeparated_isStableUnderComposition`
`quasiSeparated_eq_diagonal_is_quasiCompact` 📖	mathematical	—	`QuasiSeparated` `CategoryTheory.MorphismProperty.diagonal` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullbacks` `QuasiCompact`	—	`Scheme.Pullback.instHasPullbacks` `quasiSeparated_iff`
`quasiSeparated_iff` 📖	mathematical	—	`QuasiSeparated` `QuasiCompact` `CategoryTheory.Limits.pullback.diagonalObj` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.diagonal`	—	`Scheme.Pullback.instHasPullback`
`quasiSeparated_iff_quasiSeparatedSpace` 📖	mathematical	—	`QuasiSeparated` `QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`quasiSeparatedSpace_of_quasiSeparated` `QuasiSeparated.of_quasiSeparatedSpace`
`quasiSeparated_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `QuasiSeparated`	—	`Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal` `quasiCompact_isStableUnderBaseChange` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `Scheme.instHasPullbacksIsOpenImmersion` `HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `quasiSeparated_eq_diagonal_is_quasiCompact`
`quasiSeparated_isStableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `QuasiSeparated`	—	`Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition` `quasiCompact_isStableUnderComposition` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `Scheme.instHasPullbacksIsOpenImmersion` `HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `quasiCompact_isStableUnderBaseChange` `quasiSeparated_eq_diagonal_is_quasiCompact`
`quasiSeparated_over_affine_iff` 📖	mathematical	—	`QuasiSeparated` `QuasiSeparatedSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`quasiSeparated_iff_quasiSeparatedSpace`

AlgebraicGeometry.IsAffineOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isQuasiSeparated` 📖	mathematical	—	`IsQuasiSeparated` `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`	—	`isQuasiSeparated_iff_quasiSeparatedSpace` `TopologicalSpace.Opens.isOpen` `AlgebraicGeometry.quasiSeparatedSpace_of_isAffine`

AlgebraicGeometry.QuasiCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompact`	—	`CategoryTheory.MorphismProperty.of_postcomp` `AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated`

AlgebraicGeometry.QuasiSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonalQuasiCompact` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompact` `CategoryTheory.Limits.pullback.diagonalObj` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.diagonal`	—	`quasiCompact_diagonal`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.QuasiSeparated`	—	`AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.isAffine_affineCover` `AlgebraicGeometry.HasAffineProperty.of_openCover` `AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat` `AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.hasPullbackHorizPaste` `AlgebraicGeometry.HasAffineProperty.of_isPullback` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `CategoryTheory.IsPullback.of_hasPullback` `AlgebraicGeometry.quasiSeparated_comp` `AlgebraicGeometry.instQuasiSeparatedOfMonoScheme` `AlgebraicGeometry.IsOpenImmersion.mono` `AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Iso.isIso_hom`
`of_quasiSeparatedSpace` 📖	mathematical	—	`AlgebraicGeometry.QuasiSeparated`	—	`AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat` `AlgebraicGeometry.isAffine_Spec` `of_comp`
`quasiCompact_diagonal` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompact` `CategoryTheory.Limits.pullback.diagonalObj` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.diagonal`	—	—

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiSeparatedSpace_of_isOpenCover` 📖	mathematical	`TopologicalSpace.IsOpenCover` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `AlgebraicGeometry.IsAffineOpen` `IsCompact` `Set` `Set.instInter` `SetLike.coe` `Opens` `TopologicalSpace.Opens.instSetLike`	`QuasiSeparatedSpace`	—	`AlgebraicGeometry.isAffine_Spec` `AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace` `AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source` `AlgebraicGeometry.HasAffineProperty.isLocal_affineProperty` `AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `Pullback.instHasPullback` `isCompact_univ_iff` `Topology.IsEmbedding.isCompact_iff` `Topology.IsOpenEmbedding.toIsEmbedding` `Hom.isOpenEmbedding` `AlgebraicGeometry.IsOpenImmersion.comp` `AlgebraicGeometry.IsOpenImmersion.instFstScheme` `instIsOpenImmersionF` `Set.image_univ` `AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left` `AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left` `Opens.range_ι`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isQuasiSeparated_preimage` 📖	mathematical	`IsQuasiSeparated` `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'`	—	`isQuasiSeparated_iff_quasiSeparatedSpace` `TopologicalSpace.Opens.is_open'` `AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated` `AlgebraicGeometry.instQuasiSeparatedMorphismRestrict`

---

← Back to Index