Structures · Geometry
AlgebraicGeometry.QuasiSeparated
A morphism is QuasiSeparated if diagonal map is quasi-compact.
- Shape
- One type argument · adds quasiCompact_diagonal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances2
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
How is a type an instance?
Loading the hierarchy index…
Assumed by74
- AlgebraicGeometry.Scheme.Hom.normalization
- AlgebraicGeometry.Scheme.Hom.fromNormalization
- AlgebraicGeometry.Scheme.Hom.toNormalization
- AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso
- AlgebraicGeometry.Scheme.Hom.normalizationDesc
- AlgebraicGeometry.Scheme.Hom.normalizationOpenCover
- AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization
- AlgebraicGeometry.Scheme.Hom.normalizationObjIso
- AlgebraicGeometry.Scheme.Hom.normalizationPullback
- AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp
- AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc
- AlgebraicGeometry.Scheme.Hom.ι_fromNormalization
- AlgebraicGeometry.Scheme.Hom.normalizationGlueData
- AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated
- AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd
- 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.ι_toNormalization_assoc
- AlgebraicGeometry.IsSeparated.of_valuativeCriterion
- AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom
- AlgebraicGeometry.Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization
- AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage
- AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage
- AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc
- AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom
- AlgebraicGeometry.Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv
- AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization
- AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap
- AlgebraicGeometry.Scheme.Hom.inl_normalizationCoprodIso_hom_fromNormalization
- AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc
- AlgebraicGeometry.Scheme.Hom.inl_toNormalization_normalizationCoprodIso_inv
- AlgebraicGeometry.Scheme.Hom.fromNormalization_app
- AlgebraicGeometry.Scheme.Hom.instQuasiCompactToNormalization
- AlgebraicGeometry.Scheme.Hom.normalizationDesc.congr_simp
- AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization_assoc
- AlgebraicGeometry.Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv_assoc
- AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc
- AlgebraicGeometry.QuasiSeparated.of_comp
- AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget
- AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth
- AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp_assoc
- AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap
- AlgebraicGeometry.instQuasiSeparatedFstScheme
- AlgebraicGeometry.instQuasiSeparatedSndScheme
- AlgebraicGeometry.Scheme.Hom.normalizationObjIso.congr_simp
- AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd_assoc
- AlgebraicGeometry.Scheme.Hom.instIsDominantToNormalization
- AlgebraicGeometry.Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom
Ancestors0
No ancestors.