TheoremsSpec_essSurj, Spec_faithful, Spec_full, forgetToScheme_faithful, forgetToScheme_full, forgetToScheme_map, forgetToScheme_obj, forgetToScheme_preservesLimits, hasColimits, hasLimits, instIsEquivalenceOppositeCommRingCatOpRightOpΓ, instIsEquivalenceOppositeCommRingCatRightOpΓ, mk_obj, ΓIsEquiv, Γ_preservesLimits, affine, iff_of_isIso, of_isIso, SpecMap_appLE_fromSpec, SpecMap_appLE_fromSpec_assoc, Spec_basicOpen, Spec_map_appLE_fromSpec, Spec_map_appLE_fromSpec_assoc, algebraMap_Spec_obj, appLE_eq_away_map, app_basicOpen_eq_away_map, basicOpen, basicOpenSectionsToAffine_isIso, basicOpen_basicOpen_is_basicOpen, basicOpen_fromSpec_app, basicOpen_union_eq_self_iff, comap_primeIdealOf_appLE, exists_basicOpen_le, fromSpec_app_of_le, fromSpec_app_self, fromSpec_app_self_apply, fromSpec_image_basicOpen, fromSpec_image_zeroLocus, fromSpec_preimage_basicOpen, fromSpec_preimage_basicOpen', fromSpec_preimage_self, fromSpec_preimage_zeroLocus, fromSpec_primeIdealOf, fromSpec_toSpecΓ, fromSpec_toSpecΓ_assoc, fromSpec_top, iSup_basicOpen_eq_self_iff, ideal_ext_iff, ideal_le_iff, image_of_isOpenImmersion, instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, instIsAffineToSchemeBasicOpen, isCompact, isLocalization_basicOpen, isLocalization_of_eq_basicOpen, isLocalization_stalk, isLocalization_stalk', isOpenImmersion_fromSpec, isoSpec_hom, isoSpec_hom_appTop, isoSpec_hom_apply, isoSpec_hom_base_apply, isoSpec_inv, isoSpec_inv_appTop, isoSpec_inv_toSpecΓ, isoSpec_inv_toSpecΓ_assoc, isoSpec_inv_ι, isoSpec_inv_ι_assoc, map_fromSpec, map_fromSpec_assoc, mem_ideal_iff, opensRange_fromSpec, preimage_of_isIso, preimage_of_isOpenImmersion, primeIdealOf_eq_map_closedPoint, primeIdealOf_isMaximal_of_isClosed, range_fromSpec, self_le_basicOpen_union_iff, self_le_iSup_basicOpen_iff, stalkMap_injective, toSpecΓ_fromSpec, toSpecΓ_fromSpec_assoc, toSpecΓ_isoSpec_inv, toSpecΓ_isoSpec_inv_assoc, ΓSpecIso_hom_fromSpec_app, ι_basicOpen_preimage, affineOpensEquiv_apply_coe_coe, affineOpensEquiv_symm_apply_coe, isAffineOpen_iff_of_isOpenImmersion, liftQuotient_comp, liftQuotient_comp_assoc, toSpecΓ_SpecMap_appLE, toSpecΓ_SpecMap_appLE_assoc, toSpecΓ_SpecMap_map, toSpecΓ_SpecMap_map_assoc, toSpecΓ_SpecMap_presheaf_map, toSpecΓ_SpecMap_presheaf_map_assoc, toSpecΓ_SpecMap_presheaf_map_top, toSpecΓ_SpecMap_presheaf_map_top_assoc, toSpecΓ_appTop, toSpecΓ_appTop_assoc, toSpecΓ_naturality, toSpecΓ_naturality_assoc, toSpecΓ_preimage_basicOpen, toSpecΓ_preimage_zeroLocus, toSpecΓ_top, affineBasicOpen_coe, affineBasicOpen_le, compactSpace_of_isAffine, eq_zeroLocus_of_isClosed_of_isAffine, isAffine_affineBasisCover, isAffine_affineCover, isAffine_affineOpenCover, isBasis_affineOpens, isoSpec_Spec, isoSpec_Spec_hom, isoSpec_Spec_inv, isoSpec_hom, isoSpec_hom_naturality, isoSpec_hom_naturality_assoc, isoSpec_image_zeroLocus, isoSpec_inv_image_zeroLocus, isoSpec_inv_naturality, isoSpec_inv_naturality_assoc, isoSpec_inv_preimage_zeroLocus, isoSpec_inv_toSpecΓ, isoSpec_inv_toSpecΓ_assoc, localRingHom_comp_stalkIso, localRingHom_comp_stalkIso_apply, map_PrimeSpectrum_basicOpen_of_affine, toSpecΓ_image_zeroLocus, toSpecΓ_isoSpec_inv, toSpecΓ_isoSpec_inv_assoc, toSpecΓ_preimage_zeroLocus, zeroLocus_biInf, zeroLocus_biInf_of_nonempty, zeroLocus_iInf, zeroLocus_iInf_of_nonempty, zeroLocus_inf, algebraMap_stalkIso_inv, algebraMap_stalkIso_inv_assoc, germ_stalkMapIso_hom, germ_stalkMapIso_hom_assoc, affineOpensRestrict_apply_coe_coe, affineOpensRestrict_symm_apply_coe, eq_of_SpecMap_comp_eq_of_isAffineOpen, essImage_Spec, exists_basicOpen_le_affine_inter, exists_isAffineOpen_mem_and_subset, ext_of_isAffine, iSup_affineOpens_eq_top, iSup_basicOpen_of_span_eq_top, instIsAffineObjOppositeCommRingCatSchemeSpec, instIsAffineToSchemeValOpensMemSetAffineOpens, instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, instIsAffineXSchemeFiniteSubcover, instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, isAffineOpen_opensRange, isAffineOpen_top, isAffine_Spec, isAffine_affineScheme, isBasis_affine_open, isBasis_basicOpen, isLocalization_away_of_isAffine, of_affine_open_cover, preservesColimit_Γ, preservesLimit_rightOp_Γ, specTargetImageFactorization_app_injective, specTargetImageFactorization_comp, specTargetImageFactorization_comp_assoc, specTargetImageRingHom_surjective, stalkMap_injective_of_isAffine, Γ_restrict_isLocalization | 173 |