Opens 📖 | CompData | 1629 mathmath: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, OpenNhds.coe_id, AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.Hom.resLE_map_assoc, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, smoothSheafCommRing.ι_forgetStalk_inv, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_resLE, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, TopCat.PrelocalPredicate.res, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, Opens.id_apply, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, Opens.coe_interior, PrimeSpectrum.isClopen_iff_mul_add, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, Opens.map_id_obj_unop, AlgebraicGeometry.Scheme.zeroLocus_iInf, AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, Opens.inclusion'_hom_apply, AlgebraicGeometry.Etale.etale_appLE, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, ProjectiveSpectrum.mem_basicOpen, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, AlgebraicGeometry.LocallyQuasiFinite.quasiFinite_appLE, TopCat.presheafToType_map, TopCat.Sheaf.interUnionPullbackCone_snd, Opens.map_coe, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, IsOpenMap.exists_opens_image_eq_of_prespectralSpace, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, Polynomial.mem_image_comap_C_basicOpen, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, Opens.mem_top, AlgebraicGeometry.Scheme.ofRestrict_appIso, LocalizedModule.subsingleton_iff_disjoint, OpenPartialHomeomorph.map_subtype_source, AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, ModelWithCorners.interior_open, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr, Topology.IsOpenEmbedding.functor_isContinuous, PrimeSpectrum.eq_biUnion_of_isOpen, AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset, AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ, AlgebraicGeometry.mono_pushoutSection_of_iSup_eq, Opens.instIsManifoldSubtypeMem, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.StructureSheaf.comap_id, Opens.coe_iSup, RingHom.IsStableUnderBaseChange.pullback_fst_appTop, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck, TopCat.Presheaf.germ_eq_of_isBasis, AlgebraicGeometry.IsAffineOpen.map_fromSpec, IsOpenMap.pullbackIso_hom_app_app, AlgebraicGeometry.StructureSheaf.const_mul_rev, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc, TopCat.Presheaf.Pushforward.id_inv_app, Closeds.coe_compl, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, Opens.chartAt_eq, TopCat.Presheaf.germ_stalkPullbackHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, skyscraperPresheaf_obj, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, Opens.isCompactElement_iff, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, TopCat.GlueData.open_image_open, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, AlgebraicGeometry.StructureSheaf.comap_comp, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc, OpenPartialHomeomorph.subtypeRestr_coe, 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.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, Closeds.complOrderIso_symm_apply, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, Opens.coe_inclusion', AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, Opens.mem_sup, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, OpenNhds.inclusionMapIso_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.StructureSheaf.const_self, Opens.comap_mono, AlgebraicGeometry.Scheme.mem_basicOpen', AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, Opens.pretopology_toGrothendieck, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.pow_apply, Opens.chartAt_subtype_val_symm_eventuallyEq, TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext_iff, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem', AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, eq_induced_by_maps_to_sierpinski, Opens.mayerVietorisSquare_X₃, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.Scheme.Hom.id_appTop, IsOpenCover.iSup_set_eq_univ, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, smoothSheafCommRing.ι_evalHom_apply, TopCat.Presheaf.germ_exist_of_isBasis, Opens.CompleteCopy.dist_eq, PrimeSpectrum.basicOpen_injOn_isIdempotentElem, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.Proj.map_preimage_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_mul, MvPolynomial.image_comap_C_basicOpen, AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.StructureSheaf.comap_id', Opens.map_functor_eq', OpenNhds.comp_apply, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, Opens.ne_bot_iff_nonempty, AlgebraicGeometry.SpecMap_preimage_basicOpen, Algebra.basicOpen_subset_etaleLocus_iff_etale, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, smoothSheafCommRing.eval_germ, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, IsLocalRing.closedPoint_mem_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp, Opens.isCoatom_iff, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, Locale.localePointOfSpacePoint_toFun, AlgebraicGeometry.StructureSheaf.const_add, Opens.map_obj, Opens.comp_apply, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.Hom.preimage_le_preimage_of_le, AlgebraicGeometry.Scheme.Hom.coe_resLE_base, OpenNhds.val_apply, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, Module.basicOpen_subset_freeLocus_iff, AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, TopCat.GlueData.ofOpenSubsets_toGlueData_U, Opens.instIsContinuousCompGrothendieckTopology, IsOpenMap.pullbackObjIso_hom_app, OpenNhds.inclusionMapIso_inv, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.structureSheafInType.mul_apply, TopCat.Presheaf.germ_stalkSpecializes_apply, contMDiff_inclusion, AlgebraicGeometry.StructureSheaf.exists_const, IsOpenMap.functorNhds_obj_coe, skyscraperPresheafCocone_pt, Manifold.IsImmersionAtOfComplement.ofOpen, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, TopCat.Sheaf.pushforward_map, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, Opens.infLELeft_apply_mk, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, Opens.isBasis_iff_nbhd, AlgebraicGeometry.locallyQuasiFinite_iff, Opens.iSup_mk, AlgebraicGeometry.Scheme.preimage_comp, smoothSheaf.ι_evalHom_apply, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, Algebra.basicOpen_subset_unramifiedLocus_iff, Topology.IsLocallyConstructible.iff_of_isOpenCover, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, IsOpenMap.pullbackObjIso_hom_naturality, TopCat.Presheaf.pushforwardToOfIso_app, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp, Opens.complOrderIso_apply, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, Homeomorph.opensCongr_apply, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, TopCat.Presheaf.germ_res', AlgebraicGeometry.PresheafedSpace.Γ_obj_op, Opens.map_comp_obj_unop, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', TopCat.Sheaf.interUnionPullbackCone_fst, AlgebraicGeometry.functionField_isScalarTower, TopCat.PrelocalPredicate.sheafify_inductionOn, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TopCat.Presheaf.stalkPushforward_germ_apply, TopCat.GlueData.MkCore.V_id, Opens.comap_comap, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, Manifold.IsImmersion.of_opens, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, IsOpenCover.comap, TopCat.Presheaf.germ_res_apply, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Proj.one_apply, OnePoint.infty_mem_opensOfCompl, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, Topology.IsLocallyConstructible.iff_isConstructible_of_isOpenCover, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, TopCat.Presheaf.germ_stalkPullbackInv_assoc, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.eqToHom_c_app, TopCat.Sheaf.exact_iff_stalkFunctor_map_exact, TopCat.GlueData.ofOpenSubsets_toGlueData_t, AlgebraicGeometry.Scheme.Hom.resLE_app_top, Opens.complOrderIso_symm_apply, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, IsOpenMap.functor_faithful, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, IsOpenCover.generalizingMap_iff_comp, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, Opens.mem_comap, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, PrimeSpectrum.le_basicOpen_pow, PrimeSpectrum.iSup_basicOpen_eq_top_iff, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.RingedSpace.exists_res_eq_zero_of_germ_eq_zero, TopCat.Sheaf.id_app, Opens.isOpenEmbedding_obj_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, Opens.chart_eq', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.StructureSheaf.comap_const, AlgebraicGeometry.Scheme.Hom.appLE_map', AlgebraicGeometry.Scheme.isoSpec_hom_naturality, topCatOpToFrm_map, AlgebraicGeometry.Scheme.zeroLocus_singleton, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.component_nontrivial, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.Proj.sub_apply, AlgebraicGeometry.isLocallyArtinian_iff_of_isOpenCover, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.resLE_map, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, AlgebraicGeometry.Scheme.Hom.comp_app, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, Opens.mapId_hom_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.Proj.ι_comp_map, PrimeSpectrum.isConstructible_basicOpen, ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val, Opens.mapComp_hom_app, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.Hom.coe_resLE_apply, Opens.frameHom_toFun, smoothSheaf.ι_evalHom_assoc, Opens.mk_univ, PrimeSpectrum.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, OpenSubgroup.mem_toOpens, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.StructureSheaf.comap_apply, AlgebraicGeometry.Scheme.Hom.smooth_appLE, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, IsOpenMap.functorFullOfMono, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, IsOpenCover.isOpenMap_iff_comp, PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, AlgebraicGeometry.Scheme.comp_appLE, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, AlgebraicGeometry.isIso_fromTildeΓ_of_presentation, ModelWithCorners.boundary_open, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, TopCat.stalkToFiber_germ, Opens.map_id_obj', AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.ofRestrict_appLE, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Hom.id_app, TopCat.Presheaf.comp_app, AlgebraicGeometry.Scheme.Γ_obj, Opens.isOpenEmbedding', AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, TopCat.Presheaf.germ_stalkSpecializes_assoc, Opens.chartAt_inclusion_symm_eventuallyEq, ProjectiveSpectrum.basicOpen_mul_le_left, AlgebraicGeometry.StructureSheaf.const_congr, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, Opens.mem_inf, AlgebraicGeometry.Scheme.ΓSpecIso_inv, MeasureTheory.Content.innerContent_iSup_nat, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, OpenNhds.map_obj, TopCat.Presheaf.stalkPushforward_germ_assoc, AlgebraicGeometry.Scheme.opensRange_homOfLE, TopCat.Presheaf.pushforward_map_app, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.Scheme.germToFunctionField_injective, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', MeasureTheory.Content.innerContent_exists_compact, Opens.map_homOfLE, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, Opens.instHasGroupoid, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, TopCat.continuousPrelocal_pred, AlgebraicGeometry.Scheme.zeroLocus_setMul, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, Alexandrov.principals_map, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, Opens.inclusion'_top_functor, TopCat.Presheaf.stalk_open_algebraMap, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, IsCompactOpenCovered.image, TopCat.GlueData.instIsIsoT, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map, TopCat.Presheaf.pushforwardEq_hom_app, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.RingedSpace.basicOpen_pow, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc, PrimeSpectrum.basicOpen_le_basicOpen_iff_algebraMap_isUnit, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, TopCat.presheafToTop_obj, AlgebraicGeometry.HasRingHomProperty.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, AlgebraicGeometry.PresheafedSpace.Γ_map_op, Manifold.IsImmersionAt.of_opens, TopCat.Presheaf.pullbackObjObjOfImageOpen_hom_naturality, AlgebraicGeometry.IsLocalAtSource.iff_exists_resLE, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, TopCat.Presheaf.germ_ext, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, Opens.map_functor_eq, Opens.instSecondCountableOpens, AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem', TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, IsOpenCover.isClosed_iff_coe_preimage, Algebra.basicOpen_subset_smoothLocus_iff_smooth, TopCat.Sheaf.extend_hom_app, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, TopCat.Presheaf.map_germ_eq_Γgerm, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, IsCompactOpenCovered.exists_mem_of_isBasis, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem', AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, Opens.map_id_obj, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, MeasureTheory.Content.is_mul_left_invariant_innerContent, AlgebraicGeometry.locallyOfFiniteType_iff, Closeds.complOrderIso_apply, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, TopCat.Presheaf.SheafConditionEqualizerProducts.w, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, TopCat.Presheaf.isSheaf_iff_isSheaf_comp, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.Scheme.zeroLocus_def, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, Opens.chart_eq, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.tilde.isoTop_hom, AlgebraicGeometry.Scheme.restrict_presheaf_obj, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, PrimeSpectrum.mem_image_comap_basicOpen, ModuleCat.Tilde.toOpen_res, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, productOfMemOpens_isEmbedding, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, IsOpenMap.pullbackIso_inv_app_app, PrimeSpectrum.basicOpen_zero, AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE, PrimeSpectrum.isClopen_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, Opens.gc, AlgebraicGeometry.Spec.map_appLE, AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE, smoothSheafCommRing.ι_evalHom, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.morphismRestrict_appLE, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, AlgebraicGeometry.Scheme.Hom.app_eq, Opens.coe_eq_empty, AlgebraicGeometry.RingedSpace.res_zero, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.comp_appLE, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, TopCat.Presheaf.germ_res_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Alexandrov.principalOpen_le_iff, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.ΓSpecIso_obj_hom, Opens.map_comp_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality_assoc, Opens.isBasis_sigma, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, AlgebraicGeometry.FormallyUnramified.formallyUnramified_of_affine_subset, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.formallySmooth_stalkMap_iff, AlgebraicGeometry.Scheme.Modules.restrict_map, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, AlgebraicGeometry.injective_germ_basicOpen, Opens.functor_obj_map_obj, smoothSheafCommRing.evalHom_germ, AlgebraicGeometry.WeaklyEtale.instMorphismRestrict, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map_assoc, Topology.IsInducing.mem_functorObj_iff, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, AlgebraicGeometry.Scheme.Opens.exists_toScheme, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, IsOpenCover.quasiSober_iff_forall, TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective, Opens.map_comp_obj', AlgebraicGeometry.StructureSheaf.const_mul_cancel, Opens.mapMapIso_functor, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.HasAffineProperty.restrict, Opens.CompleteCopy.dist_val_le_dist, Opens.nonempty_coe, Opens.compl_bijective, Opens.openPartialHomeomorphSubtypeCoe_coe, AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, Opens.mapIso_inv_app, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, AlgebraicGeometry.Scheme.component_nontrivial, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, Opens.coe_overEquivalence_functor_obj, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.Scheme.basicOpen_pow, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, AlgebraicGeometry.HasRingHomProperty.appLE, AlgebraicGeometry.Scheme.Hom.ker_apply, TopCat.Sheaf.existsUnique_gluing, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, productOfMemOpens_injective, Opens.coe_finset_sup, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, OpenNhds.id_apply, Opens.instIsSimpleOrderOfNonemptyOfIndiscreteTopology, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, IsCompactOpenCovered.iff_of_unique, AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_notMem_basicOpen, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, MeasureTheory.Content.outerMeasure_le, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, TopCat.Presheaf.stalk_mono_of_mono, AlgebraicGeometry.Proj.val_sectionInBasicOpen_apply, TopCat.Presheaf.map_germ_eq_Γgerm_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, Opens.op_map_id_obj, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective, AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ, AlgebraicGeometry.Scheme.zeroLocus_radical, TopCat.Sheaf.interUnionPullbackConeLift_right, Opens.instIsThinPointOpensGrothendieckTopology, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.exists_map_preimage_eq_map_preimage, AlgebraicGeometry.Scheme.Hom.map_appLE_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, Opens.mapMapIso_unitIso, AlgebraicGeometry.RingedSpace.basicOpen_le, AlgebraicGeometry.StructureSheaf.const_one, AlgebraicGeometry.Scheme.Opens.ι_appIso, MeasureTheory.Content.innerContent_bot, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc, Opens.overEquivalence_unitIso_hom_app_left, productOfMemOpens_isInducing, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, Opens.isConservativeFamilyOfPoints_pointsGrothendieckTopology, Opens.isOpenEmbedding, AlgebraicGeometry.exists_of_res_zero_of_qcqs_of_top, AlgebraicGeometry.Scheme.zeroLocus_map, AlgebraicGeometry.Scheme.Hom.finite_app, TopCat.Presheaf.stalk_hom_ext_iff, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.exists_preimage_eq, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.Scheme.evaluation_naturality, TopCat.GlueData.range_fromOpenSubsetsGlue, Alexandrov.principals_obj, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, Opens.IsBasis.of_isInducing, AlgebraicGeometry.Scheme.Hom.appIso_hom', TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, AlgebraicGeometry.Scheme.zeroLocus_inf, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, TopCat.PrelocalPredicate.sheafify_inductionOn', AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.germ_injective_of_isIntegral, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.StructureSheaf.smul_const, TopCat.Presheaf.pushforward_obj_obj, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, Opens.mem_bot, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, StructureGroupoid.LocalInvariantProp.liftProp_subtype_val, IsOpenMap.pullbackObjIso_inv_app, AlgebraicGeometry.Scheme.Hom.resLE_congr, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective, OpenPartialHomeomorph.subtypeRestr_symm_apply, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, Opens.mayerVietorisSquare_X₂, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, Opens.coe_finset_inf, AlgebraicGeometry.Scheme.Hom.app_invApp', TopCat.GlueData.MkCore.t_inv, AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.exists_appTop_map_eq_zero_of_isAffine_of_isLimit, AlgebraicGeometry.tilde.isIso_toOpen_top, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, TopCat.Presheaf.SubmonoidPresheaf.map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, TopCat.Sheaf.existsUnique_gluing', AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, Topology.IsUpperSet.isSheaf_of_isRightKanExtension, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.StructureSheaf.const_zero, Opens.coe_id, AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc, AlgebraicGeometry.IsProper.instMorphismRestrict, TopCat.presheafToTypes_map, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, Opens.set_range_inclusion', AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, IsOpenCover.jacobsonSpace_iff, TopCat.Sheaf.comp_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, smoothSheafCommRing.ι_forgetStalk_inv_apply, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι, AlgebraicGeometry.SheafedSpace.Γ_map, OpenAddSubgroup.toOpens_inf, Opens.coe_mayerVietorisSquare_X₁, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections, Opens.mem_iSup, Opens.IsBasis.isOpenCover_mem_and_le, AlgebraicGeometry.germ_stalkClosedPointIso_hom, TopCat.Presheaf.isLocallySurjective_iff, TopCat.Sheaf.IsFlasque.epi_of_shortExact, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, Alexandrov.self_mem_principalOpen, Algebra.basicOpen_subset_etaleLocus_iff, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, Opens.nonempty_coeSort, AlgebraicGeometry.Proj.awayToSection_comp_appLE, StructureGroupoid.LocalInvariantProp.section_spec, Opens.mapMapIso_inverse, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen, TopCat.Presheaf.Pushforward.comp_inv_app, TopCat.Presheaf.covering_presieve_eq_self, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, AlgebraicGeometry.Scheme.evaluation_naturality_apply, Opens.comap_comp, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appLE_map_assoc, ContMDiff.extend_zero, smoothSheaf.obj_eq, PrimeSpectrum.isOpen_basicOpen, Opens.mapId_inv_app, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, PrimeSpectrum.exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.Scheme.basicOpen_one, PrimeSpectrum.isTopologicalBasis_basic_opens, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.Modules.Hom.id_app, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, Opens.inclusion'_map_eq_top, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, TopCat.Sheaf.pushforward_obj_val, Opens.IsBasis.exists_finite_of_isCompact, PrimeSpectrum.basicOpen_mul_le_left, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc, TopCat.Sheaf.sections_exact_of_left_exact, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, TopCat.Presheaf.stalkFunctor_map_germ_apply, TopCat.Presheaf.germ_res_apply', TopCat.Opens.coverDense_inducedFunctor, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.Modules.Hom.comp_app, Opens.overEquivalence_counitIso_inv_app, Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, AlgebraicGeometry.Scheme.map_basicOpen, Opens.adjunction_counit_map_functor, noetherianSpace_iff_opens, TopCat.Presheaf.generateEquivalenceOpensLe_functor, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Proj.zero_apply, Opens.coe_mk, TopCat.Presheaf.stalkFunctor_map_unit_toSheafify_isIso, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, Homeomorph.opensCongr_symm, AlgebraicGeometry.exists_affineOpens_le_appLE_of_appLE, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, Opens.overEquivalence_unitIso_inv_app_left, AlgebraicGeometry.StructureSheaf.const_algebraMap, AlgebraicGeometry.Scheme.Hom.id_appIso, smoothSheafCommRing.ι_forgetStalk_inv_assoc, skyscraperPresheafCocone_ι_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.PresheafedSpace.map_id_c_app, compatiblePreserving_opens_map, TopCat.Presheaf.germ_exist, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π, AlgebraicGeometry.Scheme.local_affine, TopCat.Presheaf.germ_res, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE_assoc, AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, Opens.adjunction_counit_app_self, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, Opens.mem_map, ProjectiveSpectrum.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.etale_appLE, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, IsOpenMap.coverPreserving, AlgebraicGeometry.Scheme.isoSpec_Spec, Opens.openPartialHomeomorphSubtypeCoe_target, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.Scheme.Hom.appLE_congr, MeasureTheory.Content.outerMeasure_exists_open, TopCat.Presheaf.Pushforward.id_hom_app, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, TopCat.Presheaf.pullback_obj_obj_ext_iff, instBorelSpaceSubtypeMemOpens, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, TopCat.Opens.coverDense_iff_isBasis, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.Scheme.Hom.preimage_sup, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero, TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, topCatOpToFrm_obj_coe, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, TopCat.Sheaf.interUnionPullbackConeLift_left, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE, TopCat.subpresheafToTypes_map_coe, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, Alexandrov.lowerCone_π_app, Manifold.IsImmersionOfComplement.ofOpen, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, IsOpenCover.isTopologicalBasis, topToLocale_map, IsOpenCover.exists_mem, Opens.map_comp_eq, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.SheafedSpace.Γ_obj_op, AlgebraicGeometry.Scheme.Hom.comp_preimage, TestFunction.tsupport_subset, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, Opens.carrier_eq_coe, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, TopCat.Presheaf.pushforward_map_app', AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot, AlgebraicGeometry.Scheme.homOfLE_appLE, Alexandrov.exists_le_of_le_sup, TopCat.Presheaf.pushforward_obj_map, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.Scheme.Hom.isIso_app, AlgebraicGeometry.Scheme.basicOpen_appLE, Opens.map_iSup, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, AlgebraicGeometry.structureSheafInType.add_apply, ModelWithCorners.BoundarylessManifold.open, Opens.eq_bot_or_top, AlgebraicGeometry.morphismRestrict_appTop, IsLocalRing.closed_point_mem_iff, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, TopCat.Presheaf.stalkPushforward_germ, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, germ_skyscraperPresheafStalkOfSpecializes_hom_assoc, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, AlgebraicGeometry.Proj.isBasis_basicOpen, AlgebraicGeometry.Proj.ext_iff, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, PrimeSpectrum.isClopen_basicOpen_of_mul_add, TopCat.Presheaf.germ_stalkPullbackHom_assoc, TopCat.subsheafToTypes_obj, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, AlgebraicGeometry.LocallyRingedSpace.Γ_map, StructureGroupoid.trans_restricted, AlgebraicGeometry.Flat.flat_of_affine_subset, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj, AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, smoothSheaf.eval_germ, ProjectiveSpectrum.isTopologicalBasis_basic_opens, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, Opens.mem_sSup, MeasureTheory.Content.outerMeasure_caratheodory, TopCat.GlueData.MkCore.t_id, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map, MeasureTheory.Content.outerMeasure_exists_compact, Opens.instHasEnoughPointsOpensGrothendieckTopology, Opens.isOpen, Opens.mk_empty, IsOpenMap.functorNhds_map, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.PresheafedSpace.Γ_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, Topology.IsOpenEmbedding.functor_obj_injective, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.IsLocalAtTarget.restrict, Topology.IsInducing.map_functorObj, TopCat.Presheaf.germ_stalkPullbackInv, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, Manifold.IsImmersionAtOfComplement.of_opens, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, Opens.leSupr_apply_mk, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, AlgebraicGeometry.Scheme.stalkMap_germ_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, Polynomial.image_comap_C_basicOpen, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, AlgebraicGeometry.Scheme.toOpen_eq, TopCat.Presheaf.map_restrict, AlgebraicGeometry.Scheme.Modules.restrict_obj, Opens.openPartialHomeomorphSubtypeCoe_source, OpenSubgroup.coe_toOpens, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, StructureGroupoid.LocalInvariantProp.liftProp_inclusion, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality, OpenSubgroup.toOpens_inf, Opens.functor_map_eq_inf, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, IsOpenCover.isOpen_iff_coe_preimage, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.StructureSheaf.comapₗ_const, TopCat.Presheaf.restrictOpenCommRingCat_apply, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, ProjectiveSpectrum.basicOpen_zero, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ, Alexandrov.principalOpen_le, AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, AlgebraicGeometry.StructureSheaf.res_apply, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.Scheme.Modules.Hom.add_app, ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.comap_basicOpen, OpenNhds.isOpenEmbedding, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.exists_map_preimage_le_map_preimage, Opens.IsBasis.isOpenCover, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.Scheme.Hom.map_appLE', AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, RealRMK.exists_open_approx, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.Flat.flat_appLE, AlgebraicGeometry.isIntegralHom_iff, TopCat.GlueData.ofOpenSubsets_toGlueData_V, Opens.iSup_def, AlgebraicGeometry.RingedSpace.basicOpen_res_eq, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE, AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, ProjectiveSpectrum.isOpen_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, AlgebraicGeometry.exists_of_res_eq_of_qcqs_of_top, AlgebraicGeometry.Scheme.Hom.finiteType_appLE, AlgebraicGeometry.exists_app_map_eq_map_of_isLimit, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, TopCat.GlueData.ofOpenSubsets_toGlueData_f, OpenAddSubgroup.coe_toOpens, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, TopCat.Presheaf.isSheaf_iff_isSheaf_comp', AlgebraicGeometry.StructureSheaf.algebraMap_germ, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, OpenNhds.inclusion_obj, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top, Opens.coe_compl, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, ProjectiveSpectrum.basicOpen_eq_union_of_projection, exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, Opens.coe_bot, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem, smoothSheafCommRing.ι_forgetStalk_hom_apply, OpenNhds.map_id_obj', TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.StructureSheaf.const_mul_cancel', AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, Opens.coe_sSup, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, Topology.IsInducing.functorNhds_obj_coe, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, AlgebraicGeometry.IsFinite.finite_app, TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂, AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType, OpenNhds.le_def, Opens.coe_overEquivalence_inverse_obj_left, Topology.IsInducing.functor_obj, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.forall_toScheme, TopCat.Presheaf.IsFlasque.epi, smoothSheafCommRing.ι_forgetStalk_hom_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe, AlgebraicGeometry.Proj.awayMap_awayToSection, MeasureTheory.Content.outerMeasure_opens, AlgebraicGeometry.Scheme.Hom.map_resLE, AlgebraicGeometry.finite_appTop_of_universallyClosed, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, IsOpenCover.iSup_eq_top, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, OpenPartialHomeomorph.subtypeRestr_symm_eqOn, contMDiffAt_subtype_iff, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.Scheme.Hom.resLE_preimage, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, ModelWithCorners.isBoundaryPoint_iff_isBoundaryPoint_val, Opens.mem_interior, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, AlgebraicGeometry.Scheme.Hom.le_preimage_resLE_iff, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, Opens.op_map_comp_obj, AlgebraicGeometry.SheafedSpace.id_c_app, TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, AlgebraicGeometry.Scheme.Hom.appIso_hom, Opens.instFinite, OpenPartialHomeomorph.subtypeRestr_def, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, AlgebraicGeometry.Scheme.evaluation_naturality_assoc, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.tilde.toOpen_res, Alexandrov.projSup_obj, AlgebraicGeometry.tilde.toOpen_res_assoc, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, AlgebraicGeometry.Scheme.emptyTo_c_app, TopCat.presheafToType_obj, Opens.comap_injective, OpenPartialHomeomorph.subtypeRestr_target_subset, MeasureTheory.Content.is_add_left_invariant_innerContent, AlgebraicGeometry.Scheme.Hom.map_resLE_assoc, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Opens.coe_comap, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, IsOpenCover.iUnion_inter, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, AlgebraicGeometry.smoothOfRelativeDimension_iff, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.Scheme.empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, TopCat.Presheaf.germ_res'_assoc, AlgebraicGeometry.Scheme.Opens.ι_app_self, Opens.mapComp_inv_app, AlgebraicGeometry.ΓSpec.toSpecΓ_of, AlgebraicGeometry.Scheme.zeroLocus_span, AlgebraicGeometry.StructureSheaf.toOpen_germ, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.Scheme.Hom.naturality, OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, AlgebraicGeometry.Proj.stalkIso'_germ, TopCat.Presheaf.isGluing_iff_pairwise, Alexandrov.lowerCone_pt, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, PrimeSpectrum.isCompact_basicOpen, AlgebraicGeometry.SheafedSpace.Γ_obj, AlgebraicGeometry.Scheme.restrict_presheaf_map, Opens.instNontrivialOfNonempty, Clopens.coe_toOpens, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.formallyUnramified_iff, Opens.map_comp_obj, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, PrimeSpectrum.basicOpen_mul_le_right, TopCat.Sheaf.eq_app_of_locally_eq, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, ContinuousMap.coe_opensOfIdeal, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, Closeds.compl_bijective, TestFunction.monoCLM_apply, Opens.mapIso_hom_app, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, smoothSheaf.ι_evalHom, Manifold.IsImmersion.ofOpen, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.Scheme.comp_appTop, smoothSheafCommRing.ι_evalHom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, TopCat.Presheaf.Pushforward.comp_hom_app, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpen, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, PrimeSpectrum.basicOpen_le_basicOpen_iff, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.germ_eq_zero_of_pow_mul_eq_zero, AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const, AlgebraicGeometry.isIso_pushoutSection_iff, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, Opens.coe_sup, AlgebraicGeometry.Smooth.smooth_appLE, TopCat.GlueData.MkCore.t_inter, AlgebraicGeometry.StructureSheaf.res_const, smoothSheaf.contMDiff_section, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, PrimeSpectrum.mem_basicOpen, AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine, 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.exists_of_res_zero_of_qcqs, Opens.mayerVietorisSquare'_toSquare, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, smoothSheafCommRing.ι_forgetStalk_hom, AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen, AlgebraicGeometry.Scheme.homOfLE_base, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.mem_basicOpen_den, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, Opens.coe_mayerVietorisSquare_X₄, AlgebraicGeometry.PresheafedSpace.congr_app, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app, Opens.coe_disjoint, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.IsAffineOpen.fromSpec_top, Opens.isBasis_iff_cover, IsOpenCover.exists_finite_clopen_cover, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, OpenAddSubgroup.mem_toOpens, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.Scheme.Hom.comp_appTop, Manifold.IsImmersionAt.ofOpen, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.Hom.preimage_mono, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.exists_map_eq_top, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk', AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE_assoc, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, skyscraperPresheafCoconeOfSpecializes_ι_app, Opens.apply_mk, Opens.infLELeft_apply, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, ProjectiveSpectrum.mem_coe_basicOpen, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj, AlgebraicGeometry.etale_iff, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, Opens.isOpenEmbedding_of_le, IsOpenCover.isLocallyClosed_iff_coe_preimage, AlgebraicGeometry.Scheme.germ_residue_assoc, instIsContinuousOpensCarrierMapGrothendieckTopology, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc, PrespectralSpace.isBasis_opens, TopCat.Presheaf.Γgerm_res_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.exists_appTop_map_eq_zero_of_isLimit, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE, AlgebraicGeometry.tilde.toOpen_map_app_assoc, AlgebraicGeometry.exists_app_map_eq_zero_of_isLimit, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, AlgebraicGeometry.Scheme.Opens.ι_appLE, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.appLE_comp_appLE, ContMDiff.extend_one, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE, AlgebraicGeometry.Scheme.Hom.resLE_appLE, TopCat.Presheaf.germ_stalkSpecializes, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Scheme.Opens.ι_app, Opens.toPretopology_grothendieckTopology, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.locallyOfFinitePresentation_iff, AlgebraicGeometry.exists_basicOpen_le_affine_inter, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.PresheafedSpace.restrict_presheaf, TopCat.Presheaf.germ_eq, MeasureTheory.Content.innerContent_comap, OpenSubgroup.toOpens_top, AlgebraicGeometry.Scheme.germ_residue, PrimeSpectrum.zeroLocus_eq_basicOpen_of_mul_add, Opens.map_top, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.Presheaf.presheafEquivOfIso_functor_map_app, Topology.IsInducing.le_functorObj_iff, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, Opens.comap_id, Opens.overEquivalence_inverse_obj_right_as, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CompactOpens.coe_toOpens, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.Scheme.Hom.map_appLE, ProjectiveSpectrum.basicOpen_one, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, Opens.apply_def, AlgebraicGeometry.Scheme.Γevaluation_naturality, Opens.coe_inj, AlgebraicGeometry.IsSeparated.instMorphismRestrict, AlgebraicGeometry.basicOpen_eq_bot_iff, Manifold.IsImmersionOfComplement.of_opens, OpenAddSubgroup.toOpens_top, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, Opens.coe_inf, Opens.mapMapIso_counitIso, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, Opens.mk_coe, Opens.toTopCat_map, AlgebraicGeometry.Spec.fromSpecStalk_eq, skyscraperPresheafCoconeOfSpecializes_pt, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, TopCat.Presheaf.stalkFunctor_map_germ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom_assoc, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, ProjectiveSpectrum.basicOpen_mul_le_right, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, TopCat.Presheaf.toPushforwardOfIso_app, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, TestFunctionClass.tsupport_map_subset, AlgebraicGeometry.Scheme.Hom.flat_appLE, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.Scheme.comp_app_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, TopCat.Presheaf.restrict_sum, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, SkyscraperPresheafFunctor.map'_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, PresheafOfModules.germ_ringCat_smul, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, TopCat.Sheaf.eq_of_locally_eq_iff, AlgebraicGeometry.exists_lift_of_germInjective_aux, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, Opens.ext_iff, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.Scheme.Γ_obj_op, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, StructureGroupoid.subtypeRestr_mem_maximalAtlas, coverPreserving_opens_map, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.Hom.appLE_map, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, IsOpenMap.coe_functor_obj, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Proj.res_apply, TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.topIso_hom, Opens.overEquivalence_counitIso_hom_app, AlgebraicGeometry.StructureSheaf.toOpen_res, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.OpenCover.restrict_X, PresheafOfModules.germ_smul, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, PrimeSpectrum.basicOpen_one, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, Manifold.IsSmoothEmbedding.of_opens, AlgebraicGeometry.StructureSheaf.const_mul, AlgebraicGeometry.AffineSpace.map_appTop_coord, OpenPartialHomeomorph.subtypeRestr_source, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, PrimeSpectrum.iSup_basicOpen_eq_top_iff', TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.isIso_fromTildeΓ_iff, TopCat.Sheaf.interUnionPullbackCone_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, Algebra.basicOpen_subset_smoothLocus_iff, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.Scheme.zero_of_zero_cover, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.StructureSheaf.const_apply, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.exists_of_res_eq_of_qcqs, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, TopCat.Presheaf.coveringOfPresieve_apply, Opens.not_nonempty_iff_eq_bot, TopCat.Sheaf.isLocallySurjective_iff_epi, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, TestFunction.tsupport_subset', TopCat.subpresheafToTypes_obj, TopCat.Presheaf.submonoidPresheafOfStalk_obj, TopCat.Presheaf.stalkFunctor_map_germ_apply', AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, TopCat.GlueData.MkCore.cocycle, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, OpenNhds.inclusionMapIso_inv_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, OpenNhdsOf.toOpens_injective, AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, PrimeSpectrum.localization_away_comap_range, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Proj.stalkIso'_symm_mk, AlgebraicGeometry.structureSheafInType.smul_apply, Opens.instSubsingletonObjOpensFiber, OpenNhds.apply_mk, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.Scheme.Hom.le_resLE_preimage_iff, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, TopCat.PrelocalPredicate.sheafify_inductionOn₂, PrimeSpectrum.isRetrocompact_basicOpen, AlgebraicGeometry.coe_opensRestrict_apply_coe, PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.RingedSpace.mem_basicOpen, AlgebraicGeometry.Scheme.Hom.app_injective, CategoryTheory.Functor.mapPresheaf_obj_presheaf, TopCat.Presheaf.mono_iff_stalk_mono, AlgebraicGeometry.Scheme.Modules.inv_app, Opens.coe_top, TopCat.Presheaf.ext_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, PrimeSpectrum.isBasis_basic_opens, Topology.IsOpenEmbedding.compatiblePreserving, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, TopCat.Presheaf.presheafEquivOfIso_functor_obj_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, AlgebraicGeometry.Scheme.stalkMap_germ, Opens.coe_eq_univ, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, IsOpenCover.isOpen_iff_inter, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, TopCat.Presheaf.stalkFunctor_map_germ_assoc, OpenNhds.inclusionMapIso_hom_app, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk, Opens.mapIso_refl, AlgebraicGeometry.Scheme.comp_appLE_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Proj.awayToSection_comp_appLE_assoc, ContinuousMap.idealOfSet_isMaximal_iff, AlgebraicGeometry.Scheme.Hom.eqToHom_app, TopCat.presheafToTypes_obj, instRepresentablyFlatOpensCarrierMap, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover, AlgebraicGeometry.Scheme.id_app, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpenPowersToOpenₗ, Alexandrov.projSup_map, StructureGroupoid.restriction_mem_maximalAtlas_subtype, AlgebraicGeometry.flat_iff, Topology.IsInducing.functorNhds_map, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply, AlgebraicGeometry.Scheme.homOfLE_apply, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, TopCat.Presheaf.sections_exact_of_exact, Opens.val_apply, ContinuousMap.idealOpensGI_choice, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, germ_skyscraperPresheafStalkOfSpecializes_hom, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, MvPolynomial.mem_image_comap_C_basicOpen, contMDiff_subtype_val, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.Scheme.IdealSheafData.le_def, Topology.IsInducing.functor_map, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, TopCat.Presheaf.isSheaf_of_isOpenEmbedding, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, Opens.IsBasis.le_iff, PrimeSpectrum.basicOpen_eq_bot_iff, Opens.instCanLiftSetCoeIsOpen, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp, skyscraperPresheaf_map, TopCat.Presheaf.generateEquivalenceOpensLe_inverse, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.Scheme.mem_basicOpen, TopCat.PrelocalPredicate.sheafify_inductionOn₂', AlgebraicGeometry.SheafedSpace.comp_c_app', IsOpenCover.exists_mem_nhds, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, AlgebraicGeometry.Spec.map_app, Opens.mk_inf_mk, AlgebraicGeometry.exists_lift_of_germInjective, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.tilde.toOpen_map_app, Opens.map_id_eq, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ, Opens.mem_mk, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
|