Documentation Verification Report

UniversallyOpen

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

Statistics

Metric	Count
Definitions `UniversallyOpen`	1
Theorems `generalizingMap`, `isOpenMap`, `eq`, `fst`, `instCompScheme`, `instIsMultiplicativeScheme`, `instIsStableUnderBaseChangeScheme`, `instIsStableUnderCompositionScheme`, `instIsStableUnderCompositionSchemeTopologicallyIsOpenMap`, `instIsZariskiLocalAtSource`, `instIsZariskiLocalAtTarget`, `instOfIsOpenImmersion`, `instRespectsIsoScheme`, `of_flat`, `out`, `snd`, `universally_isOpenMap`, `instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat`, `isOpenMap_of_generalizingMap`, `universallyOpen_iff`	20
Total	21

AlgebraicGeometry

Definitions

Name	Category	Theorems
`UniversallyOpen` 📖	CompData	15 math math: `UniversallyOpen.of_flat`, `UniversallyOpen.instIsStableUnderBaseChangeScheme`, `UniversallyOpen.instIsMultiplicativeScheme`, `UniversallyOpen.instOfIsOpenImmersion`, `UniversallyOpen.snd`, `UniversallyOpen.fst`, `UniversallyOpen.instIsZariskiLocalAtSource`, `UniversallyOpen.eq`, `universallyOpen_iff`, `instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat`, `UniversallyOpen.instIsStableUnderCompositionScheme`, `UniversallyOpen.instIsZariskiLocalAtTarget`, `UniversallyOpen.instCompScheme`, `UniversallyOpen.instRespectsIsoScheme`, `descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat` 📖	mathematical	—	`UniversallyOpen`	—	`Spec.map_surjective` `CategoryTheory.MorphismProperty.universally_mk'` `instRespectsIsoSchemeTopologicallyIsOpenMap` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_inv` `Algebra.to_smulCommClass` `pullbackSpecIso_inv_fst` `PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field` `Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `isOpenImmersion_stableUnderBaseChange` `IsZariskiLocalAtTarget.iff_of_openCover` `isOpenMap_isZariskiLocalAtTarget` `CategoryTheory.Limits.hasPullbackHorizPaste` `CategoryTheory.Limits.hasPullback_symmetry` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd` `CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst` `Scheme.local_affine` `Equiv.subsingleton` `instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat` `Finite.of_subsingleton` `Subsingleton.discreteTopology` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `UniversallyOpen.instRespectsIsoScheme` `instIsIntegralSpecOfIsDomainCarrier` `instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral` `isField_of_isIntegral_of_subsingleton` `IsZariskiLocalAtSource.iff_of_openCover` `UniversallyOpen.instIsZariskiLocalAtSource`
`isOpenMap_of_generalizingMap` 📖	mathematical	`GeneralizingMap` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	`IsOpenMap`	—	`Spec.map_surjective` `PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation` `Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap` `HasRingHomProperty.Spec_iff` `instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation` `IsZariskiLocalAtSource.iff_of_openCover` `instIsZariskiLocalAtSourceTopologicallyIsOpenMap` `locallyOfFinitePresentation_comp` `locallyOfFinitePresentation_of_isOpenImmersion` `Scheme.instIsOpenImmersionF` `IsZariskiLocalAtSource.comp` `instIsZariskiLocalAtSourceTopologicallyGeneralizingMap` `Scheme.local_affine` `Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `isOpenImmersion_stableUnderBaseChange` `Scheme.Pullback.instHasPullback` `IsZariskiLocalAtTarget.iff_of_openCover` `isOpenMap_isZariskiLocalAtTarget` `instLocallyOfFinitePresentationSndScheme` `IsZariskiLocalAtTarget.of_isPullback` `instIsZariskiLocalAtTargetTopologicallyGeneralizingMap` `CategoryTheory.IsPullback.of_hasPullback`
`universallyOpen_iff` 📖	mathematical	—	`UniversallyOpen` `CategoryTheory.MorphismProperty.universally` `Scheme` `Scheme.instCategory` `topologically` `IsOpenMap`	—	—

AlgebraicGeometry.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`generalizingMap` 📖	mathematical	—	`GeneralizingMap` `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` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	—	`AlgebraicGeometry.HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget` `AlgebraicGeometry.instIsZariskiLocalAtTargetTopologicallyGeneralizingMap` `AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyGeneralizingMap` `AlgebraicGeometry.HasRingHomProperty.iff_appLE` `Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap` `Algebra.HasGoingDown.of_flat` `AlgebraicGeometry.HasRingHomProperty.appLE` `instHasRingHomPropertyFlat`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenMap` 📖	mathematical	—	`IsOpenMap` `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.UniversallyOpen.universally_isOpenMap` `CategoryTheory.IsPullback.of_id_snd`

AlgebraicGeometry.UniversallyOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`AlgebraicGeometry.UniversallyOpen` `CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `IsOpenMap`	—	`AlgebraicGeometry.universallyOpen_iff`
`fst` 📖	mathematical	—	`AlgebraicGeometry.UniversallyOpen` `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`
`instCompScheme` 📖	mathematical	—	`AlgebraicGeometry.UniversallyOpen` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.comp_mem` `instIsStableUnderCompositionScheme`
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.UniversallyOpen`	—	`instOfIsOpenImmersion` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `instIsStableUnderCompositionScheme`
`instIsStableUnderBaseChangeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.UniversallyOpen`	—	`CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange` `eq`
`instIsStableUnderCompositionScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.UniversallyOpen`	—	`eq` `CategoryTheory.MorphismProperty.IsStableUnderComposition.universally` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `instIsStableUnderCompositionSchemeTopologicallyIsOpenMap`
`instIsStableUnderCompositionSchemeTopologicallyIsOpenMap` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `IsOpenMap`	—	`IsOpenMap.comp`
`instIsZariskiLocalAtSource` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtSource` `AlgebraicGeometry.UniversallyOpen`	—	`eq` `AlgebraicGeometry.universally_isZariskiLocalAtSource` `AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyIsOpenMap`
`instIsZariskiLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtTarget` `AlgebraicGeometry.UniversallyOpen`	—	`eq` `AlgebraicGeometry.universally_isZariskiLocalAtTarget` `TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage` `AlgebraicGeometry.morphismRestrict_base`
`instOfIsOpenImmersion` 📖	mathematical	—	`AlgebraicGeometry.UniversallyOpen`	—	`eq` `CategoryTheory.MorphismProperty.of_isPullback` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `CategoryTheory.IsPullback.flip` `Topology.IsOpenEmbedding.isOpenMap` `AlgebraicGeometry.Scheme.Hom.isOpenEmbedding`
`instRespectsIsoScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.UniversallyOpen`	—	`CategoryTheory.MorphismProperty.universally_respectsIso` `eq`
`of_flat` 📖	mathematical	—	`AlgebraicGeometry.UniversallyOpen`	—	`CategoryTheory.MorphismProperty.universally_mk'` `AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap` `AlgebraicGeometry.isOpenMap_of_generalizingMap` `AlgebraicGeometry.instLocallyOfFinitePresentationFstScheme` `AlgebraicGeometry.Flat.generalizingMap` `AlgebraicGeometry.Flat.instFstScheme`
`out` 📖	mathematical	—	`CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `IsOpenMap`	—	`universally_isOpenMap`
`snd` 📖	mathematical	—	`AlgebraicGeometry.UniversallyOpen` `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`
`universally_isOpenMap` 📖	mathematical	—	`CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `IsOpenMap`	—	—

---

← Back to Index