Structures · Geometry
AlgebraicGeometry.QuasiCompact
A morphism is "quasi-compact" if the underlying map of topological spaces is, i.e. if the preimages of quasi-compact open sets are quasi-compact.
- Shape
- One type argument · adds isCompact_preimage
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Concrete types that are instances6
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.Scheme.IdealSheafData.subscheme
- CategoryTheory.Limits.equalizer
- AlgebraicGeometry.Proj
- AlgebraicGeometry.Scheme.GlueData.glued
How is a type an instance?
Loading the hierarchy index…
Assumed by129
- AlgebraicGeometry.Scheme.Hom.normalization
- AlgebraicGeometry.Scheme.Hom.fromNormalization
- AlgebraicGeometry.Scheme.Hom.toNormalization
- AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso
- AlgebraicGeometry.Scheme.Hom.ker_apply
- AlgebraicGeometry.Scheme.Hom.normalizationDesc
- AlgebraicGeometry.Scheme.Hom.normalizationOpenCover
- AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace
- AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization
- AlgebraicGeometry.Scheme.Hom.support_ker
- AlgebraicGeometry.Scheme.Hom.normalizationObjIso
- AlgebraicGeometry.QuasiCompact.isCompact_preimage
- AlgebraicGeometry.Scheme.Hom.normalizationPullback
- AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp
- AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton
- AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc
- AlgebraicGeometry.Scheme.Hom.ι_fromNormalization
- AlgebraicGeometry.Scheme.Hom.normalizationGlueData
- AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd
- AlgebraicGeometry.Scheme.Hom.isSpectralMap
- AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton
- AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc_assoc
- AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst
- AlgebraicGeometry.Scheme.Hom.ι_toNormalization
- AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage
- AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply
- AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc
- AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion
- AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage
- AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization
- AlgebraicGeometry.Scheme.Hom.app_injective
- AlgebraicGeometry.isClosedMap_iff_specializingMap
- AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom
- AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isDominant
- AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage
- AlgebraicGeometry.Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization
- AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp
- AlgebraicGeometry.Scheme.Hom.toImage_app_injective
- AlgebraicGeometry.Flat.isQuotientMap_of_surjective
- AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage
- AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc
- AlgebraicGeometry.AlgebraicCycle.map
- AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom
- AlgebraicGeometry.Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv
- AlgebraicGeometry.Scheme.IdealSheafData.ideal_map
- AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image
- AlgebraicGeometry.IsSchemeTheoreticallyDominant.isReduced
- AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization
- AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap
- AlgebraicGeometry.UniversallyClosed.of_valuativeCriterion
Ancestors0
No ancestors.