Documentation Verification Report

Proper

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

Statistics

Metric	Count
Definitions `IsProper`	1
Theorems `eq_isProper_inf_isAffineHom`, `iff_isProper_and_isAffineHom`, `comp_iff`, `instCompScheme`, `instFstScheme`, `instIsMultiplicativeScheme`, `instIsZariskiLocalAtTarget`, `instMorphismRestrict`, `instOfIsFinite`, `instRespectsIsoScheme`, `instSndScheme`, `isStableUnderBaseChange`, `of_comp`, `of_comp_of_isSeparated`, `stableUnderComposition`, `toIsSeparated`, `toLocallyOfFiniteType`, `toUniversallyClosed`, `of_comp_of_isSeparated`, `finite_appTop_of_universallyClosed`, `instHasOfPostcompPropertySchemeIsProperIsSeparated`, `instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated`, `instIsProperOfIsFinite`, `instUniversallyClosedToImage`, `isField_of_universallyClosed`, `isIntegral_appTop_of_universallyClosed`, `isProper_eq`, `isProper_iff`	28
Total	29

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsProper` 📖	CompData	26 math math: `IsProper.instCompScheme`, `IsProper.instFstScheme`, `IsProper.instSndScheme`, `IsClosedImmersion.eq_proper_inf_monomorphisms`, `IsFinite.iff_isProper_and_isAffineHom`, `IsProper.isStableUnderBaseChange`, `IsFinite.eq_proper_inf_locallyQuasiFinite`, `IsProper.of_comp`, `IsProper.instMorphismRestrict`, `IsProper.stableUnderComposition`, `IsProper.of_comp_of_isSeparated`, `isProper_iff`, `IsProper.comp_iff`, `isProper_eq`, `instHasOfPostcompPropertySchemeIsProperIsSeparated`, `IsProper.instIsMultiplicativeScheme`, `IsProper.eq_valuativeCriterion`, `IsFinite.iff_isProper_and_locallyQuasiFinite`, `instIsProperOfIsFinite`, `IsProper.instIsZariskiLocalAtTarget`, `IsClosedImmersion.iff_isProper_and_mono`, `IsFinite.eq_isProper_inf_isAffineHom`, `IsProper.of_valuativeCriterion`, `Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `IsProper.instRespectsIsoScheme`, `IsProper.instOfIsFinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_appTop_of_universallyClosed` 📖	mathematical	—	`RingHom.Finite` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `CommRingCat.of` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appTop`	—	`IsIntegral.nonempty` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `Scheme.isBasis_affineOpens` `Set.mem_univ` `isOpen_univ` `isField_of_universallyClosed` `RingHom.finite_of_algHom_finiteType_of_isJacobsonRing` `instIsJacobsonRingOfKrullDimLEOfNatNat` `PrimeSpectrum.instKrullDimLEOfNatNat` `isArtinian_of_fg_of_artinian'` `MulEquiv.isField` `Field.toIsField` `DivisionRing.instIsArtinianRing` `FiniteDimensional.finiteDimensional_self` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `Scheme.component_nontrivial` `le_top` `Scheme.Hom.finiteType_appLE` `isAffineOpen_top` `isAffine_Spec`
`instHasOfPostcompPropertySchemeIsProperIsSeparated` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `Scheme` `Scheme.instCategory` `IsProper` `IsSeparated`	—	`Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal` `IsProper.isStableUnderBaseChange` `IsProper.instIsMultiplicativeScheme` `IsSeparated.isStableUnderBaseChange` `IsProper.instOfIsFinite` `IsFinite.instOfIsClosedImmersion` `IsSeparated.diagonal_isClosedImmersion`
`instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `Scheme` `Scheme.instCategory` `UniversallyClosed` `IsSeparated`	—	`Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal` `universallyClosed_isStableUnderBaseChange` `instIsMultiplicativeSchemeUniversallyClosed` `IsSeparated.isStableUnderBaseChange` `IsProper.toUniversallyClosed` `IsProper.instOfIsFinite` `IsFinite.instOfIsClosedImmersion` `IsSeparated.diagonal_isClosedImmersion`
`instIsProperOfIsFinite` 📖	mathematical	—	`IsProper`	—	`IsFinite.iff_isProper_and_isAffineHom`
`instUniversallyClosedToImage` 📖	mathematical	—	`UniversallyClosed` `Scheme.Hom.image` `Scheme.Hom.toImage`	—	`Scheme.Hom.toImage_imageι` `UniversallyClosed.of_comp_of_isSeparated` `IsProper.toIsSeparated` `IsProper.instOfIsFinite` `IsFinite.instOfIsClosedImmersion` `IsClosedImmersion.instSubschemeι`
`isField_of_universallyClosed` 📖	mathematical	—	`IsField` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`RingHom.isIntegral_respectsIso` `isIntegral_appTop_of_universallyClosed` `isAffine_Spec` `isField_of_isIntegral_of_isField'` `instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral` `Field.toIsField`
`isIntegral_appTop_of_universallyClosed` 📖	mathematical	—	`RingHom.IsIntegral` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommRingCat.commRing` `CommRing.toRing` `CommRingCat.Hom.hom` `Scheme.Hom.appTop`	—	`quasiCompact_iff_compactSpace` `quasiSeparatedSpace_of_isAffine` `Scheme.compactSpace_of_isAffine` `instQuasiCompactOfUniversallyClosed` `Scheme.toSpecΓ_naturality` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `Scheme.instHasPullbacksIsOpenImmersion` `universallyClosed_isZariskiLocalAtTarget` `IsAffine.affine` `UniversallyClosed.of_comp_of_isSeparated` `IsSeparated.instMap` `IsIntegralHom.SpecMap_iff` `IsIntegralHom.iff_universallyClosed_and_isAffineHom` `UniversallyClosed.of_comp_surjective` `Surjective.of_universallyClosed_of_isDominant` `instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat` `isAffineHom_of_isAffine` `isAffine_Spec`
`isProper_eq` 📖	mathematical	—	`IsProper` `CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `IsSeparated` `UniversallyClosed` `LocallyOfFiniteType`	—	`isProper_iff`
`isProper_iff` 📖	mathematical	—	`IsProper` `IsSeparated` `UniversallyClosed` `LocallyOfFiniteType`	—	—

AlgebraicGeometry.IsFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_isProper_inf_isAffineHom` 📖	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.IsAffineHom`	—	`inf_eq_left` `AlgebraicGeometry.IsSeparated.of_isAffineHom` `inf_comm` `AlgebraicGeometry.isProper_eq` `inf_assoc` `eq_inf` `AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom` `inf_left_comm`
`iff_isProper_and_isAffineHom` 📖	mathematical	—	`AlgebraicGeometry.IsFinite` `AlgebraicGeometry.IsProper` `AlgebraicGeometry.IsAffineHom`	—	`eq_isProper_inf_isAffineHom`

AlgebraicGeometry.IsProper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_iff` 📖	mathematical	—	`AlgebraicGeometry.IsProper` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`of_comp` `toIsSeparated` `instCompScheme`
`instCompScheme` 📖	mathematical	—	`AlgebraicGeometry.IsProper` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`AlgebraicGeometry.IsSeparated.instCompScheme` `toIsSeparated` `AlgebraicGeometry.universallyClosedTypeComp` `toUniversallyClosed` `AlgebraicGeometry.locallyOfFiniteType_comp` `toLocallyOfFiniteType`
`instFstScheme` 📖	mathematical	—	`AlgebraicGeometry.IsProper` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsSeparated.instFstScheme` `toIsSeparated` `AlgebraicGeometry.universallyClosed_fst` `toUniversallyClosed` `AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme` `toLocallyOfFiniteType`
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsProper`	—	`AlgebraicGeometry.isProper_eq` `CategoryTheory.MorphismProperty.IsMultiplicative.inf` `AlgebraicGeometry.IsSeparated.instIsMultiplicativeScheme` `AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyClosed` `AlgebraicGeometry.instIsMultiplicativeSchemeLocallyOfFiniteType`
`instIsZariskiLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtTarget` `AlgebraicGeometry.IsProper`	—	`AlgebraicGeometry.isProper_eq` `CategoryTheory.MorphismProperty.IsLocalAtTarget.inf` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `AlgebraicGeometry.IsSeparated.instIsZariskiLocalAtTarget` `AlgebraicGeometry.universallyClosed_isZariskiLocalAtTarget` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget` `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType`
`instMorphismRestrict` 📖	mathematical	—	`AlgebraicGeometry.IsProper` `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.IsSeparated.instMorphismRestrict` `toIsSeparated` `AlgebraicGeometry.instUniversallyClosedMorphismRestrict` `toUniversallyClosed` `AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict` `toLocallyOfFiniteType`
`instOfIsFinite` 📖	mathematical	—	`AlgebraicGeometry.IsProper`	—	`AlgebraicGeometry.IsSeparated.of_isAffineHom` `AlgebraicGeometry.IsFinite.toIsAffineHom` `AlgebraicGeometry.IsIntegralHom.instUniversallyClosed` `AlgebraicGeometry.IsFinite.instIsIntegralHom` `AlgebraicGeometry.IsFinite.instLocallyOfFiniteType`
`instRespectsIsoScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsProper`	—	`AlgebraicGeometry.isProper_eq` `CategoryTheory.MorphismProperty.inf` `AlgebraicGeometry.IsSeparated.instRespectsIsoScheme` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `AlgebraicGeometry.universallyClosed_isZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource` `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType`
`instSndScheme` 📖	mathematical	—	`AlgebraicGeometry.IsProper` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsSeparated.instSndScheme` `toIsSeparated` `AlgebraicGeometry.universallyClosed_snd` `toUniversallyClosed` `AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme` `toLocallyOfFiniteType`
`isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsProper`	—	`AlgebraicGeometry.isProper_eq` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf` `AlgebraicGeometry.IsSeparated.isStableUnderBaseChange` `AlgebraicGeometry.universallyClosed_isStableUnderBaseChange` `AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.IsProper`	—	`CategoryTheory.MorphismProperty.of_postcomp` `AlgebraicGeometry.instHasOfPostcompPropertySchemeIsProperIsSeparated`
`of_comp_of_isSeparated` 📖	mathematical	—	`AlgebraicGeometry.IsProper`	—	`of_comp`
`stableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsProper`	—	`AlgebraicGeometry.isProper_eq` `CategoryTheory.MorphismProperty.IsStableUnderComposition.inf` `AlgebraicGeometry.IsSeparated.stableUnderComposition` `AlgebraicGeometry.universallyClosed_isStableUnderComposition` `AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType`
`toIsSeparated` 📖	mathematical	—	`AlgebraicGeometry.IsSeparated`	—	—
`toLocallyOfFiniteType` 📖	mathematical	—	`AlgebraicGeometry.LocallyOfFiniteType`	—	—
`toUniversallyClosed` 📖	mathematical	—	`AlgebraicGeometry.UniversallyClosed`	—	—

AlgebraicGeometry.UniversallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_comp_of_isSeparated` 📖	mathematical	—	`AlgebraicGeometry.UniversallyClosed`	—	`CategoryTheory.MorphismProperty.of_postcomp` `AlgebraicGeometry.instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated`

---

← Back to Index