QuasiFinite

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

Statistics

Metric	Count
Definitions `LocallyQuasiFinite`, `QuasiFiniteAt`	2
Theorems `finite_preimage_singleton`, `of_locallyQuasiFinite`, `of_locallyQuasiFinite`, `comp_iff`, `of_comp`, `of_fiberToSpecResidueField`, `of_finite_preimage_singleton`, `of_injective`, `of_isFinite_fiberToSpecResidueField`, `quasiFinite_appLE`, `isClopen_singleton_asFiber`, `quasiFiniteAt`, `finite_preimage`, `finite_preimage_singleton`, `isDiscrete_preimage`, `isDiscrete_preimage_singleton`, `quasiFiniteAt`, `quasiFiniteAt_comp_iff`, `quasiFiniteAt_comp_iff_of_isOpenImmersion`, `quasiFiniteAt_iff`, `quasiFiniteAt_iff_isOpen_singleton_asFiber`, `tendsto_cofinite_cofinite`, `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite`, `instIsArtinianSchemeFiberOfLocallyQuasiFiniteOfQuasiCompact`, `instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact`, `instIsLocallyArtinianFiberOfLocallyQuasiFinite`, `instIsMultiplicativeSchemeLocallyQuasiFinite`, `instIsStableUnderBaseChangeSchemeLocallyQuasiFinite`, `instIsStableUnderCompositionSchemeLocallyQuasiFinite`, `instLocallyQuasiFiniteCompScheme`, `instLocallyQuasiFiniteFstScheme`, `instLocallyQuasiFiniteMorphismRestrict`, `instLocallyQuasiFiniteOfIsFinite`, `instLocallyQuasiFiniteOfIsImmersion`, `instLocallyQuasiFiniteOfIsPreimmersion`, `instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective`, `instLocallyQuasiFiniteResLE`, `instLocallyQuasiFiniteSndScheme`, `instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion`, `locallyQuasiFinite_iff`, `locallyQuasiFinite_iff_finite_preimage_singleton`, `locallyQuasiFinite_iff_isDiscrete_preimage_singleton`, `locallyQuasiFinite_iff_isFinite_fiber`	43
Total	45

AlgebraicGeometry

Definitions

Name	Category	Theorems
`LocallyQuasiFinite` 📖	CompData	27 math math: `instLocallyQuasiFiniteSndScheme`, `instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus`, `instLocallyQuasiFiniteFstScheme`, `locallyQuasiFinite_iff`, `LocallyQuasiFinite.comp_iff`, `instIsStableUnderBaseChangeSchemeLocallyQuasiFinite`, `IsFinite.eq_proper_inf_locallyQuasiFinite`, `instLocallyQuasiFiniteOfIsFinite`, `instIsStableUnderCompositionSchemeLocallyQuasiFinite`, `locallyQuasiFinite_iff_isFinite_fiber`, `instLocallyQuasiFiniteOfIsPreimmersion`, `instLocallyQuasiFiniteMorphismRestrict`, `instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective`, `LocallyQuasiFinite.of_injective`, `instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion`, `Scheme.Hom.quasiFiniteLocus_eq_top_iff`, `locallyQuasiFinite_iff_isDiscrete_preimage_singleton`, `Scheme.Hom.quasiFiniteAt_iff`, `instIsMultiplicativeSchemeLocallyQuasiFinite`, `instLocallyQuasiFiniteResLE`, `IsFinite.iff_isProper_and_locallyQuasiFinite`, `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite`, `LocallyQuasiFinite.of_finite_preimage_singleton`, `locallyQuasiFinite_iff_finite_preimage_singleton`, `instLocallyQuasiFiniteCompScheme`, `LocallyQuasiFinite.of_comp`, `instLocallyQuasiFiniteOfIsImmersion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` 📖	mathematical	—	`HasRingHomProperty` `LocallyQuasiFinite` `RingHom.QuasiFinite`	—	`RingHom.QuasiFinite.propertyIsLocal` `CategoryTheory.MorphismProperty.ext`
`instIsArtinianSchemeFiberOfLocallyQuasiFiniteOfQuasiCompact` 📖	mathematical	—	`IsArtinianScheme` `Scheme.Hom.fiber`	—	`instIsLocallyArtinianFiberOfLocallyQuasiFinite` `instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact`
`instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact` 📖	mathematical	—	`IsFinite` `Scheme.Hom.fiber` `Spec` `Scheme.residueField` `Scheme.Hom.fiberToSpecResidueField`	—	`IsFinite.of_locallyQuasiFinite` `instLocallyQuasiFiniteSndScheme` `instQuasiCompactSndScheme` `IsArtinianScheme.toIsLocallyArtinian` `instIsArtinianSchemeSpecOfIsArtinianRingCarrier` `instIsArtinianOfIsSemisimpleModuleOfFinite` `CommRingCat.Colimits.hasColimits_commRingCat` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`instIsLocallyArtinianFiberOfLocallyQuasiFinite` 📖	mathematical	—	`IsLocallyArtinian` `Scheme.Hom.fiber`	—	`IsLocallyArtinian.of_locallyQuasiFinite` `instLocallyQuasiFiniteSndScheme` `IsArtinianScheme.toIsLocallyArtinian` `instIsArtinianSchemeSpecOfIsArtinianRingCarrier` `instIsArtinianOfIsSemisimpleModuleOfFinite` `CommRingCat.Colimits.hasColimits_commRingCat` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`instIsMultiplicativeSchemeLocallyQuasiFinite` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `LocallyQuasiFinite`	—	`instLocallyQuasiFiniteOfIsImmersion` `IsImmersion.instOfIsClosedImmersion` `IsClosedImmersion.instOfIsIsoScheme` `CategoryTheory.IsIso.id` `instIsStableUnderCompositionSchemeLocallyQuasiFinite`
`instIsStableUnderBaseChangeSchemeLocallyQuasiFinite` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `LocallyQuasiFinite`	—	`HasRingHomProperty.isStableUnderBaseChange` `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `RingHom.QuasiFinite.isStableUnderBaseChange`
`instIsStableUnderCompositionSchemeLocallyQuasiFinite` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `LocallyQuasiFinite`	—	`HasRingHomProperty.stableUnderComposition` `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `RingHom.QuasiFinite.stableUnderComposition`
`instLocallyQuasiFiniteCompScheme` 📖	mathematical	—	`LocallyQuasiFinite` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.comp_mem` `instIsStableUnderCompositionSchemeLocallyQuasiFinite`
`instLocallyQuasiFiniteFstScheme` 📖	mathematical	—	`LocallyQuasiFinite` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.MorphismProperty.pullback_fst` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `instIsStableUnderBaseChangeSchemeLocallyQuasiFinite`
`instLocallyQuasiFiniteMorphismRestrict` 📖	mathematical	—	`LocallyQuasiFinite` `Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `Scheme.Opens` `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'` `morphismRestrict`	—	`IsZariskiLocalAtTarget.restrict` `HasRingHomProperty.instIsZariskiLocalAtTarget` `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite`
`instLocallyQuasiFiniteOfIsFinite` 📖	mathematical	—	`LocallyQuasiFinite`	—	`HasRingHomProperty.eq_affineLocally` `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `Eq.le` `targetAffineLocally_affineAnd_eq_affineLocally` `RingHom.QuasiFinite.propertyIsLocal` `targetAffineLocally_affineAnd_le` `RingHom.QuasiFinite.of_finite` `HasAffineProperty.eq_targetAffineLocally` `IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop`
`instLocallyQuasiFiniteOfIsImmersion` 📖	mathematical	—	`LocallyQuasiFinite`	—	`Scheme.Hom.liftCoborder_ι` `HasRingHomProperty.of_isOpenImmersion` `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `RingHom.HoldsForLocalizationAway.containsIdentities` `RingHom.QuasiFinite.holdsForLocalizationAway` `Scheme.Opens.instIsOpenImmersionι` `instLocallyQuasiFiniteCompScheme` `instLocallyQuasiFiniteOfIsFinite` `IsFinite.instOfIsClosedImmersion` `instIsClosedImmersionLiftCoborder`
`instLocallyQuasiFiniteOfIsPreimmersion` 📖	mathematical	—	`LocallyQuasiFinite`	—	`LocallyQuasiFinite.of_fiberToSpecResidueField` `IsClosedImmersion.of_isPreimmersion` `IsPreimmersion.instSndScheme` `isClosed_discrete` `IsLocallyArtinian.discreteTopology` `IsArtinianScheme.toIsLocallyArtinian` `instIsArtinianSchemeSpecOfIsArtinianRingCarrier` `instIsArtinianOfIsSemisimpleModuleOfFinite` `CommRingCat.Colimits.hasColimits_commRingCat` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `instLocallyQuasiFiniteOfIsImmersion` `IsImmersion.instOfIsClosedImmersion`
`instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective` 📖	mathematical	—	`LocallyQuasiFinite`	—	`LocallyQuasiFinite.of_injective` `Scheme.Hom.injective`
`instLocallyQuasiFiniteResLE` 📖	mathematical	`Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	`LocallyQuasiFinite` `Scheme.Opens.toScheme` `Scheme.Hom.resLE`	—	`instLocallyQuasiFiniteCompScheme` `instLocallyQuasiFiniteOfIsImmersion` `IsImmersion.instOfIsOpenImmersion` `instIsOpenImmersionHomOfLE` `instLocallyQuasiFiniteMorphismRestrict`
`instLocallyQuasiFiniteSndScheme` 📖	mathematical	—	`LocallyQuasiFinite` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.MorphismProperty.pullback_snd` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `instIsStableUnderBaseChangeSchemeLocallyQuasiFinite`
`instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion` 📖	mathematical	—	`CategoryTheory.MorphismProperty.Respects` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `LocallyQuasiFinite` `IsOpenImmersion`	—	`HasRingHomProperty.respects_isOpenImmersion` `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway` `RingHom.QuasiFinite.stableUnderComposition` `RingHom.QuasiFinite.holdsForLocalizationAway`
`locallyQuasiFinite_iff` 📖	mathematical	—	`LocallyQuasiFinite` `RingHom.QuasiFinite` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE`	—	—
`locallyQuasiFinite_iff_finite_preimage_singleton` 📖	mathematical	—	`LocallyQuasiFinite` `Set.Finite` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `Set` `Set.instSingletonSet`	—	`Scheme.Hom.finite_preimage_singleton` `LocallyQuasiFinite.of_finite_preimage_singleton`
`locallyQuasiFinite_iff_isDiscrete_preimage_singleton` 📖	mathematical	—	`LocallyQuasiFinite` `IsDiscrete` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `Set` `Set.instSingletonSet`	—	`Scheme.Hom.isDiscrete_preimage_singleton` `Spec.map_surjective` `instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `Algebra.QuasiFinite.iff_finite_comap_preimage_singleton` `instHasRingHomPropertyLocallyOfFiniteTypeFiniteType` `IsCompact.finite` `Scheme.Hom.isCompact_preimage_singleton` `instQuasiCompactOfIsAffineHom` `isAffineHom_of_isAffine` `isAffine_Spec` `IsZariskiLocalAtSource.iff_of_openCover` `HasRingHomProperty.instIsZariskiLocalAtSource` `locallyOfFiniteType_comp` `instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `locallyOfFinitePresentation_of_isOpenImmersion` `Scheme.instIsOpenImmersionF` `IsDiscrete.preimage` `Continuous.continuousOn` `Scheme.Hom.continuous` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding` `Scheme.Hom.isOpenEmbedding` `Scheme.local_affine` `Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `isOpenImmersion_stableUnderBaseChange` `Scheme.Pullback.instHasPullback` `IsZariskiLocalAtTarget.iff_of_openCover` `HasRingHomProperty.instIsZariskiLocalAtTarget` `instLocallyOfFiniteTypeSndScheme` `Set.ext` `CategoryTheory.Limits.pullback.condition` `IsOpenImmersion.instFstScheme`
`locallyQuasiFinite_iff_isFinite_fiber` 📖	mathematical	—	`LocallyQuasiFinite` `IsFinite` `Scheme.Hom.fiber` `Spec` `Scheme.residueField` `Scheme.Hom.fiberToSpecResidueField`	—	`instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact` `LocallyQuasiFinite.of_fiberToSpecResidueField` `instLocallyQuasiFiniteOfIsFinite`

AlgebraicGeometry.IsFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_preimage_singleton` 📖	mathematical	—	`Set.Finite` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `Set.preimage` `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'` `Set` `Set.instSingletonSet`	—	`AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton`
`of_locallyQuasiFinite` 📖	mathematical	—	`AlgebraicGeometry.IsFinite`	—	`AlgebraicGeometry.Spec.map_surjective` `Module.Finite.of_quasiFinite` `RingHom.QuasiFinite.toAlgebra` `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `AlgebraicGeometry.IsLocallyArtinian.of_locallyQuasiFinite` `AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace` `AlgebraicGeometry.Scheme.compactSpace_of_isAffine` `AlgebraicGeometry.isAffine_Spec` `AlgebraicGeometry.instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat` `AlgebraicGeometry.IsArtinianScheme.finite` `AlgebraicGeometry.IsLocallyArtinian.discreteTopology` `AlgebraicGeometry.IsArtinianScheme.toIsLocallyArtinian` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `CategoryTheory.Iso.isIso_inv` `AlgebraicGeometry.instLocallyQuasiFiniteCompScheme` `AlgebraicGeometry.instLocallyQuasiFiniteOfIsImmersion` `AlgebraicGeometry.IsImmersion.instOfIsClosedImmersion` `AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme` `AlgebraicGeometry.quasiCompact_comp` `AlgebraicGeometry.instQuasiCompactOfUniversallyClosed` `AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersion` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.instLocallyQuasiFiniteSndScheme` `AlgebraicGeometry.instQuasiCompactSndScheme` `AlgebraicGeometry.instIsLocallyArtinianXScheme` `AlgebraicGeometry.Scheme.local_affine`

AlgebraicGeometry.IsLocallyArtinian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_locallyQuasiFinite` 📖	mathematical	—	`AlgebraicGeometry.IsLocallyArtinian`	—	`AlgebraicGeometry.Spec.map_surjective` `Module.Finite.of_quasiFinite` `RingHom.QuasiFinite.toAlgebra` `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `IsArtinianRing.of_finite` `IsScalarTower.right` `AlgebraicGeometry.isLocallyArtinian_iff_openCover` `AlgebraicGeometry.instLocallyQuasiFiniteCompScheme` `AlgebraicGeometry.instLocallyQuasiFiniteOfIsImmersion` `AlgebraicGeometry.IsImmersion.instOfIsOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.Scheme.local_affine` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.instLocallyQuasiFiniteSndScheme` `AlgebraicGeometry.instIsLocallyArtinianXScheme`

AlgebraicGeometry.LocallyQuasiFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_iff` 📖	mathematical	—	`AlgebraicGeometry.LocallyQuasiFinite` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`of_comp` `AlgebraicGeometry.instLocallyQuasiFiniteCompScheme`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.LocallyQuasiFinite`	—	`AlgebraicGeometry.HasRingHomProperty.of_comp` `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `RingHom.QuasiFinite.of_comp`
`of_fiberToSpecResidueField` 📖	—	`AlgebraicGeometry.LocallyQuasiFinite` `AlgebraicGeometry.Scheme.Hom.fiber` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField`	—	—	`AlgebraicGeometry.Spec.map_surjective` `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `Algebra.to_smulCommClass` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource` `PrimeSpectrum.isPrime` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.Spec.fromSpecStalk_eq` `CategoryTheory.Category.assoc` `AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv` `CategoryTheory.Limits.pullback.map_isIso` `CategoryTheory.IsIso.id` `AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Limits.hasPullback_symmetry` `AlgebraicGeometry.pullbackSpecIso_hom_fst'` `CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst` `CategoryTheory.Limits.limit.lift_π` `Module.Finite.of_quasiFinite` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `IsLocalRing.ResidueField.finite_of_module_finite` `Algebra.IsIntegral.isLocalHom` `IsPurelyInseparable.isIntegral` `isPurelyInseparable_self` `Module.FaithfullyFlat.faithfulSMul` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Module.Free.self` `Module.Finite.instLocalizationLocalizedModule` `Module.Finite.self` `AlgebraicGeometry.HasRingHomProperty.Spec_iff` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover` `AlgebraicGeometry.IsLocallyArtinian.of_locallyQuasiFinite` `AlgebraicGeometry.IsArtinianScheme.toIsLocallyArtinian` `AlgebraicGeometry.instIsArtinianSchemeSpecOfIsArtinianRingCarrier` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion` `AlgebraicGeometry.IsImmersion.toIsPreimmersion` `AlgebraicGeometry.IsImmersion.instOfIsOpenImmersion` `AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `AlgebraicGeometry.IsOpenImmersion.mono` `isClosed_discrete` `AlgebraicGeometry.IsLocallyArtinian.discreteTopology` `AlgebraicGeometry.instLocallyQuasiFiniteCompScheme` `AlgebraicGeometry.instLocallyQuasiFiniteOfIsImmersion` `AlgebraicGeometry.IsImmersion.instOfIsClosedImmersion` `AlgebraicGeometry.Scheme.local_affine` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion` `CategoryTheory.Limits.pullback.condition` `AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField` `AlgebraicGeometry.IsOpenImmersion.instFstScheme`
`of_finite_preimage_singleton` 📖	mathematical	`Set.Finite` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `Set.preimage` `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'` `Set` `Set.instSingletonSet`	`AlgebraicGeometry.LocallyQuasiFinite`	—	`AlgebraicGeometry.Spec.map_surjective` `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `Algebra.QuasiFinite.iff_finite_comap_preimage_singleton` `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource` `AlgebraicGeometry.locallyOfFiniteType_comp` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `Set.Finite.preimage` `Function.Injective.injOn` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding` `AlgebraicGeometry.Scheme.Hom.isOpenEmbedding` `AlgebraicGeometry.Scheme.local_affine` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget` `AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme` `Set.ext` `CategoryTheory.Limits.pullback.condition` `AlgebraicGeometry.IsOpenImmersion.instFstScheme`
`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'`	`AlgebraicGeometry.LocallyQuasiFinite`	—	`of_finite_preimage_singleton` `Set.Subsingleton.finite` `Set.Subsingleton.preimage` `Set.subsingleton_singleton`
`of_isFinite_fiberToSpecResidueField` 📖	—	`AlgebraicGeometry.LocallyQuasiFinite` `AlgebraicGeometry.Scheme.Hom.fiber` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField`	—	—	`of_fiberToSpecResidueField`
`quasiFinite_appLE` 📖	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'`	`RingHom.QuasiFinite` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	—

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
`QuasiFiniteAt` 📖	MathDef	8 math math: `exists_isIso_morphismRestrict_toNormalization`, `quasiFiniteAt_comp_iff_of_isOpenImmersion`, `isOpen_quasiFiniteAt`, `quasiFiniteAt_iff`, `quasiFiniteAt_iff_isOpen_singleton_asFiber`, `quasiFiniteAt`, `mem_quasiFiniteLocus`, `quasiFiniteAt_comp_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_preimage` 📖	mathematical	—	`Set.Finite` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`Set.Finite.preimage'` `finite_preimage_singleton`
`finite_preimage_singleton` 📖	mathematical	—	`Set.Finite` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `Set` `Set.instSingletonSet`	—	`Set.image_congr` `Set.image_univ` `range_fiberι` `Set.Finite.image` `Set.finite_univ` `AlgebraicGeometry.IsArtinianScheme.finite` `AlgebraicGeometry.instIsArtinianSchemeFiberOfLocallyQuasiFiniteOfQuasiCompact`
`isDiscrete_preimage` 📖	mathematical	`IsDiscrete` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	`Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`IsDiscrete.preimage'` `Continuous.continuousOn` `continuous` `isDiscrete_preimage_singleton`
`isDiscrete_preimage_singleton` 📖	mathematical	—	`IsDiscrete` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `Set` `Set.instSingletonSet`	—	`Set.image_congr` `Set.image_univ` `range_fiberι` `IsDiscrete.image` `isDiscrete_univ_iff` `AlgebraicGeometry.IsLocallyArtinian.discreteTopology` `AlgebraicGeometry.instIsLocallyArtinianFiberOfLocallyQuasiFinite` `isEmbedding` `AlgebraicGeometry.instIsPreimmersionFiberι`
`quasiFiniteAt` 📖	mathematical	—	`QuasiFiniteAt`	—	`AlgebraicGeometry.HasRingHomProperty.stalkMap` `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `RingHom.QuasiFinite.of_comp` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `RingHom.ext` `Localization.localRingHom_to_map` `RingHom.quasiFinite_algebraMap` `Algebra.QuasiFinite.instLocalization` `RingHom.QuasiFinite.toAlgebra`
`quasiFiniteAt_comp_iff` 📖	mathematical	—	`QuasiFiniteAt` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `stalkMap_comp` `RingHom.QuasiFinite.comp_iff` `quasiFiniteAt`
`quasiFiniteAt_comp_iff_of_isOpenImmersion` 📖	mathematical	—	`QuasiFiniteAt` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `DFunLike.coe` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `stalkMap_comp` `RingHom.RespectsIso.cancel_right_isIso` `RingHom.QuasiFinite.respectsIso` `AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap`
`quasiFiniteAt_iff` 📖	mathematical	—	`QuasiFiniteAt` `AlgebraicGeometry.LocallyQuasiFinite` `AlgebraicGeometry.Spec` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.PresheafedSpace.presheaf` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.fromSpecStalk`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk` `AlgebraicGeometry.LocallyQuasiFinite.comp_iff` `AlgebraicGeometry.instLocallyQuasiFiniteOfIsPreimmersion` `AlgebraicGeometry.instIsPreimmersionFromSpecStalk` `AlgebraicGeometry.HasRingHomProperty.Spec_iff` `AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite` `QuasiFiniteAt.eq_1`
`quasiFiniteAt_iff_isOpen_singleton_asFiber` 📖	mathematical	—	`QuasiFiniteAt` `IsOpen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `fiber` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instSingletonSet` `asFiber`	—	`Homeomorph.isOpen_image` `Set.image_congr` `Set.image_singleton` `Homeomorph.apply_symm_apply` `AlgebraicGeometry.Spec.map_surjective` `PrimeSpectrum.isPrime` `Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber` `AlgebraicGeometry.HasRingHomProperty.Spec_iff` `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType` `Ideal.IsPrime.under` `Ideal.over_under` `RingHom.quasiFinite_algebraMap` `RingHom.RespectsIso.arrow_mk_iso_iff` `RingHom.QuasiFinite.respectsIso` `CommRingCat.Colimits.hasColimits_commRingCat` `Algebra.QuasiFinite.trans` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `Algebra.QuasiFinite.instLocalization` `Algebra.QuasiFinite.instOfFinite` `Module.Finite.self` `Algebra.QuasiFinite.of_restrictScalars` `AlgebraicGeometry.Scheme.Cover.exists_eq` `AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `quasiFiniteAt_comp_iff_of_isOpenImmersion` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `Topology.IsOpenEmbedding.isOpen_iff_image_isOpen` `Set.restrictPreimage_isOpenEmbedding` `isOpenEmbedding` `AlgebraicGeometry.locallyOfFiniteType_comp` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `AlgebraicGeometry.Scheme.local_affine` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback` `CategoryTheory.IsPullback.of_hasPullback` `Set.preimage_comp` `TopCat.coe_comp` `comp_base` `comp_apply` `CategoryTheory.Limits.pullback.condition` `Set.preimage_image_eq` `injective` `AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme` `AlgebraicGeometry.IsOpenImmersion.mono` `Eq.le` `Set.mapsTo_preimage` `AlgebraicGeometry.IsOpenImmersion.instFstScheme` `AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme`
`tendsto_cofinite_cofinite` 📖	mathematical	—	`Filter.Tendsto` `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` `toLRSHom'` `Filter.cofinite`	—	`Filter.Tendsto.cofinite_of_finite_preimage_singleton` `finite_preimage_singleton`

AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClopen_singleton_asFiber` 📖	mathematical	—	`IsClopen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Scheme.Hom.fiber` `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'` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instSingletonSet` `AlgebraicGeometry.Scheme.Hom.asFiber`	—	`AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber` `isClosed_singleton_of_isLocallyClosed_singleton` `AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType` `IsOpen.isLocallyClosed`
`quasiFiniteAt` 📖	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'` `Set` `Set.instMembership` `TopologicalSpace.Opens.carrier`	`RingHom.QuasiFiniteAt` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE` `PrimeSpectrum.asIdeal` `CommRing.toCommSemiring` `AlgebraicGeometry.IsAffineOpen.primeIdealOf` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `PrimeSpectrum.isPrime`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `PrimeSpectrum.isPrime` `AlgebraicGeometry.IsAffineOpen.isLocalization_stalk` `RingHom.algebraMap_toAlgebra` `RingHom.quasiFinite_algebraMap` `Algebra.QuasiFinite.of_isLocalization` `IsScalarTower.left` `Algebra.QuasiFinite.instOfFinite` `Module.Finite.self` `Localization.isLocalization` `RingHom.QuasiFiniteAt.eq_1` `Algebra.QuasiFiniteAt.eq_1` `CommRingCat.hom_comp` `AlgebraicGeometry.Scheme.Hom.germ_stalkMap` `TopCat.Presheaf.germ_res` `le_rfl` `AlgebraicGeometry.Scheme.Hom.app_eq_appLE` `LE.le.trans` `AlgebraicGeometry.Scheme.Hom.appLE_map_assoc` `RingHom.comp_assoc` `IsScalarTower.algebraMap_eq` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `RingHom.QuasiFinite.comp` `RingHom.QuasiFinite.of_finite` `RingEquiv.finite`

---

← Back to Index