QuasiCompact

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

Statistics

Metric	Count
Definitions QuasiCompact, qcCoverFamily, qcPrecoverage	3
Theorems instHasIsosQcPrecoverage, instIsStableUnderBaseChangeQcPrecoverage, instIsStableUnderCompositionQcPrecoverage, instIsStableUnderSupQcPrecoverage, precoverage_le_qcPrecoverage_of_isOpenMap, presieve₀_mem_qcPrecoverage_iff, qcCoverFamily_property, quasiCompactCover_shrink_iff, zariskiPrecoverage_le_qcPrecoverage	9
Total	12

AlgebraicGeometry

Definitions

Name	Category	Theorems
QuasiCompact 📖	CompData	49 math math: descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, instQuasiCompactOfUniversallyClosed, instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, instIsMultiplicativeSchemeQuasiCompact, quasiCompact_iff, descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, instQuasiCompactMorphismRestrict, quasiSeparated_eq_diagonal_is_quasiCompact, quasiCompact_over_affine_iff, quasiCompact_isStableUnderBaseChange, quasiCompact_comp, QuasiSeparated.diagonalQuasiCompact, instQuasiCompactOfIsLocallyNoetherianOfIsOpenImmersion, compactSpace_iff_quasiCompact, quasiCompact_isStableUnderComposition, instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated, QuasiCompact.of_comp, instQuasiCompactSndScheme, Scheme.instQuasiCompactToImage, HasAffineProperty.descendsAlong_of_affineAnd, instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact, HasRingHomProperty.descendsAlong, instQuasiCompactFstScheme, universallyClosed_eq_universallySpecializing, quasiCompact_of_isIso, Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, IsProper.eq_valuativeCriterion, quasiSeparated_iff, UniversallyClosed.eq_valuativeCriterion, instQuasiCompactOfIsAffineHom, quasiCompact_iff_forall_isAffineOpen, quasiCompact_iff_compactSpace, QuasiSeparated.quasiCompact_diagonal, IsLocalAtTarget.descendsAlong_inf_quasiCompact, quasiCompact_iff_spectral, quasiCompact_iff_isSpectralMap, quasiCompact_iff_forall_affine, quasiCompact_of_noetherianSpace_source, instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, Scheme.Hom.instQuasiCompactToNormalization, instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat, Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Scheme.IdealSheafData.instQuasiCompactSubschemeι, quasiSeparatedSpace_iff_quasiCompact_prod_lift, descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, quasiCompact_of_compactSpace

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
qcCoverFamily 📖	CompOp	1 math math: qcCoverFamily_property
qcPrecoverage 📖	CompOp	7 math math: instIsStableUnderCompositionQcPrecoverage, presieve₀_mem_qcPrecoverage_iff, instIsStableUnderSupQcPrecoverage, instHasIsosQcPrecoverage, precoverage_le_qcPrecoverage_of_isOpenMap, instIsStableUnderBaseChangeQcPrecoverage, zariskiPrecoverage_le_qcPrecoverage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasIsosQcPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.HasIsos AlgebraicGeometry.Scheme instCategory qcPrecoverage	—	CategoryTheory.Precoverage.HasIsos.of_preZeroHypercoverFamily qcCoverFamily_property quasiCompactCover_iff AlgebraicGeometry.QuasiCompactCover.singleton AlgebraicGeometry.instSurjectiveOfIsIsoScheme AlgebraicGeometry.instQuasiCompactOfIsAffineHom AlgebraicGeometry.instIsAffineHomOfIsIsoScheme
instIsStableUnderBaseChangeQcPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderBaseChange AlgebraicGeometry.Scheme instCategory qcPrecoverage	—	CategoryTheory.Precoverage.IsStableUnderBaseChange.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms isClosedUnderIsomorphisms_quasiCompactCover AlgebraicGeometry.QuasiCompactCover.instPullback₁Scheme
instIsStableUnderCompositionQcPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderComposition AlgebraicGeometry.Scheme instCategory qcPrecoverage	—	CategoryTheory.Precoverage.IsStableUnderComposition.of_preZeroHypercoverFamily AlgebraicGeometry.QuasiCompactCover.instBindScheme
instIsStableUnderSupQcPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderSup AlgebraicGeometry.Scheme instCategory qcPrecoverage	—	CategoryTheory.Precoverage.IsStableUnderSup.of_preZeroHypercoverFamily AlgebraicGeometry.QuasiCompactCover.instSumScheme_1
precoverage_le_qcPrecoverage_of_isOpenMap 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace 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 Hom.toLRSHom'	CategoryTheory.Precoverage CategoryTheory.Precoverage.instPartialOrder precoverage qcPrecoverage	—	CategoryTheory.Precoverage.le_of_zeroHypercover presieve₀_mem_qcPrecoverage_iff AlgebraicGeometry.QuasiCompactCover.of_isOpenMap instJointlySurjectivePrecoverage Cover.map_prop
presieve₀_mem_qcPrecoverage_iff 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings qcPrecoverage CategoryTheory.PreZeroHypercover.presieve₀ AlgebraicGeometry.QuasiCompactCover	—	CategoryTheory.PreZeroHypercover.presieve₀_shrink qcPrecoverage.eq_1 CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
qcCoverFamily_property 📖	mathematical	—	CategoryTheory.PreZeroHypercoverFamily.property AlgebraicGeometry.Scheme instCategory qcCoverFamily quasiCompactCover	—	—
quasiCompactCover_shrink_iff 📖	mathematical	—	AlgebraicGeometry.QuasiCompactCover CategoryTheory.PreZeroHypercover.shrink AlgebraicGeometry.Scheme instCategory	—	AlgebraicGeometry.QuasiCompactCover.of_hom
zariskiPrecoverage_le_qcPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder zariskiPrecoverage qcPrecoverage	—	precoverage_le_qcPrecoverage_of_isOpenMap Topology.IsOpenEmbedding.isOpenMap Hom.isOpenEmbedding

---

← Back to Index