SheafedSpace

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

Statistics

Metric	Count
Definitions SheafedSpace, coeCarrier, coeSort, forget, forgetToPresheafedSpace, fullyFaithfulForgetToPresheafedSpace, instCategory, instCreatesColimitsOfShapePresheafedSpaceForgetToPresheafedSpaceOfSmallOfHasLimitsOfShapeOpposite, instCreatesColimitsPresheafedSpaceForgetToPresheafedSpaceOfHasLimits, instInhabitedDiscreteUnit, instTopologicalSpaceCarrierCarrier, isoMk, ofRestrict, restrict, restrictTopIso, sheaf, toPresheafedSpace, unit, Γ	19
Theorems comp_base, comp_c_app, comp_c_app', comp_hom_base, comp_hom_c_app, comp_hom_c_app', congr_app, congr_hom_app, epi_of_base_surjective_of_stalk_mono, ext, forgetToPresheafedSpace_faithful, forgetToPresheafedSpace_full, forgetToPresheafedSpace_map, forgetToPresheafedSpace_obj, fullyFaithfulForgetToPresheafedSpace_preimage_hom, hom_stalk_ext, id_base, id_c, id_c_app, id_hom, id_hom_base, id_hom_c, id_hom_c_app, instHasColimitsOfHasLimits, instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite, instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite, instPreservesColimitsTopCatForgetOfHasLimits, is_presheafedSpace_iso, isoMk_hom, isoMk_inv, mk_coe, mono_of_base_injective_of_stalk_epi, ofRestrict_hom_base, ofRestrict_hom_c_app, restrictTopIso_hom, restrictTopIso_inv, Γ_def, Γ_map, Γ_map_op, Γ_obj, Γ_obj_op	41
Total	60

AlgebraicGeometry

Definitions

Name	Category	Theorems
SheafedSpace 📖	CompData	160 math math: SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right', LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace, ΓSpec.locallyRingedSpaceAdjunction_counit_app, LocallyRingedSpace.Γ_def, LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, SheafedSpace.forgetToPresheafedSpace_obj, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, SheafedSpace.colimit_exists_rep, SheafedSpace.IsOpenImmersion.comp, SheafedSpace.IsOpenImmersion.app_invApp, LocallyRingedSpace.homMk_toHom, LocallyRingedSpace.id_toShHom', SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_snd_of_left, SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left', SheafedSpace.IsOpenImmersion.invApp_app_apply, localRingHom_comp_stalkIso_apply, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c, LocallyRingedSpace.Hom.toShHom_mk, LocallyRingedSpace.preservesColimits_forgetToSheafedSpace, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Scheme.forgetToTop_map, SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion, LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, SheafedSpace.GlueData.f_open, Scheme.forgetToTop_obj, SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_right, SheafedSpace.isoMk_hom, SheafedSpace.comp_hom_c_app, Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion, Scheme.Opens.germ_stalkIso_inv, SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, ΓSpec.locallyRingedSpaceAdjunction_counit_app', LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace, SheafedSpace.comp_base, SheafedSpace.comp_c_app, LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, SheafedSpace.id_hom_c_app, morphismRestrict_appLE, Scheme.Opens.germ_stalkIso_inv_assoc, LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, SheafedSpace.IsOpenImmersion.image_preimage_is_empty, ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right, SheafedSpace.ofRestrict_hom_c_app, Scheme.Opens.germ_stalkIso_hom, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_base, LocallyRingedSpace.comp_toShHom, SheafedSpace.id_hom_base, Spec.sheafedSpaceMap_comp, Spec.toPresheafedSpace_map_op, ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', stalkMap_toStalk, LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace, SheafedSpace.IsOpenImmersion.to_iso, SheafedSpace.Γ_map, SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_left, Spec.sheafedSpaceMap_hom_c_app, SheafedSpace.restrictTopIso_inv, Spec.toSheafedSpace_obj, SheafedSpace.instHasColimitsOfHasLimits, SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, SheafedSpace.fullyFaithfulForgetToPresheafedSpace_preimage_hom, LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base, SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, Spec.locallyRingedSpaceMap_toHom, LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right, SheafedSpace.Γ_obj_op, SheafedSpace.comp_hom_c_app', SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_left, SheafedSpace.comp_hom_base, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, stalkMap_toStalk_apply, LocallyRingedSpace.forgetToTop_map, LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom, Spec.toSheafedSpace_map, SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left, SheafedSpace.IsOpenImmersion.sigma_ι_isOpenImmersion_aux, LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, SheafedSpace.IsOpenImmersion.app_invApp_assoc, SheafedSpace.IsOpenImmersion.stalk_iso, SheafedSpace.GlueData.ιIsOpenImmersion, SheafedSpace.IsOpenImmersion.invApp_app, LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, Scheme.Opens.germ_stalkIso_hom_assoc, SheafedSpace.forgetToPresheafedSpace_map, SheafedSpace.id_hom, PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val, SheafedSpace.id_hom_c, SheafedSpace.id_c_app, SheafedSpace.forgetToPresheafedSpace_full, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, ΓSpec.toSpecΓ_of, SheafedSpace.Γ_obj, LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, Spec.sheafedSpaceMap_hom_base, LocallyRingedSpace.is_sheafedSpace_iso, StructureSheaf.toPushforwardStalk_comp, SheafedSpace.ofRestrict_hom_base, SheafedSpace.Γ_def, SheafedSpace.IsOpenImmersion.forgetMapIsOpenImmersion, PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_c, StructureSheaf.toPushforwardStalk_comp_assoc, Spec.sheafedSpaceMap_id, LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding, LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, SheafedSpace.id_c, SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite, Spec.toPresheafedSpace_map, SheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, LocallyRingedSpace.forgetToTop_obj, SheafedSpace.instPreservesColimitsTopCatForgetOfHasLimits, LocallyRingedSpace.forgetToSheafedSpace_map, Scheme.Opens.ι_appLE, SheafedSpace.isOpenImmersion_iff_hom, SheafedSpace.id_base, SheafedSpace.congr_hom_app, SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_fst_of_right, SheafedSpace.is_presheafedSpace_iso, LocallyRingedSpace.toΓSpecMapBasicOpen_eq, LocallyRingedSpace.toStalk_stalkMap_toΓSpec, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, SheafedSpace.congr_app, SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ, LocallyRingedSpace.isLocalHom_stalkMap_congr, LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, SheafedSpace.IsOpenImmersion.invApp_app_assoc, LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, SheafedSpace.isColimit_exists_rep, SheafedSpace.IsOpenImmersion.inv_invApp, LocallyRingedSpace.forgetToSheafedSpace_obj, LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, localRingHom_comp_stalkIso, LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, SheafedSpace.forgetToPresheafedSpace_faithful, LocallyRingedSpace.preservesCoequalizer, LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, SheafedSpace.IsOpenImmersion.instMono, SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, SheafedSpace.restrictTopIso_hom, ΓSpec.toSpecΓ_unop, SheafedSpace.Γ_map_op, SheafedSpace.GlueData.ι_jointly_surjective, SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite, SheafedSpace.comp_c_app', LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, SheafedSpace.isoMk_inv, LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right

AlgebraicGeometry.SheafedSpace

Definitions

Name	Category	Theorems
coeCarrier 📖	CompOp	—
coeSort 📖	CompOp	—
forget 📖	CompOp	9 math math: AlgebraicGeometry.Scheme.forgetToTop_map, AlgebraicGeometry.Scheme.forgetToTop_obj, IsOpenImmersion.sheafedSpace_forgetPreserves_of_right, IsOpenImmersion.sheafedSpace_forgetPreserves_of_left, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map, instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_obj, instPreservesColimitsTopCatForgetOfHasLimits
forgetToPresheafedSpace 📖	CompOp	27 math math: IsOpenImmersion.hasLimit_cospan_forget_of_right', AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, forgetToPresheafedSpace_obj, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, IsOpenImmersion.hasLimit_cospan_forget_of_left', AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', fullyFaithfulForgetToPresheafedSpace_preimage_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, IsOpenImmersion.hasLimit_cospan_forget_of_right, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, IsOpenImmersion.hasLimit_cospan_forget_of_left, forgetToPresheafedSpace_map, forgetToPresheafedSpace_full, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, AlgebraicGeometry.ΓSpec.toSpecΓ_of, Γ_def, IsOpenImmersion.forgetMapIsOpenImmersion, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, forgetToPresheafedSpace_faithful, AlgebraicGeometry.ΓSpec.toSpecΓ_unop
fullyFaithfulForgetToPresheafedSpace 📖	CompOp	1 math math: fullyFaithfulForgetToPresheafedSpace_preimage_hom
instCategory 📖	CompOp	118 math math: IsOpenImmersion.hasLimit_cospan_forget_of_right', AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.LocallyRingedSpace.Γ_def, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, forgetToPresheafedSpace_obj, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, colimit_exists_rep, IsOpenImmersion.comp, AlgebraicGeometry.LocallyRingedSpace.id_toShHom', IsOpenImmersion.sheafedSpace_pullback_snd_of_left, IsOpenImmersion.hasLimit_cospan_forget_of_left', AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.Scheme.forgetToTop_map, IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, GlueData.f_open, AlgebraicGeometry.Scheme.forgetToTop_obj, IsOpenImmersion.sheafedSpace_hasPullback_of_right, isoMk_hom, comp_hom_c_app, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, IsOpenImmersion.sigma_ι_isOpenImmersion, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, comp_base, comp_c_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, id_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, IsOpenImmersion.sheafedSpace_forgetPreserves_of_right, AlgebraicGeometry.LocallyRingedSpace.comp_toShHom, id_hom_base, AlgebraicGeometry.Spec.sheafedSpaceMap_comp, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace, IsOpenImmersion.to_iso, Γ_map, IsOpenImmersion.sheafedSpace_forgetPreserves_of_left, restrictTopIso_inv, AlgebraicGeometry.Spec.toSheafedSpace_obj, instHasColimitsOfHasLimits, IsOpenImmersion.isoRestrict_hom_hom_c_app, fullyFaithfulForgetToPresheafedSpace_preimage_hom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, epi_of_base_surjective_of_stalk_mono, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, GlueData.ι_isoPresheafedSpace_inv, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, IsOpenImmersion.hasLimit_cospan_forget_of_right, Γ_obj_op, comp_hom_c_app', IsOpenImmersion.sheafedSpace_hasPullback_of_left, comp_hom_base, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map, AlgebraicGeometry.Spec.toSheafedSpace_map, IsOpenImmersion.hasLimit_cospan_forget_of_left, IsOpenImmersion.sigma_ι_isOpenImmersion_aux, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, GlueData.ιIsOpenImmersion, forgetToPresheafedSpace_map, id_hom, id_hom_c, id_c_app, forgetToPresheafedSpace_full, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, AlgebraicGeometry.ΓSpec.toSpecΓ_of, mono_of_base_injective_of_stalk_epi, Γ_obj, AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso, Γ_def, IsOpenImmersion.forgetMapIsOpenImmersion, AlgebraicGeometry.Spec.sheafedSpaceMap_id, IsOpenImmersion.sigma_ι_isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, id_c, instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite, IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_obj, instPreservesColimitsTopCatForgetOfHasLimits, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_map, id_base, IsOpenImmersion.sheafedSpace_pullback_fst_of_right, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, instEpiTopCatBaseHomPresheafedSpaceπ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, isColimit_exists_rep, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_obj, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, forgetToPresheafedSpace_faithful, AlgebraicGeometry.LocallyRingedSpace.preservesCoequalizer, AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, IsOpenImmersion.instMono, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, restrictTopIso_hom, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, Γ_map_op, GlueData.ι_jointly_surjective, instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite, comp_c_app', isoMk_inv, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right
instCreatesColimitsOfShapePresheafedSpaceForgetToPresheafedSpaceOfSmallOfHasLimitsOfShapeOpposite 📖	CompOp	1 math math: IsOpenImmersion.image_preimage_is_empty
instCreatesColimitsPresheafedSpaceForgetToPresheafedSpaceOfHasLimits 📖	CompOp	—
instInhabitedDiscreteUnit 📖	CompOp	—
instTopologicalSpaceCarrierCarrier 📖	CompOp	700 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.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.irreducibleSpace_of_isIntegral, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, AlgebraicGeometry.Scheme.isoOfEq_inv, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.zeroLocus_iInf, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, 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.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, AlgebraicGeometry.Scheme.support_nilradical, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, AlgebraicGeometry.Scheme.Hom.preimage_bot, IsOpenImmersion.app_invApp, 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.isCompact_iff_exists, AlgebraicGeometry.Scheme.RationalMap.dense_domain, 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.image_morphismRestrict_preimage, AlgebraicGeometry.Scheme.IdealSheafData.gc, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, IsOpenImmersion.instIsIsoInvApp, IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.ι_toIso_inv, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.noetherianSpace_of_isAffine, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, AlgebraicGeometry.Scheme.preimage_comp, AlgebraicGeometry.Scheme.IdealSheafData.support_mul, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.compactSpace_of_isAffine, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.Scheme.Hom.image_iSup₂, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.zeroLocus_singleton, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.isNoetherian_iff, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.IsNoetherian.toCompactSpace, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.IsNoetherian.noetherianSpace, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.Scheme.homeoOfIso_symm, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, 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.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Proj.mem_basicOpen, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.quasiCompact_over_affine_iff, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, 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.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.basicOpen_le, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.zeroLocus_def, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.tilde.isoTop_hom, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Opens.toScheme_carrier, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, 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.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Modules.restrict_map, AlgebraicGeometry.Scheme.PartialMap.restrict_id, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.Scheme.IdealSheafData.support_antitone, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, 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.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.compactSpace_iff_quasiCompact, AlgebraicGeometry.RingedSpace.basicOpen_le, AlgebraicGeometry.Scheme.Opens.ι_appIso, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.isLocalIso_iff, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, 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.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.tilde.isIso_toOpen_top, AlgebraicGeometry.Scheme.instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, AlgebraicGeometry.IsArtinianScheme.toCompactSpace, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.IdealSheafData.support_comap, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Proj.basicOpen_mono, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.Hom.isEmbedding, 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.isCompactOpen_iff_eq_finset_affine_union, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, 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.isRetrocompact_basicOpen, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.quasiSeparatedSpace_of_isAffine, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.isArtinianScheme_iff, AlgebraicGeometry.Scheme.Hom.id_appIso, AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, AlgebraicGeometry.Proj.basicOpen_one, AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.isoSpec_Spec, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.compactSpace_iff_exists, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible, AlgebraicGeometry.Scheme.Hom.preimage_sup, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.image_iSup, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.Hom.isOpen_quasiFiniteAt, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, 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, AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.Proj.isBasis_basicOpen, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.geometricallyIrreducible_iff, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.Scheme.Modules.restrict_obj, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.isBasis_affine_open, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine, 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, IsOpenImmersion.invApp_app, AlgebraicGeometry.Scheme.PartialMap.mem_domain_ofFromSpecStalk, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, 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.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.Scheme.topIso_hom, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.finite_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.Scheme.IdealSheafData.support_map, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact, AlgebraicGeometry.Scheme.IsQuasiAffine.toCompactSpace, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.affineAnd_apply, 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.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, 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.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, AlgebraicGeometry.Proj.basicOpen_zero, 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.Scheme.Hom.range_subset_ker_support, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField, AlgebraicGeometry.quasiCompact_iff_compactSpace, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.IsDominant.denseRange, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, 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.Scheme.Hom.homeomorph_apply, AlgebraicGeometry.Scheme.IdealSheafData.support_top, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.Scheme.Hom.comp_appTop, AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.Scheme.basicOpen_zero, 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.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.isAffineOpen_bot, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, AlgebraicGeometry.Scheme.Opens.ι_image_le, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.basicOpen_eq_of_affine, 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.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.spread_out_unique_of_isGermInjective', AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.toIso_inv_ι, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.Scheme.Hom.opensRange_comp, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.genericPoint_eq_bot_of_affine, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.Scheme.PartialMap.dense_domain, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.Scheme.restrictFunctor_obj_left, AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, 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.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap, AlgebraicGeometry.Scheme.Opens.ι_image_top, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, AlgebraicGeometry.exists_lift_of_germInjective_aux, AlgebraicGeometry.Scheme.zeroLocus_isClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.Γ_obj_op, 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.Scheme.Opens.topIso_hom, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.Scheme.Hom.image_le_image_iff, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.Scheme.coe_homeoOfIso, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, AlgebraicGeometry.Scheme.RationalMap.mem_domain, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat, IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, IsOpenImmersion.inv_invApp, AlgebraicGeometry.Scheme.codisjoint_zeroLocus, AlgebraicGeometry.Scheme.PartialMap.restrict_id_hom, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.coe_opensRestrict_apply_coe, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian, AlgebraicGeometry.Scheme.Hom.app_injective, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.coprodMk_inr, AlgebraicGeometry.Scheme.Hom.isProperMap, AlgebraicGeometry.Scheme.isoOfEq_hom, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, AlgebraicGeometry.Scheme.le_iff_specializes, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Scheme.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Scheme.Opens.ι_base_apply, AlgebraicGeometry.Scheme.Hom.eqToHom_app, AlgebraicGeometry.instIsAffineHomιBasicOpen, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, AlgebraicGeometry.Scheme.homOfLE_rfl, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, AlgebraicGeometry.quasiSeparated_over_affine_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.Scheme.affineBasicOpen_le, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, AlgebraicGeometry.Scheme.Hom.id_image, AlgebraicGeometry.Scheme.toSpecΓ_base
isoMk 📖	CompOp	2 math math: isoMk_hom, isoMk_inv
ofRestrict 📖	CompOp	9 math math: IsOpenImmersion.ofRestrict, IsOpenImmersion.ofRestrict_invApp, IsOpenImmersion.ofRestrict_invApp_apply, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, IsOpenImmersion.isoRestrict_hom_ofRestrict, ofRestrict_hom_c_app, ofRestrict_hom_base, IsOpenImmersion.isoRestrict_inv_ofRestrict, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc
restrict 📖	CompOp	12 math math: IsOpenImmersion.ofRestrict, IsOpenImmersion.ofRestrict_invApp, IsOpenImmersion.ofRestrict_invApp_apply, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, IsOpenImmersion.isoRestrict_hom_ofRestrict, ofRestrict_hom_c_app, restrictTopIso_inv, IsOpenImmersion.isoRestrict_hom_hom_c_app, ofRestrict_hom_base, IsOpenImmersion.isoRestrict_inv_ofRestrict, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, restrictTopIso_hom
restrictTopIso 📖	CompOp	2 math math: restrictTopIso_inv, restrictTopIso_hom
sheaf 📖	CompOp	2 math math: AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf, AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf'
toPresheafedSpace 📖	CompOp	1308 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.Spec.toPresheafedSpace_obj, 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, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, 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, forgetToPresheafedSpace_obj, 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, 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.PresheafedSpace.IsOpenImmersion.toSheafedSpace_toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, 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, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.Scheme.RationalMap.dense_domain, AlgebraicGeometry.HasRingHomProperty.stalkMap, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.homMk_toHom, 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, AlgebraicGeometry.Scheme.IdealSheafData.gc, AlgebraicGeometry.Scheme.emptyTo_base, 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, IsOpenImmersion.instIsIsoInvApp, AlgebraicGeometry.Scheme.hom_inv_apply, 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.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.Spec.sheafedSpaceObj_carrier, AlgebraicGeometry.noetherianSpace_of_isAffine, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_c, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, 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, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.Scheme.forgetToTop_map, 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ι, 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, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, 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, isoMk_hom, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.compactSpace_of_isAffine, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, 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, 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, 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, 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, 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, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, 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.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.PresheafedSpace.IsOpenImmersion.sheafedSpace_toSheafedSpace, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.RingedSpace.basicOpen_pow, 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, 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, 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, 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, id_hom_c_app, AlgebraicGeometry.Scheme.zeroLocus_def, 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.PresheafedSpace.IsOpenImmersion.scheme_toScheme, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, 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, 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, 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, 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, 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, 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.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_base, 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, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, 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, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.Spec.toPresheafedSpace_map_op, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.isLocalIso_iff, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, 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, 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, Γ_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, 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, 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, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', 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, AlgebraicGeometry.Scheme.residue_surjective, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, 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, fullyFaithfulForgetToPresheafedSpace_preimage_hom, AlgebraicGeometry.over_def, 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.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_hom_base, 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, 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ι, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, GlueData.ι_isoPresheafedSpace_inv, AlgebraicGeometry.Proj.basicOpen_one, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom, 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, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace, 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, 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, Γ_obj_op, 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, 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, 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, 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, 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, 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, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom, 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, 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, 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, IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine, 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, 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.LocallyRingedSpace.toΓSpec_base, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, forgetToPresheafedSpace_map, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom, 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, id_hom, 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.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val, 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.Scheme.residue_residueFieldMap_assoc, 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, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, id_hom_c, 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, 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, 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.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.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, Γ_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.sheafedSpaceMap_hom_base, 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.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom_c, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.Spec.toPresheafedSpace_obj_op, AlgebraicGeometry.Scheme.comp_base_apply, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, 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, 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.Spec.map_base, 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.Hom.isIso_toPshHom, AlgebraicGeometry.Scheme.IdealSheafData.support_top, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, 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, 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, id_c, AlgebraicGeometry.LocallyRingedSpace.comp_toHom, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.etale_iff, AlgebraicGeometry.isAffineOpen_bot, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, AlgebraicGeometry.Scheme.Opens.ι_image_le, AlgebraicGeometry.Spec.toPresheafedSpace_map, 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.LocallyRingedSpace.forgetToSheafedSpace_map, 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, 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, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, isOpenImmersion_iff_hom, 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, id_base, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.Scheme.toIso_inv_ι, 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, 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, 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.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.Scheme.Hom.stalkMap_id, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, is_presheafedSpace_iso, 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.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, 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.LocallyRingedSpace.id_toHom, 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, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, 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, 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, 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, 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, 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, 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, isColimit_exists_rep, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, 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, 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.localRingHom_comp_stalkIso, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, 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, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian, AlgebraicGeometry.Scheme.Hom.app_injective, 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, 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, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, AlgebraicGeometry.Scheme.IdealSheafData.le_def, restrictTopIso_hom, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, AlgebraicGeometry.Scheme.inv_base_hom_base, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, Γ_map_op, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, GlueData.ι_jointly_surjective, AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion, AlgebraicGeometry.quasiSeparated_over_affine_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, 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, comp_c_app', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, isoMk_inv, 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.sheafedSpaceObj_presheaf, 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
unit 📖	CompOp	—
Γ 📖	CompOp	6 math math: AlgebraicGeometry.LocallyRingedSpace.Γ_def, Γ_map, Γ_obj_op, Γ_obj, Γ_def, Γ_map_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier	—	comp_hom_base
comp_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace.Hom.c Opposite.op TopologicalSpace.Opens.map Opposite.unop	—	comp_hom_c_app
comp_c_app' 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace.Hom.c Opposite.op TopologicalSpace.Opens.map	—	comp_hom_c_app'
comp_hom_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier	—	—
comp_hom_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace.Hom.c Opposite.op TopologicalSpace.Opens.map Opposite.unop	—	—
comp_hom_c_app' 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace.Hom.c Opposite.op TopologicalSpace.Opens.map	—	—
congr_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	congr_hom_app
congr_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	AlgebraicGeometry.PresheafedSpace.congr_app
epi_of_base_surjective_of_stalk_mono 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Mono TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	CategoryTheory.Epi instCategory	—	hom_stalk_ext CategoryTheory.cancel_mono TopCat.Presheaf.stalkCongr_hom specializes_refl TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.id_comp AlgebraicGeometry.PresheafedSpace.stalkMap.comp CategoryTheory.ConcreteCategory.hom_ext CategoryTheory.InducedCategory.hom_ext_iff
ext 📖	—	AlgebraicGeometry.PresheafedSpace.Hom.base toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces 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 AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.whiskerRight CategoryTheory.eqToHom CategoryTheory.Functor CategoryTheory.Functor.category	—	—	CategoryTheory.InducedCategory.hom_ext AlgebraicGeometry.PresheafedSpace.ext
forgetToPresheafedSpace_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful AlgebraicGeometry.SheafedSpace instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces forgetToPresheafedSpace	—	CategoryTheory.Functor.FullyFaithful.faithful
forgetToPresheafedSpace_full 📖	mathematical	—	CategoryTheory.Functor.Full AlgebraicGeometry.SheafedSpace instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces forgetToPresheafedSpace	—	CategoryTheory.Functor.FullyFaithful.full
forgetToPresheafedSpace_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.SheafedSpace instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces forgetToPresheafedSpace CategoryTheory.InducedCategory.Hom.hom toPresheafedSpace	—	—
forgetToPresheafedSpace_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces forgetToPresheafedSpace toPresheafedSpace	—	—
fullyFaithfulForgetToPresheafedSpace_preimage_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace CategoryTheory.Functor.FullyFaithful.preimage instCategory forgetToPresheafedSpace fullyFaithfulForgetToPresheafedSpace	—	—
hom_stalk_ext 📖	—	AlgebraicGeometry.PresheafedSpace.Hom.base toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.Hom.stalkMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom TopCat.Presheaf.stalkCongr Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Inseparable Filter nhds	—	—	TopCat.Presheaf.ext CategoryTheory.ConcreteCategory.ext DFunLike.ext TopCat.Presheaf.section_ext AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.id_comp
id_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier	—	id_hom_base
id_c 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.c toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.eqToHom TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.carrier TopCat.instCategoryPresheaf AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward TopCat TopCat.instCategory TopCat.Presheaf.Pushforward.id_eq	—	id_hom_c
id_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace.Hom.c	—	id_hom_c_app
id_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory	—	—
id_hom_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier	—	—
id_hom_c 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.c toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.eqToHom TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.carrier TopCat.instCategoryPresheaf AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward TopCat TopCat.instCategory TopCat.Presheaf.Pushforward.id_eq	—	—
id_hom_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace.Hom.c	—	—
instHasColimitsOfHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits AlgebraicGeometry.SheafedSpace instCategory	—	instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape AlgebraicGeometry.SheafedSpace instCategory	—	CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf
instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape AlgebraicGeometry.SheafedSpace instCategory TopCat TopCat.instCategory forget	—	CategoryTheory.Limits.comp_preservesColimitsOfShape CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapeTopCatForget
instPreservesColimitsTopCatForgetOfHasLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesColimits AlgebraicGeometry.SheafedSpace instCategory TopCat TopCat.instCategory forget	—	instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
is_presheafedSpace_iso 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace	—	CategoryTheory.Functor.map_isIso
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgebraicGeometry.SheafedSpace instCategory isoMk CategoryTheory.InducedCategory.homMk AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlgebraicGeometry.SheafedSpace instCategory isoMk CategoryTheory.InducedCategory.homMk AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace	—	—
mk_coe 📖	mathematical	TopCat.Presheaf.IsSheaf	AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace	—	—
mono_of_base_injective_of_stalk_epi 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Epi TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	CategoryTheory.Mono instCategory	—	hom_stalk_ext CategoryTheory.cancel_epi TopCat.Presheaf.stalkCongr_hom specializes_refl TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.id_comp AlgebraicGeometry.PresheafedSpace.stalkMap.comp CategoryTheory.ConcreteCategory.hom_ext
ofRestrict_hom_base 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.PresheafedSpace.restrict CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces restrict ofRestrict	—	—
ofRestrict_hom_c_app 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace 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 AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.restrict TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces restrict ofRestrict CategoryTheory.Functor.map Opposite.op IsOpenMap.functor TopologicalSpace.Opens.map Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit IsOpenMap.adjunction	—	—
restrictTopIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgebraicGeometry.SheafedSpace instCategory restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace 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 CategoryTheory.InducedCategory.homMk AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.ofRestrict	—	TopologicalSpace.Opens.isOpenEmbedding
restrictTopIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlgebraicGeometry.SheafedSpace instCategory restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace 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 CategoryTheory.InducedCategory.homMk AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.toRestrictTop	—	TopologicalSpace.Opens.isOpenEmbedding
Γ_def 📖	mathematical	—	Γ CategoryTheory.Functor.comp Opposite AlgebraicGeometry.SheafedSpace CategoryTheory.Category.opposite instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op forgetToPresheafedSpace AlgebraicGeometry.PresheafedSpace.Γ	—	—
Γ_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite AlgebraicGeometry.SheafedSpace CategoryTheory.Category.opposite instCategory Γ CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.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.SheafedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.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.SheafedSpace CategoryTheory.Category.opposite instCategory Γ TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.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.SheafedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier toPresheafedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—

---

← Back to Index