MorphismProperty

📁 Source: Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

Statistics

Metric	Count
Definitions IsJointlySurjectivePreserving, jointlySurjectivePrecoverage, precoverage, zariskiPrecoverage	4
Theorems exists_preimage_fst_triplet_of_prop, exists_preimage_snd_triplet_of_prop, bot_mem_precoverage, instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, instHasPullbacksPrecoverageOfHasPullbacks, instIsJointlySurjectivePreservingIsOpenImmersion, instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange, instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition, ofArrows_mem_precoverage_iff, precoverage_mono, singleton_mem_precoverage_iff	11
Total	15

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
IsJointlySurjectivePreserving 📖	CompData	2 math math: isJointlySurjectivePreserving, instIsJointlySurjectivePreservingIsOpenImmersion
jointlySurjectivePrecoverage 📖	CompOp	1 math math: instIsStableUnderBaseChangeJointlySurjectivePrecoverage
precoverage 📖	CompOp	199 math math: coverOfIsIso_I₀, AffineOpenCover.openCover_f, Cover.pullbackCoverOver_X, Cover.gluedCoverT'_snd_snd_assoc, Cover.LocallyDirected.directed, AlgebraicGeometry.instIsLocallyArtinianXScheme, AffineCover.cover_I₀, affineBasisCover_is_basis, Pullback.openCoverOfLeftRight_f, mem_grothendieckTopology_iff, AlgebraicGeometry.QuasiCompactCover.instCoverOfIsIso, Cover.glued_cover_cocycle_fst, AlgebraicGeometry.sigmaOpenCover_X, Hom.iUnion_support_ker_openCover_map_comp, Pullback.openCoverOfBase_I₀, OpenCover.finiteSubcover_f, Pullback.openCoverOfBase_f, Cover.pullbackCoverOver'_X, Pullback.openCoverOfRight_I₀, instHasPullbacksPrecoverageOfHasPullbacks, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq, Cover.functorOfLocallyDirected_obj, openCoverOfIsOpenCover_I₀, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰S, Cover.glued_cover_cocycle, affineOpenCover_I₀, Cover.gluedCover_t, precoverage_mono, Cover.pullbackCoverOver_I₀, Cover.gluedCover_U, bot_mem_precoverage, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, affineOpenCover_idx, Hom.fromNormalization_preimage, Cover.ColimitGluingData.cocone_ι_transitionMap, presieve₀_mem_precoverage_iff, Cover.mkOfCovers_I₀, Pullback.left_affine_comp_pullback_hasPullback, AlgebraicGeometry.IsLocalAtSource.iff_of_openCover, Hom.ι_toNormalization, Cover.ColimitGluingData.transitionCocone_pt, GlueData.openCover_f, instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, AlgebraicGeometry.instIsAffineXSchemeAffineCover, Cover.ColimitGluingData.transitionMap_id, Hom.cover_X, directedAffineCover_f, Cover.gluedCover_V, Cover.coconeOfLocallyDirected_ι, Cover.ι_fromGlued_assoc, OpenCover.isOpenCover_opensRange, Cover.ulift_X, openCoverOfIsOpenCover_f, Cover.gluedCoverT'_fst_fst, IsLocallyDirected.openCover_f, AlgebraicGeometry.QuasiCompactCover.exists_hom, Cover.gluedCoverT'_snd_fst, isAffine_affineBasisCover, Cover.trans_id, AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp, Cover.exists_lift_trans_eq, directedAffineCover_I₀, Cover.RelativeGluingData.equifibered, Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X, OpenCover.restrict_f, OpenCover.iSup_opensRange, Cover.mkOfCovers_X, exists_cover_of_mem_pretopology, LocalRepresentability.glueData_openCover_map, Pullback.openCoverOfRight_f, Hom.iInf_ker_openCover_map_comp, AffineCover.cover_f, Cover.gluedCover_J, Cover.ColimitGluingData.transitionCocone_ι_app, Cover.sigmaFunctor_obj, Cover.glued_cover_cocycle_snd, Cover.trans_map, openCoverOfIsOpenCover_X, Cover.toSigma_s₀, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, singleton_mem_precoverage_iff, AlgebraicGeometry.QuasiCompactCover.inst, GlueData.openCover_X, Cover.LocallyDirected.trans_comp, Cover.functorOfLocallyDirected_map, directedAffineCover_X, Cover.property_trans, Cover.sigma_X, instSmallPrecoverage, Hom.cover_f, AffineZariskiSite.directedCover_X, Cover.ulift_f, OpenCover.instIsOpenImmersionTrans, AlgebraicGeometry.instSurjectiveDescI₀SchemeF, Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, Cover.pullbackCoverOver'_I₀, Cover.ulift_I₀, Cover.sigmaFunctor_map, Pullback.openCoverOfRight_X, Cover.gluedCoverT'_snd_fst_assoc, AffineZariskiSite.directedCover_f, IsLocallyDirected.openCover_I₀, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Hom.iInf_ker_openCover_map_comp_apply, Cover.pushforwardIso_f, IsLocallyDirected.openCover_X, Cover.pullbackCoverOver_f, Pullback.openCoverOfBase_X, Cover.toPresieveOver_le_arrows_iff, Pullback.openCoverOfBase'_f, Cover.gluedCover_f, Hom.ι_toNormalization_assoc, Cover.Hom.sigma_h₀, Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, Cover.LocallyDirected.trans_id, Cover.toSigma_h₀, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, directedAffineCover_trans, coverOfIsIso_X, Cover.LocallyDirected.property_trans, AffineZariskiSite.opensRange_relativeGluingData_map, Cover.ColimitGluingData.prop_trans, instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition, Cover.gluedCoverT'_fst_snd_assoc, Cover.coconeOfLocallyDirected_pt, ofArrows_mem_precoverage_iff, Cover.ColimitGluingData.trans_app_left, AffineCover.cover_X, affineBasisCover_obj, Cover.ColimitGluingData.transitionMap_comp, AlgebraicGeometry.sigmaOpenCover_I₀, Cover.Hom.sigma_s₀, Cover.sigma_I₀, instEtaleF, instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange, Cover.pushforwardIso_I₀, AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, OpenCover.finiteSubcover_X, Hom.ι_fromNormalization_assoc, Cover.trans_comp, OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, Pullback.openCoverOfLeftRight_I₀, coverOfIsIso_f, Hom.cover_I₀, precoverage_le_qcPrecoverage_of_isOpenMap, Cover.gluedCoverT'_snd_snd, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.instIsLocallyNoetherianXScheme, AlgebraicGeometry.sigmaOpenCover_f, OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, AlgebraicGeometry.isLocallyArtinian_iff_openCover, AffineOpenCover.openCover_I₀, exists_cover_of_mem_grothendieckTopology, OpenCover.restrict_I₀, Pullback.openCoverOfLeft_I₀, AlgebraicGeometry.QuasiCompactCover.homCover, instIsOpenImmersionF, affineOpenCover_f, Cover.pullbackCoverOver'_f, Cover.gluedCoverT'_fst_snd, Cover.pushforwardIso_X, AffineZariskiSite.PreservesLocalization.opensRange_map, Cover.add_toPreZeroHypercover, affineBasisCover_map_range, Cover.map_prop, Cover.LocallyDirected.w, grothendieckTopology_cover, Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, Cover.Over.isOver_map, Cover.mkOfCovers_f, Hom.ι_fromNormalization, mem_pretopology_iff, GlueData.openCover_I₀, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, Cover.ColimitGluingData.functor_map, Cover.intersectionOfLocallyDirected_f, Pullback.openCoverOfLeft_f, OpenCover.restrict_X, Cover.mem_pretopology, openCoverBasicOpenTop_f, Cover.gluedCoverT'_fst_fst_assoc, OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected, Cover.functorOfLocallyDirectedHomBase_app, AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, instJointlySurjectivePrecoverage, Cover.ColimitGluingData.functor_obj, Pullback.openCoverOfLeftRight_X, pretopology_cover, isAffine_affineCover, AffineZariskiSite.directedCover_I₀, AffineOpenCover.openCover_X, Cover.sigma_f, Pullback.openCoverOfLeft_X, Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor, Pullback.diagonalCover_map, Cover.ι_fromGlued, Cover.mem_grothendieckTopology, isAffine_affineOpenCover
zariskiPrecoverage 📖	CompOp	2 math math: instIsLocalAtTargetIsomorphismsZariskiPrecoverage, zariskiPrecoverage_le_qcPrecoverage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem_precoverage 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings precoverage Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	CategoryTheory.MorphismProperty.bot_mem_precoverage
instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso 📖	mathematical	—	CategoryTheory.Precoverage.HasIsos AlgebraicGeometry.Scheme instCategory precoverage	—	CategoryTheory.Precoverage.instHasIsosMin CategoryTheory.Precoverage.instHasIsosComap CategoryTheory.Types.instHasIsosJointlySurjectivePrecoverage CategoryTheory.MorphismProperty.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso
instHasPullbacksPrecoverageOfHasPullbacks 📖	mathematical	—	CategoryTheory.Precoverage.HasPullbacks AlgebraicGeometry.Scheme instCategory precoverage	—	CategoryTheory.MorphismProperty.hasPullback
instIsJointlySurjectivePreservingIsOpenImmersion 📖	mathematical	—	IsJointlySurjectivePreserving AlgebraicGeometry.IsOpenImmersion	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1 CategoryTheory.Limits.PreservesPullback.iso_hom_fst TopCat.pullback_fst_range TopCat.comp_app CategoryTheory.Iso.inv_hom_id_assoc
instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderBaseChange AlgebraicGeometry.Scheme instCategory precoverage	—	ofArrows_mem_precoverage_iff CategoryTheory.IsPullback.hasPullback IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop CategoryTheory.IsPullback.isoPullback_inv_fst CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.flip
instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderComposition AlgebraicGeometry.Scheme instCategory precoverage	—	CategoryTheory.Precoverage.instIsStableUnderCompositionMin CategoryTheory.Precoverage.instIsStableUnderCompositionComap CategoryTheory.Types.instIsStableUnderCompositionJointlySurjectivePrecoverage CategoryTheory.MorphismProperty.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition
ofArrows_mem_precoverage_iff 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings precoverage CategoryTheory.Presieve.ofArrows TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	—	—
precoverage_mono 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.Precoverage CategoryTheory.Precoverage.instPartialOrder precoverage	—	precoverage.eq_1 le_imp_le_of_le_of_le inf_le_inf le_refl CategoryTheory.MorphismProperty.precoverage_monotone
singleton_mem_precoverage_iff 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings precoverage CategoryTheory.Presieve.singleton TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	—	CategoryTheory.Presieve.ofArrows_pUnit ofArrows_mem_precoverage_iff

AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_preimage_fst_triplet_of_prop 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier 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'	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback.fst	—	—
exists_preimage_snd_triplet_of_prop 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier 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'	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasPullback_symmetry exists_preimage_fst_triplet_of_prop AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd

---

← Back to Index