FinitePresentation

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

Statistics

Metric	Count
Definitions LocallyOfFinitePresentation	1
Theorems finitePresentation_appLE, finitePresentation_of_affine_subset, finitePresentation_appLE, isConstructible_image, isConstructible_preimage, isLocallyConstructible_image, instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation, instIsStableUnderCompositionSchemeLocallyOfFinitePresentation, instLocallyOfFinitePresentationFstScheme, instLocallyOfFinitePresentationMorphismRestrict, instLocallyOfFinitePresentationResLE, instLocallyOfFinitePresentationSndScheme, instLocallyOfFiniteTypeOfLocallyOfFinitePresentation, locallyOfFinitePresentation_comp, locallyOfFinitePresentation_iff, locallyOfFinitePresentation_isStableUnderBaseChange, locallyOfFinitePresentation_of_isOpenImmersion	17
Total	18

AlgebraicGeometry

Definitions

Name	Category	Theorems
LocallyOfFinitePresentation 📖	CompData	15 math math: locallyOfFinitePresentation_of_isOpenImmersion, instLocallyOfFinitePresentationOfIsLocallyNoetherianOfLocallyOfFiniteType, instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, instLocallyOfFinitePresentationOfSmooth, AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite, instIsStableUnderCompositionSchemeLocallyOfFinitePresentation, instLocallyOfFinitePresentationFstScheme, instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation, locallyOfFinitePresentation_isStableUnderBaseChange, LocallyOfFinitePresentation.iff_locallyOfFiniteType, locallyOfFinitePresentation_comp, instLocallyOfFinitePresentationSndScheme, locallyOfFinitePresentation_iff, instLocallyOfFinitePresentationMorphismRestrict, instLocallyOfFinitePresentationResLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation 📖	mathematical	—	HasRingHomProperty LocallyOfFinitePresentation RingHom.FinitePresentation	—	RingHom.finitePresentation_isLocal CategoryTheory.MorphismProperty.ext locallyOfFinitePresentation_iff affineLocally_iff_forall_isAffineOpen
instIsStableUnderCompositionSchemeLocallyOfFinitePresentation 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition Scheme Scheme.instCategory LocallyOfFinitePresentation	—	HasRingHomProperty.stableUnderComposition instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation RingHom.finitePresentation_stableUnderComposition
instLocallyOfFinitePresentationFstScheme 📖	mathematical	—	LocallyOfFinitePresentation CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange locallyOfFinitePresentation_isStableUnderBaseChange
instLocallyOfFinitePresentationMorphismRestrict 📖	mathematical	—	LocallyOfFinitePresentation 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 instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation
instLocallyOfFinitePresentationResLE 📖	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'	LocallyOfFinitePresentation Scheme.Opens.toScheme Scheme.Hom.resLE	—	locallyOfFinitePresentation_comp locallyOfFinitePresentation_of_isOpenImmersion instIsOpenImmersionHomOfLE instLocallyOfFinitePresentationMorphismRestrict
instLocallyOfFinitePresentationSndScheme 📖	mathematical	—	LocallyOfFinitePresentation CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange locallyOfFinitePresentation_isStableUnderBaseChange
instLocallyOfFiniteTypeOfLocallyOfFinitePresentation 📖	mathematical	—	LocallyOfFiniteType	—	HasRingHomProperty.eq_affineLocally instHasRingHomPropertyLocallyOfFiniteTypeFiniteType affineLocally_le RingHom.FiniteType.of_finitePresentation instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation
locallyOfFinitePresentation_comp 📖	mathematical	—	LocallyOfFinitePresentation CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory	—	CategoryTheory.MorphismProperty.comp_mem instIsStableUnderCompositionSchemeLocallyOfFinitePresentation
locallyOfFinitePresentation_iff 📖	mathematical	—	LocallyOfFinitePresentation RingHom.FinitePresentation 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	—	—
locallyOfFinitePresentation_isStableUnderBaseChange 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange Scheme Scheme.instCategory LocallyOfFinitePresentation	—	HasRingHomProperty.isStableUnderBaseChange instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation RingHom.finitePresentation_isStableUnderBaseChange
locallyOfFinitePresentation_of_isOpenImmersion 📖	mathematical	—	LocallyOfFinitePresentation	—	HasRingHomProperty.of_isOpenImmersion instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation RingHom.HoldsForLocalizationAway.containsIdentities RingHom.finitePresentation_holdsForLocalizationAway

AlgebraicGeometry.LocallyOfFinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitePresentation_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.FinitePresentation CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appLE	—	—
finitePresentation_of_affine_subset 📖	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.FinitePresentation CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appLE	—	AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finitePresentation_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 toLRSHom'	RingHom.FinitePresentation CommRingCat.carrier Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom appLE	—	AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE
isConstructible_image 📖	mathematical	Topology.IsConstructible TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	Topology.IsLocallyConstructible.isConstructible AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat isLocallyConstructible_image Topology.IsConstructible.isLocallyConstructible
isConstructible_preimage 📖	mathematical	Topology.IsConstructible 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'	—	Topology.IsConstructible.preimage continuous IsRetrocompact_iff_isSpectralMap_subtypeVal AlgebraicGeometry.quasiCompact_iff_isSpectralMap CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.quasiCompact_isStableUnderBaseChange AlgebraicGeometry.isPullback_morphismRestrict
isLocallyConstructible_image 📖	mathematical	Topology.IsLocallyConstructible TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Set.image 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.Spec.map_surjective Topology.IsConstructible.isLocallyConstructible PrimeSpectrum.isConstructible_comap_image AlgebraicGeometry.HasRingHomProperty.Spec_iff AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation Topology.IsLocallyConstructible.isConstructible AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat AlgebraicGeometry.quasiSeparatedSpace_of_isAffine AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.Scheme.compactSpace_of_isAffine AlgebraicGeometry.HasAffineProperty.iff_of_isAffine AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat AlgebraicGeometry.Scheme.instIsOpenImmersionF TopologicalSpace.IsOpenCover.iUnion_inter AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange Set.image_iUnion Topology.IsLocallyConstructible.iUnion Finite.of_fintype AlgebraicGeometry.Scheme.local_affine AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage comp_base TopCat.Hom.hom.eq_1 TopCat.hom_comp ContinuousMap.coe_comp Set.image_comp Set.image_preimage_eq_inter_range coe_opensRange Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding isOpenEmbedding AlgebraicGeometry.locallyOfFinitePresentation_comp AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion Topology.IsLocallyConstructible.of_isOpenCover AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange AlgebraicGeometry.quasiCompact_isStableUnderBaseChange Set.image_injective Subtype.val_injective Subtype.range_coe_subtype Set.setOf_mem_eq isoOpensRange_hom_ι AlgebraicGeometry.Scheme.Cover.pullbackHom_map Set.image_congr AlgebraicGeometry.IsOpenImmersion.range_pullbackFst Set.image_inter_preimage Homeomorph.image_eq_preimage_symm AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv

---

← Back to Index