Finite

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

Statistics

Metric	Count
Definitions	0
Theorems `eq_isFinite_inf_mono`, `iff_isFinite_and_mono`, `SpecMap_iff`, `comp_iff`, `eq_inf`, `finite_app`, `iff_isIntegralHom_and_locallyOfFiniteType`, `instCompScheme`, `instContainsIdentitiesScheme`, `instDescScheme`, `instFstScheme`, `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop`, `instHasOfPostcompPropertySchemeIsSeparated`, `instIsIntegralHom`, `instIsMultiplicativeScheme`, `instIsStableUnderBaseChangeScheme`, `instIsStableUnderCompositionScheme`, `instLocallyOfFiniteType`, `instMorphismRestrict`, `instOfIsClosedImmersion`, `instOfIsIsoScheme`, `instSndScheme`, `of_comp`, `toIsAffineHom`, `closePoints_subset_preimage_closedPoints`, `finite_app`, `isClosed_singleton_iff_locallyOfFiniteType`, `isFinite_iff`, `isFinite_iff_locallyOfFiniteType_of_jacobsonSpace`	29
Total	29

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_singleton_iff_locallyOfFiniteType` 📖	mathematical	—	`IsClosed` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set` `Set.instSingletonSet` `LocallyOfFiniteType` `Spec` `Scheme.residueField` `Scheme.fromSpecResidueField`	—	`isClosed_singleton_iff_isClosedImmersion` `IsFinite.instLocallyOfFiniteType` `IsFinite.instOfIsClosedImmersion` `Field.instIsLocalRing` `Scheme.fromSpecResidueField_apply` `Scheme.Hom.closePoints_subset_preimage_closedPoints` `IsLocalRing.isClosed_singleton_closedPoint`
`isFinite_iff` 📖	mathematical	—	`IsFinite` `IsAffineHom` `RingHom.Finite` `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` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.app`	—	—
`isFinite_iff_locallyOfFiniteType_of_jacobsonSpace` 📖	mathematical	—	`IsFinite` `LocallyOfFiniteType`	—	`isEmpty_or_nonempty` `IsFinite.instLocallyOfFiniteType` `IsFinite.instOfIsClosedImmersion` `IsClosedImmersion.instOfIsEmptyCarrierCarrierCommRingCat` `instPreirreducibleSpaceOfSubsingleton` `affine_isIntegral_iff` `isIntegral_of_irreducibleSpace_of_isReduced` `Spec.map_surjective` `IsFinite.SpecMap_iff` `HasRingHomProperty.Spec_iff` `instHasRingHomPropertyLocallyOfFiniteTypeFiniteType` `PrimeSpectrum.t1Space_iff_isField` `T2Space.t1Space` `DiscreteTopology.toT2Space` `Subsingleton.discreteTopology` `PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace` `Module.Finite.finiteType` `finite_of_finite_type_of_isJacobsonRing` `instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat` `Finite.of_subsingleton` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `Scheme.instHasPullbacksIsOpenImmersion` `HasAffineProperty.instIsZariskiLocalAtTarget` `IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `HasRingHomProperty.instIsZariskiLocalAtSource` `Function.Injective.subsingleton` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding` `Scheme.Hom.isOpenEmbedding` `IsOpenImmersion.of_isIso` `instIsReducedSpecOfIsReducedCarrier` `IsReduced.component_reduced` `Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `isOpenImmersion_stableUnderBaseChange` `Scheme.Pullback.instHasPullback` `IsZariskiLocalAtTarget.iff_of_openCover` `HasRingHomProperty.instIsZariskiLocalAtTarget` `Scheme.instIsOpenImmersionF` `isReduced_of_isOpenImmersion` `JacobsonSpace.of_isOpenEmbedding` `Scheme.local_affine`

AlgebraicGeometry.IsClosedImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_isFinite_inf_mono` 📖	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.IsFinite` `CategoryTheory.MorphismProperty.monomorphisms`	—	`iff_isFinite_and_mono`
`iff_isFinite_and_mono` 📖	mathematical	—	`AlgebraicGeometry.IsClosedImmersion` `AlgebraicGeometry.IsFinite` `CategoryTheory.Mono` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `hasAffineProperty` `AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `RingHom.surjective_iff_epi_and_finite` `CategoryTheory.op_mono_of_epi` `CategoryTheory.unop_epi_of_mono` `CategoryTheory.Functor.mono_map_iff_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint` `CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `AlgebraicGeometry.Spec.full` `AlgebraicGeometry.Spec.faithful` `CategoryTheory.Limits.hasFiniteLimits_opposite` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.RespectsIso.monomorphisms` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `isZariskiLocalAtTarget` `AlgebraicGeometry.instIsZariskiLocalAtTargetMonomorphismsScheme` `AlgebraicGeometry.Scheme.isAffine_affineCover`

AlgebraicGeometry.IsFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SpecMap_iff` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map` `RingHom.Finite` `CommRingCat.carrier` `CommRingCat.commRing` `CommRingCat.Hom.hom`	—	`AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `AlgebraicGeometry.isAffine_Spec` `RingHom.RespectsIso.arrow_mk_iso_iff` `RingHom.finite_respectsIso`
`comp_iff` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`of_comp` `AlgebraicGeometry.IsSeparated.of_isAffineHom` `toIsAffineHom` `instCompScheme`
`eq_inf` 📖	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.IsIntegralHom` `AlgebraicGeometry.LocallyOfFiniteType`	—	`iff_isIntegralHom_and_locallyOfFiniteType`
`finite_app` 📖	mathematical	—	`RingHom.Finite` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.app`	—	—
`iff_isIntegralHom_and_locallyOfFiniteType` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `AlgebraicGeometry.IsIntegralHom` `AlgebraicGeometry.LocallyOfFiniteType`	—	`AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `AlgebraicGeometry.IsIntegralHom.hasAffineProperty` `RingHom.finite_iff_isIntegral_and_finiteType` `AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine` `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget` `AlgebraicGeometry.Scheme.isAffine_affineCover`
`instCompScheme` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem` `instIsStableUnderCompositionScheme`
`instContainsIdentitiesScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.ContainsIdentities` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsFinite`	—	`AlgebraicGeometry.HasAffineProperty.affineAnd_containsIdentities` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `RingHom.finite_respectsIso` `RingHom.finite_containsIdentities`
`instDescScheme` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `CategoryTheory.Limits.coprod` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `AlgebraicGeometry.Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.desc`	—	`AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `RingHom.finite_respectsIso` `RingHom.finite_algebraMap` `Module.Finite.prod`
`instFstScheme` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `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` `instIsStableUnderBaseChangeScheme`
`instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` 📖	mathematical	—	`AlgebraicGeometry.HasAffineProperty` `AlgebraicGeometry.IsFinite` `AlgebraicGeometry.IsAffine` `RingHom.Finite` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appTop`	—	`AlgebraicGeometry.HasAffineProperty.affineAnd_iff` `RingHom.finite_respectsIso` `RingHom.LocalizationPreserves.away` `RingHom.finite_localizationPreserves` `RingHom.finite_ofLocalizationSpan`
`instHasOfPostcompPropertySchemeIsSeparated` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsFinite` `AlgebraicGeometry.IsSeparated`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal` `instIsStableUnderBaseChangeScheme` `instIsMultiplicativeScheme` `AlgebraicGeometry.IsSeparated.isStableUnderBaseChange` `instOfIsClosedImmersion` `AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion`
`instIsIntegralHom` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom`	—	`iff_isIntegralHom_and_locallyOfFiniteType`
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsFinite`	—	`instContainsIdentitiesScheme` `instIsStableUnderCompositionScheme`
`instIsStableUnderBaseChangeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsFinite`	—	`AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `RingHom.finite_respectsIso` `RingHom.finite_isStableUnderBaseChange`
`instIsStableUnderCompositionScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsFinite`	—	`AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop` `RingHom.finite_stableUnderComposition`
`instLocallyOfFiniteType` 📖	mathematical	—	`AlgebraicGeometry.LocallyOfFiniteType`	—	`iff_isIntegralHom_and_locallyOfFiniteType`
`instMorphismRestrict` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `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` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop`
`instOfIsClosedImmersion` 📖	mathematical	—	`AlgebraicGeometry.IsFinite`	—	`AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono`
`instOfIsIsoScheme` 📖	mathematical	—	`AlgebraicGeometry.IsFinite`	—	`CategoryTheory.MorphismProperty.of_isIso` `instContainsIdentitiesScheme` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop`
`instSndScheme` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `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` `instIsStableUnderBaseChangeScheme`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.IsFinite`	—	`CategoryTheory.MorphismProperty.of_postcomp` `instHasOfPostcompPropertySchemeIsSeparated`
`toIsAffineHom` 📖	mathematical	—	`AlgebraicGeometry.IsAffineHom`	—	—

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closePoints_subset_preimage_closedPoints` 📖	mathematical	—	`Set` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `Set.instHasSubset` `closedPoints` `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'`	—	`AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion` `AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace` `Unique.instSubsingleton` `AlgebraicGeometry.instIsReducedSpecOfIsReducedCarrier` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `AlgebraicGeometry.locallyOfFiniteType_comp` `AlgebraicGeometry.IsFinite.instLocallyOfFiniteType` `AlgebraicGeometry.IsFinite.instOfIsClosedImmersion` `Set.range_comp` `AlgebraicGeometry.Scheme.range_fromSpecResidueField` `Set.image_singleton` `IsClosedMap.isClosed_range` `isClosedMap` `AlgebraicGeometry.IsIntegralHom.instUniversallyClosed` `AlgebraicGeometry.IsFinite.instIsIntegralHom`
`finite_app` 📖	mathematical	—	`RingHom.Finite` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `app`	—	`AlgebraicGeometry.IsFinite.finite_app`

---

← Back to Index