QuasiCompact

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

Statistics

Metric	Count
Definitions QuasiCompact, forgetQc, ofQuasiCompactCover, qculift, propQCPrecoverage, propQCTopology, qcCoverFamily, qcPrecoverage	8
Theorems forgetQc_toPreZeroHypercover, mem_propQCTopology, ofQuasiCompactCover_toPreZeroHypercover, generate_singleton_mem_propQCTopology, singleton_mem_propQCPrecoverage, singleton_mem_qcPrecoverage, bot_mem_propQCPrecoverage, bot_mem_propQCTopology, bot_mem_qcPrecoverage, instHasIsosQcPrecoverage, instIsStableUnderBaseChangeQcPrecoverage, instIsStableUnderCompositionQcPrecoverage, instIsStableUnderSupQcPrecoverage, instQuasiCompactCover, instQuasiCompactCoverForgetQc, instQuasiCompactCoverQculift, instSmallPropQCPrecoverage, mem_propQCPrecoverage_iff_exists_quasiCompactCover, precoverage_le_qcPrecoverage_of_isOpenMap, presieve₀_mem_qcPrecoverage_iff, propQCPrecoverage_le_precoverage, propQCPrecoverage_monotone, qcCoverFamily_property, quasiCompactCover_shrink_iff, zariskiPrecoverage_le_propQCPrecoverage, zariskiPrecoverage_le_qcPrecoverage, zariskiTopology_le_propQCTopology	27
Total	35

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
propQCPrecoverage 📖	CompOp	10 math math: mem_propQCPrecoverage_iff_exists_quasiCompactCover, instQuasiCompactCover, Cover.ofQuasiCompactCover_toPreZeroHypercover, Cover.forgetQc_toPreZeroHypercover, zariskiPrecoverage_le_propQCPrecoverage, instSmallPropQCPrecoverage, Hom.singleton_mem_propQCPrecoverage, bot_mem_propQCPrecoverage, propQCPrecoverage_le_precoverage, propQCPrecoverage_monotone
propQCTopology 📖	CompOp	8 math math: AlgebraicGeometry.isSheaf_propQCTopology_iff, AlgebraicGeometry.isSheaf_type_propQCTopology_iff, Cover.mem_propQCTopology, proetaleTopology_eq_propQCTopology, fpqcTopology_eq_propQCTopology, zariskiTopology_le_propQCTopology, bot_mem_propQCTopology, Hom.generate_singleton_mem_propQCTopology
qcCoverFamily 📖	CompOp	1 math math: qcCoverFamily_property
qcPrecoverage 📖	CompOp	9 math math: instIsStableUnderCompositionQcPrecoverage, Hom.singleton_mem_qcPrecoverage, presieve₀_mem_qcPrecoverage_iff, instIsStableUnderSupQcPrecoverage, instHasIsosQcPrecoverage, precoverage_le_qcPrecoverage_of_isOpenMap, bot_mem_qcPrecoverage, instIsStableUnderBaseChangeQcPrecoverage, zariskiPrecoverage_le_qcPrecoverage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem_propQCPrecoverage 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings propQCPrecoverage Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_mem_qcPrecoverage bot_mem_precoverage
bot_mem_propQCTopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve propQCTopology Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	CategoryTheory.Sieve.generate_bot CategoryTheory.Precoverage.generate_mem_toGrothendieck bot_mem_propQCPrecoverage
bot_mem_qcPrecoverage 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings qcPrecoverage Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	CategoryTheory.PreZeroHypercover.presieve₀_empty presieve₀_mem_qcPrecoverage_iff AlgebraicGeometry.QuasiCompactCover.instOfIsEmptyCarrierCarrierCommRingCat
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
instQuasiCompactCover 📖	mathematical	—	AlgebraicGeometry.QuasiCompactCover CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme instCategory propQCPrecoverage	—	presieve₀_mem_qcPrecoverage_iff CategoryTheory.Precoverage.ZeroHypercover.mem₀
instQuasiCompactCoverForgetQc 📖	mathematical	—	AlgebraicGeometry.QuasiCompactCover CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme instCategory precoverage Cover.forgetQc	—	instQuasiCompactCover
instQuasiCompactCoverQculift 📖	mathematical	—	AlgebraicGeometry.QuasiCompactCover CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme instCategory precoverage Cover.qculift	—	AlgebraicGeometry.QuasiCompactCover.of_hom AlgebraicGeometry.QuasiCompactCover.instUlift
instSmallPropQCPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.Small AlgebraicGeometry.Scheme instCategory propQCPrecoverage	—	instQuasiCompactCoverForgetQc instJointlySurjectivePrecoverage presieve₀_mem_qcPrecoverage_iff AlgebraicGeometry.QuasiCompactCover.of_hom AlgebraicGeometry.QuasiCompactCover.instUlift presieve₀_mem_precoverage_iff Cover.covers Cover.map_prop
mem_propQCPrecoverage_iff_exists_quasiCompactCover 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings propQCPrecoverage Cover precoverage AlgebraicGeometry.QuasiCompactCover CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover CategoryTheory.PreZeroHypercover.presieve₀	—	CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover propQCPrecoverage_le_precoverage presieve₀_mem_qcPrecoverage_iff CategoryTheory.Precoverage.ZeroHypercover.mem₀
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 AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder 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
propQCPrecoverage_le_precoverage 📖	mathematical	—	CategoryTheory.Precoverage AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder propQCPrecoverage precoverage	—	inf_le_right
propQCPrecoverage_monotone 📖	mathematical	—	Monotone CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Precoverage PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Precoverage.instPartialOrder propQCPrecoverage	—	propQCPrecoverage.eq_1 inf_le_inf le_refl precoverage_mono
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_propQCPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder zariskiPrecoverage propQCPrecoverage	—	propQCPrecoverage.eq_1 le_inf_iff zariskiPrecoverage_le_qcPrecoverage precoverage_mono AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
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
zariskiTopology_le_propQCTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme instCategory CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology zariskiTopology propQCTopology	—	CategoryTheory.Precoverage.toGrothendieck_mono zariskiPrecoverage_le_propQCPrecoverage CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
forgetQc 📖	CompOp	2 math math: AlgebraicGeometry.Scheme.instQuasiCompactCoverForgetQc, forgetQc_toPreZeroHypercover
ofQuasiCompactCover 📖	CompOp	1 math math: ofQuasiCompactCover_toPreZeroHypercover
qculift 📖	CompOp	1 math math: AlgebraicGeometry.Scheme.instQuasiCompactCoverQculift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forgetQc_toPreZeroHypercover 📖	mathematical	—	CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.precoverage forgetQc AlgebraicGeometry.Scheme.propQCPrecoverage	—	—
mem_propQCTopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve AlgebraicGeometry.Scheme.propQCTopology CategoryTheory.Sieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Precoverage.generate_mem_toGrothendieck AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff CategoryTheory.Precoverage.ZeroHypercover.mem₀
ofQuasiCompactCover_toPreZeroHypercover 📖	mathematical	—	CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.propQCPrecoverage ofQuasiCompactCover AlgebraicGeometry.Scheme.precoverage	—	—

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generate_singleton_mem_propQCTopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve AlgebraicGeometry.Scheme.propQCTopology CategoryTheory.Sieve.generate CategoryTheory.Presieve.singleton	—	CategoryTheory.Precoverage.generate_mem_toGrothendieck singleton_mem_propQCPrecoverage
singleton_mem_propQCPrecoverage 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings AlgebraicGeometry.Scheme.propQCPrecoverage CategoryTheory.Presieve.singleton	—	singleton_mem_qcPrecoverage
singleton_mem_qcPrecoverage 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings AlgebraicGeometry.Scheme.qcPrecoverage CategoryTheory.Presieve.singleton	—	AlgebraicGeometry.Scheme.qcPrecoverage.eq_1 CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff AlgebraicGeometry.QuasiCompactCover.homCover presieve₀_cover

---

← Back to Index