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 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'	—	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