Documentation Verification Report

ZariskisMainTheorem

📁 Source: Mathlib/AlgebraicGeometry/ZariskisMainTheorem.lean

Statistics

Metric	Count
Definitions `quasiFiniteLocus`	1
Theorems `eq_proper_inf_monomorphisms`, `iff_isProper_and_mono`, `eq_proper_inf_locallyQuasiFinite`, `iff_isProper_and_locallyQuasiFinite`, `of_isProper_of_locallyQuasiFinite`, `exists_isIso_morphismRestrict_toNormalization`, `exists_mem_and_isIso_morphismRestrict_toNormalization`, `isOpen_quasiFiniteAt`, `mem_quasiFiniteLocus`, `quasiFiniteLocus_comp`, `quasiFiniteLocus_eq_top`, `quasiFiniteLocus_eq_top_iff`, `exists_etale_isCompl_of_quasiFiniteAt`, `exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage`, `exists_isFinite_morphismRestrict_of_finite_preimage_singleton`, `instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization`, `instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType`, `instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus`, `instUniversallyClosedToNormalization`	19
Total	20

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_etale_isCompl_of_quasiFiniteAt` 📖	mathematical	`DFunLike.coe` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	`Etale` `Set` `Set.instMembership` `Set.range` `IsCompl` `Scheme.Opens` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `TopologicalSpace.Opens.instPartialOrder` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CompleteLattice.toBoundedOrder` `TopologicalSpace.Opens.instCompleteLattice` `IsFinite` `Scheme.Opens.toScheme` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Scheme.Opens.ι` `CategoryTheory.Limits.pullback.snd` `CategoryTheory.Limits.pullback.fst` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	`Scheme.Pullback.instHasPullback` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `Scheme.isBasis_affineOpens` `Set.mem_univ` `isOpen_univ` `TopologicalSpace.Opens.is_open'` `Scheme.Hom.finiteType_appLE` `Homeomorph.injective` `CategoryTheory.Iso.isIso_inv` `IsAffineOpen.toSpecΓ_isoSpec_inv` `CategoryTheory.Category.id_comp` `Scheme.Opens.toSpecΓ_SpecMap_appLE` `CategoryTheory.Category.assoc` `CategoryTheory.Category.comp_id` `Scheme.Hom.resLE_comp_ι` `PrimeSpectrum.isPrime` `Scheme.Hom.QuasiFiniteAt.quasiFiniteAt` `Algebra.to_smulCommClass` `IsScalarTower.right` `RingHom.instRingHomClass` `Ideal.over_def` `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq` `RingHom.finite_algebraMap` `RingHom.etale_algebraMap` `HasRingHomProperty.Spec_iff` `Etale.instHasRingHomPropertyEtale` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `CategoryTheory.Limits.hasPullback_symmetry` `CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst` `pullbackSpecIso_inv_snd` `IsAffineOpen.SpecMap_appLE_fromSpec` `IsOpenImmersion.comp` `IsOpenImmersion.of_isIso` `CategoryTheory.Iso.isIso_hom` `Scheme.pullback_map_isOpenImmersion` `IsAffineOpen.isOpenImmersion_fromSpec` `CategoryTheory.IsIso.id` `IsOpenImmersion.mono` `Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap` `Scheme.Hom.opensRange_comp` `TopologicalSpace.Opens.ext` `PrimeSpectrum.localization_away_comap_range` `Localization.isLocalization` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `Scheme.instHasPullbacksIsOpenImmersion` `HasAffineProperty.instIsZariskiLocalAtTarget` `IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `pullbackSpecIso_inv_fst` `IsOpenImmersion.isoOfRangeEq.congr_simp` `IsOpenImmersion.isoOfRangeEq_hom_fac_assoc` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd` `IsFinite.of_comp` `IsSeparated.instSndScheme` `Scheme.Opens.range_ι` `IsClosedMap.isClosed_range` `Scheme.Hom.isClosedMap` `IsProper.toUniversallyClosed` `IsProper.instOfIsFinite` `Etale.etale_comp` `Etale.instOfIsOpenImmersion` `PrimeSpectrum.ext` `IsAffineOpen.fromSpec_primeIdealOf` `Set.inter_compl_self` `Set.union_compl_self` `Ideal.IsPrime.comap` `Mathlib.Tactic.Reassoc.eq_whisker'`
`exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage` 📖	mathematical	—	`TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsFinite` `Scheme.Opens.toScheme` `Scheme.Hom.image` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Scheme.Hom.imageι` `morphismRestrict`	—	`IsProper.of_comp` `Scheme.Hom.toImage_imageι_assoc` `IsProper.toUniversallyClosed` `UniversallyClosed.of_comp_surjective` `Surjective.of_universallyClosed_of_isDominant` `instUniversallyClosedToImage` `Scheme.instIsDominantToImageOfQuasiCompact` `instQuasiCompactOfUniversallyClosed` `IsSeparated.instCompScheme` `IsProper.toIsSeparated` `IsProper.instOfIsFinite` `IsFinite.instOfIsClosedImmersion` `IsClosedImmersion.instSubschemeι` `locallyOfFiniteType_comp` `IsProper.toLocallyOfFiniteType` `exists_isFinite_morphismRestrict_of_finite_preimage_singleton` `Set.Finite.of_finite_image` `Set.Finite.subset` `Scheme.Hom.surjective` `Scheme.Hom.toImage_imageι` `Function.Injective.injOn` `Topology.IsEmbedding.injective` `Topology.IsClosedEmbedding.toIsEmbedding` `Scheme.Hom.isClosedEmbedding`
`exists_isFinite_morphismRestrict_of_finite_preimage_singleton` 📖	mathematical	—	`TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsFinite` `Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `morphismRestrict`	—	`IsProper.toLocallyOfFiniteType` `IsClosed.isOpen_compl` `Scheme.Hom.isClosedMap` `IsProper.toUniversallyClosed` `IsOpen.isClosed_compl` `TopologicalSpace.Opens.isOpen` `Equiv.finite_iff` `Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber` `isOpen_discrete` `instDiscreteTopologyOfFiniteOfJacobsonSpace` `instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType` `Set.image_congr` `instLocallyOfFiniteTypeMorphismRestrict` `Scheme.Hom.quasiFiniteLocus_eq_top_iff` `TopologicalSpace.Opens.ext` `Set.ext` `Scheme.Hom.quasiFiniteAt_comp_iff` `instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective` `instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `locallyOfFinitePresentation_of_isOpenImmersion` `Scheme.Opens.instIsOpenImmersionι` `instUniversallyInjectiveOfMonoScheme` `IsOpenImmersion.mono` `morphismRestrict_ι` `Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion` `IsFinite.of_isProper_of_locallyQuasiFinite` `IsProper.instMorphismRestrict`
`instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization` 📖	mathematical	—	`IsOpenImmersion` `Scheme.Opens.toScheme` `Scheme.Hom.quasiFiniteLocus` `Scheme.Hom.normalization` `IsSeparated.instQuasiSeparated` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Scheme.Opens.ι` `Scheme.Hom.toNormalization`	—	`IsSeparated.instQuasiSeparated` `Scheme.Hom.exists_isIso_morphismRestrict_toNormalization` `SetLike.coe_injective` `morphismRestrict_ι` `Scheme.isoOfEq_hom_ι_assoc` `IsOpenImmersion.comp` `IsOpenImmersion.of_isIso` `CategoryTheory.Iso.isIso_hom` `Scheme.Opens.instIsOpenImmersionι`
`instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType` 📖	mathematical	—	`IsOpenImmersion` `Scheme.Hom.normalization` `IsSeparated.instQuasiSeparated` `Scheme.Hom.toNormalization`	—	`IsSeparated.instQuasiSeparated` `Scheme.Hom.quasiFiniteLocus_eq_top` `Scheme.isoOfEq_inv_ι_assoc` `Scheme.toIso_inv_ι_assoc` `IsOpenImmersion.comp` `IsOpenImmersion.of_isIso` `CategoryTheory.Iso.isIso_inv` `instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization`
`instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus` 📖	mathematical	—	`LocallyQuasiFinite` `Scheme.Opens.toScheme` `Scheme.Hom.quasiFiniteLocus` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Scheme.Opens.ι`	—	`locallyOfFiniteType_comp` `instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `locallyOfFinitePresentation_of_isOpenImmersion` `Scheme.Opens.instIsOpenImmersionι` `Scheme.Hom.quasiFiniteLocus_eq_top_iff` `Scheme.Hom.quasiFiniteLocus_comp` `Scheme.Opens.ι_preimage_self`
`instUniversallyClosedToNormalization` 📖	mathematical	—	`UniversallyClosed` `Scheme.Hom.normalization` `instQuasiCompactOfUniversallyClosed` `Scheme.Hom.toNormalization`	—	`instQuasiCompactOfUniversallyClosed` `Scheme.Hom.toNormalization_fromNormalization` `UniversallyClosed.of_comp_of_isSeparated` `IsSeparated.of_isAffineHom` `IsIntegralHom.toIsAffineHom` `Scheme.Hom.instIsIntegralHomFromNormalization`

AlgebraicGeometry.IsClosedImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_proper_inf_monomorphisms` 📖	mathematical	—	`AlgebraicGeometry.IsClosedImmersion` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.IsProper` `CategoryTheory.MorphismProperty.monomorphisms`	—	`iff_isProper_and_mono`
`iff_isProper_and_mono` 📖	mathematical	—	`AlgebraicGeometry.IsClosedImmersion` `AlgebraicGeometry.IsProper` `CategoryTheory.Mono` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`AlgebraicGeometry.instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective` `AlgebraicGeometry.IsProper.toLocallyOfFiniteType` `AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme` `iff_isFinite_and_mono` `AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite`

AlgebraicGeometry.IsFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_proper_inf_locallyQuasiFinite` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.IsProper` `AlgebraicGeometry.LocallyQuasiFinite`	—	`iff_isProper_and_locallyQuasiFinite`
`iff_isProper_and_locallyQuasiFinite` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `AlgebraicGeometry.IsProper` `AlgebraicGeometry.LocallyQuasiFinite`	—	`AlgebraicGeometry.IsProper.instOfIsFinite` `AlgebraicGeometry.instLocallyQuasiFiniteOfIsFinite` `of_isProper_of_locallyQuasiFinite`
`of_isProper_of_locallyQuasiFinite` 📖	mathematical	—	`AlgebraicGeometry.IsFinite`	—	`AlgebraicGeometry.instQuasiCompactOfUniversallyClosed` `AlgebraicGeometry.IsProper.toUniversallyClosed` `AlgebraicGeometry.IsSeparated.instQuasiSeparated` `AlgebraicGeometry.IsProper.toIsSeparated` `AlgebraicGeometry.isIso_iff_isOpenImmersion_and_surjective` `AlgebraicGeometry.instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType` `AlgebraicGeometry.IsProper.toLocallyOfFiniteType` `AlgebraicGeometry.Surjective.of_universallyClosed_of_isDominant` `AlgebraicGeometry.instUniversallyClosedToNormalization` `AlgebraicGeometry.Scheme.Hom.instIsDominantToNormalization` `iff_isIntegralHom_and_locallyOfFiniteType` `AlgebraicGeometry.Scheme.Hom.toNormalization_fromNormalization` `AlgebraicGeometry.IsIntegralHom.instCompScheme` `instIsIntegralHom` `instOfIsClosedImmersion` `AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme` `AlgebraicGeometry.Scheme.Hom.instIsIntegralHomFromNormalization`

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
`quasiFiniteLocus` 📖	CompOp	6 math math: `quasiFiniteLocus_comp`, `AlgebraicGeometry.instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus`, `quasiFiniteLocus_eq_top`, `AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization`, `quasiFiniteLocus_eq_top_iff`, `mem_quasiFiniteLocus`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isIso_morphismRestrict_toNormalization` 📖	mathematical	—	`CategoryTheory.IsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `normalization` `AlgebraicGeometry.IsSeparated.instQuasiSeparated` `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` `toLRSHom'` `toNormalization` `AlgebraicGeometry.morphismRestrict` `TopologicalSpace.Opens.carrier` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `setOf` `QuasiFiniteAt`	—	`AlgebraicGeometry.IsSeparated.instQuasiSeparated` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms` `AlgebraicGeometry.IsOpenImmersion.comp` `AlgebraicGeometry.Scheme.homOfLE_ι` `opensRange.congr_simp` `AlgebraicGeometry.Scheme.Opens.opensRange_ι` `Set.ext` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `TopologicalSpace.Opens.isOpen` `AlgebraicGeometry.instIsOpenImmersionHomOfLE` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `AlgebraicGeometry.isAffineOpen_opensRange` `opensRange_comp` `LE.le.trans` `image_le_opensRange` `comp_preimage` `AlgebraicGeometry.morphismRestrict_ι` `AlgebraicGeometry.Scheme.opensRange_homOfLE` `preimage_image_eq` `image_preimage_eq_opensRange_inf` `inf_eq_right` `Set.mem_univ` `isOpen_univ` `AlgebraicGeometry.exists_basicOpen_le_affine_inter` `AlgebraicGeometry.IsAffineOpen.preimage` `AlgebraicGeometry.IsIntegralHom.toIsAffineHom` `instIsIntegralHomFromNormalization` `toNormalization_fromNormalization` `Eq.ge` `preimage_basicOpen` `AlgebraicGeometry.IsAffineOpen.basicOpen` `Eq.trans_le` `AlgebraicGeometry.Scheme.basicOpen_le` `le_imp_le_of_le_of_le` `preimage_mono` `le_refl` `le_rfl` `app_eq_appLE` `appLE_comp_appLE` `appLE.congr_simp` `image_injective` `instIsIsoCommRingCatApp` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_mono` `Eq.le` `AlgebraicGeometry.image_morphismRestrict_preimage` `inf_of_le_right` `AlgebraicGeometry.morphismRestrict_appLE` `finiteType_appLE` `CommRingCat.hom_comp` `RingHom.RespectsIso.cancel_right_isIso` `RingHom.QuasiFinite.respectsIso` `RingHom.QuasiFinite.of_isIntegral_of_finiteType` `AlgebraicGeometry.IsIntegralHom.isIntegral_app` `AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen` `RingHom.finiteType_respectsIso` `comp_apply` `RingHom.QuasiFinite.of_comp` `CommRingCat.Colimits.hasColimits_commRingCat` `germ_stalkMap` `TopCat.Presheaf.germ_res` `appLE_map_assoc` `RingHom.QuasiFinite.comp` `PrimeSpectrum.isPrime` `AlgebraicGeometry.IsAffineOpen.isLocalization_stalk` `RingHom.algebraMap_toAlgebra` `RingHom.quasiFinite_algebraMap` `Algebra.QuasiFinite.of_isLocalization` `IsScalarTower.left` `Algebra.IsUnramifiedAt.instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified` `Algebra.EssFiniteType.of_finiteType` `Algebra.FiniteType.of_finitePresentation` `Algebra.Etale.finitePresentation` `Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat` `Algebra.IsStandardSmoothOfRelativeDimension.id` `Algebra.FormallyUnramified.inst` `TopologicalSpace.Opens.coe_iSup` `Set.preimage_iUnion` `exists_mem_and_isIso_morphismRestrict_toNormalization`
`exists_mem_and_isIso_morphismRestrict_toNormalization` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `normalization` `AlgebraicGeometry.IsSeparated.instQuasiSeparated` `AlgebraicGeometry.Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `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` `toLRSHom'` `toNormalization` `CategoryTheory.IsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.morphismRestrict`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsSeparated.instQuasiSeparated` `AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt` `AlgebraicGeometry.instQuasiCompactSndScheme` `AlgebraicGeometry.instQuasiSeparatedSndScheme` `eq_compl_iff_isCompl` `IsCompl.symm` `IsCompl.map` `FrameHomClass.toBoundedLatticeHomClass` `FrameHom.instFrameHomClass` `AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion` `AlgebraicGeometry.IsImmersion.toIsPreimmersion` `AlgebraicGeometry.IsImmersion.instOfIsOpenImmersion` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `AlgebraicGeometry.Scheme.Opens.range_ι` `eq_compl_comm` `TopologicalSpace.Opens.isOpen` `TopologicalSpace.Opens.is_open'` `AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl` `AlgebraicGeometry.Scheme.Opens.opensRange_ι` `AlgebraicGeometry.quasiCompact_comp` `AlgebraicGeometry.instQuasiCompactOfUniversallyClosed` `AlgebraicGeometry.IsProper.toUniversallyClosed` `AlgebraicGeometry.IsProper.instOfIsFinite` `AlgebraicGeometry.IsFinite.instOfIsClosedImmersion` `AlgebraicGeometry.quasiSeparated_comp` `AlgebraicGeometry.IsProper.toIsSeparated` `AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instIsIsoToNormalizationOfIsIntegralHom` `AlgebraicGeometry.IsFinite.instIsIntegralHom` `AlgebraicGeometry.instIsOpenImmersionInlScheme` `AlgebraicGeometry.Scheme.Opens.ι_apply` `comp_apply` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.comp_inv_eq` `instIsIntegralHomFromNormalization` `CategoryTheory.Limits.coprod.map_desc` `toNormalization_normalizationDesc` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.isIso_comp_right_iff` `AlgebraicGeometry.instIsIsoSchemeMorphismRestrict` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.morphismRestrict_comp` `CategoryTheory.Iso.isIso_inv` `le_antisymm` `CanLift.prf` `Subtype.canLift` `Eq.ge` `CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom` `toNormalization_normalizationDesc_assoc` `CategoryTheory.Limits.coprod.map_map` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.Category.comp_id` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Limits.coprod.inr_map` `Set.disjoint_iff_forall_ne` `IsCompl.disjoint` `AlgebraicGeometry.isCompl_range_inl_inr` `AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso` `isIso_toLRSHom` `inv_image` `SetLike.coe_subset_coe` `instIsConcreteLE` `AlgebraicGeometry.IsOpenImmersion.comp` `opensFunctor.congr_simp` `opensRange.congr_simp` `Set.range_comp` `Set.subset_preimage_image` `CategoryTheory.Iso.inv_comp_eq` `CategoryTheory.cancel_mono` `AlgebraicGeometry.IsOpenImmersion.mono` `AlgebraicGeometry.morphismRestrict_ι` `AlgebraicGeometry.Scheme.isoOfEq_inv_ι_assoc` `CategoryTheory.Limits.coprod.inl_map` `AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac` `isOpenMap` `AlgebraicGeometry.UniversallyOpen.instCompScheme` `AlgebraicGeometry.UniversallyOpen.instOfIsOpenImmersion` `instIsIsoNormalizationPullbackOfSmooth` `AlgebraicGeometry.Etale.instSmooth` `AlgebraicGeometry.UniversallyOpen.fst` `AlgebraicGeometry.UniversallyOpen.of_flat` `AlgebraicGeometry.instFlatOfSmooth` `AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth` `toNormalization_normalizationPullback_fst` `coe_resLE_apply` `CategoryTheory.IsPullback.of_bot` `resLE_comp_ι` `CategoryTheory.IsPullback.paste_vert` `AlgebraicGeometry.isPullback_morphismRestrict` `toNormalization_fromNormalization` `CategoryTheory.IsPullback.of_right` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.IsPullback.of_iso'` `CategoryTheory.Limits.pullback.hom_ext` `normalizationPullback_snd` `AlgebraicGeometry.morphismRestrict_ι_assoc` `resLE_comp_ι_assoc` `CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong` `AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget` `AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact` `AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage` `AlgebraicGeometry.Flat.instResLE` `AlgebraicGeometry.Flat.comp` `AlgebraicGeometry.Flat.instOfIsOpenImmersion` `AlgebraicGeometry.Flat.instFstScheme` `AlgebraicGeometry.instLocallyOfFinitePresentationResLE` `AlgebraicGeometry.locallyOfFinitePresentation_comp` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `AlgebraicGeometry.instLocallyOfFinitePresentationFstScheme`
`isOpen_quasiFiniteAt` 📖	mathematical	—	`IsOpen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `setOf` `QuasiFiniteAt`	—	`AlgebraicGeometry.instQuasiCompactOfIsAffineHom` `AlgebraicGeometry.IsSeparated.instQuasiSeparated` `AlgebraicGeometry.IsSeparated.of_isAffineHom` `exists_isIso_morphismRestrict_toNormalization` `TopologicalSpace.Opens.is_open'` `isOpen_iff_forall_mem_open` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `Set.mem_univ` `isOpen_univ` `AlgebraicGeometry.isAffineHom_of_isAffine` `quasiFiniteAt_comp_iff_of_isOpenImmersion` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `resLE_comp_ι` `quasiFiniteAt_comp_iff` `AlgebraicGeometry.instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme` `AlgebraicGeometry.IsOpenImmersion.mono` `Topology.IsOpenEmbedding.isOpenMap` `IsOpen.isOpenEmbedding_subtypeVal` `AlgebraicGeometry.instLocallyOfFiniteTypeResLE`
`mem_quasiFiniteLocus` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `quasiFiniteLocus` `QuasiFiniteAt`	—	—
`quasiFiniteLocus_comp` 📖	mathematical	—	`quasiFiniteLocus` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.locallyOfFiniteType_comp` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `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` `toLRSHom'`	—	`TopologicalSpace.Opens.ext` `AlgebraicGeometry.locallyOfFiniteType_comp` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `Set.ext`
`quasiFiniteLocus_eq_top` 📖	mathematical	—	`quasiFiniteLocus` `Top.top` `AlgebraicGeometry.Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`top_le_iff` `quasiFiniteAt`
`quasiFiniteLocus_eq_top_iff` 📖	mathematical	—	`quasiFiniteLocus` `Top.top` `AlgebraicGeometry.Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AlgebraicGeometry.LocallyQuasiFinite`	—	`AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton` `isDiscrete_iff_discreteTopology` `discreteTopology_iff_isOpen_singleton` `Homeomorph.isOpen_image` `Set.image_singleton` `IsClopen.isOpen` `QuasiFiniteAt.isClopen_singleton_asFiber` `Eq.ge` `Set.mem_univ` `quasiFiniteLocus_eq_top`

---

← Back to Index