Separated

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Statistics

Metric	Count
Definitions IsSeparated, IsSeparated	2
Theorems comp_iff, of_comp, comp_iff, of_comp, comp_iff, diagonal_isClosedImmersion, hasAffineProperty, instCompScheme, instFstScheme, instIsClosedImmersionLiftSchemeId, instIsClosedImmersionMapDescScheme, instIsMultiplicativeScheme, instIsZariskiLocalAtTarget, instMap, instMorphismRestrict, instQuasiSeparated, instResLE, instRespectsIsoScheme, instSndScheme, isClosedImmersion_diagonal, isSeparated_eq_diagonal_isClosedImmersion, isSeparated_of_mono, isStableUnderBaseChange, of_comp, of_isAffineHom, stableUnderComposition, isSeparated_terminal_from, diagonalCoverDiagonalRange_eq_top_of_injective, range_diagonal_subset_diagonalCoverDiagonalRange, instIsClosedImmersionLiftIdOfIsSeparated, instIsClosedImmersionιOfIsSeparated, instIsSeparatedOfIsAffine, instIsSeparatedOfIsSeparated, instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated, isSeparated_iff, isSeparated_iff_isClosedImmersion_prod_lift, ext_of_fromSpecResidueField_eq, ext_of_isDominant, ext_of_isDominant_of_isSeparated, ext_of_isDominant_of_isSeparated', instHasOfPostcompPropertySchemeIsAffineHomIsSeparated, instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated, instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, instIsClosedImmersionInclusion, isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, isClosedImmersion_equalizer_ι_left, isSeparated_iff, isSeparated_of_injective	48
Total	50

AlgebraicGeometry

Definitions

Name	Category	Theorems
IsSeparated 📖	CompData	35 math math: instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated, IsSeparated.isStableUnderBaseChange, IsSeparated.isSeparated_of_mono, IsSeparated.eq_valuativeCriterion, instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated, IsSeparated.of_comp, IsSeparated.isSeparated_eq_diagonal_isClosedImmersion, Proj.isSeparated, isSeparated_of_injective, Scheme.instIsSeparatedOfIsSeparated, IsSeparated.of_isAffineHom, IsSeparated.instResLE, isSeparated_iff, isProper_iff, IsSeparated.of_valuativeCriterion, IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated, isProper_eq, instHasOfPostcompPropertySchemeIsProperIsSeparated, IsSeparated.stableUnderComposition, IsSeparated.instCompScheme, Scheme.isSeparated_iff, instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, IsSeparated.instMap, instHasOfPostcompPropertySchemeIsAffineHomIsSeparated, IsSeparated.instIsMultiplicativeScheme, IsProper.toIsSeparated, IsSeparated.instRespectsIsoScheme, Scheme.IsSeparated.isSeparated_terminal_from, IsSeparated.instMorphismRestrict, IsSeparated.instIsZariskiLocalAtTarget, IsSeparated.comp_iff, IsSeparated.hasAffineProperty, IsFinite.instHasOfPostcompPropertySchemeIsSeparated, IsSeparated.instFstScheme, IsSeparated.instSndScheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_of_fromSpecResidueField_eq 📖	—	Dense TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec Scheme.residueField Scheme.fromSpecResidueField	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instHasFiniteLimitsScheme Dense.mono Scheme.Hom.comp_apply CategoryTheory.Limits.equalizer.lift_ι Scheme.fromSpecResidueField_apply ext_of_isDominant_of_isSeparated CategoryTheory.Limits.equalizer.condition
ext_of_isDominant 📖	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory	—	—	ext_of_isDominant_of_isSeparated instHasTerminalScheme Scheme.IsSeparated.isSeparated_terminal_from CategoryTheory.Limits.terminal.hom_ext
ext_of_isDominant_of_isSeparated 📖	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Over.instHasEqualizers CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instHasFiniteLimitsScheme IsDominant.of_comp CategoryTheory.Over.OverMorphism.ext CategoryTheory.Over.comp_left CategoryTheory.Limits.equalizer.lift_ι surjective_of_isDominant_of_isClosed_range Topology.IsClosedEmbedding.isClosed_range Scheme.Hom.isClosedEmbedding isClosedImmersion_equalizer_ι_left isIso_of_isClosedImmersion_of_surjective CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Limits.equalizer.condition
ext_of_isDominant_of_isSeparated' 📖	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory	—	—	ext_of_isDominant_of_isSeparated CategoryTheory.comp_over
instHasOfPostcompPropertySchemeIsAffineHomIsSeparated 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty Scheme Scheme.instCategory IsAffineHom IsSeparated	—	Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal isAffineHom_isStableUnderBaseChange instIsMultiplicativeSchemeIsAffineHom IsSeparated.isStableUnderBaseChange IsClosedImmersion.instIsAffineHom IsSeparated.diagonal_isClosedImmersion
instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty Scheme Scheme.instCategory IsClosedImmersion IsSeparated	—	Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal IsClosedImmersion.isStableUnderBaseChange IsClosedImmersion.instIsMultiplicativeScheme IsSeparated.isStableUnderBaseChange IsSeparated.diagonal_isClosedImmersion
instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty Scheme Scheme.instCategory IsSeparated Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	IsSeparated.of_comp
instIsClosedImmersionInclusion 📖	mathematical	Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder Scheme.IdealSheafData.instPartialOrder	IsClosedImmersion Scheme.IdealSheafData.subscheme Scheme.IdealSheafData.inclusion	—	Scheme.IdealSheafData.inclusion_subschemeι IsClosedImmersion.instSubschemeι IsClosedImmersion.of_comp IsSeparated.isSeparated_of_mono IsPreimmersion.instMonoScheme Scheme.IdealSheafData.instIsPreimmersionSubschemeι
isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange 📖	mathematical	IsAffine CategoryTheory.PreZeroHypercover.X Scheme Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover Scheme.precoverage IsOpenImmersion CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.f Scheme.Pullback.instHasPullback	IsClosedImmersion Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens CategoryTheory.Limits.pullback.diagonalObj Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.diagonal Scheme.Pullback.diagonalCoverDiagonalRange morphismRestrict	—	Scheme.Pullback.instHasPullback Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange Scheme.instIsJointlySurjectivePreservingIsOpenImmersion isOpenImmersion_stableUnderBaseChange Scheme.instIsOpenImmersionF Scheme.Opens.instIsOpenImmersionι Scheme.Hom.image_preimage_eq_opensRange_inf inf_eq_right Scheme.Opens.opensRange_ι le_iSup TopologicalSpace.Opens.map_iSup Scheme.Opens.ι_preimage_self IsZariskiLocalAtTarget.iff_of_iSup_eq_top IsClosedImmersion.isZariskiLocalAtTarget CategoryTheory.MorphismProperty.arrow_mk_iso_iff IsClosedImmersion.respectsIso IsSeparated.diagonal_isClosedImmersion IsSeparated.of_isAffineHom isAffineHom_of_isAffine
isClosedImmersion_equalizer_ι_left 📖	mathematical	—	IsClosedImmersion CategoryTheory.Comma.left Scheme Scheme.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.equalizer CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Over.instHasEqualizers CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instHasFiniteLimitsScheme CategoryTheory.Limits.instFinCategoryWalkingParallelPair CategoryTheory.Limits.parallelPair CategoryTheory.CommaMorphism.left CategoryTheory.Limits.equalizer.ι	—	CategoryTheory.MorphismProperty.of_isPullback IsClosedImmersion.isStableUnderBaseChange CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Over.instHasEqualizers CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instHasFiniteLimitsScheme CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.map CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.widePullbackShape_connected Scheme.Pullback.instHasPullbacks CategoryTheory.Limits.isPullback_equalizer_prod Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.cancel_right_of_respectsIso IsClosedImmersion.respectsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Over.prodLeftIsoPullback_hom_fst CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullback.diagonal_fst CategoryTheory.Over.prodLeftIsoPullback_hom_snd CategoryTheory.Limits.pullback.diagonal_snd IsSeparated.diagonal_isClosedImmersion
isSeparated_iff 📖	mathematical	—	IsSeparated IsClosedImmersion CategoryTheory.Limits.pullback.diagonalObj Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	Scheme.Pullback.instHasPullback
isSeparated_of_injective 📖	mathematical	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	IsSeparated	—	Scheme.Pullback.instHasPullback IsZariskiLocalAtTarget.of_iSup_eq_top IsClosedImmersion.isZariskiLocalAtTarget ciSup_unique Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange Scheme.isAffine_affineCover

AlgebraicGeometry.IsAffineHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_iff 📖	mathematical	—	AlgebraicGeometry.IsAffineHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	of_comp AlgebraicGeometry.IsSeparated.of_isAffineHom AlgebraicGeometry.instIsAffineHomCompScheme
of_comp 📖	mathematical	—	AlgebraicGeometry.IsAffineHom	—	CategoryTheory.MorphismProperty.of_postcomp AlgebraicGeometry.instHasOfPostcompPropertySchemeIsAffineHomIsSeparated

AlgebraicGeometry.IsClosedImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_iff 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	of_comp AlgebraicGeometry.IsSeparated.isSeparated_of_mono AlgebraicGeometry.IsPreimmersion.instMonoScheme instIsPreimmersion comp
of_comp 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion	—	CategoryTheory.MorphismProperty.of_postcomp AlgebraicGeometry.instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated

AlgebraicGeometry.IsSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_iff 📖	mathematical	—	AlgebraicGeometry.IsSeparated CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	of_comp instCompScheme
diagonal_isClosedImmersion 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	isClosedImmersion_diagonal
hasAffineProperty 📖	mathematical	—	AlgebraicGeometry.HasAffineProperty AlgebraicGeometry.IsSeparated AlgebraicGeometry.Scheme.IsSeparated	—	AlgebraicGeometry.instHasTerminalScheme AlgebraicGeometry.Scheme.isSeparated_iff CategoryTheory.Limits.terminal.comp_from comp_iff AlgebraicGeometry.Scheme.IsSeparated.isSeparated_terminal_from AlgebraicGeometry.Scheme.instIsSeparatedOfIsAffine AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget instIsZariskiLocalAtTarget
instCompScheme 📖	mathematical	—	AlgebraicGeometry.IsSeparated CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem stableUnderComposition
instFstScheme 📖	mathematical	—	AlgebraicGeometry.IsSeparated CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange isStableUnderBaseChange
instIsClosedImmersionLiftSchemeId 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.id_comp	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.id_comp CategoryTheory.MorphismProperty.cancel_left_of_respectsIso AlgebraicGeometry.IsClosedImmersion.respectsIso CategoryTheory.Limits.pullback_fst_iso_of_right_iso CategoryTheory.IsIso.id CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Limits.pullback.congrHom_inv CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback.condition instIsClosedImmersionMapDescScheme
instIsClosedImmersionMapDescScheme 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.mapDesc	—	CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback_map_diagonal_isPullback AlgebraicGeometry.Scheme.Pullback.instHasPullbacks diagonal_isClosedImmersion
instIsMultiplicativeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsSeparated	—	isSeparated_of_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.id stableUnderComposition
instIsZariskiLocalAtTarget 📖	mathematical	—	AlgebraicGeometry.IsZariskiLocalAtTarget AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks isSeparated_eq_diagonal_isClosedImmersion AlgebraicGeometry.instIsZariskiLocalAtTargetDiagonalScheme AlgebraicGeometry.IsClosedImmersion.isZariskiLocalAtTarget
instMap 📖	mathematical	—	AlgebraicGeometry.IsSeparated AlgebraicGeometry.Spec AlgebraicGeometry.Spec.map	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.diagonal_SpecMap CategoryTheory.MorphismProperty.cancel_right_of_respectsIso AlgebraicGeometry.IsClosedImmersion.respectsIso CategoryTheory.Iso.isIso_inv AlgebraicGeometry.IsClosedImmersion.spec_of_surjective Algebra.TensorProduct.lmul'_apply_tmul one_mul
instMorphismRestrict 📖	mathematical	—	AlgebraicGeometry.IsSeparated AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.morphismRestrict	—	AlgebraicGeometry.IsZariskiLocalAtTarget.restrict instIsZariskiLocalAtTarget
instQuasiSeparated 📖	mathematical	—	AlgebraicGeometry.QuasiSeparated	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instQuasiCompactOfIsAffineHom AlgebraicGeometry.IsClosedImmersion.instIsAffineHom diagonal_isClosedImmersion
instResLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	AlgebraicGeometry.IsSeparated AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Hom.resLE	—	instCompScheme isSeparated_of_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.instIsOpenImmersionHomOfLE instMorphismRestrict
instRespectsIsoScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks isSeparated_eq_diagonal_isClosedImmersion CategoryTheory.MorphismProperty.RespectsIso.diagonal AlgebraicGeometry.IsClosedImmersion.respectsIso
instSndScheme 📖	mathematical	—	AlgebraicGeometry.IsSeparated CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange isStableUnderBaseChange
isClosedImmersion_diagonal 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	—
isSeparated_eq_diagonal_isClosedImmersion 📖	mathematical	—	AlgebraicGeometry.IsSeparated CategoryTheory.MorphismProperty.diagonal AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullbacks AlgebraicGeometry.IsClosedImmersion	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks AlgebraicGeometry.isSeparated_iff
isSeparated_of_mono 📖	mathematical	—	AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono
isStableUnderBaseChange 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks isSeparated_eq_diagonal_isClosedImmersion CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange AlgebraicGeometry.IsClosedImmersion.respectsIso
of_comp 📖	mathematical	—	AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback diagonal_isClosedImmersion AlgebraicGeometry.IsClosedImmersion.of_comp CategoryTheory.Limits.hasLimitOfHasLimitsOfShape AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback.diagonal_comp instCompScheme isSeparated_of_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv instSndScheme CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Limits.pullback.instIsSplitMonoDiagonal
of_isAffineHom 📖	mathematical	—	AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.HasAffineProperty.iff_of_isAffine AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine CategoryTheory.MorphismProperty.arrow_mk_iso_iff instRespectsIsoScheme instMap AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top instIsZariskiLocalAtTarget AlgebraicGeometry.iSup_affineOpens_eq_top AlgebraicGeometry.IsZariskiLocalAtTarget.restrict AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget
stableUnderComposition 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks isSeparated_eq_diagonal_isClosedImmersion CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.IsClosedImmersion.instIsMultiplicativeScheme AlgebraicGeometry.IsClosedImmersion.respectsIso AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
IsSeparated 📖	CompData	6 math math: AlgebraicGeometry.Proj.instIsSeparated, instIsSeparatedOfIsAffine, isSeparated_iff_isClosedImmersion_prod_lift, isSeparated_iff, instIsSeparatedOfIsQuasiAffine, AlgebraicGeometry.IsSeparated.hasAffineProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedImmersionLiftIdOfIsSeparated 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.Limits.prod AlgebraicGeometry.Scheme instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts AlgebraicGeometry.instCartesianMonoidalCategoryScheme Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype isSeparated_iff_isClosedImmersion_prod_lift
instIsClosedImmersionιOfIsSeparated 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.Limits.equalizer AlgebraicGeometry.Scheme instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits AlgebraicGeometry.instHasFiniteLimitsScheme CategoryTheory.Limits.instFinCategoryWalkingParallelPair CategoryTheory.Limits.parallelPair CategoryTheory.Limits.equalizer.ι	—	CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits AlgebraicGeometry.instHasFiniteLimitsScheme CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.IsPullback.flip CategoryTheory.Limits.isPullback_equalizer_prod instIsClosedImmersionLiftIdOfIsSeparated
instIsSeparatedOfIsAffine 📖	mathematical	—	IsSeparated	—	AlgebraicGeometry.instHasTerminalScheme AlgebraicGeometry.IsSeparated.of_isAffineHom AlgebraicGeometry.isAffineHom_of_isAffine AlgebraicGeometry.instIsAffineTerminalScheme
instIsSeparatedOfIsSeparated 📖	mathematical	—	AlgebraicGeometry.IsSeparated	—	AlgebraicGeometry.IsSeparated.of_comp AlgebraicGeometry.instHasTerminalScheme CategoryTheory.Limits.terminal.comp_from IsSeparated.isSeparated_terminal_from
instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated 📖	mathematical	—	QuasiSeparatedSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated AlgebraicGeometry.instHasTerminalScheme AlgebraicGeometry.quasiSeparatedSpace_of_isAffine AlgebraicGeometry.instIsAffineTerminalScheme AlgebraicGeometry.IsSeparated.instQuasiSeparated IsSeparated.isSeparated_terminal_from
isSeparated_iff 📖	mathematical	—	IsSeparated AlgebraicGeometry.IsSeparated CategoryTheory.Limits.terminal AlgebraicGeometry.Scheme instCategory AlgebraicGeometry.instHasTerminalScheme CategoryTheory.Limits.terminal.from	—	AlgebraicGeometry.instHasTerminalScheme
isSeparated_iff_isClosedImmersion_prod_lift 📖	mathematical	—	IsSeparated AlgebraicGeometry.IsClosedImmersion CategoryTheory.Limits.prod AlgebraicGeometry.Scheme instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts AlgebraicGeometry.instCartesianMonoidalCategoryScheme Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype AlgebraicGeometry.instHasTerminalScheme isSeparated_iff Pullback.instHasPullback AlgebraicGeometry.isSeparated_iff Pullback.instHasPullbacks CategoryTheory.MorphismProperty.cancel_right_of_respectsIso AlgebraicGeometry.IsClosedImmersion.respectsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Limits.pullback.diagonal_fst CategoryTheory.Category.assoc prodIsoPullback_hom_fst CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullback.diagonal_snd prodIsoPullback_hom_snd

AlgebraicGeometry.Scheme.IsSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparated_terminal_from 📖	mathematical	—	AlgebraicGeometry.IsSeparated CategoryTheory.Limits.terminal AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.instHasTerminalScheme CategoryTheory.Limits.terminal.from	—	—

AlgebraicGeometry.Scheme.Pullback

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagonalCoverDiagonalRange_eq_top_of_injective 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	diagonalCoverDiagonalRange Top.top AlgebraicGeometry.Scheme.Opens CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instHasPullback top_le_iff AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange isOpen_iUnion TopologicalSpace.Opens.is_open' AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.pullback.condition AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage AlgebraicGeometry.Scheme.Cover.covers exists_preimage_pullback diagonalCover_map range_map AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.instIsOpenImmersionF
range_diagonal_subset_diagonalCoverDiagonalRange 📖	mathematical	—	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.diagonal SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier diagonalCoverDiagonalRange	—	instHasPullback AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange isOpen_iUnion TopologicalSpace.Opens.is_open' AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage AlgebraicGeometry.Scheme.Cover.covers exists_preimage_pullback AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullback.diagonal_fst_assoc CategoryTheory.Limits.pullback.diagonal_fst CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback.diagonal_snd_assoc CategoryTheory.Limits.pullback.diagonal_snd

---

← Back to Index