Opens

📁 Source: Mathlib/Topology/Sets/Opens.lean

Statistics

Metric	Count
Definitions Opens, opensCongr, OpenNhdsOf, comap, instDistribLattice, instInhabited, instMax, instMin, instOrderTop, instPartialOrder, instSetLike, instUniqueOfSubsingleton, toOpens, Opens, IsBasis, carrier, comap, frameHom, frameMinimalAxioms, gi, inclusion, instCompleteLattice, instFrame, instInhabited, instPartialOrder, instSetLike, instUniqueOfIsEmpty, interior	28
Theorems opensCongr_apply, opensCongr_symm, basis_nhds, canLiftSet, isOpen, mem, mem', toOpens_injective, exists_finite_of_isCompact, isCompact_open_iff_eq_finite_iUnion, le_iff, of_isInducing, carrier_eq_coe, coe_bot, coe_comap, coe_disjoint, coe_eq_empty, coe_eq_univ, coe_finset_inf, coe_finset_sup, coe_iSup, coe_inf, coe_inj, coe_interior, coe_mk, coe_sSup, coe_sup, coe_top, comap_comap, comap_comp, comap_id, comap_injective, comap_mono, eq_bot_or_top, ext, ext_iff, forall, frameHom_toFun, gc, iSup_def, iSup_mk, instCanLiftSetCoeIsOpen, instFinite, instIsSimpleOrderOfNonemptyOfIndiscreteTopology, instNontrivialOfNonempty, instSecondCountableOpens, isBasis_iff_cover, isBasis_iff_nbhd, isBasis_sigma, isCompactElement_iff, isOpen, isOpenEmbedding', isOpenEmbedding_of_le, is_open', mem_bot, mem_comap, mem_iSup, mem_inf, mem_interior, mem_mk, mem_sSup, mem_sup, mem_top, mk_coe, mk_empty, mk_inf_mk, mk_univ, ne_bot_iff_nonempty, nonempty_coe, nonempty_coeSort, not_nonempty_iff_eq_bot	71
Total	99

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
Opens 📖	CompOp	685 math math: toSpecΓ_apply, Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, Hom.smoothLocus_eq_top_iff, Modules.pushforward_obj_presheaf_map, ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, coprodPresheafObjIso_hom_fst_assoc, Hom.toPartialMap_hom, map_PrimeSpectrum_basicOpen_of_affine, isoOfEq_inv, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, zeroLocus_iInf, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, Hom.opensRange_pullbackSnd, AffineZariskiSite.instFaithfulOpensToOpensFunctor, Hom.image_preimage_eq_opensRange_inter, IsQuasiAffine.toIsImmersion, ofRestrict_appIso, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, Hom.quasiFiniteLocus_comp, app_eq, IdealSheafData.glueDataObjHom_ι_assoc, AlgebraicGeometry.opensCone_pt, zeroLocus_empty_eq_univ, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.morphismRestrict_base_coe, Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, Opens.toSpecΓ_naturality, Opens.toSpecΓ_SpecMap_presheaf_map_top, restrictFunctorΓ_inv_app, Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, Opens.mem_ι_image_iff, Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, IdealSheafData.ideal_sSup, fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, Modules.pushforward_obj_obj, Hom.preimage_bot, mem_basicOpen', AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, Hom.mem_opensRange, zeroLocus_eq_univ_iff_subset_nilradical, Opens.topIso_inv, AlgebraicGeometry.isCompact_iff_exists, RationalMap.dense_domain, Hom.resLE_eq_morphismRestrict, inv_app, Hom.id_appTop, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, AlgebraicGeometry.image_morphismRestrict_preimage, zeroLocus_mul, AlgebraicGeometry.SpecMap_preimage_basicOpen, ideal_ker_le_ker_ΓSpecIso_inv_comp, isoSpec_inv_toSpecΓ, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, ι_toIso_inv, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact, Hom.preimageIso_hom_ι_assoc, IdealSheafData.equivOfIsAffine_apply, IdealSheafData.glueDataObjHom_ι, IdealSheafData.equivOfIsAffine_symm_apply, congr_app, IdealSheafData.ideal_mul, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, Opens.stalkIso_inv, SpecΓIdentity_hom_app, AlgebraicGeometry.locallyQuasiFinite_iff, preimage_comp, Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.functionField_isScalarTower, Hom.preimage_top, coprodPresheafObjIso_hom_snd_assoc, Hom.toNormalization_app_preimage, Hom.toImage_app_injective, isoSpec_hom, ι_toIso_inv_assoc, Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.instQuasiCompactMorphismRestrict, eqToHom_c_app, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, zeroLocus_biInf, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, Hom.image_preimage_le, AffineZariskiSite.generate_presieveOfSections, Hom.image_top_eq_opensRange, Hom.fromNormalization_preimage, toSpecΓ_naturality_assoc, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, AlgebraicGeometry.IsIntegralHom.isIntegral_app, ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, Hom.image_iSup₂, isoSpec_hom_naturality, zeroLocus_singleton, toSpecΓ_isoSpec_inv_assoc, IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.isLocallyArtinian_iff_of_isOpenCover, AlgebraicGeometry.IsImmersion.instMorphismRestrict, Hom.comp_app, IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, toSpecΓ_naturality, Hom.quasiFiniteLocus_eq_top, Hom.ι_toNormalization, IdealSheafData.ideal_pow, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, Hom.congr_app, Hom.preimage_iSup, Hom.toPartialMap_domain, Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, Hom.id_app, Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Proj.mem_basicOpen, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, preimage_basicOpen_top, directedAffineCover_f, ΓSpecIso_inv, Hom.app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, Hom.coequifibered_normalizationDiagramMap, isoSpec_hom_naturality_assoc, isoSpec_inv_image_zeroLocus, IdealSheafData.range_glueDataObjι_ι, germToFunctionField_injective, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', AlgebraicGeometry.morphismRestrict_base, Opens.ι_image_basicOpen_topIso_inv, zeroLocus_setMul, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, Opens.nonempty_iff, toSpecΓ_preimage_zeroLocus, Hom.preimage_image_eq, AlgebraicGeometry.isBasis_preimage_isAffineOpen, Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.affineLocally_iff_affineOpens_le, fromSpecStalk_appTop, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, Opens.toScheme_presheaf_obj, IdealSheafData.vanishingIdeal_ideal, id_appTop, Spec_map_presheaf_map_eqToHom, Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, fromSpecStalk_toSpecΓ, ker_toSpecΓ, IdealSheafData.ideal_bot, ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, Hom.mem_preimage, Γevaluation_naturality_apply, IdealSheafData.subschemeCover_map_subschemeι, basicOpen_le, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, AlgebraicGeometry.liftCoborder_app, Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, zeroLocus_def, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, Hom.preimage_smoothLocus_eq, AlgebraicGeometry.tilde.isoTop_hom, IdealSheafData.mem_supportSet_iff, Opens.toSpecΓ_appTop, IdealSheafData.mem_support_iff, directedAffineCover_I₀, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Γ_restrict_isLocalization, Hom.appIso_inv_app_presheafMap, Opens.toScheme_carrier, Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, Modules.restrictFunctorComp_hom_app_app, Hom.preimageIso_inv_ι, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Hom.apply_mem_image_iff, Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.Proj.basicOpen_mul, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, IdealSheafData.le_ofIdeals_iff, Hom.preimage_basicOpen_top, Modules.restrict_map, PartialMap.restrict_id, IsLocallyDirected.homOfLE_tAux, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, OpenCover.iSup_opensRange, AlgebraicGeometry.HasAffineProperty.restrict, Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, IdealSheafData.coe_support_ofIdealTop, component_nontrivial, zeroLocus_iInf_of_nonempty, AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, basicOpen_pow, Opens.toSpecΓ_top, Hom.ker_apply, IdealSheafData.ideal_comap_of_isOpenImmersion, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, AffineZariskiSite.restrictIsoSpec_hom_app, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, Hom.appIso_inv_app, Hom.liftCoborder_preimage, Hom.opensRange_pullbackFst, zeroLocus_radical, Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AffineZariskiSite.presieveOfSections_surjective, Opens.ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, Hom.appIso_inv_naturality, basicOpen_add_le, Hom.comp_app_assoc, comp_app, Hom.finite_app, AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, Hom.appIso_hom', zeroLocus_inf, IdealSheafData.ofIdeals_mono, instIsOpenImmersionToSpecΓOfIsQuasiAffine, 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, Hom.preimage_basicOpen, IdealSheafData.subschemeι_app, PartialMap.equiv_iff_of_isSeparated, isoSpec_Spec_hom, basicOpen_res_eq, Hom.isAffineOpen_iff_of_isOpenImmersion, image_basicOpen, AlgebraicGeometry.tilde.isIso_toOpen_top, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.IsProper.instMorphismRestrict, isPullback_toSpecΓ_toSpecΓ, Hom.genericPoint_mem_smoothLocus_of_perfectField, instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, ΓSpecIso_naturality, restrictFunctorΓ_hom_app, Modules.restrictFunctorCongr_hom_app_app, directedAffineCover_X, Modules.restrictFunctorId_inv_app_app, AlgebraicGeometry.germ_stalkClosedPointIso_hom, toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.opensDiagram_obj, Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Proj.basicOpen_mono, toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.opensCone_π_app, toSpecΓ_appTop, Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AffineZariskiSite.directedCover_X, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, Hom.comp_appIso, basicOpen_one, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, Hom.appIso_inv_app_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, Opens.ι_appTop, Hom.map_mem_image_iff, coprodPresheafObjIso_hom_snd, map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.isRetrocompact_basicOpen, Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, Hom.id_appIso, Hom.preimageIso_inv_ι_assoc, Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, comp_appTop_assoc, AlgebraicGeometry.Proj.basicOpen_one, IdealSheafData.ideal_top, AffineZariskiSite.directedCover_f, isoSpec_Spec, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, Hom.preimage_sup, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, Spec.algebraMap_residueFieldIso_inv, eq_zeroLocus_of_isClosed_of_isAffine, Opens.ι_preimage_self, toSpecΓ_image_zeroLocus, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, Hom.image_iSup, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, Hom.comp_preimage, Hom.naturality_assoc, IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, Hom.iInf_ker_openCover_map_comp_apply, isoOfEq_rfl, inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.morphismRestrict_appTop, Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, Hom.ι_toNormalization_assoc, AlgebraicGeometry.IsLocalAtTarget.restrict, Hom.fromNormalization_app_assoc, isoSpec_inv_toSpecΓ_assoc, IdealSheafData.ideal_iInf, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, Hom.isoImage_inv_ι, IdealSheafData.range_glueDataObjι, Hom.isoImage_inv_ι_assoc, Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, ker_morphismRestrict_ideal, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, coprodPresheafObjIso_hom_fst, toOpen_eq, Modules.restrict_obj, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.isCompl_opensRange_inl_inr, Hom.isIntegral_app, Hom.app_eq_appLE, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, affineBasicOpen_coe, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, IdealSheafData.instIsPreimmersionGlueDataObjι, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, Hom.inv_appTop, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.Spec_zeroLocus, basicOpen_mul, ΓSpecIso_inv_naturality, IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, PartialMap.mem_domain_ofFromSpecStalk, zeroLocus_biInf_of_nonempty, SpecΓIdentity_inv_app, Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.basicOpen_eq_of_affine', Hom.coe_image, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, Hom.coe_preimage, Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, isoSpec_Spec_inv, IdealSheafData.supportSet_subset_zeroLocus, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, topIso_hom, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.finite_appTop_of_universallyClosed, AffineZariskiSite.toOpens_mono, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.specTargetImageFactorization_app_injective, IdealSheafData.zeroLocus_inter_subset_supportSet, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, Hom.preimage_inf, AlgebraicGeometry.isPullback_morphismRestrict, IdealSheafData.map_ideal', Hom.appIso_hom, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, IdealSheafData.ideal_sup, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, Hom.ι_fromNormalization_assoc, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, Opens.mem_basicOpen_toScheme, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, Hom.image_le_opensRange, 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, Hom.mem_smoothLocus, AlgebraicGeometry.instSmoothMorphismRestrict, IdealSheafData.ideal_mono, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, Opens.ι_app_self, zeroLocus_span, IdealSheafData.ideal_iSup, Hom.naturality, Hom.image_injective, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, restrict_presheaf_map, AlgebraicGeometry.Proj.basicOpen_zero, AlgebraicGeometry.formallyUnramified_iff, mem_basicOpen_top, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, Opens.ι_image_basicOpen', AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, Opens.ι_apply, Hom.dense_smoothLocus_of_perfectField, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, basicOpen_res, AlgebraicGeometry.Smooth.exists_isStandardSmooth, comp_appTop, IdealSheafData.radical_ideal, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AffineZariskiSite.mem_grothendieckTopology, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, IdealSheafData.ideal_inf, AlgebraicGeometry.exists_of_res_zero_of_qcqs, Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, IdealSheafData.subschemeι_app_surjective, preimage_zeroLocus, AffineZariskiSite.toOpens_injective, AffineZariskiSite.cocone_ι_app, Hom.smoothLocus_eq_top, IdealSheafData.coe_support_inter, AlgebraicGeometry.IsAffineOpen.fromSpec_top, map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, Hom.comp_appTop, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, germ_stalkClosedPointTo_Spec, basicOpen_zero, IdealSheafData.ideal_ofIdeals_le, IsLocallyDirected.exists_of_pullback_V_V, 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.etale_iff, AlgebraicGeometry.spread_out_unique_of_isGermInjective, AlgebraicGeometry.isAffineOpen_bot, IsLocallyDirected.V_self, Opens.ι_image_le, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, mem_basicOpen'', AffineZariskiSite.cocone_pt, AlgebraicGeometry.basicOpen_eq_of_affine, ΓSpecIso_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, Hom.comp_image, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, Opens.ι_app, IdealSheafData.supportSet_inter, AlgebraicGeometry.locallyOfFinitePresentation_iff, Hom.isoImage_hom_ι, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, AlgebraicGeometry.spread_out_unique_of_isGermInjective', AlgebraicGeometry.instUniversallyClosedMorphismRestrict, toIso_inv_ι, Hom.instIsIsoCommRingCatApp, Hom.inv_image, AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, Hom.opensRange_comp, Hom.ι_fromNormalization, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, Γevaluation_naturality, AlgebraicGeometry.IsSeparated.instMorphismRestrict, PartialMap.dense_domain, AlgebraicGeometry.basicOpen_eq_bot_iff, IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, Hom.appIso_inv_app_apply, restrictFunctor_obj_left, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, IdealSheafData.ideal_biInf, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', basicOpen_restrict, Hom.opensRange_of_isIso, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, IdealSheafData.glueDataObjι_ι, preimage_basicOpen, Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, restrictFunctor_map_left, comp_app_assoc, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, PartialMap.le_domain_toRationalMap, Opens.ι_image_top, Hom.toImage_app, Modules.restrictFunctorId_hom_app_app, AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, Modules.Hom.app_smul, Γ_obj_op, Hom.mem_quasiFiniteLocus, AlgebraicGeometry.quasiCompactCover_iff, image_zeroLocus, basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, Hom.isoImage_hom_ι_assoc, Opens.topIso_hom, IsLocallyDirected.homOfLE_tAux_assoc, OpenCover.restrict_X, zeroLocus_univ, Hom.image_le_image_iff, Hom.comp_appTop_assoc, AlgebraicGeometry.AffineSpace.map_appTop_coord, toSpecΓ_preimage_basicOpen, Hom.app_appIso_inv, Hom.normalizationObjIso_hom_val, openCoverBasicOpenTop_f, Hom.appLE_eq_app, RationalMap.mem_domain, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.exists_of_res_eq_of_qcqs, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, IdealSheafData.strictMono_ideal, codisjoint_zeroLocus, PartialMap.restrict_id_hom, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Etale.instMorphismRestrict, isoSpec_image_zeroLocus, AffineZariskiSite.basicOpen_coe, IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, Modules.pushforward_map_app, AlgebraicGeometry.coe_opensRestrict_apply_coe, AffineZariskiSite.presieveOfSections_eq_ofArrows, Hom.inv_app, restrictFunctor_obj_hom, Hom.app_injective, Opens.toSpecΓ_preimage_zeroLocus, exists_isOpenCover_and_isAffine, isoOfEq_hom, AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, IdealSheafData.map_ideal_basicOpen, AffineZariskiSite.toOpensFunctor_obj, mem_zeroLocus_iff, Hom.fromNormalization_app, Opens.ι_base_apply, Hom.eqToHom_app, AlgebraicGeometry.instIsAffineHomιBasicOpen, id_app, AlgebraicGeometry.flat_iff, zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, homOfLE_rfl, AlgebraicGeometry.IsOpenImmersion.lift_app, AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, IdealSheafData.le_def, AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, IdealSheafData.supportSet_eq_iInter_zeroLocus, Modules.map_smul, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, affineBasicOpen_le, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.Spec.map_app, Spec_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, Hom.id_image, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth

Homeomorph

Definitions

Name	Category	Theorems
opensCongr 📖	CompOp	2 math math: opensCongr_apply, opensCongr_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opensCongr_apply 📖	mathematical	—	DFunLike.coe RelIso TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder RelIso.instFunLike opensCongr FrameHom TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap toContinuousMap Homeomorph EquivLike.toFunLike instEquivLike instContinuousMapClass symm	—	—
opensCongr_symm 📖	mathematical	—	OrderIso.symm TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder opensCongr symm	—	—

TopologicalSpace

Definitions

Name	Category	Theorems
OpenNhdsOf 📖	CompData	7 math math: MeasureTheory.Measure.haar.nonempty_iInter_clAddPrehaar, OpenNhdsOf.canLiftSet, OpenNhdsOf.mem, OpenNhdsOf.isOpen, OpenNhdsOf.basis_nhds, MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar, OpenNhdsOf.toOpens_injective
Opens 📖	CompData	1323 math math: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, OpenNhds.coe_id, AlgebraicGeometry.Scheme.toSpecΓ_apply, 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.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.Scheme.Hom.opensRange_pullbackSnd, ProjectiveSpectrum.mem_basicOpen, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, TopCat.presheafToType_map, TopCat.Sheaf.interUnionPullbackCone_snd, Opens.map_coe, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, 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, 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.Scheme.zeroLocus_empty_eq_univ, Opens.instIsManifoldSubtypeMem, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.StructureSheaf.comap_id, Opens.coe_iSup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, AlgebraicGeometry.IsAffineOpen.map_fromSpec, TopCat.Presheaf.Pushforward.id_inv_app, Closeds.coe_compl, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, Opens.chartAt_eq, 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, 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, Opens.mem_sup, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, OpenNhds.inclusionMapIso_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality, 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.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.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, 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, 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, OpenNhds.val_apply, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, Module.basicOpen_subset_freeLocus_iff, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, TopCat.GlueData.ofOpenSubsets_toGlueData_U, Opens.instIsContinuousCompGrothendieckTopology, OpenNhds.inclusionMapIso_inv, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.structureSheafInType.mul_apply, 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, 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.StructureSheaf.toOpen_comp_comap, TopCat.Presheaf.pushforwardToOfIso_app, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, 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, AlgebraicGeometry.PresheafedSpace.Γ_obj_op, Opens.map_comp_obj_unop, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', TopCat.Sheaf.interUnionPullbackCone_fst, AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TopCat.GlueData.MkCore.V_id, Opens.comap_comap, Manifold.IsImmersion.of_opens, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, IsOpenCover.comap, 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, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.eqToHom_c_app, TopCat.GlueData.ofOpenSubsets_toGlueData_t, Opens.complOrderIso_symm_apply, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, 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, 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, TopCat.Sheaf.id_app, Opens.isOpenEmbedding_obj_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.StructureSheaf.comap_const, 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, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, Opens.mapId_hom_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, PrimeSpectrum.isConstructible_basicOpen, ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val, Opens.mapComp_hom_app, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, 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.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, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, ModelWithCorners.boundary_open, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, Opens.map_id_obj', AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, 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, ProjectiveSpectrum.basicOpen_mul_le_left, 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, 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, Opens.partialHomeomorphSubtypeCoe_target, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', MeasureTheory.Content.innerContent_exists_compact, 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, 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, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, Opens.map_functor_eq, Opens.instSecondCountableOpens, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, IsOpenCover.isClosed_iff_coe_preimage, Algebra.basicOpen_subset_smoothLocus_iff_smooth, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, IsCompactOpenCovered.exists_mem_of_isBasis, AlgebraicGeometry.Scheme.ker_of_isAffine, 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, AlgebraicGeometry.ΓSpec.adjunction_counit_app, 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.Scheme.IdealSheafData.mem_supportSet_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, productOfMemOpens_isEmbedding, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, PrimeSpectrum.basicOpen_zero, PrimeSpectrum.isClopen_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, Opens.gc, smoothSheafCommRing.ι_evalHom, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Hom.app_eq, Opens.coe_eq_empty, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Alexandrov.principalOpen_le_iff, Opens.pretopology_ofGrothendieck, 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.StructureSheaf.IsLocalization.to_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.Scheme.Modules.restrict_map, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, Opens.functor_obj_map_obj, 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, Opens.map_comp_obj', 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.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.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, 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, AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_notMem_basicOpen, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, TopCat.Presheaf.stalk_mono_of_mono, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, Opens.op_map_id_obj, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.zeroLocus_radical, TopCat.Sheaf.interUnionPullbackConeLift_right, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_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, 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.isOpenEmbedding, 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.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, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.germ_injective_of_isIntegral, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, 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, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, 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.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.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, Topology.IsUpperSet.isSheaf_of_isRightKanExtension, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, Opens.coe_id, AlgebraicGeometry.IsProper.instMorphismRestrict, TopCat.presheafToTypes_map, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, 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, Opens.partialHomeomorphSubtypeCoe_coe, 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, StructureGroupoid.LocalInvariantProp.section_spec, Opens.mapMapIso_inverse, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, 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, smoothSheaf.obj_eq, PrimeSpectrum.isOpen_basicOpen, TopCat.subsheafToTypes_val, 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.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.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, 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, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, AlgebraicGeometry.Scheme.map_basicOpen, Opens.adjunction_counit_map_functor, noetherianSpace_iff_opens, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Proj.zero_apply, Opens.coe_mk, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, Homeomorph.opensCongr_symm, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, Opens.overEquivalence_unitIso_inv_app_left, 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, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, Opens.adjunction_counit_app_self, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, Opens.mem_map, ProjectiveSpectrum.basicOpen_mul, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, IsOpenMap.coverPreserving, AlgebraicGeometry.Scheme.isoSpec_Spec, Opens.openPartialHomeomorphSubtypeCoe_target, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, 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.Scheme.Spec.algebraMap_residueFieldIso_inv, topCatOpToFrm_obj_coe, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, TopCat.Sheaf.interUnionPullbackConeLift_left, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, TopCat.subpresheafToTypes_map_coe, 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, 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, TopCat.Presheaf.pushforward_obj_map, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.Scheme.Hom.isIso_app, 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, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, 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, AlgebraicGeometry.LocallyRingedSpace.Γ_map, StructureGroupoid.trans_restricted, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, ProjectiveSpectrum.isTopologicalBasis_basic_opens, 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.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, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, 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, 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, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, AlgebraicGeometry.Scheme.toOpen_eq, 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.restriction_in_maximalAtlas, 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.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, 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, Opens.IsBasis.isOpenCover, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, RealRMK.exists_open_approx, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.isIntegralHom_iff, TopCat.GlueData.ofOpenSubsets_toGlueData_V, Opens.iSup_def, AlgebraicGeometry.RingedSpace.basicOpen_res_eq, AlgebraicGeometry.Spec_zeroLocus, 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.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.IsOpenImmersion.app_ΓIso_hom, 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, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, Opens.coe_sSup, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, Topology.IsInducing.functorNhds_obj_coe, AlgebraicGeometry.IsFinite.finite_app, Opens.coe_overEquivalence_inverse_obj_left, Topology.IsInducing.functor_obj, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.forall_toScheme, smoothSheafCommRing.ι_forgetStalk_hom_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection, MeasureTheory.Content.outerMeasure_opens, 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, 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, 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, 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.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.IdealSheafData.ideal_mono, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.Scheme.empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, Opens.mapComp_inv_app, AlgebraicGeometry.ΓSpec.toSpecΓ_of, AlgebraicGeometry.Scheme.zeroLocus_span, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, 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, 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.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, 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, TopCat.Presheaf.Pushforward.comp_hom_app, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen, PrimeSpectrum.basicOpen_le_basicOpen_iff, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, Opens.coe_sup, smoothSheaf.contMDiff_section, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, PrimeSpectrum.mem_basicOpen, 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, smoothSheafCommRing.ι_forgetStalk_hom, AlgebraicGeometry.Scheme.homOfLE_base, 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, 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, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.Hom.preimage_mono, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, skyscraperPresheafCoconeOfSpecializes_ι_app, Opens.infLELeft_apply, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.isFinite_iff, ProjectiveSpectrum.mem_coe_basicOpen, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj, AlgebraicGeometry.etale_iff, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, IsOpenCover.isLocallyClosed_iff_coe_preimage, instIsContinuousOpensCarrierMapGrothendieckTopology, PrespectralSpace.isBasis_opens, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.tilde.toOpen_map_app_assoc, 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.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, 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.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, MeasureTheory.Content.innerContent_comap, OpenSubgroup.toOpens_top, PrimeSpectrum.zeroLocus_eq_basicOpen_of_mul_add, Opens.map_top, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, 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.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, ProjectiveSpectrum.basicOpen_one, 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.Spec.germ_stalkMapIso_hom, Opens.coe_inf, Opens.mapMapIso_counitIso, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, Opens.mk_coe, AlgebraicGeometry.Spec.fromSpecStalk_eq, skyscraperPresheafCoconeOfSpecializes_pt, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, ProjectiveSpectrum.basicOpen_mul_le_right, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, 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.affineOpenCover_X, AlgebraicGeometry.Scheme.comp_app_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, SkyscraperPresheafFunctor.map'_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, TopCat.Sheaf.eq_of_locally_eq_iff, 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.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, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, PrimeSpectrum.basicOpen_one, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, Manifold.IsSmoothEmbedding.of_opens, 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.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, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, TestFunction.tsupport_subset', TopCat.subpresheafToTypes_obj, TopCat.Presheaf.submonoidPresheafOfStalk_obj, 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, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, OpenNhds.inclusionMapIso_inv_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, 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, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, 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.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.Scheme.stalkMap_germ, Opens.coe_eq_univ, Opens.partialHomeomorphSubtypeCoe_source, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, IsOpenCover.isOpen_iff_inter, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, OpenNhds.inclusionMapIso_hom_app, Opens.mapIso_refl, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, 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, 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, Opens.val_apply, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, 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, 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, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.Scheme.mem_basicOpen, 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.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.tilde.toOpen_map_app, Opens.map_id_eq, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, Opens.mem_mk, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth

TopologicalSpace.OpenNhdsOf

Definitions

Name	Category	Theorems
comap 📖	CompOp	—
instDistribLattice 📖	CompOp	—
instInhabited 📖	CompOp	—
instMax 📖	CompOp	—
instMin 📖	CompOp	—
instOrderTop 📖	CompOp	—
instPartialOrder 📖	CompOp	—
instSetLike 📖	CompOp	4 math math: canLiftSet, mem, isOpen, basis_nhds
instUniqueOfSubsingleton 📖	CompOp	—
toOpens 📖	CompOp	2 math math: mem', toOpens_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_nhds 📖	mathematical	—	Filter.HasBasis TopologicalSpace.OpenNhdsOf nhds SetLike.coe instSetLike	—	Filter.HasBasis.to_hasBasis nhds_basis_opens Set.Subset.rfl mem isOpen
canLiftSet 📖	mathematical	—	CanLift Set TopologicalSpace.OpenNhdsOf SetLike.coe instSetLike IsOpen Set.instMembership	—	—
isOpen 📖	mathematical	—	IsOpen SetLike.coe TopologicalSpace.OpenNhdsOf instSetLike	—	TopologicalSpace.Opens.is_open'
mem 📖	mathematical	—	TopologicalSpace.OpenNhdsOf SetLike.instMembership instSetLike	—	mem'
mem' 📖	mathematical	—	Set Set.instMembership TopologicalSpace.Opens.carrier toOpens	—	—
toOpens_injective 📖	mathematical	—	TopologicalSpace.OpenNhdsOf TopologicalSpace.Opens toOpens	—	—

TopologicalSpace.Opens

Definitions

Name	Category	Theorems
IsBasis 📖	MathDef	11 math math: isBasis_iff_nbhd, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.isBasis_basicOpen, TopCat.Opens.coverDense_iff_isBasis, AlgebraicGeometry.Proj.isBasis_basicOpen, AlgebraicGeometry.isBasis_affine_open, isBasis_iff_cover, PrespectralSpace.isBasis_opens, AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, PrimeSpectrum.isBasis_basic_opens
carrier 📖	CompOp	47 math math: TopologicalSpace.IsOpenCover.isInducing_iff_restrictPreimage, IsOpenMap.exists_opens_image_eq_of_prespectralSpace, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, TopologicalSpace.IsOpenCover.isHomeomorph_iff_restrictPreimage, AlgebraicGeometry.Scheme.zeroLocus_def, isBasis_sigma, TopologicalSpace.OpenNhdsOf.mem', AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, IsCompactOpenCovered.iff_of_unique, IsBasis.of_isInducing, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.exists_isAffineOpen_mem_and_subset, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, carrier_eq_coe, germ_skyscraperPresheafStalkOfSpecializes_hom_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage, TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage, is_open', AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage, TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, IsLocalDiffeomorph.image_coe, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, germ_skyscraperPresheafStalkOfSpecializes_hom, TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage, TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage, AlgebraicGeometry.Spec.map_app
comap 📖	CompOp	20 math math: comap_mono, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, Homeomorph.opensCongr_apply, comap_comap, TopologicalSpace.IsOpenCover.comap, mem_comap, topCatOpToFrm_map, MeasureTheory.Content.is_mul_left_invariant_innerContent, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, comap_comp, topToLocale_map, PrimeSpectrum.comap_basicOpen, comap_injective, MeasureTheory.Content.is_add_left_invariant_innerContent, coe_comap, AlgebraicGeometry.StructureSheaf.comap_basicOpen, MeasureTheory.Content.innerContent_comap, comap_id
frameHom 📖	CompOp	1 math math: frameHom_toFun
frameMinimalAxioms 📖	CompOp	—
gi 📖	CompOp	—
inclusion 📖	CompOp	3 math math: contMDiff_inclusion, chartAt_inclusion_symm_eventuallyEq, StructureGroupoid.LocalInvariantProp.liftProp_inclusion
instCompleteLattice 📖	CompOp	441 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, TopCat.Sheaf.interUnionPullbackCone_snd, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, mem_top, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, coe_iSup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint, mem_sup, comap_mono, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, Opens.pretopology_toGrothendieck, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, AlgebraicGeometry.Scheme.Hom.id_appTop, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, IsLocalRing.closedPoint_mem_iff, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, isCoatom_iff, Locale.localePointOfSpacePoint_toFun, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.ι_toIso_inv, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, iSup_mk, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, 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, AlgebraicGeometry.PresheafedSpace.Γ_obj_op, TopCat.Sheaf.interUnionPullbackCone_fst, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TopCat.GlueData.MkCore.V_id, comap_comap, TopologicalSpace.IsOpenCover.comap, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, mem_comap, PrimeSpectrum.iSup_basicOpen_eq_top_iff, isOpenEmbedding_obj_top, 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.Scheme.Hom.image_iSup₂, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, frameHom_toFun, mk_univ, PrimeSpectrum.basicOpen_mul, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.Scheme.Hom.toPartialMap_domain, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, mem_inf, AlgebraicGeometry.Scheme.ΓSpecIso_inv, MeasureTheory.Content.innerContent_iSup_nat, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, inclusion'_top_functor, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.PresheafedSpace.Γ_map_op, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, TopCat.Presheaf.map_germ_eq_Γgerm, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, MeasureTheory.Content.is_mul_left_invariant_innerContent, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, TopCat.Presheaf.SheafConditionEqualizerProducts.w, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.tilde.isoTop_hom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, coe_eq_empty, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Opens.pretopology_ofGrothendieck, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.Proj.basicOpen_mul, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, functor_obj_map_obj, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, TopCat.Sheaf.existsUnique_gluing, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, coe_finset_sup, instIsSimpleOrderOfNonemptyOfIndiscreteTopology, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff, TopCat.Presheaf.map_germ_eq_Γgerm_assoc, TopCat.Sheaf.interUnionPullbackConeLift_right, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.AffineSpace.comp_homOfVector, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, mem_bot, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, coe_finset_inf, AlgebraicGeometry.tilde.isIso_toOpen_top, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.SheafedSpace.Γ_map, OpenAddSubgroup.toOpens_inf, TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections, mem_iSup, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, comap_comp, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, inclusion'_map_eq_top, IsBasis.exists_finite_of_isCompact, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, AlgebraicGeometry.Scheme.map_basicOpen, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, AlgebraicGeometry.isRetrocompact_basicOpen, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.comp_appTop_assoc, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π, AlgebraicGeometry.Proj.basicOpen_one, ProjectiveSpectrum.basicOpen_mul, AlgebraicGeometry.Scheme.isoSpec_Spec, 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, TopCat.Sheaf.interUnionPullbackConeLift_left, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.Scheme.Hom.image_iSup, Alexandrov.lowerCone_π_app, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.SheafedSpace.Γ_obj_op, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Scheme.basicOpen_appLE, map_iSup, eq_bot_or_top, AlgebraicGeometry.morphismRestrict_appTop, IsLocalRing.closed_point_mem_iff, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, mem_sSup, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompact, mk_empty, AlgebraicGeometry.PresheafedSpace.Γ_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, leSupr_apply_mk, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, AlgebraicGeometry.Scheme.toOpen_eq, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, OpenSubgroup.toOpens_inf, functor_map_eq_inf, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, PrimeSpectrum.comap_basicOpen, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, iSup_def, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, AlgebraicGeometry.IsAffineOpen.biSup_of_disjoint, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, ProjectiveSpectrum.basicOpen_eq_union_of_projection, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, coe_bot, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, coe_sSup, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Scheme.topIso_hom, AlgebraicGeometry.finite_appTop_of_universallyClosed, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, TopologicalSpace.IsOpenCover.iSup_eq_top, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, Alexandrov.projSup_obj, comap_injective, MeasureTheory.Content.is_add_left_invariant_innerContent, AlgebraicGeometry.affineAnd_apply, coe_comap, AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply, AlgebraicGeometry.ΓSpec.toSpecΓ_of, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, TopCat.Presheaf.isGluing_iff_pairwise, Alexandrov.lowerCone_pt, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.SheafedSpace.Γ_obj, AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.basicOpen_res, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.Scheme.fromSpecStalk_app, coe_sup, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, coe_disjoint, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_top, isBasis_iff_cover, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.Scheme.Hom.comp_appTop, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, infLELeft_apply, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, TopCat.Presheaf.Γgerm_res_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, 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.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, Opens.toPretopology_grothendieckTopology, AlgebraicGeometry.Scheme.toIso_inv_ι, MeasureTheory.Content.innerContent_comap, OpenSubgroup.toOpens_top, map_top, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, comap_id, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, ProjectiveSpectrum.basicOpen_one, AlgebraicGeometry.Scheme.Γevaluation_naturality, OpenAddSubgroup.toOpens_top, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, coe_inf, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineOpen.sup_of_disjoint, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.Opens.ι_image_top, TopCat.Sheaf.eq_of_locally_eq_iff, AlgebraicGeometry.isPullback_opens_inf_le, AlgebraicGeometry.Scheme.Γ_obj_op, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, PrimeSpectrum.basicOpen_one, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, PrimeSpectrum.iSup_basicOpen_eq_top_iff', AlgebraicGeometry.isIso_fromTildeΓ_iff, TopCat.Sheaf.interUnionPullbackCone_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, coe_top, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, coe_eq_univ, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, ContinuousMap.idealOfSet_isMaximal_iff, AlgebraicGeometry.instIsAffineHomιBasicOpen, Alexandrov.projSup_map, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, mk_inf_mk, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.Scheme.toSpecΓ_base
instFrame 📖	CompOp	24 math math: AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Hom.preimage_bot, topCatOpToFrm_map, PrimeSpectrum.basicOpen_zero, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, MeasureTheory.Content.innerContent_bot, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, topToLocale_map, eq_bot_or_top, ProjectiveSpectrum.basicOpen_zero, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, AlgebraicGeometry.Proj.basicOpen_zero, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.isAffineOpen_bot, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, not_nonempty_iff_eq_bot, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, PrimeSpectrum.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	1224 math math: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, AlgebraicGeometry.Scheme.toSpecΓ_apply, 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.Scheme.map_PrimeSpectrum_basicOpen_of_affine, TopCat.PrelocalPredicate.res, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, id_apply, AlgebraicGeometry.Scheme.isoOfEq_inv, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, 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, inclusion'_hom_apply, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, TopCat.presheafToType_map, TopCat.Sheaf.interUnionPullbackCone_snd, map_coe, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, AlgebraicGeometry.Scheme.ofRestrict_appIso, AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.opensCone_pt, Topology.IsOpenEmbedding.functor_isContinuous, AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.StructureSheaf.comap_id, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc, TopCat.Presheaf.Pushforward.id_inv_app, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, 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, isCompactElement_iff, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, AlgebraicGeometry.StructureSheaf.comap_comp, 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.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, TopologicalSpace.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, coe_inclusion', AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, TopologicalSpace.OpenNhds.inclusionMapIso_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.mem_basicOpen', AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, 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, TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext_iff, AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, Opens.mayerVietorisSquare_X₃, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.Scheme.Hom.id_appTop, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, smoothSheafCommRing.ι_evalHom_apply, TopCat.Presheaf.germ_exist_of_isBasis, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.Scheme.zeroLocus_mul, AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.StructureSheaf.comap_id', map_functor_eq', AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, AlgebraicGeometry.SpecMap_preimage_basicOpen, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, smoothSheafCommRing.eval_germ, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp, isCoatom_iff, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, map_obj, comp_apply, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, TopCat.GlueData.ofOpenSubsets_toGlueData_U, instIsContinuousCompGrothendieckTopology, TopologicalSpace.OpenNhds.inclusionMapIso_inv, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.structureSheafInType.mul_apply, TopCat.Presheaf.germ_stalkSpecializes_apply, AlgebraicGeometry.StructureSheaf.exists_const, IsOpenMap.functorNhds_obj_coe, skyscraperPresheafCocone_pt, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, TopCat.Sheaf.pushforward_map, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, infLELeft_apply_mk, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, isBasis_iff_nbhd, AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.Scheme.preimage_comp, smoothSheaf.ι_evalHom_apply, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, TopCat.Presheaf.pushforwardToOfIso_app, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp, complOrderIso_apply, 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, map_comp_obj_unop, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', TopCat.Sheaf.interUnionPullbackCone_fst, AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TopCat.Presheaf.stalkPushforward_germ_apply, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, 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, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, 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.GlueData.ofOpenSubsets_toGlueData_t, 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.Hom.image_preimage_le, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, IsOpenMap.functor_faithful, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, PrimeSpectrum.le_basicOpen_pow, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, TopCat.Sheaf.id_app, isOpenEmbedding_obj_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.StructureSheaf.comap_const, AlgebraicGeometry.Scheme.Hom.image_iSup₂, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, 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, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, mapId_hom_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, mapComp_hom_app, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, smoothSheaf.ι_evalHom_assoc, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.StructureSheaf.comap_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, IsOpenMap.functorFullOfMono, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, map_id_obj', AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Hom.id_app, TopCat.Presheaf.comp_app, AlgebraicGeometry.Scheme.Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, TopCat.Presheaf.germ_stalkSpecializes_assoc, ProjectiveSpectrum.basicOpen_mul_le_left, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, TopologicalSpace.OpenNhds.map_obj, TopCat.Presheaf.stalkPushforward_germ_assoc, TopCat.Presheaf.pushforward_map_app, 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.Modules.germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, 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, inclusion'_top_functor, TopCat.Presheaf.stalk_open_algebraMap, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, 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, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, map_functor_eq, 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, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, map_id_obj, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.basicOpen_le, AlgebraicGeometry.locallyOfFiniteType_iff, TopologicalSpace.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, AlgebraicGeometry.ΓSpec.adjunction_counit_app, 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, ModuleCat.Tilde.toOpen_res, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, gc, AlgebraicGeometry.opensDiagram_map, smoothSheafCommRing.ι_evalHom, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, TopCat.Presheaf.germ_res_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, Alexandrov.principalOpen_le_iff, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom, Opens.pretopology_ofGrothendieck, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.ΓSpecIso_obj_hom, map_comp_map, 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.StructureSheaf.IsLocalization.to_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.Scheme.Modules.restrict_map, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, AlgebraicGeometry.Scheme.PartialMap.restrict_id, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, functor_obj_map_obj, smoothSheafCommRing.evalHom_germ, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, map_comp_obj', mapMapIso_functor, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, mapIso_inv_app, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.Scheme.component_nontrivial, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, 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.Scheme.Hom.ker_apply, 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, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, instIsSimpleOrderOfNonemptyOfIndiscreteTopology, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_notMem_basicOpen, 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, TopCat.Presheaf.map_germ_eq_Γgerm_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, op_map_id_obj, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.zeroLocus_radical, TopCat.Sheaf.interUnionPullbackConeLift_right, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, mapMapIso_unitIso, AlgebraicGeometry.RingedSpace.basicOpen_le, AlgebraicGeometry.StructureSheaf.const_one, AlgebraicGeometry.Scheme.Opens.ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, overEquivalence_unitIso_hom_app_left, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, isOpenEmbedding, AlgebraicGeometry.Scheme.Hom.finite_app, TopCat.Presheaf.stalk_hom_ext_iff, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.exists_preimage_eq, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.Scheme.evaluation_naturality, 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, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.Scheme.zeroLocus_inf, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.germ_injective_of_isIntegral, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, TopCat.Presheaf.pushforward_obj_obj, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, Opens.mayerVietorisSquare_X₂, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, TopCat.GlueData.MkCore.t_inv, AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top, AlgebraicGeometry.Scheme.image_basicOpen, 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, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, Topology.IsUpperSet.isSheaf_of_isRightKanExtension, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, coe_id, AlgebraicGeometry.IsProper.instMorphismRestrict, TopCat.presheafToTypes_map, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, 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, set_range_inclusion', AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, TopCat.Sheaf.comp_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, smoothSheafCommRing.ι_forgetStalk_inv_apply, AlgebraicGeometry.SheafedSpace.Γ_map, Opens.coe_mayerVietorisSquare_X₁, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, IsBasis.isOpenCover_mem_and_le, AlgebraicGeometry.germ_stalkClosedPointIso_hom, TopCat.Presheaf.isLocallySurjective_iff, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Proj.basicOpen_mono, mapMapIso_inverse, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, TopCat.Presheaf.Pushforward.comp_inv_app, TopCat.Presheaf.covering_presieve_eq_self, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, AlgebraicGeometry.Scheme.evaluation_naturality_apply, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, smoothSheaf.obj_eq, TopCat.subsheafToTypes_val, mapId_inv_app, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.Scheme.basicOpen_one, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.Modules.Hom.id_app, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, inclusion'_map_eq_top, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, TopCat.Sheaf.pushforward_obj_val, PrimeSpectrum.basicOpen_mul_le_left, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, 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, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.Modules.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, overEquivalence_counitIso_inv_app, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, adjunction_counit_map_functor, TopCat.Presheaf.generateEquivalenceOpensLe_functor, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Proj.zero_apply, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, Homeomorph.opensCongr_symm, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, overEquivalence_unitIso_inv_app_left, AlgebraicGeometry.Scheme.Hom.id_appIso, smoothSheafCommRing.ι_forgetStalk_inv_assoc, skyscraperPresheafCocone_ι_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.isAffineHom_iff, 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.IdealSheafData.ideal_top, adjunction_counit_app_self, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, mem_map, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, IsOpenMap.coverPreserving, AlgebraicGeometry.Scheme.isoSpec_Spec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, TopCat.Presheaf.Pushforward.id_hom_app, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, TopCat.Presheaf.pullback_obj_obj_ext_iff, 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, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, 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, TopCat.subpresheafToTypes_map_coe, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Hom.image_iSup, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, Alexandrov.lowerCone_π_app, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, map_comp_eq, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.SheafedSpace.Γ_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, TopCat.Presheaf.pushforward_map_app', AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot, TopCat.Presheaf.pushforward_obj_map, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, map_iSup, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, AlgebraicGeometry.structureSheafInType.add_apply, AlgebraicGeometry.morphismRestrict_appTop, 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.IsAffineOpen.fromSpec_preimage_basicOpen, TopCat.Presheaf.germ_stalkPullbackHom_assoc, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, 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, IsOpenMap.functorNhds_map, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.PresheafedSpace.Γ_obj, Topology.IsOpenEmbedding.functor_obj_injective, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.IsLocalAtTarget.restrict, Topology.IsInducing.map_functorObj, TopCat.Presheaf.germ_stalkPullbackInv, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, leSupr_apply_mk, AlgebraicGeometry.Scheme.stalkMap_germ_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.Scheme.Modules.restrict_obj, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.Hom.preimage_iSup_eq_top, functor_map_eq_inf, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, 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, TopologicalSpace.OpenNhds.isOpenEmbedding, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.isIntegralHom_iff, TopCat.GlueData.ofOpenSubsets_toGlueData_V, 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.exists_of_res_eq_of_qcqs_of_top, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, TopCat.GlueData.ofOpenSubsets_toGlueData_f, 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.isSheaf_iff_isSheaf_comp', AlgebraicGeometry.StructureSheaf.algebraMap_germ, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, TopologicalSpace.OpenNhds.inclusion_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem, smoothSheafCommRing.ι_forgetStalk_hom_apply, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, Topology.IsInducing.functorNhds_obj_coe, AlgebraicGeometry.IsFinite.finite_app, coe_overEquivalence_inverse_obj_left, Topology.IsInducing.functor_obj, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, smoothSheafCommRing.ι_forgetStalk_hom_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.finite_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.IsIntegralHom.integral_app, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, op_map_comp_obj, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, AlgebraicGeometry.Scheme.Hom.appIso_hom, 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, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, AlgebraicGeometry.Scheme.Hom.image_le_opensRange, 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.instSmoothMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.Scheme.empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, TopCat.Presheaf.germ_res'_assoc, AlgebraicGeometry.Scheme.Opens.ι_app_self, 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, AlgebraicGeometry.Scheme.Hom.image_injective, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, AlgebraicGeometry.Proj.stalkIso'_germ, TopCat.Presheaf.isGluing_iff_pairwise, Alexandrov.lowerCone_pt, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.SheafedSpace.Γ_obj, AlgebraicGeometry.Scheme.restrict_presheaf_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.formallyUnramified_iff, 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, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, 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, mapIso_hom_app, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, smoothSheaf.ι_evalHom, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.Scheme.comp_appTop, smoothSheafCommRing.ι_evalHom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, TopCat.Presheaf.Pushforward.comp_hom_app, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, PrimeSpectrum.basicOpen_le_basicOpen_iff, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, TopCat.GlueData.MkCore.t_inter, 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, smoothSheafCommRing.ι_forgetStalk_hom, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, Opens.coe_mayerVietorisSquare_X₄, AlgebraicGeometry.PresheafedSpace.congr_app, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app, coe_disjoint, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.IsAffineOpen.fromSpec_top, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.Scheme.Hom.comp_appTop, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, 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, skyscraperPresheafCoconeOfSpecializes_ι_app, apply_mk, infLELeft_apply, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj, AlgebraicGeometry.etale_iff, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.Scheme.germ_residue_assoc, instIsContinuousOpensCarrierMapGrothendieckTopology, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, AlgebraicGeometry.Scheme.Opens.ι_image_le, TopCat.Presheaf.Γgerm_res_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.tilde.toOpen_map_app_assoc, 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.IdealSheafData.mem_supportSet_iff_of_mem, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, 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.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, AlgebraicGeometry.Scheme.Hom.isCompact_preimage, 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, AlgebraicGeometry.Scheme.germ_residue, map_top, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.Presheaf.presheafEquivOfIso_functor_map_app, AlgebraicGeometry.Scheme.Hom.opensRange_comp, Topology.IsInducing.le_functorObj_iff, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, overEquivalence_inverse_obj_right_as, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, apply_def, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.IsSeparated.instMorphismRestrict, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, mapMapIso_counitIso, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.Scheme.restrictFunctor_obj_left, toTopCat_map, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, skyscraperPresheafCoconeOfSpecializes_pt, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π, TopCat.Presheaf.stalkFunctor_map_germ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.Scheme.basicOpen_restrict, AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom_assoc, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, ProjectiveSpectrum.basicOpen_mul_le_right, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, TopCat.Presheaf.toPushforwardOfIso_app, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.Scheme.comp_app_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, SkyscraperPresheafFunctor.map'_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, PresheafOfModules.germ_ringCat_smul, AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Opens.ι_image_top, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, TopCat.Sheaf.eq_of_locally_eq_iff, 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.PresheafedSpace.IsOpenImmersion.inv_invApp, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, coverPreserving_opens_map, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, IsOpenMap.coe_functor_obj, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc, 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, overEquivalence_counitIso_hom_app, AlgebraicGeometry.StructureSheaf.toOpen_res, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.OpenCover.restrict_X, PresheafOfModules.germ_smul, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, AlgebraicGeometry.Scheme.Hom.image_le_image_iff, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.isIso_fromTildeΓ_iff, TopCat.Sheaf.interUnionPullbackCone_pt, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.exists_of_res_eq_of_qcqs, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, TopCat.Presheaf.coveringOfPresieve_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, TopCat.subpresheafToTypes_obj, TopCat.Presheaf.submonoidPresheafOfStalk_obj, TopCat.Presheaf.stalkFunctor_map_germ_apply', AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, TopCat.GlueData.MkCore.cocycle, TopologicalSpace.OpenNhds.inclusionMapIso_inv_app, AlgebraicGeometry.Scheme.PartialMap.restrict_id_hom, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Proj.stalkIso'_symm_mk, AlgebraicGeometry.structureSheafInType.smul_apply, 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.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.coe_opensRestrict_apply_coe, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage, 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, TopCat.Presheaf.ext_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, Topology.IsOpenEmbedding.compatiblePreserving, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, TopCat.Presheaf.presheafEquivOfIso_functor_obj_map, AlgebraicGeometry.Scheme.isoOfEq_hom, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, AlgebraicGeometry.Scheme.stalkMap_germ, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, TopCat.Presheaf.stalkFunctor_map_germ_assoc, TopologicalSpace.OpenNhds.inclusionMapIso_hom_app, mapIso_refl, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, ContinuousMap.idealOfSet_isMaximal_iff, AlgebraicGeometry.Scheme.Hom.eqToHom_app, TopCat.presheafToTypes_obj, instRepresentablyFlatOpensCarrierMap, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, AlgebraicGeometry.Scheme.id_app, Alexandrov.projSup_map, AlgebraicGeometry.flat_iff, Topology.IsInducing.functorNhds_map, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, val_apply, ContinuousMap.idealOpensGI_choice, AlgebraicGeometry.Scheme.homOfLE_rfl, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, germ_skyscraperPresheafStalkOfSpecializes_hom, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, 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.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, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.Scheme.mem_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.Scheme.affineBasicOpen_le, AlgebraicGeometry.SheafedSpace.comp_c_app', 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.IsAffineOpen.preimage, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.tilde.toOpen_map_app, map_id_eq, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ, AlgebraicGeometry.Scheme.Hom.id_image, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
instSetLike 📖	CompOp	363 math math: TopologicalSpace.OpenNhds.coe_id, TopCat.PrelocalPredicate.res, id_apply, coe_interior, PrimeSpectrum.isClopen_iff_mul_add, AlgebraicGeometry.Scheme.zeroLocus_iInf, inclusion'_hom_apply, ProjectiveSpectrum.mem_basicOpen, TopCat.presheafToType_map, map_coe, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, IsOpenMap.exists_opens_image_eq_of_prespectralSpace, Polynomial.mem_image_comap_C_basicOpen, mem_top, LocalizedModule.subsingleton_iff_disjoint, ModelWithCorners.interior_open, OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr, PrimeSpectrum.eq_biUnion_of_isOpen, instIsManifoldSubtypeMem, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.morphismRestrict_base_coe, coe_iSup, TopologicalSpace.Closeds.coe_compl, chartAt_eq, skyscraperPresheaf_obj, isCompactElement_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, TopCat.GlueData.open_image_open, AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff, OpenPartialHomeomorph.subtypeRestr_coe, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, coe_inclusion', mem_sup, AlgebraicGeometry.Scheme.mem_basicOpen', AlgebraicGeometry.Scheme.Hom.mem_opensRange, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.pow_apply, AlgebraicGeometry.isCompact_iff_exists, chartAt_subtype_val_symm_eventuallyEq, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem', AlgebraicGeometry.Scheme.RationalMap.dense_domain, TopologicalSpace.eq_induced_by_maps_to_sierpinski, TopologicalSpace.IsOpenCover.iSup_set_eq_univ, CompleteCopy.dist_eq, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, MvPolynomial.image_comap_C_basicOpen, AlgebraicGeometry.Proj.mul_apply, TopologicalSpace.OpenNhds.comp_apply, ne_bot_iff_nonempty, Algebra.basicOpen_subset_etaleLocus_iff_etale, IsLocalRing.closedPoint_mem_iff, PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add, Locale.localePointOfSpacePoint_toFun, comp_apply, AlgebraicGeometry.Scheme.Hom.coe_resLE_base, TopologicalSpace.OpenNhds.val_apply, Module.basicOpen_subset_freeLocus_iff, AlgebraicGeometry.structureSheafInType.mul_apply, contMDiff_inclusion, IsOpenMap.functorNhds_obj_coe, Manifold.IsImmersionAtOfComplement.ofOpen, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, isBasis_iff_nbhd, Algebra.basicOpen_subset_unramifiedLocus_iff, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, Topology.IsLocallyConstructible.iff_of_isOpenCover, AlgebraicGeometry.functionField_isScalarTower, Manifold.IsImmersion.of_opens, AlgebraicGeometry.Proj.one_apply, OnePoint.infty_mem_opensOfCompl, TopCat.GlueData.ofOpenSubsets_toGlueData_t, AlgebraicGeometry.Scheme.zeroLocus_biInf, TopologicalSpace.IsOpenCover.generalizingMap_iff_comp, mem_comap, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.Scheme.zeroLocus_singleton, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.Proj.sub_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, PrimeSpectrum.isConstructible_basicOpen, ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val, AlgebraicGeometry.Scheme.Hom.coe_resLE_apply, frameHom_toFun, OpenSubgroup.mem_toOpens, AlgebraicGeometry.StructureSheaf.comap_apply, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, TopologicalSpace.IsOpenCover.isOpenMap_iff_comp, PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem, ModelWithCorners.boundary_open, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt, isOpenEmbedding', PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem, chartAt_inclusion_symm_eventuallyEq, AlgebraicGeometry.Proj.mem_basicOpen, mem_inf, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, partialHomeomorphSubtypeCoe_target, MeasureTheory.Content.innerContent_exists_compact, instHasGroupoid, TopCat.continuousPrelocal_pred, AlgebraicGeometry.Scheme.Opens.nonempty_iff, TopCat.Presheaf.stalk_open_algebraMap, AlgebraicGeometry.coe_opensRestrict_symm_apply, instSecondCountableOpens, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem', TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage, Algebra.basicOpen_subset_smoothLocus_iff_smooth, IsCompactOpenCovered.exists_mem_of_isBasis, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem', AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, PrimeSpectrum.mem_image_comap_basicOpen, PrimeSpectrum.isClopen_iff, gc, AlgebraicGeometry.morphismRestrict_appLE, AlgebraicGeometry.Scheme.Opens.toScheme_carrier, coe_eq_empty, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, Alexandrov.principalOpen_le_iff, Topology.IsInducing.mem_functorObj_iff, Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, AlgebraicGeometry.Scheme.Opens.exists_toScheme, TopologicalSpace.IsOpenCover.quasiSober_iff_forall, CompleteCopy.dist_val_le_dist, nonempty_coe, openPartialHomeomorphSubtypeCoe_coe, AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff, coe_overEquivalence_functor_obj, coe_finset_sup, TopologicalSpace.OpenNhds.id_apply, overEquivalence_unitIso_hom_app_left, AlgebraicGeometry.Scheme.zeroLocus_map, TopCat.GlueData.range_fromOpenSubsetsGlue, IsBasis.of_isInducing, mem_bot, AlgebraicGeometry.isLocalIso_iff, StructureGroupoid.LocalInvariantProp.liftProp_subtype_val, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, coe_finset_inf, coe_id, TopCat.presheafToTypes_map, AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField, set_range_inclusion', TopologicalSpace.IsOpenCover.jacobsonSpace_iff, Opens.coe_mayerVietorisSquare_X₁, mem_iSup, TopCat.Presheaf.isLocallySurjective_iff, partialHomeomorphSubtypeCoe_coe, Alexandrov.self_mem_principalOpen, Algebra.basicOpen_subset_etaleLocus_iff, nonempty_coeSort, StructureGroupoid.LocalInvariantProp.section_spec, smoothSheaf.obj_eq, PrimeSpectrum.isOpen_basicOpen, PrimeSpectrum.exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, PrimeSpectrum.isTopologicalBasis_basic_opens, PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, overEquivalence_counitIso_inv_app, TopologicalSpace.noetherianSpace_iff_opens, AlgebraicGeometry.Proj.zero_apply, coe_mk, AlgebraicGeometry.isRetrocompact_basicOpen, overEquivalence_unitIso_inv_app_left, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.local_affine, mem_map, openPartialHomeomorphSubtypeCoe_target, MeasureTheory.Content.outerMeasure_exists_open, instBorelSpaceSubtypeMemOpens, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, TopCat.subpresheafToTypes_map_coe, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, Manifold.IsImmersionOfComplement.ofOpen, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, TopologicalSpace.IsOpenCover.exists_mem, TestFunction.tsupport_subset, carrier_eq_coe, AlgebraicGeometry.structureSheafInType.add_apply, ModelWithCorners.BoundarylessManifold.open, IsLocalRing.closed_point_mem_iff, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, PrimeSpectrum.isClopen_basicOpen_of_mul_add, StructureGroupoid.trans_restricted, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, ProjectiveSpectrum.isTopologicalBasis_basic_opens, mem_sSup, MeasureTheory.Content.outerMeasure_caratheodory, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, MeasureTheory.Content.outerMeasure_exists_compact, isOpen, IsOpenMap.functorNhds_map, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, Manifold.IsImmersionAtOfComplement.of_opens, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, Polynomial.image_comap_C_basicOpen, openPartialHomeomorphSubtypeCoe_source, OpenSubgroup.coe_toOpens, StructureGroupoid.LocalInvariantProp.liftProp_inclusion, StructureGroupoid.restriction_in_maximalAtlas, TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage, AlgebraicGeometry.StructureSheaf.comapₗ_const, AlgebraicGeometry.StructureSheaf.res_apply, ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl, TopologicalSpace.OpenNhds.isOpenEmbedding, RealRMK.exists_open_approx, iSup_def, ProjectiveSpectrum.isOpen_basicOpen, AlgebraicGeometry.Scheme.PartialMap.mem_domain_ofFromSpecStalk, OpenAddSubgroup.coe_toOpens, coe_compl, TopologicalSpace.exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.Scheme.Hom.coe_preimage, coe_bot, coe_sSup, Topology.IsInducing.functorNhds_obj_coe, coe_overEquivalence_inverse_obj_left, AlgebraicGeometry.Scheme.Opens.forall_toScheme, MeasureTheory.Content.outerMeasure_opens, OpenPartialHomeomorph.subtypeRestr_symm_eqOn, contMDiffAt_subtype_iff, ModelWithCorners.isBoundaryPoint_iff_isBoundaryPoint_val, mem_interior, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, OpenPartialHomeomorph.subtypeRestr_def, OpenPartialHomeomorph.subtypeRestr_target_subset, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, coe_comap, TopologicalSpace.IsOpenCover.iUnion_inter, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, PrimeSpectrum.isCompact_basicOpen, TopologicalSpace.Clopens.coe_toOpens, AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, ContinuousMap.coe_opensOfIdeal, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField, Manifold.IsImmersion.ofOpen, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, coe_sup, smoothSheaf.contMDiff_section, PrimeSpectrum.mem_basicOpen, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.mem_basicOpen_den, Opens.coe_mayerVietorisSquare_X₄, coe_disjoint, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, TopologicalSpace.IsOpenCover.exists_finite_clopen_cover, OpenAddSubgroup.mem_toOpens, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', infLELeft_apply, ProjectiveSpectrum.mem_coe_basicOpen, isOpenEmbedding_of_le, TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage, AlgebraicGeometry.spread_out_unique_of_isGermInjective, PrespectralSpace.isBasis_opens, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.Scheme.Opens.ι_appLE, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.spread_out_unique_of_isGermInjective', AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, PrimeSpectrum.zeroLocus_eq_basicOpen_of_mul_add, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, overEquivalence_inverse_obj_right_as, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, TopologicalSpace.CompactOpens.coe_toOpens, AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen, apply_def, coe_inj, AlgebraicGeometry.Scheme.PartialMap.dense_domain, Manifold.IsImmersionOfComplement.of_opens, coe_inf, mk_coe, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, AlgebraicGeometry.quasiCompact_iff_forall_affine, TestFunctionClass.tsupport_map_subset, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, SkyscraperPresheafFunctor.map'_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, ext_iff, AlgebraicGeometry.Scheme.Hom.mem_quasiFiniteLocus, StructureGroupoid.subtypeRestr_mem_maximalAtlas, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, IsOpenMap.coe_functor_obj, AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Proj.res_apply, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, overEquivalence_counitIso_hom_app, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion, AlgebraicGeometry.Scheme.zeroLocus_univ, Manifold.IsSmoothEmbedding.of_opens, OpenPartialHomeomorph.subtypeRestr_source, Algebra.basicOpen_subset_smoothLocus_iff, AlgebraicGeometry.Scheme.RationalMap.mem_domain, AlgebraicGeometry.StructureSheaf.const_apply, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, not_nonempty_iff_eq_bot, TestFunction.tsupport_subset', TopCat.Presheaf.submonoidPresheafOfStalk_obj, AlgebraicGeometry.Scheme.codisjoint_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, PrimeSpectrum.localization_away_comap_range, AlgebraicGeometry.structureSheafInType.smul_apply, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, PrimeSpectrum.isRetrocompact_basicOpen, AlgebraicGeometry.coe_opensRestrict_apply_coe, PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply, coe_top, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, coe_eq_univ, partialHomeomorphSubtypeCoe_source, TopologicalSpace.IsOpenCover.isOpen_iff_inter, AlgebraicGeometry.Scheme.mem_zeroLocus_iff, ContinuousMap.idealOfSet_isMaximal_iff, AlgebraicGeometry.Scheme.Opens.ι_base_apply, TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover, StructureGroupoid.restriction_mem_maximalAtlas_subtype, AlgebraicGeometry.Scheme.homOfLE_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, val_apply, MvPolynomial.mem_image_comap_C_basicOpen, contMDiff_subtype_val, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, IsBasis.le_iff, instCanLiftSetCoeIsOpen, skyscraperPresheaf_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, AlgebraicGeometry.RingedSpace.mem_basicOpen', TopologicalSpace.IsOpenCover.exists_mem_nhds, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, mem_mk
instUniqueOfIsEmpty 📖	CompOp	—
interior 📖	CompOp	3 math math: coe_interior, gc, mem_interior

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
carrier_eq_coe 📖	mathematical	—	carrier SetLike.coe TopologicalSpace.Opens instSetLike	—	—
coe_bot 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Set Set.instEmptyCollection	—	—
coe_comap 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike DFunLike.coe FrameHom instCompleteLattice FrameHom.instFunLike comap Set.preimage ContinuousMap ContinuousMap.instFunLike	—	—
coe_disjoint 📖	mathematical	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe TopologicalSpace.Opens instSetLike instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice	—	—
coe_eq_empty 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike Set Set.instEmptyCollection Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	SetLike.coe_injective
coe_eq_univ 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike Set.univ Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	SetLike.coe_injective
coe_finset_inf 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike Finset.inf Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder CompleteLattice.toBoundedOrder Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop	—	map_finset_inf InfTopHom.instInfTopHomClass coe_inf coe_top
coe_finset_sup 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike Finset.sup Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toBoundedOrder Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	map_finset_sup SupBotHom.instSupBotHomClass coe_sup coe_bot
coe_iSup 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.iUnion	—	Set.iUnion_congr_Prop Set.iUnion_exists Set.iUnion_iUnion_eq'
coe_inf 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instInter	—	—
coe_inj 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike	—	SetLike.ext'_iff
coe_interior 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike interior interior	—	—
coe_mk 📖	mathematical	IsOpen	SetLike.coe TopologicalSpace.Opens instSetLike	—	—
coe_sSup 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.iUnion Set Set.instMembership	—	—
coe_sup 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instUnion	—	—
coe_top 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.univ	—	—
comap_comap 📖	mathematical	—	DFunLike.coe FrameHom TopologicalSpace.Opens instCompleteLattice FrameHom.instFunLike comap ContinuousMap.comp	—	—
comap_comp 📖	mathematical	—	comap ContinuousMap.comp FrameHom.comp TopologicalSpace.Opens instCompleteLattice	—	—
comap_id 📖	mathematical	—	comap ContinuousMap.id FrameHom.id TopologicalSpace.Opens instCompleteLattice	—	FrameHom.ext ext
comap_injective 📖	mathematical	—	ContinuousMap FrameHom TopologicalSpace.Opens instCompleteLattice comap	—	ContinuousMap.ext Inseparable.eq inseparable_iff_forall_isOpen DFunLike.congr_fun Set.ext_iff
comap_mono 📖	mathematical	TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe FrameHom instCompleteLattice FrameHom.instFunLike comap	—	OrderHomClass.mono BoundedOrderHomClass.toRelHomClass BoundedLatticeHomClass.toBoundedOrderHomClass FrameHomClass.toBoundedLatticeHomClass FrameHom.instFrameHomClass
eq_bot_or_top 📖	mathematical	—	Bot.bot TopologicalSpace.Opens OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra instFrame HeytingAlgebra.toOrderBot Top.top OrderTop.toTop CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	coe_eq_empty coe_eq_univ IndiscreteTopology.isOpen_iff is_open'
ext 📖	—	SetLike.coe TopologicalSpace.Opens instSetLike	—	—	SetLike.coe_injective
ext_iff 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike	—	ext
forall 📖	—	—	—	—	is_open'
frameHom_toFun 📖	mathematical	—	DFunLike.coe FrameHom TopologicalSpace.Opens Set instCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra FrameHom.instFunLike frameHom SetLike.coe instSetLike	—	—
gc 📖	mathematical	—	GaloisConnection TopologicalSpace.Opens Set PartialOrder.toPreorder instPartialOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.coe instSetLike interior	—	interior_maximal isOpen le_trans interior_subset
iSup_def 📖	mathematical	—	iSup TopologicalSpace.Opens ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.iUnion SetLike.coe instSetLike isOpen_iUnion is_open'	—	ext isOpen_iUnion is_open' coe_iSup
iSup_mk 📖	mathematical	IsOpen	iSup TopologicalSpace.Opens ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.iUnion isOpen_iUnion	—	iSup_def
instCanLiftSetCoeIsOpen 📖	mathematical	—	CanLift Set TopologicalSpace.Opens SetLike.coe instSetLike IsOpen	—	—
instFinite 📖	mathematical	—	Finite TopologicalSpace.Opens	—	Finite.of_injective Set.instFinite SetLike.coe_injective
instIsSimpleOrderOfNonemptyOfIndiscreteTopology 📖	mathematical	—	IsSimpleOrder TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder instPartialOrder CompleteLattice.toBoundedOrder instCompleteLattice	—	instNontrivialOfNonempty eq_bot_or_top
instNontrivialOfNonempty 📖	mathematical	—	Nontrivial TopologicalSpace.Opens	—	Set.empty_ne_univ
instSecondCountableOpens 📖	mathematical	—	SecondCountableTopology TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype	—	TopologicalSpace.Subtype.secondCountableTopology
isBasis_iff_cover 📖	mathematical	—	IsBasis Set TopologicalSpace.Opens Set.instHasSubset SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	ext coe_sSup TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' isOpen Set.sUnion_eq_biUnion iSup_and iSup_image isBasis_iff_nbhd mem_sSup le_sSup
isBasis_iff_nbhd 📖	mathematical	—	IsBasis TopologicalSpace.Opens Set Set.instMembership SetLike.instMembership instSetLike Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	TopologicalSpace.IsTopologicalBasis.mem_nhds_iff IsOpen.mem_nhds TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds is_open'
isBasis_sigma 📖	mathematical	IsBasis	instTopologicalSpaceSigma Set.iUnion TopologicalSpace.Opens Set.image carrier isOpenMap_sigmaMk is_open'	—	isOpenMap_sigmaMk is_open' Set.image_iUnion Set.image_congr TopologicalSpace.IsTopologicalBasis.sigma
isCompactElement_iff 📖	mathematical	—	IsCompactElement TopologicalSpace.Opens instPartialOrder IsCompact SetLike.coe instSetLike	—	isCompact_iff_finite_subcover CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup isOpen_iUnion Set.Subset.trans coe_finset_sup Finset.sup_eq_iSup subset_refl Set.instReflSubset isOpen coe_iSup Finset.le_sup
isOpen 📖	mathematical	—	IsOpen SetLike.coe TopologicalSpace.Opens instSetLike	—	is_open'
isOpenEmbedding' 📖	mathematical	—	Topology.IsOpenEmbedding TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype	—	IsOpen.isOpenEmbedding_subtypeVal isOpen
isOpenEmbedding_of_le 📖	mathematical	TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder instPartialOrder	Topology.IsOpenEmbedding Set.Elem SetLike.coe instSetLike instTopologicalSpaceSubtype Set Set.instMembership Set.inclusion Set.instHasSubset SetLike.coe_subset_coe instIsConcreteLE	—	SetLike.coe_subset_coe instIsConcreteLE Topology.IsEmbedding.inclusion Set.range_inclusion IsOpen.preimage continuous_subtype_val isOpen
is_open' 📖	mathematical	—	IsOpen carrier	—	—
mem_bot 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
mem_comap 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike DFunLike.coe FrameHom instCompleteLattice FrameHom.instFunLike comap ContinuousMap ContinuousMap.instFunLike	—	—
mem_iSup 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	SetLike.mem_coe coe_iSup
mem_inf 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	—
mem_interior 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike interior Set Set.instMembership interior	—	—
mem_mk 📖	mathematical	IsOpen	TopologicalSpace.Opens SetLike.instMembership instSetLike Set Set.instMembership	—	—
mem_sSup 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instMembership	—	sSup_eq_iSup
mem_sup 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	—
mem_top 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
mk_coe 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike isOpen	—	isOpen
mk_empty 📖	mathematical	—	Set Set.instEmptyCollection isOpen_empty Bot.bot TopologicalSpace.Opens OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	isOpen_empty
mk_inf_mk 📖	mathematical	IsOpen	TopologicalSpace.Opens SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra IsOpen.inter	—	—
mk_univ 📖	mathematical	—	Set.univ isOpen_univ Top.top TopologicalSpace.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	isOpen_univ
ne_bot_iff_nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe TopologicalSpace.Opens instSetLike	—	not_nonempty_iff_eq_bot
nonempty_coe 📖	mathematical	—	Set.Nonempty SetLike.coe TopologicalSpace.Opens instSetLike SetLike.instMembership	—	—
nonempty_coeSort 📖	mathematical	—	TopologicalSpace.Opens SetLike.instMembership instSetLike Set.Nonempty SetLike.coe	—	Set.nonempty_coe_sort
not_nonempty_iff_eq_bot 📖	mathematical	—	Set.Nonempty SetLike.coe TopologicalSpace.Opens instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra instFrame HeytingAlgebra.toOrderBot	—	coe_bot Set.not_nonempty_iff_eq_empty

TopologicalSpace.Opens.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finite_of_isCompact 📖	mathematical	TopologicalSpace.Opens.IsBasis IsCompact TopologicalSpace.Opens.carrier	Set TopologicalSpace.Opens Set.instHasSubset Set.Finite SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	—	TopologicalSpace.Opens.isBasis_iff_cover IsCompact.elim_finite_subcover TopologicalSpace.Opens.is_open' Set.iUnion_coe_set Set.iUnion_congr_Prop Set.instReflSubset subset_trans Set.instIsTransSubset Finset.coe_image Subtype.coe_preimage_self Finset.finite_toSet le_antisymm Set.iUnion_exists le_trans sSup_le_sSup Eq.ge
isCompact_open_iff_eq_finite_iUnion 📖	mathematical	TopologicalSpace.Opens.IsBasis Set.range TopologicalSpace.Opens IsCompact SetLike.coe TopologicalSpace.Opens.instSetLike	IsOpen Set.Finite Set.iUnion Set Set.instMembership	—	isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis Set.ext
le_iff 📖	mathematical	TopologicalSpace.Opens.IsBasis	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder IsOpen SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	TopologicalSpace.IsTopologicalBasis.eq_generateFrom
of_isInducing 📖	mathematical	TopologicalSpace.Opens.IsBasis Topology.IsInducing	setOf TopologicalSpace.Opens Set Set.instMembership Set.preimage SetLike.coe TopologicalSpace.Opens.instSetLike IsOpen.preimage Topology.IsInducing.continuous TopologicalSpace.Opens.carrier TopologicalSpace.Opens.is_open'	—	IsOpen.preimage Topology.IsInducing.continuous TopologicalSpace.Opens.is_open' Set.ext TopologicalSpace.IsTopologicalBasis.isInducing

---

← Back to Index