PresheafedSpace

📁 Source: Mathlib/Geometry/RingedSpace/PresheafedSpace.lean

Statistics

Metric	Count
Definitions PresheafedSpace, base, c, toPshHom, carrier, categoryOfPresheafedSpaces, coeCarrier, comp, const, forget, homInhabited, id, instCoeFunHomForallCarrierCarrier, instCoeSortType, instInhabited, instTopologicalSpaceCarrierCarrier, isoOfComponents, ofRestrict, presheaf, restrict, restrictTopIso, sheafIsoOfIso, toRestrictTop, Γ, mapPresheaf, onPresheaf	26
Theorems ext, base_isIso_of_iso, c_isIso_of_iso, comp_base, comp_base_assoc, comp_c, comp_c_app, comp_c_app_assoc, congr_app, ext, forget_map, forget_obj, hext, id_base, id_c, id_c_app, isIso_of_components, isoOfComponents_hom, isoOfComponents_inv, ofRestrict_base, ofRestrict_c_app, ofRestrict_mono, ofRestrict_top_c, restrictTopIso_hom, restrictTopIso_inv, restrict_carrier, restrict_presheaf, restrict_top_presheaf, sheafIsoOfIso_hom, sheafIsoOfIso_inv, toRestrictTop_base, toRestrictTop_c, Γ_map, Γ_map_op, Γ_obj, Γ_obj_op, mapPresheaf_map_c, mapPresheaf_map_f, mapPresheaf_obj_X, mapPresheaf_obj_presheaf	40
Total	66

AlgebraicGeometry

Definitions

Name	Category	Theorems
PresheafedSpace 📖	CompData	211 math math: SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right', Spec.toPresheafedSpace_obj, ΓSpec.locallyRingedSpaceAdjunction_counit_app, SheafedSpace.forgetToPresheafedSpace_obj, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, PresheafedSpace.IsOpenImmersion.mono, SheafedSpace.colimit_exists_rep, SheafedSpace.IsOpenImmersion.app_invApp, PresheafedSpace.isoOfComponents_inv, PresheafedSpace.IsOpenImmersion.ofIso, LocallyRingedSpace.homMk_toHom, PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left', SheafedSpace.IsOpenImmersion.invApp_app_apply, PresheafedSpace.GlueData.ιIsOpenImmersion, localRingHom_comp_stalkIso_apply, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c, PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, LocallyRingedSpace.Hom.toShHom_mk, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, PresheafedSpace.Γ_obj_op, Scheme.forgetToTop_map, LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, PresheafedSpace.componentwiseDiagram_map, SheafedSpace.isoMk_hom, SheafedSpace.comp_hom_c_app, PresheafedSpace.isoOfComponents_hom, PresheafedSpace.comp_c_app, CategoryTheory.Functor.mapPresheaf_map_f, PresheafedSpace.GlueData.snd_invApp_t_app_assoc, Scheme.Opens.germ_stalkIso_inv, SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, PresheafedSpace.GlueData.pullback_base, SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, ΓSpec.locallyRingedSpaceAdjunction_counit_app', LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace, PresheafedSpace.Γ_map_op, PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft, PresheafedSpace.IsOpenImmersion.pullbackFstOfRight, PresheafedSpace.IsOpenImmersion.to_iso, SheafedSpace.comp_base, PresheafedSpace.colimitCocone_ι_app_base, SheafedSpace.comp_c_app, LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, SheafedSpace.id_hom_c_app, Spec_map_localization_isIso, PresheafedSpace.GlueData.ι_image_preimage_eq, morphismRestrict_appLE, PresheafedSpace.instPreservesColimitsOfShapeTopCatForget, PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion, Scheme.Opens.germ_stalkIso_inv_assoc, PresheafedSpace.isIso_of_components, PresheafedSpace.forget_obj, PresheafedSpace.instHasColimitsOfShape, SheafedSpace.IsOpenImmersion.image_preimage_is_empty, PresheafedSpace.IsOpenImmersion.isoOfRangeEq_hom, ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, PresheafedSpace.GlueData.opensImagePreimageMap_app, PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, SheafedSpace.ofRestrict_hom_c_app, Scheme.Opens.germ_stalkIso_hom, PresheafedSpace.ofRestrict_mono, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_base, PresheafedSpace.GlueData.opensImagePreimageMap_app', SheafedSpace.id_hom_base, PresheafedSpace.forget_map, PresheafedSpace.stalkMap.id, Spec.toPresheafedSpace_map_op, PresheafedSpace.restrictTopIso_hom, PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, PresheafedSpace.sheafIsoOfIso_inv, ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', stalkMap_toStalk, PresheafedSpace.IsOpenImmersion.lift_fac_assoc, SheafedSpace.Γ_map, PresheafedSpace.GlueData.f_invApp_f_app_assoc, Spec.sheafedSpaceMap_hom_c_app, PresheafedSpace.GlueData.ι_isOpenEmbedding, PresheafedSpace.GlueData.f_open, SheafedSpace.restrictTopIso_inv, PresheafedSpace.IsOpenImmersion.hasPullback_of_right, PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst, PresheafedSpace.comp_c_app_assoc, SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, SheafedSpace.fullyFaithfulForgetToPresheafedSpace_preimage_hom, LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, PresheafedSpace.IsOpenImmersion.isoOfRangeEq_inv, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base, PresheafedSpace.instHasColimits, PresheafedSpace.GlueData.componentwise_diagram_π_isIso, PresheafedSpace.map_id_c_app, SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, PresheafedSpace.GlueData.f_invApp_f_app, Spec.locallyRingedSpaceMap_toHom, LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right, PresheafedSpace.sheafIsoOfIso_hom, PresheafedSpace.colimit_presheaf, PresheafedSpace.id_base, SheafedSpace.comp_hom_c_app', PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion, PresheafedSpace.componentwiseDiagram_obj, PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, PresheafedSpace.Γ_obj, SheafedSpace.comp_hom_base, PresheafedSpace.forget_preservesColimits, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, stalkMap_toStalk_apply, LocallyRingedSpace.forgetToTop_map, PresheafedSpace.comp_base, PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom, PresheafedSpace.GlueData.snd_invApp_t_app, SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left, CategoryTheory.Functor.mapPresheaf_map_c, PresheafedSpace.IsOpenImmersion.hasPullback_of_left, SheafedSpace.IsOpenImmersion.app_invApp_assoc, SheafedSpace.IsOpenImmersion.stalk_iso, SheafedSpace.IsOpenImmersion.invApp_app, LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, Scheme.Opens.germ_stalkIso_hom_assoc, Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, PresheafedSpace.IsOpenImmersion.comp, PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, SheafedSpace.forgetToPresheafedSpace_map, PresheafedSpace.IsOpenImmersion.lift_fac, SheafedSpace.id_hom, PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val, isIso_SpecMap_stakMap_localization, PresheafedSpace.pushforwardDiagramToColimit_map, PresheafedSpace.Γ_map, SheafedSpace.id_hom_c, SheafedSpace.id_c_app, SheafedSpace.forgetToPresheafedSpace_full, PresheafedSpace.stalkMap.comp, PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight, PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft, CategoryTheory.Functor.mapPresheaf_obj_X, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, ΓSpec.toSpecΓ_of, PresheafedSpace.comp_base_assoc, LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, Spec.sheafedSpaceMap_hom_base, PresheafedSpace.pushforwardDiagramToColimit_obj, StructureSheaf.toPushforwardStalk_comp, SheafedSpace.ofRestrict_hom_base, SheafedSpace.Γ_def, SheafedSpace.IsOpenImmersion.forgetMapIsOpenImmersion, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_c, StructureSheaf.toPushforwardStalk_comp_assoc, Spec.toPresheafedSpace_obj_op, PresheafedSpace.GlueData.ι_jointly_surjective, LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, Scheme.Hom.isIso_toPshHom, PresheafedSpace.id_c_app, SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding, LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, SheafedSpace.id_c, LocallyRingedSpace.comp_toHom, PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, Spec.toPresheafedSpace_map, SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, LocallyRingedSpace.forgetToSheafedSpace_map, PresheafedSpace.id_c, Scheme.Opens.ι_appLE, SheafedSpace.isOpenImmersion_iff_hom, SheafedSpace.id_base, PresheafedSpace.colimit_carrier, SheafedSpace.congr_hom_app, PresheafedSpace.GlueData.ιInvApp_π, PresheafedSpace.GlueData.π_ιInvApp_π, SheafedSpace.is_presheafedSpace_iso, LocallyRingedSpace.toΓSpecMapBasicOpen_eq, PresheafedSpace.ColimitCoconeIsColimit.desc_fac, LocallyRingedSpace.toStalk_stalkMap_toΓSpec, LocallyRingedSpace.id_toHom, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, SheafedSpace.congr_app, SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, LocallyRingedSpace.isLocalHom_stalkMap_congr, PresheafedSpace.restrictTopIso_inv, LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, SheafedSpace.IsOpenImmersion.invApp_app_assoc, PresheafedSpace.map_comp_c_app, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, SheafedSpace.isColimit_exists_rep, SheafedSpace.IsOpenImmersion.inv_invApp, PresheafedSpace.GlueData.π_ιInvApp_eq_id, localRingHom_comp_stalkIso, PresheafedSpace.GlueData.snd_invApp_t_app', CategoryTheory.Functor.mapPresheaf_obj_presheaf, LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, SheafedSpace.forgetToPresheafedSpace_faithful, PresheafedSpace.colimitCocone_ι_app_c, PresheafedSpace.colimitCocone_pt, SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, SheafedSpace.restrictTopIso_hom, ΓSpec.toSpecΓ_unop, SheafedSpace.Γ_map_op, SheafedSpace.GlueData.ι_jointly_surjective, SheafedSpace.comp_c_app', LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, SheafedSpace.isoMk_inv

AlgebraicGeometry.PresheafedSpace

Definitions

Name	Category	Theorems
carrier 📖	CompOp	1349 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.irreducibleSpace_of_isIntegral, AlgebraicGeometry.Scheme.height_of_isClosed, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, AlgebraicGeometry.Scheme.isoOfEq_inv, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.zeroLocus_iInf, AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp, AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, IsOpenImmersion.stalk_iso, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, AlgebraicGeometry.Scheme.support_nilradical, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral, AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.range_eq_range_of_surjective, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.SheafedSpace.colimit_exists_rep, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, AlgebraicGeometry.Scheme.Hom.range_fiberι, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.Cover.iUnion_range, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.mem_basicOpen', AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.Scheme.Hom.mem_opensRange, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.Scheme.SpecToEquivOfField_eq_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.isCompact_iff_exists, isoOfComponents_inv, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Scheme.RationalMap.dense_domain, AlgebraicGeometry.HasRingHomProperty.stalkMap, IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.Scheme.Hom.id_appTop, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, AlgebraicGeometry.image_morphismRestrict_preimage, IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.Scheme.IdealSheafData.gc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.Scheme.zeroLocus_mul, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.SpecMap_preimage_basicOpen, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp, AlgebraicGeometry.Scheme.hom_inv_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.Hom.range_asFiberHom, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite, AlgebraicGeometry.Scheme.ι_toIso_inv, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.Spec.sheafedSpaceObj_carrier, AlgebraicGeometry.noetherianSpace_of_isAffine, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.Scheme.preimage_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.IdealSheafData.support_mul, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Γ_obj_op, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, IsOpenImmersion.isoRestrict_hom_c_app, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.forget_obj, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, colimitPresheafObjIsoComponentwiseLimit_hom_π, componentwiseDiagram_map, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, IsOpenImmersion.invApp_app, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.compactSpace_of_isAffine, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, AlgebraicGeometry.Scheme.comp_base, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, isoOfComponents_hom, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.Scheme.Hom.image_iSup₂, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.zeroLocus_singleton, AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme, comp_c_app, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.component_nontrivial, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.Scheme.hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.isNoetherian_iff, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.Scheme.toSpecΓ_naturality, GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.IsNoetherian.toCompactSpace, AlgebraicGeometry.IsIntegral.nonempty, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.IsNoetherian.noetherianSpace, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.Scheme.homeoOfIso_symm, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Scheme.comp_coeBase_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.Scheme.Hom.toPartialMap_domain, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.RingedSpace.zeroLocus_isClosed, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.hy, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Hom.id_app, AlgebraicGeometry.Scheme.Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Proj.mem_basicOpen, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.Scheme.preimage_basicOpen_top, GlueData.pullback_base, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.quasiCompact_over_affine_iff, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.Scheme.germToFunctionField_injective, AlgebraicGeometry.Scheme.Hom.isIso_base, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', AlgebraicGeometry.Scheme.hom_base_inv_base_assoc, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, AlgebraicGeometry.Scheme.zeroLocus_setMul, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AlgebraicGeometry.Scheme.Opens.nonempty_iff, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.RingedSpace.basicOpen_pow, IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Modules.toPresheaf_obj, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, Γ_map_op, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, AlgebraicGeometry.SheafedSpace.comp_base, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.isInitial_iff_isEmpty, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.basicOpen_le, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.Scheme.Modules.isSheaf, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.Scheme.zeroLocus_def, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.tilde.isoTop_hom, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.IsArtinianScheme.finite, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, ModuleCat.Tilde.toOpen_res, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, AlgebraicGeometry.Scheme.id.base, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, GlueData.ι_image_preimage_eq, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, stalkMap.congr, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Scheme.residue_descResidueField, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Opens.toScheme_carrier, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_apply, AlgebraicGeometry.LocallyRingedSpace.stalkMap_id, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.Proj.basicOpen_mul, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.homeoOfIso_apply, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Modules.restrict_map, AlgebraicGeometry.Scheme.PartialMap.restrict_id, AlgebraicGeometry.isIso_stalkMap_coprodSpec, forget_obj, AlgebraicGeometry.AffineSpace.spec_le_iff, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.Opens.exists_toScheme, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.Scheme.IdealSheafData.support_antitone, AlgebraicGeometry.Scheme.component_nontrivial, AlgebraicGeometry.isCompl_range_inl_inr, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, GlueData.opensImagePreimageMap_app, AlgebraicGeometry.Scheme.basicOpen_pow, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, AlgebraicGeometry.LocallyRingedSpace.comp_base, AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.isSpectralMap, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, AlgebraicGeometry.mem_range_iff_of_surjective, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.Modules.toPresheaf_map, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support, AlgebraicGeometry.Scheme.zeroLocus_radical, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.compactSpace_iff_quasiCompact, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, AlgebraicGeometry.RingedSpace.basicOpen_le, AlgebraicGeometry.Scheme.Opens.ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.Scheme.comp_base_assoc, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.Scheme.stalkMap_id, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, GlueData.opensImagePreimageMap_app', AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, AlgebraicGeometry.SheafedSpace.id_hom_base, AlgebraicGeometry.LocallyRingedSpace.restrict_carrier, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.isIso_iff_isOpenImmersion, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.Scheme.zeroLocus_inf, AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.surjective_iff, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, stalkMap.id, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, restrictTopIso_hom, IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.isLocalIso_iff, sheafIsoOfIso_inv, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.stalkMap_toStalk, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.IsLocallyArtinian.discreteTopology, AlgebraicGeometry.Scheme.Hom.isOpenMap, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.tilde.isIso_toOpen_top, AlgebraicGeometry.Scheme.instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.Hom.prop, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, stalkMap.isIso, AlgebraicGeometry.IsProper.instMorphismRestrict, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.IsArtinianScheme.toCompactSpace, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, AlgebraicGeometry.Scheme.IdealSheafData.support_comap, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.SheafedSpace.Γ_map, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField, AlgebraicGeometry.Scheme.iso_inv_base_hom_base, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.range_eq_univ, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Proj.basicOpen_mono, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, AlgebraicGeometry.Scheme.residueFieldCongr_trans, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.pointOfClosedPoint_apply, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, GlueData.ι_isOpenEmbedding, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton, AlgebraicGeometry.Scheme.stalkMap_comp, comp_c_app_assoc, AlgebraicGeometry.Scheme.residue_surjective, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing, AlgebraicGeometry.Scheme.basicOpen_one, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, base_isIso_of_iso, AlgebraicGeometry.over_def, IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.Modules.Hom.id_app, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, AlgebraicGeometry.Scheme.Cover.ulift_I₀, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.Modules.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, AlgebraicGeometry.coprodSpec_coprodMk, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.isRetrocompact_basicOpen, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, AlgebraicGeometry.quasiSeparatedSpace_of_isAffine, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.SheafedSpace.mk_coe, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, AlgebraicGeometry.Spec_carrier, AlgebraicGeometry.isArtinianScheme_iff, AlgebraicGeometry.Scheme.Hom.id_appIso, AlgebraicGeometry.Scheme.empty_carrier_carrier, AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι, map_id_c_app, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, AlgebraicGeometry.Proj.basicOpen_one, GlueData.f_invApp_f_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.Scheme.isoSpec_Spec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, c_isIso_of_iso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.compactSpace_iff_exists, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible, AlgebraicGeometry.Scheme.Hom.preimage_sup, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.Scheme.iso_hom_base_inv_base, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.residueFieldCongr_refl, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, ofRestrict_top_c, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.Scheme.Hom.image_iSup, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.SheafedSpace.Γ_obj_op, sheafIsoOfIso_hom, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.Scheme.Hom.isOpen_quasiFiniteAt, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, id_base, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.Proj.isBasis_basicOpen, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, componentwiseDiagram_obj, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.geometricallyIrreducible_iff, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, AlgebraicGeometry.Scheme.Hom.fiberι_asFiber, AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.Scheme.default_asIdeal, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.Hom.id_base, IsOpenImmersion.c_iso, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.AffineCover.covers, Γ_obj, AlgebraicGeometry.SheafedSpace.comp_hom_base, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsFinite.finite_preimage_singleton, toRestrictTop_c, AlgebraicGeometry.IsLocalAtTarget.restrict, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, comp_base, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, AlgebraicGeometry.Scheme.Modules.restrict_obj, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, GlueData.snd_invApp_t_app, IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.Scheme.Modules.Hom.add_app, AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.isBasis_affine_open, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.RingedSpace.basicOpen_res_eq, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, AlgebraicGeometry.Flat.stalkMap, AlgebraicGeometry.Scheme.Pullback.range_snd, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, IsOpenImmersion.pullback_cone_of_left_condition, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.IsPreimmersion.base_embedding, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.forall_toScheme, AlgebraicGeometry.Scheme.topIso_hom, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, AlgebraicGeometry.finite_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.Scheme.inv_hom_apply, AlgebraicGeometry.instIsPreimmersionFromSpecStalk, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_map, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, stalkMap.congr_hom, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, Γ_map, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.SheafedSpace.id_hom_c, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', AlgebraicGeometry.Scheme.residue_residueFieldCongr, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, AlgebraicGeometry.LocallyRingedSpace.isLocalRing, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, stalkMap.comp, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact, AlgebraicGeometry.Scheme.IsQuasiAffine.toCompactSpace, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.Scheme.Hom.comp_base_assoc, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, CategoryTheory.Functor.mapPresheaf_obj_X, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, AlgebraicGeometry.Scheme.Hom.image_le_opensRange, AlgebraicGeometry.noetherianSpace_of_isAffineOpen, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, AlgebraicGeometry.smoothOfRelativeDimension_iff, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE, AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, AlgebraicGeometry.ΓSpec.toSpecΓ_of, AlgebraicGeometry.Scheme.zeroLocus_span, comp_base_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, AlgebraicGeometry.Scheme.Hom.image_injective, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, AlgebraicGeometry.SheafedSpace.Γ_obj, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, AlgebraicGeometry.Proj.basicOpen_zero, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.formallyUnramified_iff, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.isClosedImmersion_iff, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.Spec_closedPoint, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.Hom.finite_preimage, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField, AlgebraicGeometry.quasiCompact_iff_compactSpace, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.Surjective.surj, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.Scheme.comp_base_apply, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, GlueData.ι_jointly_surjective, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.IsDominant.denseRange, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, congr_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.compactSpace_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.fromSpec_top, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, AlgebraicGeometry.Scheme.Hom.homeomorph_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.Scheme.IdealSheafData.support_top, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, id_c_app, AlgebraicGeometry.Scheme.Hom.comp_appTop, AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.Scheme.Hom.surjective, AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.SheafedSpace.id_c, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.etale_iff, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.isAffineOpen_bot, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, AlgebraicGeometry.Scheme.Opens.ι_image_le, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, AlgebraicGeometry.tilde.toOpen_map_app_assoc, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, id_c, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, AlgebraicGeometry.Scheme.Hom.comp_image, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued, toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.residue_descResidueField_assoc, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.instIsPreimmersionAsFiberHom, AlgebraicGeometry.locallyOfFinitePresentation_iff, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, AlgebraicGeometry.SheafedSpace.id_base, colimit_carrier, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.Scheme.toIso_inv_ι, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, GlueData.ιInvApp_π, AlgebraicGeometry.Scheme.Hom.opensRange_comp, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Scheme.Hom.comp_base, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.genericPoint_eq_bot_of_affine, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, IsOpenImmersion.base_open, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.IsSeparated.instMorphismRestrict, AlgebraicGeometry.Scheme.PartialMap.dense_domain, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, AlgebraicGeometry.Scheme.restrictFunctor_obj_left, AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.Scheme.Hom.stalkMap_id, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, GlueData.π_ιInvApp_π, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.Scheme.basicOpen_restrict, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Opens.ι_image_top, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.range_fromSpecResidueField, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.Scheme.zeroLocus_isClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.Scheme.Γ_obj_op, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, IsOpenImmersion.inv_invApp, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, comp_c, AlgebraicGeometry.Scheme.Hom.mem_quasiFiniteLocus, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.inv_base_hom_base_assoc, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, AlgebraicGeometry.Scheme.JointlySurjective.exists_eq, AlgebraicGeometry.Scheme.Hom.image_le_image_iff, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom_assoc, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.isIso_fromTildeΓ_iff, AlgebraicGeometry.Scheme.residueFieldCongr_inv, AlgebraicGeometry.Scheme.coe_homeoOfIso, restrictTopIso_inv, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, AlgebraicGeometry.Scheme.RationalMap.mem_domain, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.spec_punit_isEmpty, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian, map_comp_c_app, AlgebraicGeometry.isReduced_stalk_of_isReduced, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, AlgebraicGeometry.SheafedSpace.isColimit_exists_rep, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.codisjoint_zeroLocus, AlgebraicGeometry.Scheme.PartialMap.restrict_id_hom, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.initial_isEmpty, AlgebraicGeometry.Scheme.residueFieldMap_comp, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm, AlgebraicGeometry.Scheme.comp_coeBase, GlueData.π_ιInvApp_eq_id, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, restrict_top_presheaf, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.coe_opensRestrict_apply_coe, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Scheme.Hom.inv_app, GlueData.snd_invApp_t_app', AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian, AlgebraicGeometry.Scheme.Hom.app_injective, CategoryTheory.Functor.mapPresheaf_obj_presheaf, AlgebraicGeometry.Scheme.Modules.inv_app, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.coprodMk_inr, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, AlgebraicGeometry.Scheme.instEpiCommRingCatResidue, AlgebraicGeometry.Scheme.Hom.isProperMap, AlgebraicGeometry.Scheme.isoOfEq_hom, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, AlgebraicGeometry.Scheme.le_iff_specializes, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, colimitCocone_ι_app_c, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Scheme.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Spec_stalkClosedPointIso, AlgebraicGeometry.Scheme.Opens.ι_base_apply, AlgebraicGeometry.Scheme.Hom.eqToHom_app, AlgebraicGeometry.instIsAffineHomιBasicOpen, AlgebraicGeometry.Scheme.id_app, AlgebraicGeometry.flat_iff, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.Scheme.residueFieldCongr_symm, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base_apply, AlgebraicGeometry.Scheme.homOfLE_rfl, AlgebraicGeometry.Scheme.fromSpecResidueField_apply, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, AlgebraicGeometry.Scheme.IdealSheafData.le_def, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, AlgebraicGeometry.Scheme.inv_base_hom_base, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective, IsOpenImmersion.instIsIsoInvApp, AlgebraicGeometry.quasiSeparated_over_affine_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, stalkMap.congr_point, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.Scheme.affineBasicOpen_le, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.Scheme.Cover.fromGlued_injective, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.Spec.map_base_apply, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, AlgebraicGeometry.tilde.toOpen_map_app, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, AlgebraicGeometry.Scheme.Hom.id_image, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
categoryOfPresheafedSpaces 📖	CompOp	211 math math: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right', AlgebraicGeometry.Spec.toPresheafedSpace_obj, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_obj, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, IsOpenImmersion.pullbackConeOfLeftLift_snd, IsOpenImmersion.mono, AlgebraicGeometry.SheafedSpace.colimit_exists_rep, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, isoOfComponents_inv, IsOpenImmersion.ofIso, AlgebraicGeometry.LocallyRingedSpace.homMk_toHom, IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, GlueData.ιIsOpenImmersion, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, IsOpenImmersion.toSheafedSpaceHom_hom_c, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom_mk, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Γ_obj_op, AlgebraicGeometry.Scheme.forgetToTop_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, IsOpenImmersion.isoRestrict_hom_c_app, colimitPresheafObjIsoComponentwiseLimit_hom_π, componentwiseDiagram_map, AlgebraicGeometry.SheafedSpace.isoMk_hom, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, isoOfComponents_hom, comp_c_app, CategoryTheory.Functor.mapPresheaf_map_f, GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, GlueData.pullback_base, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, IsOpenImmersion.sheafedSpace_toSheafedSpace, Γ_map_op, IsOpenImmersion.pullbackSndOfLeft, IsOpenImmersion.pullbackFstOfRight, IsOpenImmersion.to_iso, AlgebraicGeometry.SheafedSpace.comp_base, colimitCocone_ι_app_base, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.Spec_map_localization_isIso, GlueData.ι_image_preimage_eq, AlgebraicGeometry.morphismRestrict_appLE, instPreservesColimitsOfShapeTopCatForget, IsOpenImmersion.pullbackToBaseIsOpenImmersion, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, isIso_of_components, forget_obj, instHasColimitsOfShape, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, IsOpenImmersion.isoOfRangeEq_hom, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, GlueData.opensImagePreimageMap_app, ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, ofRestrict_mono, IsOpenImmersion.toSheafedSpaceHom_base, GlueData.opensImagePreimageMap_app', AlgebraicGeometry.SheafedSpace.id_hom_base, forget_map, stalkMap.id, AlgebraicGeometry.Spec.toPresheafedSpace_map_op, restrictTopIso_hom, IsOpenImmersion.isoRestrict_hom_ofRestrict, sheafIsoOfIso_inv, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.stalkMap_toStalk, IsOpenImmersion.lift_fac_assoc, AlgebraicGeometry.SheafedSpace.Γ_map, GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, GlueData.ι_isOpenEmbedding, GlueData.f_open, AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, IsOpenImmersion.hasPullback_of_right, IsOpenImmersion.pullbackConeOfLeftLift_fst, comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace_preimage_hom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, IsOpenImmersion.isoOfRangeEq_inv, IsOpenImmersion.toSheafedSpaceHom_hom_base, instHasColimits, GlueData.componentwise_diagram_π_isIso, map_id_c_app, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, GlueData.f_invApp_f_app, AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right, sheafIsoOfIso_hom, colimit_presheaf, id_base, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', IsOpenImmersion.pullbackConeSndIsOpenImmersion, componentwiseDiagram_obj, IsOpenImmersion.pullback_snd_isIso_of_range_subset, Γ_obj, AlgebraicGeometry.SheafedSpace.comp_hom_base, forget_preservesColimits, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map, comp_base, GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom, GlueData.snd_invApp_t_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left, CategoryTheory.Functor.mapPresheaf_map_c, IsOpenImmersion.hasPullback_of_left, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, IsOpenImmersion.comp, IsOpenImmersion.pullback_cone_of_left_condition, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map, IsOpenImmersion.lift_fac, AlgebraicGeometry.SheafedSpace.id_hom, IsOpenImmersion.toLocallyRingedSpaceHom_val, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, pushforwardDiagramToColimit_map, Γ_map, AlgebraicGeometry.SheafedSpace.id_hom_c, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full, stalkMap.comp, IsOpenImmersion.forget_preservesLimitsOfRight, IsOpenImmersion.forget_preservesLimitsOfLeft, CategoryTheory.Functor.mapPresheaf_obj_X, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, AlgebraicGeometry.ΓSpec.toSpecΓ_of, comp_base_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_base, pushforwardDiagramToColimit_obj, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_base, AlgebraicGeometry.SheafedSpace.Γ_def, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetMapIsOpenImmersion, IsOpenImmersion.toSheafedSpaceHom_c, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.Spec.toPresheafedSpace_obj_op, GlueData.ι_jointly_surjective, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.Scheme.Hom.isIso_toPshHom, id_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, AlgebraicGeometry.SheafedSpace.id_c, AlgebraicGeometry.LocallyRingedSpace.comp_toHom, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.Spec.toPresheafedSpace_map, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_map, id_c, AlgebraicGeometry.Scheme.Opens.ι_appLE, AlgebraicGeometry.SheafedSpace.isOpenImmersion_iff_hom, AlgebraicGeometry.SheafedSpace.id_base, colimit_carrier, AlgebraicGeometry.SheafedSpace.congr_hom_app, GlueData.ιInvApp_π, GlueData.π_ιInvApp_π, AlgebraicGeometry.SheafedSpace.is_presheafedSpace_iso, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, ColimitCoconeIsColimit.desc_fac, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.LocallyRingedSpace.id_toHom, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, restrictTopIso_inv, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, map_comp_c_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.SheafedSpace.isColimit_exists_rep, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, GlueData.π_ιInvApp_eq_id, AlgebraicGeometry.localRingHom_comp_stalkIso, GlueData.snd_invApp_t_app', CategoryTheory.Functor.mapPresheaf_obj_presheaf, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful, colimitCocone_ι_app_c, colimitCocone_pt, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.SheafedSpace.isoMk_inv
coeCarrier 📖	CompOp	—
comp 📖	CompOp	1 math math: comp_c
const 📖	CompOp	—
forget 📖	CompOp	14 math math: colimitCocone_ι_app_base, instPreservesColimitsOfShapeTopCatForget, forget_obj, ColimitCoconeIsColimit.desc_c_naturality, forget_map, sheafIsoOfIso_inv, colimit_presheaf, forget_preservesColimits, pushforwardDiagramToColimit_map, IsOpenImmersion.forget_preservesLimitsOfRight, IsOpenImmersion.forget_preservesLimitsOfLeft, pushforwardDiagramToColimit_obj, colimit_carrier, colimitCocone_ι_app_c
homInhabited 📖	CompOp	—
id 📖	CompOp	—
instCoeFunHomForallCarrierCarrier 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instInhabited 📖	CompOp	—
instTopologicalSpaceCarrierCarrier 📖	CompOp	15 math math: GlueData.snd_invApp_t_app_assoc, IsOpenImmersion.inv_naturality_assoc, GlueData.ι_image_preimage_eq, GlueData.opensImagePreimageMap_app, GlueData.opensImagePreimageMap_app', GlueData.ι_isOpenEmbedding, IsOpenImmersion.app_invApp, GlueData.f_invApp_f_app, IsOpenImmersion.c_iso, GlueData.opensImagePreimageMap_app_assoc, GlueData.snd_invApp_t_app, IsOpenImmersion.inv_naturality, IsOpenImmersion.base_open, IsOpenImmersion.app_invApp_assoc, GlueData.snd_invApp_t_app'
isoOfComponents 📖	CompOp	2 math math: isoOfComponents_inv, isoOfComponents_hom
ofRestrict 📖	CompOp	16 math math: IsOpenImmersion.isoRestrict_inv_ofRestrict, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, IsOpenImmersion.ofRestrict_invApp, IsOpenImmersion.ofRestrict_invApp_apply, ofRestrict_stalkMap_isIso, ofRestrict_mono, restrictTopIso_hom, IsOpenImmersion.isoRestrict_hom_ofRestrict, IsOpenImmersion.ofRestrict, ofRestrict_top_c, IsOpenImmersion.pullback_cone_of_left_condition, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, restrictStalkIso_inv_eq_ofRestrict, ofRestrict_base, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, ofRestrict_c_app
presheaf 📖	CompOp	874 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, AlgebraicGeometry.Scheme.zeroLocus_iInf, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, AlgebraicGeometry.Etale.etale_appLE, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, AlgebraicGeometry.LocallyQuasiFinite.quasiFinite_appLE, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, IsOpenImmersion.stalk_iso, stalkMap_germ, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.Scheme.ofRestrict_appIso, AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset, AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral, AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.mem_basicOpen', AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, isoOfComponents_inv, AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.HasRingHomProperty.stalkMap, IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.Scheme.Hom.id_appTop, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, AlgebraicGeometry.Scheme.zeroLocus_mul, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk, AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponents, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, IsOpenImmersion.app_inv_app', AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_compHom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Γ_obj_op, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, IsOpenImmersion.isoRestrict_hom_c_app, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, colimitPresheafObjIsoComponentwiseLimit_hom_π, componentwiseDiagram_map, stalkMap_germ_assoc, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, stalkMap.stalkSpecializes_stalkMap, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, IsOpenImmersion.isIso_of_subset, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, isoOfComponents_hom, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.Scheme.Hom.appLE_map', AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.zeroLocus_singleton, comp_c_app, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.component_nontrivial, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.isLocallyArtinian_iff_of_isOpenCover, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.Scheme.toSpecΓ_naturality, GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.Scheme.Hom.smooth_appLE, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, AlgebraicGeometry.Scheme.comp_appLE, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.ofRestrict_appLE, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Hom.id_app, AlgebraicGeometry.Scheme.Γ_obj, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι_assoc, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.Scheme.germToFunctionField_injective, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, AlgebraicGeometry.Scheme.zeroLocus_setMul, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.RingedSpace.basicOpen_pow, IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, Γ_map_op, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, stalkMap.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.Scheme.zeroLocus_def, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.Scheme.restrict_presheaf_obj, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, stalkMap.congr, AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE, AlgebraicGeometry.Scheme.residue_descResidueField, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.RingedSpace.res_zero, restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Scheme.Hom.comp_appLE, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk, AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.LocallyRingedSpace.stalkMap_id, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, AlgebraicGeometry.FormallyUnramified.formallyUnramified_of_affine_subset, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.formallySmooth_stalkMap_iff, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map_assoc, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, AlgebraicGeometry.Scheme.component_nontrivial, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, GlueData.opensImagePreimageMap_app, AlgebraicGeometry.Scheme.basicOpen_pow, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, AlgebraicGeometry.HasRingHomProperty.appLE, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, IsOpenImmersion.app_inv_app'_assoc, ofRestrict_stalkMap_isIso, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.zeroLocus_radical, AlgebraicGeometry.Scheme.Hom.map_appLE_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, AlgebraicGeometry.Scheme.Opens.ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.Scheme.stalkMap_id, AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, GlueData.opensImagePreimageMap_app', AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.zeroLocus_map, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.Scheme.evaluation_naturality, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.Scheme.zeroLocus_inf, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.germ_injective_of_isIntegral, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, stalkMap.id, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, sheafIsoOfIso_inv, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.stalkMap_toStalk, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.Scheme.Hom.app_invApp', AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.Hom.prop, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc, stalkMap.isIso, AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.SheafedSpace.Γ_map, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι, AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, AlgebraicGeometry.Scheme.evaluation_naturality_apply, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appLE_map_assoc, AlgebraicGeometry.Scheme.stalkMap_comp, comp_c_app_assoc, AlgebraicGeometry.Scheme.residue_surjective, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.Scheme.basicOpen_one, AlgebraicGeometry.over_def, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE_assoc, IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, AlgebraicGeometry.Scheme.Hom.id_appIso, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, map_id_c_app, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, GlueData.f_invApp_f_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.Scheme.Hom.etale_appLE, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.Scheme.isoSpec_Spec, c_isIso_of_iso, AlgebraicGeometry.Scheme.Hom.appLE_congr, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, ofRestrict_top_c, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, stalkMap_germ_apply, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.SheafedSpace.Γ_obj_op, sheafIsoOfIso_hom, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, colimit_presheaf, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot, AlgebraicGeometry.Scheme.homOfLE_appLE, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.Scheme.Hom.isIso_app, AlgebraicGeometry.Scheme.basicOpen_appLE, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.Flat.flat_of_affine_subset, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, componentwiseDiagram_obj, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, IsOpenImmersion.c_iso, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, Γ_obj, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', toRestrictTop_c, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.stalkMap_germ_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, GlueData.snd_invApp_t_app, IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.Scheme.Hom.map_appLE', AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, IsOpenImmersion.c_iso', AlgebraicGeometry.Flat.flat_appLE, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.RingedSpace.basicOpen_res_eq, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE, AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.Hom.finiteType_appLE, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, AlgebraicGeometry.Flat.stalkMap, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.finite_appTop_of_universallyClosed, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.instIsPreimmersionFromSpecStalk, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, stalkMap.congr_hom, Γ_map, AlgebraicGeometry.SheafedSpace.id_hom_c, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', AlgebraicGeometry.Scheme.residue_residueFieldCongr, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, AlgebraicGeometry.LocallyRingedSpace.isLocalRing, AlgebraicGeometry.Scheme.evaluation_naturality_assoc, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, stalkMap.comp, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, AlgebraicGeometry.smoothOfRelativeDimension_iff, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE, AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.Scheme.empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, AlgebraicGeometry.Scheme.zeroLocus_span, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.SheafedSpace.Γ_obj, AlgebraicGeometry.Scheme.restrict_presheaf_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.formallyUnramified_iff, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.IsAffineOpen.fromSpecStalk_isPreimmersion, AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, pushforwardDiagramToColimit_obj, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.isIso_pushoutSection_iff, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.Smooth.smooth_appLE, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, congr_app, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.IsAffineOpen.fromSpec_top, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.Scheme.map_basicOpen_map, id_c_app, AlgebraicGeometry.Scheme.Hom.comp_appTop, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE_assoc, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.SheafedSpace.id_c, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.etale_iff, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.Scheme.germ_residue_assoc, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, id_c, AlgebraicGeometry.Scheme.Opens.ι_appLE, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.appLE_comp_appLE, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.residue_descResidueField_assoc, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.locallyOfFinitePresentation_iff, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, restrict_presheaf, AlgebraicGeometry.Scheme.germ_residue, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', GlueData.ιInvApp_π, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.Scheme.Hom.map_appLE, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.Scheme.Hom.stalkMap_id, GlueData.π_ιInvApp_π, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.Scheme.basicOpen_restrict, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, AlgebraicGeometry.Scheme.Hom.flat_appLE, AlgebraicGeometry.Scheme.comp_app_assoc, IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, stalkMap.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.Scheme.Γ_obj_op, IsOpenImmersion.inv_invApp, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, comp_c, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.Hom.appLE_map, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen, restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian, map_comp_c_app, AlgebraicGeometry.isReduced_stalk_of_isReduced, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, GlueData.π_ιInvApp_eq_id, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, restrict_top_presheaf, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Scheme.Hom.inv_app, GlueData.snd_invApp_t_app', AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.RingedSpace.mem_basicOpen, AlgebraicGeometry.Scheme.Hom.app_injective, CategoryTheory.Functor.mapPresheaf_obj_presheaf, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, AlgebraicGeometry.Scheme.instEpiCommRingCatResidue, AlgebraicGeometry.Scheme.stalkMap_germ, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Scheme.comp_appLE_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Spec_stalkClosedPointIso, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.eqToHom_app, AlgebraicGeometry.Scheme.id_app, AlgebraicGeometry.flat_iff, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, AlgebraicGeometry.Scheme.IdealSheafData.le_def, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact, IsOpenImmersion.instIsIsoInvApp, stalkMap.congr_point, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.Scheme.mem_basicOpen, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, ofRestrict_c_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
restrict 📖	CompOp	31 math math: AlgebraicGeometry.Scheme.restrict_toPresheafedSpace, IsOpenImmersion.isoRestrict_inv_ofRestrict, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, IsOpenImmersion.isoRestrict_hom_c_app, IsOpenImmersion.ofRestrict_invApp, IsOpenImmersion.ofRestrict_invApp_apply, restrictStalkIso_hom_eq_germ, ofRestrict_stalkMap_isIso, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, ofRestrict_mono, restrictTopIso_hom, IsOpenImmersion.isoRestrict_hom_ofRestrict, IsOpenImmersion.ofRestrict, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, ofRestrict_top_c, toRestrictTop_c, IsOpenImmersion.pullback_cone_of_left_condition, restrict_carrier, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_base, restrictStalkIso_inv_eq_germ, toRestrictTop_base, restrict_presheaf, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, restrictStalkIso_inv_eq_ofRestrict, restrictStalkIso_hom_eq_germ_assoc, restrictTopIso_inv, restrict_top_presheaf, restrictStalkIso_inv_eq_germ_assoc, ofRestrict_base, ofRestrict_c_app
restrictTopIso 📖	CompOp	2 math math: restrictTopIso_hom, restrictTopIso_inv
sheafIsoOfIso 📖	CompOp	2 math math: sheafIsoOfIso_inv, sheafIsoOfIso_hom
toRestrictTop 📖	CompOp	4 math math: AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, toRestrictTop_c, toRestrictTop_base, restrictTopIso_inv
Γ 📖	CompOp	5 math math: Γ_obj_op, Γ_map_op, Γ_obj, Γ_map, AlgebraicGeometry.SheafedSpace.Γ_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_isIso_of_iso 📖	mathematical	—	CategoryTheory.IsIso TopCat TopCat.instCategory carrier Hom.base	—	CategoryTheory.Iso.isIso_hom
c_isIso_of_iso 📖	mathematical	—	CategoryTheory.IsIso TopCat.Presheaf carrier TopCat.instCategoryPresheaf presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward Hom.base Hom.c	—	CategoryTheory.Iso.isIso_hom
comp_base 📖	mathematical	—	Hom.base CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct categoryOfPresheafedSpaces TopCat TopCat.instCategory carrier	—	—
comp_base_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory carrier Hom.base AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_base
comp_c 📖	mathematical	—	Hom.c comp CategoryTheory.CategoryStruct.comp TopCat.Presheaf carrier CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward Hom.base CategoryTheory.Functor.map	—	—
comp_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct categoryOfPresheafedSpaces Hom.c Opposite.op TopologicalSpace.Opens.map Opposite.unop	—	—
comp_c_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces CategoryTheory.NatTrans.app Hom.c Opposite.op TopologicalSpace.Opens.map Opposite.unop	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_c_app
congr_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base Hom.c CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
ext 📖	—	Hom.base CategoryTheory.CategoryStruct.comp TopCat.Presheaf carrier CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.Opens.map Hom.c CategoryTheory.Functor.whiskerRight CategoryTheory.eqToHom CategoryTheory.Functor CategoryTheory.Functor.category	—	—	Hom.ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces TopCat TopCat.instCategory forget Hom.base	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces TopCat TopCat.instCategory forget carrier	—	—
hext 📖	—	Hom.base Quiver.Hom TopCat.Presheaf carrier CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward Hom.c	—	—	—
id_base 📖	mathematical	—	Hom.base CategoryTheory.CategoryStruct.id AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct categoryOfPresheafedSpaces TopCat TopCat.instCategory carrier	—	—
id_c 📖	mathematical	—	Hom.c CategoryTheory.CategoryStruct.id AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct categoryOfPresheafedSpaces TopCat.Presheaf carrier TopCat.instCategoryPresheaf presheaf	—	—
id_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base CategoryTheory.CategoryStruct.id AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct categoryOfPresheafedSpaces Hom.c CategoryTheory.Functor.map CategoryTheory.CategoryStruct.opposite	—	id_c CategoryTheory.Functor.map_id
isIso_of_components 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces	—	CategoryTheory.Iso.isIso_hom
isoOfComponents_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces isoOfComponents TopCat TopCat.instCategory carrier CategoryTheory.Iso.inv TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward presheaf	—	—
isoOfComponents_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces isoOfComponents TopCat TopCat.instCategory carrier TopCat.Presheaf.toPushforwardOfIso presheaf CategoryTheory.Iso.hom TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward	—	—
ofRestrict_base 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	Hom.base restrict ofRestrict	—	—
ofRestrict_c_app 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf CategoryTheory.Functor.obj TopCat.Presheaf restrict TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.c ofRestrict CategoryTheory.Functor.map CategoryTheory.Functor.op IsOpenMap.functor TopologicalSpace.Opens.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp Opposite.unop CategoryTheory.Functor.id CategoryTheory.Adjunction.counit IsOpenMap.adjunction	—	—
ofRestrict_mono 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Mono AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces restrict ofRestrict	—	ext CategoryTheory.cancel_mono TopCat.mono_iff_injective Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding TopCat.Presheaf.ext Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.ext Set.preimage_image_eq congr_app CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Adjunction.whiskerLeft_counit_iso_of_L_fully_faithful IsOpenMap.functorFullOfMono IsOpenMap.functor_faithful CategoryTheory.Category.assoc ofRestrict_c_app comp_c_app CategoryTheory.Functor.congr_obj CategoryTheory.eqToHom_app CategoryTheory.eqToHom_map CategoryTheory.instIsIsoEqToHom CategoryTheory.eqToHom_op CategoryTheory.eqToHom_trans CategoryTheory.inv_eqToHom CategoryTheory.NatTrans.naturality CategoryTheory.NatTrans.naturality_assoc
ofRestrict_top_c 📖	mathematical	—	Hom.c restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding ofRestrict CategoryTheory.eqToHom TopCat.Presheaf CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf presheaf TopCat.Presheaf.pushforward Hom.base	—	TopCat.Presheaf.ext TopologicalSpace.Opens.isOpenEmbedding Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.functor_map_eq_inf inf_of_le_left CategoryTheory.eqToHom_map CategoryTheory.Functor.congr_obj CategoryTheory.eqToHom_app
restrictTopIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding restrictTopIso ofRestrict	—	TopologicalSpace.Opens.isOpenEmbedding
restrictTopIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding restrictTopIso toRestrictTop	—	TopologicalSpace.Opens.isOpenEmbedding
restrict_carrier 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	restrict	—	—
restrict_presheaf 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier carrier TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	presheaf restrict CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op IsOpenMap.functor	—	—
restrict_top_presheaf 📖	mathematical	—	presheaf restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.Iso.inv TopologicalSpace.Opens.inclusionTopIso	—	TopologicalSpace.Opens.isOpenEmbedding Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.inclusion'_top_functor
sheafIsoOfIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom TopCat.Presheaf carrier TopCat.instCategoryPresheaf presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward Hom.base AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces sheafIsoOfIso Hom.c	—	—
sheafIsoOfIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv TopCat.Presheaf carrier TopCat.instCategoryPresheaf presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward Hom.base CategoryTheory.Iso.hom AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces sheafIsoOfIso TopCat.Presheaf.pushforwardToOfIso TopCat TopCat.instCategory forget CategoryTheory.Iso.symm CategoryTheory.Functor.mapIso Hom.c	—	—
toRestrictTop_base 📖	mathematical	—	Hom.base restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding toRestrictTop CategoryTheory.Iso.inv TopologicalSpace.Opens.inclusionTopIso	—	TopologicalSpace.Opens.isOpenEmbedding
toRestrictTop_c 📖	mathematical	—	Hom.c restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding toRestrictTop CategoryTheory.eqToHom TopCat.Presheaf CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf presheaf TopCat.Presheaf.pushforward CategoryTheory.Iso.inv TopologicalSpace.Opens.inclusionTopIso restrict_top_presheaf	—	TopologicalSpace.Opens.isOpenEmbedding
Γ_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.opposite categoryOfPresheafedSpaces Γ CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier carrier Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Hom.c Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
Γ_map_op 📖	mathematical	—	CategoryTheory.Functor.map Opposite AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.opposite categoryOfPresheafedSpaces Γ Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base Hom.c Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
Γ_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.opposite categoryOfPresheafedSpaces Γ TopologicalSpace.Opens TopCat.carrier carrier Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
Γ_obj_op 📖	mathematical	—	CategoryTheory.Functor.obj Opposite AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.opposite categoryOfPresheafedSpaces Γ Opposite.op TopologicalSpace.Opens TopCat.carrier carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—

AlgebraicGeometry.PresheafedSpace.Hom

Definitions

Name	Category	Theorems
base 📖	CompOp	746 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_resLE, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.QuasiCompact.isCompact_preimage, AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc, AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.range_eq_range_of_surjective, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, AlgebraicGeometry.SheafedSpace.colimit_exists_rep, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, AlgebraicGeometry.Scheme.Hom.range_fiberι, AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.Cover.iUnion_range, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.Scheme.Hom.mem_opensRange, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.isCompact_iff_exists, AlgebraicGeometry.HasRingHomProperty.stalkMap, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.Scheme.emptyTo_base, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, AlgebraicGeometry.SpecMap_preimage_basicOpen, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base, AlgebraicGeometry.Scheme.hom_inv_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.Hom.range_asFiberHom, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite, AlgebraicGeometry.Scheme.Hom.preimage_le_preimage_of_le, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.Scheme.preimage_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, AlgebraicGeometry.Scheme.comp_base, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, CategoryTheory.Functor.mapPresheaf_map_f, AlgebraicGeometry.Scheme.hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Scheme.comp_coeBase_assoc, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.hy, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.Scheme.opensRange_homOfLE, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.Scheme.Hom.isIso_base, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Scheme.hom_base_inv_base_assoc, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, AlgebraicGeometry.PresheafedSpace.Γ_map_op, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, AlgebraicGeometry.SheafedSpace.comp_base, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.Scheme.Hom.isConstructible_preimage, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_base, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.id.base, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, AlgebraicGeometry.PresheafedSpace.stalkMap.congr, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_apply, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.homeoOfIso_apply, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.isCompl_range_inl_inr, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.LocallyRingedSpace.comp_base, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.Scheme.Hom.isSpectralMap, AlgebraicGeometry.mem_range_iff_of_surjective, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_base, AlgebraicGeometry.Scheme.comp_base_assoc, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.SheafedSpace.id_hom_base, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.isIso_iff_isOpenImmersion, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.exists_preimage_eq, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.PresheafedSpace.forget_map, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.surjective_iff, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.Hom.isOpenMap, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, AlgebraicGeometry.Scheme.Hom.app_invApp', AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.Hom.prop, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.PresheafedSpace.stalkMap.isIso, AlgebraicGeometry.IsProper.instMorphismRestrict, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, AlgebraicGeometry.Scheme.IdealSheafData.support_comap, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.SheafedSpace.Γ_map, AlgebraicGeometry.Scheme.iso_inv_base_hom_base, AlgebraicGeometry.range_eq_univ, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.pointOfClosedPoint_apply, AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AlgebraicGeometry.Scheme.stalkMap_comp, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, AlgebraicGeometry.coprodSpec_coprodMk, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι, AlgebraicGeometry.PresheafedSpace.map_id_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.compactSpace_iff_exists, AlgebraicGeometry.Scheme.Hom.preimage_sup, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Scheme.iso_hom_base_inv_base, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Hom.isIso_app, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.PresheafedSpace.id_base, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, AlgebraicGeometry.Scheme.Hom.fiberι_asFiber, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.Hom.id_base, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.AffineCover.covers, AlgebraicGeometry.SheafedSpace.comp_hom_base, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsFinite.finite_preimage_singleton, AlgebraicGeometry.IsLocalAtTarget.restrict, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.PresheafedSpace.comp_base, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup_eq_top, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Flat.stalkMap, AlgebraicGeometry.Scheme.Pullback.range_snd, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_base, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective, AlgebraicGeometry.IsPreimmersion.base_embedding, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, AlgebraicGeometry.Scheme.inv_hom_apply, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_map, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.PresheafedSpace.stalkMap.comp, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.comp_base_assoc, AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, AlgebraicGeometry.PresheafedSpace.comp_base_assoc, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.isClosedImmersion_iff, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_base, AlgebraicGeometry.Spec_closedPoint, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.finite_preimage, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_base, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, AlgebraicGeometry.Scheme.Hom.isConstructible_image, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.Surjective.surj, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.Scheme.comp_base_apply, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.IsDominant.denseRange, AlgebraicGeometry.Scheme.homOfLE_base, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, AlgebraicGeometry.PresheafedSpace.congr_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.Spec.map_base, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.Scheme.Hom.homeomorph_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.Hom.preimage_mono, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Hom.surjective, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.instIsPreimmersionAsFiberHom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, AlgebraicGeometry.SheafedSpace.id_base, AlgebraicGeometry.Scheme.Hom.isCompact_preimage, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.Scheme.Hom.comp_base, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.IsSeparated.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.range_fromSpecResidueField, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, AlgebraicGeometry.PresheafedSpace.comp_c, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.inv_base_hom_base_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.Scheme.JointlySurjective.exists_eq, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.Scheme.coe_homeoOfIso, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, AlgebraicGeometry.SheafedSpace.isColimit_exists_rep, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.residueFieldMap_comp, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm, AlgebraicGeometry.Scheme.comp_coeBase, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage, AlgebraicGeometry.Scheme.Hom.app_injective, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, AlgebraicGeometry.coprodMk_inr, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, AlgebraicGeometry.Scheme.Hom.isProperMap, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Opens.ι_base_apply, AlgebraicGeometry.Scheme.Hom.eqToHom_app, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage, AlgebraicGeometry.Scheme.homOfLE_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, AlgebraicGeometry.PresheafedSpace.ofRestrict_base, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base_apply, AlgebraicGeometry.Scheme.fromSpecResidueField_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, AlgebraicGeometry.Scheme.inv_base_hom_base, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Cover.fromGlued_injective, AlgebraicGeometry.Spec.map_base_apply, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, AlgebraicGeometry.Scheme.toSpecΓ_base
c 📖	CompOp	108 math math: AlgebraicGeometry.PresheafedSpace.stalkMap_germ, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.PresheafedSpace.Γ_map_op, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.SheafedSpace.Γ_map, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, AlgebraicGeometry.PresheafedSpace.map_id_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.SheafedSpace.id_hom_c, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_c, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.PresheafedSpace.congr_app, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.SheafedSpace.id_c, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, AlgebraicGeometry.PresheafedSpace.id_c, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.PresheafedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.LocallyRingedSpace.comp_c_app, AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ
toPshHom 📖	CompOp	3 math math: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom, AlgebraicGeometry.Scheme.Hom.isIso_toPshHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	base CategoryTheory.CategoryStruct.comp TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op TopologicalSpace.Opens.map c CategoryTheory.Functor.whiskerRight CategoryTheory.eqToHom CategoryTheory.Functor CategoryTheory.Functor.category	—	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.whiskerRight_id'

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapPresheaf 📖	CompOp	4 math math: mapPresheaf_map_f, mapPresheaf_map_c, mapPresheaf_obj_X, mapPresheaf_obj_presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapPresheaf_map_c 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.c obj AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces mapPresheaf map whiskerRight Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base	—	—
mapPresheaf_map_f 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base obj AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces mapPresheaf map	—	—
mapPresheaf_obj_X 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.carrier obj AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces mapPresheaf	—	—
mapPresheaf_obj_presheaf 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.presheaf obj AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces mapPresheaf comp Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
onPresheaf 📖	CompOp	—

---

← Back to Index