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	304 math math: Pullback.gluedLiftPullbackMap_snd, mem_propQCPrecoverage_iff_exists_quasiCompactCover, coverOfIsIso_I₀, Cover.pullbackCoverOverProp_I₀, AffineOpenCover.openCover_f, Cover.RelativeGluingData.cover_X, AlgebraicGeometry.instIsAffineXSchemeCover, Cover.pullbackCoverOver_X, Cover.gluedCoverT'_snd_snd_assoc, Cover.LocallyDirected.directed, Pullback.gluedLiftPullbackMap_snd_assoc, AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover, AlgebraicGeometry.instIsLocallyArtinianXScheme, Cover.LocallyDirected.ofIsBasisOpensRange_le_iff, AffineCover.cover_I₀, affineBasisCover_is_basis, Pullback.openCoverOfLeftRight_f, mem_grothendieckTopology_iff, OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc, instQuasiCompactCoverQculift, Cover.copy_f, AlgebraicGeometry.QuasiCompactCover.instCoverOfIsIso, Pullback.t'_snd_fst_fst_assoc, Cover.glued_cover_cocycle_fst, AlgebraicGeometry.sigmaOpenCover_X, Hom.iUnion_support_ker_openCover_map_comp, Pullback.openCoverOfBase_I₀, Cover.copy_X, OpenCover.finiteSubcover_f, Pullback.openCoverOfBase_f, Cover.pullbackCoverOver'_X, Pullback.openCoverOfRight_I₀, Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, instHasPullbacksPrecoverageOfHasPullbacks, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq, Cover.functorOfLocallyDirected_obj, Cover.ColimitGluingData.isPullback, openCoverOfIsOpenCover_I₀, instQuasiCompactCoverForgetQc, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰S, Cover.glued_cover_cocycle, affineOpenCover_I₀, Cover.gluedCover_t, Pullback.t_fst_snd_assoc, Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, Cover.RelativeGluingData.cover_I₀, precoverage_mono, Cover.pullbackCoverOver_I₀, Cover.gluedCover_U, OpenCover.map_glueMorphismsOfLocallyDirected_assoc, bot_mem_precoverage, Cover.ofQuasiCompactCover_toPreZeroHypercover, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, affineOpenCover_idx, Hom.fromNormalization_preimage, Cover.ColimitGluingData.cocone_ι_transitionMap, OpenCover.map_glueMorphismsOverOfLocallyDirected_left, presieve₀_mem_precoverage_iff, OpenCover.map_glueMorphismsOfLocallyDirected, Cover.mkOfCovers_I₀, Cover.isSheafFor_sigma_iff, Pullback.left_affine_comp_pullback_hasPullback, AlgebraicGeometry.IsLocalAtSource.iff_of_openCover, Hom.ι_toNormalization, Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, Cover.pullbackCoverOverProp_f, Cover.ColimitGluingData.transitionCocone_pt, Pullback.cocycle, Pullback.pullbackP1Iso_hom_snd, GlueData.openCover_f, instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, AlgebraicGeometry.instIsAffineXSchemeAffineCover, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, Cover.ColimitGluingData.transitionMap_id, Hom.cover_X, directedAffineCover_f, Pullback.t'_fst_fst_snd_assoc, Cover.gluedCover_V, AlgebraicGeometry.HasAffineProperty.iff_of_openCover, Cover.coconeOfLocallyDirected_ι, Cover.ι_fromGlued_assoc, OpenCover.isOpenCover_opensRange, Cover.ulift_X, AlgebraicGeometry.QuasiCompactCover.instCoverOfIsAffineOfFiniteI₀, Cover.RelativeGluingData.ι_toBase, openCoverOfIsOpenCover_f, Cover.gluedCoverT'_fst_fst, Pullback.pullbackFstιToV_fst_assoc, 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, Cover.exists_of_f_eq_f, Pullback.t_snd, directedAffineCover_I₀, Cover.RelativeGluingData.ι_toBase_assoc, Pullback.gluing_J, Cover.RelativeGluingData.equifibered, Pullback.gluing_f, Pullback.pullbackP1Iso_hom_fst_assoc, Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X, Pullback.pullbackP1Iso_hom_ι_assoc, OpenCover.restrict_f, Pullback.pullbackFstιToV_fst, OpenCover.iSup_opensRange, Cover.mkOfCovers_X, Pullback.pullbackP1Iso_inv_snd_assoc, Pullback.t_fst_fst, exists_cover_of_mem_pretopology, Cover.ColimitGluingData.fst_gluedCocone_ι, LocalRepresentability.glueData_openCover_map, Pullback.openCoverOfRight_f, Cover.forgetQc_toPreZeroHypercover, Pullback.t'_snd_snd, Hom.iInf_ker_openCover_map_comp, Cover.LocallyDirected.ofIsBasisOpensRange_trans, AffineCover.cover_f, Cover.gluedCover_J, Cover.ColimitGluingData.transitionCocone_ι_app, Cover.sigmaFunctor_obj, mem_overGrothendieckTopology, Cover.glued_cover_cocycle_snd, Cover.trans_map, openCoverOfIsOpenCover_X, Pullback.pullbackP1Iso_inv_fst, Cover.toSigma_s₀, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, Pullback.pullbackP1Iso_inv_fst_assoc, singleton_mem_precoverage_iff, AlgebraicGeometry.QuasiCompactCover.inst, Cover.pullbackCoverOverProp'_X, Pullback.t'_snd_fst_fst, GlueData.openCover_X, Cover.LocallyDirected.trans_comp, Cover.pullbackCoverOverProp'_f, Cover.functorOfLocallyDirected_map, directedAffineCover_X, Cover.property_trans, Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, Cover.sigma_X, Pullback.gluing_U, Pullback.t'_fst_fst_fst, 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.mem_propQCTopology, Cover.exists_of_trans_eq_trans, Cover.sigmaFunctor_map, Pullback.cocycle_fst_fst_snd, Pullback.openCoverOfRight_X, Cover.gluedCoverT'_snd_fst_assoc, Cover.ι_glueMorphisms, AffineZariskiSite.directedCover_f, IsLocallyDirected.openCover_I₀, Cover.ι_glueMorphisms_assoc, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Hom.iInf_ker_openCover_map_comp_apply, Cover.pushforwardIso_f, IsLocallyDirected.openCover_X, Cover.copy_I₀, Cover.RelativeGluingData.cover_f, Cover.pullbackCoverOver_f, Pullback.openCoverOfBase_X, Pullback.pullbackP1Iso_hom_snd_assoc, Cover.toPresieveOver_le_arrows_iff, Pullback.cocycle_fst_fst_fst, Pullback.openCoverOfBase'_f, Cover.gluedCover_f, Pullback.t_fst_snd, Hom.ι_toNormalization_assoc, Cover.Hom.sigma_h₀, Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, Cover.LocallyDirected.trans_id, Cover.toSigma_h₀, Pullback.gluedLiftPullbackMap_fst_assoc, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, directedAffineCover_trans, Pullback.t'_snd_fst_snd, coverOfIsIso_X, Cover.LocallyDirected.property_trans, AffineZariskiSite.opensRange_relativeGluingData_map, Cover.ColimitGluingData.prop_trans, instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition, Cover.pullbackCoverOverProp_X, Pullback.cocycle_snd_fst_fst, Pullback.pullbackP1Iso_inv_snd, Cover.gluedCoverT'_fst_snd_assoc, Cover.coconeOfLocallyDirected_pt, ofArrows_mem_precoverage_iff, Cover.ColimitGluingData.trans_app_left, AffineCover.cover_X, Pullback.t'_fst_fst_snd, affineBasisCover_obj, Cover.ColimitGluingData.transitionMap_comp, AlgebraicGeometry.sigmaOpenCover_I₀, Cover.Hom.sigma_s₀, Cover.sigma_I₀, instEtaleF, instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange, Cover.pushforwardIso_I₀, Pullback.cocycle_fst_snd, AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, OpenCover.finiteSubcover_X, fppfPrecoverage_eq_inf, Hom.ι_fromNormalization_assoc, Cover.trans_comp, propQCPrecoverage_le_precoverage, OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, Pullback.pullbackP1Iso_hom_ι, Pullback.openCoverOfLeftRight_I₀, Pullback.t'_snd_snd_assoc, coverOfIsIso_f, instWeaklyEtaleF, 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₀, Pullback.t'_fst_snd_assoc, exists_cover_of_mem_grothendieckTopology, OpenCover.restrict_I₀, Pullback.openCoverOfLeft_I₀, AlgebraicGeometry.QuasiCompactCover.homCover, Pullback.pullbackFstιToV_snd_assoc, instIsOpenImmersionF, affineOpenCover_f, Pullback.t'_fst_snd, Cover.pullbackCoverOver'_f, Cover.gluedCoverT'_fst_snd, Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, mem_smallGrothendieckTopology, Cover.presieve₀_sigma, Cover.pushforwardIso_X, AffineZariskiSite.PreservesLocalization.opensRange_map, Pullback.pullbackFstιToV_snd, Pullback.t'_fst_fst_fst_assoc, Cover.add_toPreZeroHypercover, Cover.RelativeGluingData.preimage_toBase_eq_range_ι, affineBasisCover_map_range, Cover.map_prop, Cover.LocallyDirected.w, Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, Cover.Over.isOver_map, Pullback.cocycle_snd_snd, Cover.mkOfCovers_f, Hom.ι_fromNormalization, mem_pretopology_iff, Cover.pullbackCoverOverProp'_I₀, Pullback.t_snd_assoc, GlueData.openCover_I₀, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, Pullback.cocycle_snd_fst_snd, Cover.ColimitGluingData.functor_map, Cover.intersectionOfLocallyDirected_f, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, Pullback.openCoverOfLeft_f, OpenCover.restrict_X, Cover.mem_pretopology, affineOneHypercover_toPreOneHypercover_toPreZeroHypercover, Pullback.t_fst_fst_assoc, Pullback.pullbackP1Iso_hom_fst, openCoverBasicOpenTop_f, Cover.pullbackHom_map_assoc, Cover.gluedCoverT'_fst_fst_assoc, OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected, Cover.ColimitGluingData.pullbackGluedIso_inv_snd, Cover.functorOfLocallyDirectedHomBase_app, Cover.ColimitGluingData.pullbackGluedIso_inv_fst, AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, instJointlySurjectivePrecoverage, Cover.ColimitGluingData.functor_obj, Pullback.openCoverOfLeftRight_X, Pullback.lift_comp_ι, Cover.ColimitGluingData.relativeGluingData_natTrans_app, Cover.pullbackHom_map, isAffine_affineCover, AffineZariskiSite.directedCover_I₀, AffineOpenCover.openCover_X, Cover.sigma_f, Pullback.openCoverOfLeft_X, Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor, Cover.RelativeGluingData.isPullback_natTrans_ι_toBase, Pullback.diagonalCover_map, Pullback.t'_snd_fst_snd_assoc, Cover.ι_fromGlued, Hom.presieve₀_cover, Cover.mem_grothendieckTopology, Pullback.gluedLiftPullbackMap_fst, isAffine_affineOpenCover
zariskiPrecoverage 📖	CompOp	5 math math: zariskiPrecoverage_le_fppfPrecoverage, zariskiPrecoverage_le_propQCPrecoverage, zariskiPrecoverage_le_fpqcPrecoverage, 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 AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder 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'	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory 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' 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'	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory 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' 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