Documentation Verification Report

UniversallyClosed

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

Statistics

Metric	Count
Definitions `UniversallyClosed`	1
Theorems `isClosedMap`, `isProperMap`, `of_universallyClosed_of_isDominant`, `of_comp_surjective`, `out`, `universally_isClosedMap`, `compactSpace_of_universallyClosed`, `instIsMultiplicativeSchemeUniversallyClosed`, `instQuasiCompactOfUniversallyClosed`, `instUniversallyClosedMorphismRestrict`, `instUniversallyClosedOfIsClosedImmersion`, `isClosedMap_isStableUnderComposition`, `universallyClosedTypeComp`, `universallyClosed_eq`, `universallyClosed_eq_universallySpecializing`, `universallyClosed_fst`, `universallyClosed_iff`, `universallyClosed_isStableUnderBaseChange`, `universallyClosed_isStableUnderComposition`, `universallyClosed_isZariskiLocalAtTarget`, `universallyClosed_respectsIso`, `universallyClosed_snd`	22
Total	23

AlgebraicGeometry

Definitions

Name	Category	Theorems
`UniversallyClosed` 📖	CompData	28 math math: `descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact`, `instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated`, `universallyClosedTypeComp`, `UniversallyClosed.of_comp_surjective`, `IsIntegralHom.iff_universallyClosed_and_isAffineHom`, `UniversallyClosed.of_comp_of_isSeparated`, `universallyClosed_isZariskiLocalAtTarget`, `universallyClosed_isStableUnderBaseChange`, `universallyClosed_isStableUnderComposition`, `UniversallyClosed.of_valuativeCriterion`, `instUniversallyClosedToImage`, `isProper_iff`, `universallyClosed_fst`, `isProper_eq`, `Proj.instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `IsIntegralHom.instUniversallyClosed`, `universallyClosed_eq_universallySpecializing`, `instIsMultiplicativeSchemeUniversallyClosed`, `UniversallyClosed.eq_valuativeCriterion`, `IsProper.toUniversallyClosed`, `instUniversallyClosedOfIsClosedImmersion`, `instUniversallyClosedToNormalization`, `instUniversallyClosedMorphismRestrict`, `universallyClosed_iff`, `universallyClosed_respectsIso`, `IsIntegralHom.eq_universallyClosed_inf_isAffineHom`, `universallyClosed_eq`, `universallyClosed_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_of_universallyClosed` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`Scheme.instIsOpenImmersionF` `Scheme.Pullback.instHasPullback` `TopologicalSpace.Opens.coe_iSup` `isOpen_iUnion` `IsOpen.inter` `Continuous.isOpen_preimage` `Scheme.Hom.continuous` `TopologicalSpace.Opens.is_open'` `IsClosed.isOpen_compl` `Scheme.Hom.isClosedMap` `universallyClosed_snd` `MvPolynomial.aeval_X` `NeZero.one` `EuclideanDomain.toNontrivial` `Scheme.instJointlySurjectivePrecoverage` `Scheme.Cover.covers` `TopologicalSpace.Opens.isBasis_iff_nbhd` `PrimeSpectrum.isBasis_basic_opens` `MvPolynomial.aeval_ite_mem_eq_self` `subset_rfl` `Set.instReflSubset` `Set.iUnion₂_eq_univ_iff` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_forall_eq` `Set.image_congr` `Scheme.Pullback.exists_preimage_pullback` `Unique.instSubsingleton` `PrimeSpectrum.continuous_comap` `PrimeSpectrum.basicOpen_zero` `PrimeSpectrum.comap_basicOpen` `Set.compl_iUnion` `Finset.isCompact_biUnion` `isCompact_range` `Scheme.compactSpace_of_isAffine` `Scheme.isAffine_affineCover`
`instIsMultiplicativeSchemeUniversallyClosed` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `UniversallyClosed`	—	`instUniversallyClosedOfIsClosedImmersion` `IsClosedImmersion.instOfIsIsoScheme` `CategoryTheory.IsIso.id` `universallyClosed_isStableUnderComposition`
`instQuasiCompactOfUniversallyClosed` 📖	mathematical	—	`QuasiCompact`	—	`IsProperMap.isCompact_preimage` `Scheme.Hom.isProperMap`
`instUniversallyClosedMorphismRestrict` 📖	mathematical	—	`UniversallyClosed` `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` `universallyClosed_isZariskiLocalAtTarget`
`instUniversallyClosedOfIsClosedImmersion` 📖	mathematical	—	`UniversallyClosed`	—	`universallyClosed_eq` `CategoryTheory.MorphismProperty.of_isPullback` `IsClosedImmersion.isStableUnderBaseChange` `CategoryTheory.IsPullback.flip` `Topology.IsClosedEmbedding.isClosedMap` `Scheme.Hom.isClosedEmbedding`
`isClosedMap_isStableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `topologically` `IsClosedMap`	—	`IsClosedMap.comp`
`universallyClosedTypeComp` 📖	mathematical	—	`UniversallyClosed` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.comp_mem` `universallyClosed_isStableUnderComposition`
`universallyClosed_eq` 📖	mathematical	—	`UniversallyClosed` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory` `topologically` `IsClosedMap`	—	`universallyClosed_iff`
`universallyClosed_eq_universallySpecializing` 📖	mathematical	—	`UniversallyClosed` `CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `CategoryTheory.MorphismProperty.universally` `topologically` `SpecializingMap` `QuasiCompact`	—	`CategoryTheory.MorphismProperty.universally_eq_iff` `quasiCompact_isStableUnderBaseChange` `CategoryTheory.MorphismProperty.universally_inf` `le_antisymm` `universallyClosed_isStableUnderBaseChange` `CategoryTheory.MorphismProperty.universally_mono` `IsClosedMap.specializingMap` `Scheme.Hom.isClosedMap` `instQuasiCompactOfUniversallyClosed` `universallyClosed_eq` `isClosedMap_iff_specializingMap`
`universallyClosed_fst` 📖	mathematical	—	`UniversallyClosed` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.MorphismProperty.pullback_fst` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `universallyClosed_isStableUnderBaseChange`
`universallyClosed_iff` 📖	mathematical	—	`UniversallyClosed` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory` `topologically` `IsClosedMap`	—	—
`universallyClosed_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `UniversallyClosed`	—	`CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange` `universallyClosed_eq`
`universallyClosed_isStableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `UniversallyClosed`	—	`universallyClosed_eq` `CategoryTheory.MorphismProperty.IsStableUnderComposition.universally` `Scheme.Pullback.instHasPullbacks` `isClosedMap_isStableUnderComposition`
`universallyClosed_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `UniversallyClosed`	—	`universallyClosed_eq` `universally_isZariskiLocalAtTarget` `TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage` `morphismRestrict_base`
`universallyClosed_respectsIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `UniversallyClosed`	—	`CategoryTheory.MorphismProperty.universally_respectsIso` `universallyClosed_eq`
`universallyClosed_snd` 📖	mathematical	—	`UniversallyClosed` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.MorphismProperty.pullback_snd` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `universallyClosed_isStableUnderBaseChange`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedMap` 📖	mathematical	—	`IsClosedMap` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`AlgebraicGeometry.UniversallyClosed.universally_isClosedMap` `CategoryTheory.IsPullback.of_id_snd`
`isProperMap` 📖	mathematical	—	`IsProperMap` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`isProperMap_iff_isClosedMap_and_compact_fibers` `continuous` `isClosedMap` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.compactSpace_of_universallyClosed` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.universallyClosed_snd` `AlgebraicGeometry.Scheme.range_fromSpecResidueField` `AlgebraicGeometry.Scheme.Pullback.range_fst` `isCompact_range`

AlgebraicGeometry.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_universallyClosed_of_isDominant` 📖	mathematical	—	`AlgebraicGeometry.Surjective`	—	`AlgebraicGeometry.surjective_iff` `Set.range_eq_univ` `DenseRange.closure_range` `AlgebraicGeometry.Scheme.Hom.denseRange` `IsClosed.closure_eq` `IsClosedMap.isClosed_range` `AlgebraicGeometry.Scheme.Hom.isClosedMap`

AlgebraicGeometry.UniversallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_comp_surjective` 📖	mathematical	—	`AlgebraicGeometry.UniversallyClosed`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `universally_isClosedMap` `CategoryTheory.IsPullback.paste_horiz` `CategoryTheory.IsPullback.of_hasPullback` `IsClosedMap.of_comp_surjective` `AlgebraicGeometry.Surjective.surj` `CategoryTheory.MorphismProperty.pullback_fst` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme` `AlgebraicGeometry.Scheme.Hom.continuous`
`out` 📖	mathematical	—	`CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `IsClosedMap`	—	`universally_isClosedMap`
`universally_isClosedMap` 📖	mathematical	—	`CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `IsClosedMap`	—	—

---

← Back to Index