SheafQuasiCompact

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

Statistics

Metric	Count
Definitions	0
Theorems isSheaf_propQCTopology_iff, isSheaf_type_propQCTopology_iff	2
Total	2

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_propQCTopology_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf Scheme Scheme.instCategory Scheme.propQCTopology Scheme.zariskiTopology CategoryTheory.Presieve.IsSheafFor Spec CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op CategoryTheory.Presieve.singleton Spec.map	—	—
isSheaf_type_propQCTopology_iff 📖	mathematical	—	CategoryTheory.Presieve.IsSheaf Scheme Scheme.instCategory Scheme.propQCTopology Scheme.zariskiTopology CategoryTheory.Presieve.IsSheafFor Spec CategoryTheory.Presieve.singleton Spec.map	—	CategoryTheory.Presieve.isSheaf_of_le Scheme.zariskiTopology_le_propQCTopology CategoryTheory.Presieve.IsSheaf.isSheafFor Scheme.Hom.presieve₀_cover Scheme.Cover.mem_propQCTopology QuasiCompactCover.homCover instQuasiCompactOfIsAffineHom isAffineHom_of_isAffine isAffine_Spec CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small CategoryTheory.Precoverage.instIsStableUnderBaseChangeMin Scheme.instIsStableUnderBaseChangeQcPrecoverage Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange Scheme.isJointlySurjectivePreserving CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks Scheme.Pullback.instHasPullbacks Scheme.instSmallPropQCPrecoverage UnivLE.self Scheme.Cover.forgetQc_toPreZeroHypercover univLE_of_max Scheme.Cover.isSheafFor_sigma_iff CategoryTheory.Presieve.ofArrows_of_unique instIsAffineSigmaObjScheme Spec.map_surjective CategoryTheory.Presieve.isSheafFor_singleton_iff_of_iso CategoryTheory.Iso.hom_inv_id_assoc IsZariskiLocalAtSource.comp Scheme.Cover.map_prop IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small instSurjectiveCompScheme instSurjectiveOfIsIsoScheme QuasiCompactCover.exists_hom IsZariskiLocalAtSource.respectsLeft_isOpenImmersion Scheme.compactSpace_of_isAffine Scheme.instQuasiCompactCoverForgetQc Scheme.Pullback.instHasPullback CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks Scheme.instHasPullbacksPrecoverageOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks CategoryTheory.Sieve.pullbackArrows_comm CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Presieve.ofArrows_pullback CategoryTheory.Presieve.isSheafFor_iff_generate Scheme.local_affine QuasiCompactCover.instPullback₂Scheme QuasiCompactCover.instCoverOfIsAffineOfFiniteI₀ IsAffine.of_isIso CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Iso.isIso_hom instIsAffinePullbackSchemeOfIsAffineHom_1 Scheme.isAffine_affineCover CategoryTheory.Presieve.isSeparatedFor_iff_generate CategoryTheory.Presieve.IsSheafFor.isSeparatedFor CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff

---

← Back to Index