| Metric | Count |
DefinitionsScheme, toLRSHom, app, appLE, appTop, arrowStalkMapIsoOfEq, copyBase, homeomorph, stalkMap, toLRSHom, toLRSHom', SpecΓIdentity, algebra_section_section_basicOpen, arrowStalkMapIsoOfEq, basicOpen, delabAdjoinNotation, delabCoeFunAppNotation, delabCoeFunNotation, empty, forget, forgetToLocallyRingedSpace, forgetToTop, forgetToTop_obj_eq_coe, forget_obj_eq_coe, fullyFaithfulForgetToLocallyRingedSpace, hasCoeToTopCat, homeoOfIso, instCategory, instCoeFunHomForallCarrierCarrierCommRingCat, instCoeSortType, instEmptyCollection, instPreorderCarrierCarrierCommRingCat, instUniqueCarrierCarrierCommRingCatSpecOf, sheaf, toLocallyRingedSpace, zeroLocus, Γ, ΓSpecIso, map, «term_⁻¹ᵁ_», «termΓ(_,_)»»), schemeIsoToHomeo, «termSpec(_)»») | 43 |
TheoremsappLE_comp_appLE, appLE_comp_appLE_assoc, appLE_congr, appLE_eq_app, appLE_map, appLE_map', appLE_map'_assoc, appLE_map_assoc, app_eq, app_eq_appLE, coe_preimage, comp_app, comp_appLE, comp_appLE_assoc, comp_appTop, comp_appTop_assoc, comp_app_assoc, comp_apply, comp_base, comp_base_assoc, comp_preimage, comp_toLRSHom, comp_toLRSHom_assoc, congr_app, continuous, copyBase_eq, eqToHom_app, ext, ext', germ_stalkMap, germ_stalkMap_apply, germ_stalkMap_assoc, homeomorph_apply, iSup_preimage_eq_top, id_app, id_appTop, id_base, id_preimage, instIsIsoCommRingCatApp, instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, inv_app, inv_appTop, isIso_base, isIso_toLRSHom, isIso_toPshHom, map_appLE, map_appLE', map_appLE'_assoc, map_appLE_assoc, mem_preimage, naturality, naturality_assoc, preimage_basicOpen, preimage_basicOpen_top, preimage_bot, preimage_iSup, preimage_iSup_eq_top, preimage_inf, preimage_le_preimage_of_le, preimage_mono, preimage_sup, preimage_top, stalkMap_comp, stalkMap_congr, stalkMap_congr_assoc, stalkMap_congr_hom, stalkMap_congr_hom_assoc, stalkMap_congr_point, stalkMap_congr_point_assoc, stalkMap_hom_inv, stalkMap_hom_inv_apply, stalkMap_hom_inv_assoc, stalkMap_id, stalkMap_inv_hom, stalkMap_inv_hom_apply, stalkMap_inv_hom_assoc, stalkSpecializes_stalkMap, stalkSpecializes_stalkMap_apply, stalkSpecializes_stalkMap_assoc, SpecMap_presheaf_map_eqToHom, Spec_map, Spec_map_presheaf_map_eqToHom, Spec_obj, SpecΓIdentity_app, SpecΓIdentity_hom_app, SpecΓIdentity_inv_app, appLE_comp_appLE, app_eq, basicOpen_add_le, basicOpen_appLE, basicOpen_le, basicOpen_mul, basicOpen_of_isUnit, basicOpen_one, basicOpen_pow, basicOpen_res, basicOpen_res_eq, basicOpen_restrict, basicOpen_zero, codisjoint_zeroLocus, coe_homeoOfIso, coe_homeoOfIso_symm, comp_app, comp_appLE, comp_appLE_assoc, comp_appTop, comp_appTop_assoc, comp_app_assoc, comp_base, comp_base_apply, comp_base_assoc, comp_coeBase, comp_coeBase_assoc, comp_toLRSHom, comp_toLRSHom_assoc, congr_app, default_asIdeal, empty_carrier_carrier, empty_presheaf, eqToHom_c_app, forgetToLocallyRingedSpace_map, forgetToLocallyRingedSpace_obj, forgetToTop_map, forgetToTop_obj, forget_map, forget_obj, fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom, height_of_isClosed, hom_base_inv_base, hom_base_inv_base_assoc, hom_inv_apply, homeoOfIso_apply, homeoOfIso_symm, base, id_app, id_appTop, instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace, instFullLocallyRingedSpaceForgetToLocallyRingedSpace, instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, inv_app, inv_appTop, inv_base_hom_base, inv_base_hom_base_assoc, inv_hom_apply, isEmpty_of_commSq, iso_hom_base_inv_base, iso_hom_base_inv_base_apply, iso_inv_base_hom_base, iso_inv_base_hom_base_apply, le_iff_specializes, local_affine, mem_basicOpen, mem_basicOpen', mem_basicOpen'', mem_basicOpen_top, mem_zeroLocus_iff, preimage_basicOpen, preimage_basicOpen_top, preimage_comp, preimage_zeroLocus, presheaf_map_eqToHom_op, stalkMap_comp, stalkMap_congr, stalkMap_congr_assoc, stalkMap_congr_hom, stalkMap_congr_hom_assoc, stalkMap_congr_point, stalkMap_congr_point_assoc, stalkMap_germ, stalkMap_germ_apply, stalkMap_germ_assoc, stalkMap_hom_inv, stalkMap_hom_inv_apply, stalkMap_hom_inv_assoc, stalkMap_id, stalkMap_inv_hom, stalkMap_inv_hom_apply, stalkMap_inv_hom_assoc, stalkSpecializes_stalkMap, stalkSpecializes_stalkMap_apply, stalkSpecializes_stalkMap_assoc, toOpen_eq, zeroLocus_def, zeroLocus_empty_eq_univ, zeroLocus_iUnion, zeroLocus_isClosed, zeroLocus_map, zeroLocus_map_of_eq, zeroLocus_mono, zeroLocus_mul, zeroLocus_radical, zeroLocus_setMul, zeroLocus_singleton, zeroLocus_span, zeroLocus_univ, ΓSpecIso_inv, ΓSpecIso_inv_naturality, ΓSpecIso_inv_naturality_assoc, ΓSpecIso_naturality, ΓSpecIso_naturality_assoc, Γ_def, Γ_map, Γ_map_op, Γ_obj, Γ_obj_op, map_app, map_appLE, map_apply, map_base, map_base_apply, map_comp, map_comp_assoc, map_eqToHom, map_id, map_inv, SpecMap_preimage_basicOpen, Spec_carrier, Spec_closedPoint, Spec_presheaf, Spec_sheaf, Spec_toLocallyRingedSpace, Spec_zeroLocus, Spec_zeroLocus_eq_zeroLocus, basicOpen_eq_of_affine, basicOpen_eq_of_affine', germ_eq_zero_of_pow_mul_eq_zero, instIsIsoSchemeMapOfCommRingCat, instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier | 228 |
| Total | 271 |
| Name | Category | Theorems |
Scheme 📖 | CompData | 1351 mathmath: AffineSpace.not_isIntegralHom, Scheme.Hom.resLE_map_assoc, Surjective.instFstScheme, AffineSpace.map_Spec_map, Scheme.GlueData.oneHypercover_I₁, instIsStableUnderBaseChangeSchemeGeometricallyIrreducible, Scheme.coprodPresheafObjIso_hom_fst_assoc, Scheme.Hom.toPartialMap_hom, descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', Scheme.map_PrimeSpectrum_basicOpen_of_affine, Scheme.bot_mem_grothendieckTopology, Scheme.Modules.pseudofunctor_map_adj, Scheme.coverOfIsIso_I₀, IsImmersion.isStableUnderBaseChange, instLocallyQuasiFiniteSndScheme, Scheme.isoOfEq_inv, IsAffineOpen.isoSpec_inv_appTop, Spec.map_eq_id, AffineSpace.map_toSpecMvPoly_assoc, Scheme.AffineOpenCover.openCover_f, Scheme.Modules.pushforwardId_inv_app_app, IsClosedImmersion.instIsIsoSchemeToImage, AffineSpace.map_reindex, IsAffineOpen.map_fromSpec_assoc, Scheme.Pullback.Triplet.specTensorTo_fst, Scheme.Hom.opensRange_pullbackSnd, Scheme.Cover.pullbackCoverOver_X, IsProper.instCompScheme, Scheme.Cover.gluedCoverT'_snd_snd_assoc, instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, Scheme.Spec_map_stalkMap_fromSpecStalk, Scheme.Cover.LocallyDirected.directed, descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, Scheme.PartialMap.ext_iff, instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated, pointOfClosedPoint_comp_assoc, Scheme.isEmpty_pullback_iff, instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian, AffineSpace.isoOfIsAffine_inv, IsSeparated.isStableUnderBaseChange, Scheme.Hom.quasiFiniteLocus_comp, isCommMonObj_of_isProper_of_geometricallyIntegral, instIsAffinePullbackSchemeOfIsAffineHom_1, Scheme.IdealSheafData.glueDataObjHom_ι_assoc, instIsLocallyArtinianXScheme, opensCone_pt, Proj.basicOpenIsoSpec_inv_ι_assoc, coprodSpec_apply, RingHom.IsStableUnderBaseChange.pullback_fst_appTop, instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc, Scheme.AffineCover.cover_I₀, Scheme.Hom.toNormalization_normalizationPullback_fst, instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus, IsOpenImmersion.hasLimit_cospan_forget_of_right', instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec, Etale.instFstScheme, IsAffineOpen.map_fromSpec, ΓSpec.isIso_adjunction_counit, instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, injective_isStableUnderComposition, Scheme.affineBasisCover_is_basis, instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion, Scheme.Opens.toSpecΓ_naturality, instLocallyQuasiFiniteFstScheme, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, Scheme.Pullback.openCoverOfLeftRight_f, Scheme.comp_toLRSHom_assoc, Scheme.restrictFunctorΓ_inv_app, Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv, Scheme.mem_grothendieckTopology_iff, Scheme.Pullback.Triplet.ofPoint_x, Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology, universallyClosedTypeComp, quasiSeparated_comp, HasAffineProperty.affineAnd_le_affineAnd, Proj.fromOfGlobalSections_toSpecZero_assoc, Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AffineSpace.toSpecMvPolyIntEquiv_symm_apply, morphismRestrict_ι_assoc, Scheme.fromSpecStalk_toSpecΓ_assoc, Scheme.Modules.pushforwardCongr_hom_app_app, AffineSpace.SpecIso_hom_appTop, sourceLocalClosure.instIsMultiplicativeSchemeOfIsStableUnderBaseChange, IsSeparated.isClosedImmersion_diagonal, instIsAffineSigmaObjScheme, Scheme.zariskiTopology_le_etaleTopology, isIso_SpecMap_iff, Scheme.zariskiTopology_eq, Scheme.Cover.iUnion_range, IsDominant.respectsIso, QuasiCompactCover.instCoverOfIsIso, pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, Spec.map_surjective, IsProper.instFstScheme, IsAffineOpen.isCompact_pullback_inf, instFinitaryExtensiveScheme, pointsPi_surjective_of_isAffine, isOpenImmersion_isStableUnderComposition, Scheme.Cover.glued_cover_cocycle_fst, Scheme.instIsStableUnderCompositionQcPrecoverage, IsSeparated.instIsClosedImmersionMapDescScheme, sigmaOpenCover_X, GeometricallyIrreducible.comp, Scheme.Hom.iUnion_support_ker_openCover_map_comp, UniversallyOpen.instIsStableUnderBaseChangeScheme, diagonal_SpecMap, AffineTargetMorphismProperty.IsLocal.respectsIso, Scheme.inv_app, Scheme.Pullback.openCoverOfBase_I₀, Scheme.Hom.id_appTop, ι_right_coprodIsoSigma_inv, ι_sigmaSpec, Scheme.emptyTo_base, Scheme.Cover.instIsIsoFromGlued, Scheme.Hom.le_ker_comp, Spec.map_injective, coprodSpec_inr, IsOpenImmersion.comp_lift_assoc, IsProper.instSndScheme, Scheme.OpenCover.finiteSubcover_f, instIsIsoSchemeSigmaSpecOfFinite, Scheme.Spec_map_stalkSpecializes_fromSpecStalk, Scheme.Pullback.openCoverOfBase_f, HasRingHomProperty.comp_of_isOpenImmersion, Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, Scheme.Cover.pullbackCoverOver'_X, Scheme.stalkMap_congr_assoc, Scheme.Pullback.openCoverOfRight_I₀, Scheme.Opens.toSpecΓ_SpecMap_map, Scheme.isoSpec_inv_toSpecΓ, Scheme.Pullback.SpecTensorTo_SpecOfPoint, UniversallyInjective.iff_diagonal, instIsStableUnderCompositionSchemeSmooth, Scheme.hom_inv_apply, pointsPi_injective, Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom, Scheme.instHasPullbacksPrecoverageOfHasPullbacks, Scheme.ι_toIso_inv, instIsMultiplicativeSchemeQuasiCompact, Scheme.instIsOverFromSpecStalkOfMem, isPullback_opens_inf, Scheme.Cover.functorOfLocallyDirected_obj, Scheme.Hom.preimageIso_hom_ι_assoc, Scheme.isoOfEq_inv_ι, Scheme.openCoverOfIsOpenCover_I₀, instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, ExistsHomHomCompEqCompAux.h𝒰S, Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom, UniversallyOpen.instIsMultiplicativeScheme, HasAffineProperty.isStableUnderBaseChange, HasAffineProperty.affineAnd_isStableUnderBaseChange, Scheme.Cover.glued_cover_cocycle, Scheme.Pullback.instHasPullbacks, Scheme.IdealSheafData.glueDataObjHom_ι, Scheme.affineOpenCover_I₀, isImmersion_eq_inf, Scheme.Cover.gluedCover_t, Scheme.SpecΓIdentity_hom_app, locallyOfFiniteType_isStableUnderBaseChange, Scheme.preimage_comp, instIsZariskiLocalAtTargetMonomorphismsScheme, Scheme.Hom.stalkMap_congr_hom_assoc, Scheme.quasiCompactCover_shrink_iff, sourceLocalClosure.iff_forall_exists, Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, Scheme.forget_map, sigmaMk_mk, Scheme.Pullback.Triplet.specTensorTo_base_snd, Scheme.Hom.isOver_iff, Scheme.PartialMap.fromSpecStalkOfMem_compHom, affineAnd_respectsIso, descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, Scheme.isoSpec_inv_preimage_zeroLocus, Flat.instDescScheme, Scheme.Cover.pullbackCoverOver_I₀, instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant, AffineSpace.map_over_assoc, Scheme.IdealSheafData.inclusion_subschemeι_assoc, IsClosedImmersion.comp, Scheme.Modules.pseudofunctor_map_l, Scheme.instIsClosedImmersionιOfIsSeparated, Scheme.Cover.gluedCover_U, Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, IsSeparated.instIsClosedImmersionLiftSchemeId, Scheme.Pullback.tensorCongr_SpecTensorTo, IsSeparated.eq_valuativeCriterion, Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, instGeometricallyReducedSndScheme, instCoproductsOfShapeDisjointSchemeOfSmall, IsImmersion.comp, Scheme.Hom.toNormalization_fromNormalization_assoc, Flat.epi_of_flat_of_surjective, Scheme.forgetToTop_map, UniversallyOpen.out, IsClosedImmersion.eq_proper_inf_monomorphisms, Scheme.bot_mem_precoverage, IsImmersion.instιScheme, isSmooth_isStableUnderBaseChange, Scheme.coprodPresheafObjIso_hom_snd_assoc, AffineScheme.mk_obj, Scheme.isoSpec_hom, Scheme.ι_toIso_inv_assoc, Scheme.Hom.id_preimage, Scheme.Modules.pseudofunctor_right_unitality_assoc, Scheme.Hom.toImage_imageι, SpecToEquivOfLocalRing_apply_snd_coe, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, HasAffineProperty.diagonal_iff, Scheme.forget_obj, Scheme.eqToHom_c_app, instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated, AffineSpace.homOverEquiv_symm_apply_coe, Scheme.forgetToTop_obj, Scheme.affineOpenCover_idx, Scheme.Opens.isoOfLE_hom_ι_assoc, Scheme.Hom.fromNormalization_preimage, IsIntegralHom.instSndScheme, Scheme.toSpecΓ_naturality_assoc, Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, Scheme.Modules.pushforwardComp_inv_app_app, LocallyQuasiFinite.comp_iff, IsSchemeTheoreticallyDominant.pullbackSnd, IsFinite.comp_iff, HasRingHomProperty.respects_isOpenImmersion, Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, Scheme.Pullback.Triplet.specTensorTo_fst_assoc, Scheme.isoOfEq_hom_ι, IsAffineHom.comp_iff, AffineScheme.forgetToScheme_preservesLimits, HasRingHomProperty.containsIdentities, Scheme.presieve₀_mem_precoverage_iff, Scheme.comp_base, IsClosedImmersion.lift_fac_assoc, AffineSpace.isoOfIsAffine_inv_appTop_coord, AffineSpace.isoOfIsAffine_inv_over_assoc, isIso_iff_isIso_stalkMap, IsZariskiLocalAtSource.iff_of_iSup_eq_top, Scheme.isoSpec_hom_naturality, instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme, Scheme.homOfLE_ι, Scheme.toSpecΓ_isoSpec_inv_assoc, Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, IsOpenImmersion.range_pullbackSnd, Scheme.Hom.resLE_map, Scheme.Cover.mkOfCovers_I₀, Scheme.Hom.comp_app, IsIntegralHom.instIsStableUnderCompositionScheme, IsSeparated.isSeparated_eq_diagonal_isClosedImmersion, Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, Scheme.Pullback.left_affine_comp_pullback_hasPullback, Scheme.hom_base_inv_base, HasAffineProperty.affineAnd_isStableUnderComposition, IsLocalAtSource.iff_of_openCover, Scheme.GlueData.instHasMulticoequalizerDiagram, Scheme.forgetToLocallyRingedSpace_map, IsOpenImmersion.range_pullback_fst_of_right, Scheme.toSpecΓ_naturality, IsSeparated.diagonal_isClosedImmersion, pointEquivClosedPoint_apply_coe, instIsStableUnderBaseChangeSchemeLocallyQuasiFinite, Scheme.Hom.ι_toNormalization, geometrically_eq_universally, instGeometricallyIntegralSndScheme, Spec.faithful, Spec.preimage_id, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, Scheme.homeoOfIso_symm, Scheme.Cover.ColimitGluingData.transitionCocone_pt, Scheme.comp_coeBase_assoc, instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, Surjective.instIsStableUnderBaseChangeScheme, IsLocalIso.le_of_isZariskiLocalAtSource, IsFinite.instIsStableUnderBaseChangeScheme, IsProper.isStableUnderBaseChange, quasiSeparated_eq_diagonal_is_quasiCompact, IsOpenImmersion.hasLimit_cospan_forget_of_left, Scheme.IdealSheafData.inclusion_subschemeι, coprodMk_inl, IsClosedImmersion.respectsIso, Scheme.Opens.toSpecΓ_naturality_assoc, Scheme.GlueData.openCover_f, instSmoothOfRelativeDimensionOfNatNatCompScheme, Scheme.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, IsAffineOpen.isoSpec_inv, instIsMultiplicativeSchemeSurjective, Scheme.Hom.id_app, Scheme.Γ_obj, Scheme.Opens.fromSpecStalkOfMem_ι_assoc, instIsAffineXSchemeAffineCover, Scheme.kerAdjunction_unit_app, Scheme.Hom.liftQuotient_comp, Scheme.Pullback.carrierEquiv_symm_fst, instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, Scheme.Cover.ColimitGluingData.transitionMap_id, Proj.pullbackAwayιIso_inv_snd_assoc, Scheme.Hom.asFiberHom_fiberι_assoc, instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, instIsAffineHomDescScheme, Scheme.IdealSheafData.comapIso_hom_snd_assoc, Scheme.Hom.cover_X, Scheme.directedAffineCover_f, IsImmersion.isPullback_toImage_liftCoborder, Flat.instFstScheme, instIsOverTerminalScheme, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Scheme.IdealSheafData.comap_id, Scheme.Pullback.range_fst_comp, instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, ΓSpec.adjunction_counit_app', quasiCompact_isStableUnderBaseChange, Proj.SpecMap_awayMap_awayι_assoc, Scheme.isoSpec_hom_naturality_assoc, pullbackSpecIso_inv_snd, IsImmersion.instMapDescScheme, Scheme.isoSpec_inv_image_zeroLocus, Scheme.IdealSheafData.range_glueDataObjι_ι, instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall, HasAffineProperty.affineAnd_eq_of_propertyIsLocal, quasiCompact_comp, SurjectiveOnStalks.mono_of_injective, Etale.instSndScheme, Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, IsOpenImmersion.isIso, Scheme.Cover.gluedCover_V, Proj.pullbackAwayιIso_inv_fst, isIso_morphismRestrict_iff_isIso_app, Scheme.hom_base_inv_base_assoc, isPullback_inl_inl_coprodMap, IsFinite.eq_proper_inf_locallyQuasiFinite, SpecMap_ΓSpecIso_inv_toSpecΓ, AffineSpace.map_comp, Scheme.over_def, Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, IsOpenImmersion.instπWalkingCospanSchemeCospanOne, Proj.basicOpenToSpec_SpecMap_awayMap, Scheme.Cover.coconeOfLocallyDirected_ι, Flat.instIsMultiplicativeScheme, Scheme.Cover.ι_fromGlued_assoc, universallyInjective_iff, instHasFiniteLimitsScheme, Scheme.GlueData.glue_condition, Scheme.GlueData.f_open, Scheme.OpenCover.isOpenCover_opensRange, pullbackRestrictIsoRestrict_inv_fst, Scheme.Cover.ulift_X, Scheme.openCoverOfIsOpenCover_f, instIsAffineCoprodScheme, Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.id_appTop, Scheme.Cover.gluedCoverT'_fst_fst, pullbackSpecIso_hom_base, Scheme.Cover.covers, IsOpenImmersion.comp, smooth_comp, ValuativeCriterion.Existence.eq, Scheme.isCommMonObj_asOver_pullback, QuasiCompactCover.exists_hom, Scheme.GlueData.isOpen_iff, Surjective.sigmaDesc_of_union_range_eq_univ, QuasiCompactCover.isCompactOpenCovered_of_isCompact, Scheme.fromSpecStalk_toSpecΓ, IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, instRespectsIsoSchemeTopologicallyIsOpenEmbedding, Scheme.isMonHom_fst_id_right, IsLocalIso.eq_iInf, ValuativeCriterion.Existence.stableUnderBaseChange, Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated, Etale.instIsMultiplicativeScheme, isInitial_iff_isEmpty, AffineSpace.reindex_over, Scheme.IdealSheafData.subschemeCover_map_subschemeι, Scheme.Cover.gluedCoverT'_snd_fst, AffineSpace.map_over, Scheme.isAffine_affineBasisCover, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, topologically_iso_le, Scheme.Cover.trans_id, sourceLocalClosure.property_coverMap_comp, Scheme.Cover.exists_lift_trans_eq, Scheme.Hom.toImage_imageι_assoc, instIsStableUnderCompositionSchemeLocallyQuasiFinite, QuasiSeparated.diagonalQuasiCompact, Scheme.GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, ΓSpec.adjunction_counit_app, instRespectsIsoSchemeTopologicallyIsClosedEmbedding, instGeometricallyReducedFstScheme, Scheme.Hom.preimage_smoothLocus_eq, Scheme.coe_homeoOfIso_symm, Spec.map_id, instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, Scheme.stalkMap_hom_inv_assoc, universallyInjective_eq, instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty, Proj.basicOpenIsoSpec_inv_ι, Scheme.id.base, Scheme.Γ_def, Scheme.Hom.isoOpensRange_hom_ι_assoc, instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact, Spec.full, Scheme.Pullback.Triplet.specTensorTo_snd, Scheme.directedAffineCover_I₀, opensDiagram_map, Scheme.Hom.isoOpensRange_hom_ι, instHasOfPrecompPropertySchemeSurjective, morphismRestrict_ι, Scheme.Modules.restrictFunctorComp_hom_app_app, Scheme.Hom.preimageIso_inv_ι, Scheme.SpecMap_stalkSpecializes_fromSpecStalk, Scheme.descResidueField_fromSpecResidueField, Scheme.Cover.RelativeGluingData.equifibered, Spec.map_preimage_unop, Scheme.IdealSheafData.map_comp, instIsClosedImmersionSndScheme, Scheme.Modules.restrictFunctorComp_inv_app_app, Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, IsOpenImmersion.isPullback_lift_id, IsLocalIso.le_of_isLocalAtSource, Proj.pullbackAwayιIso_inv_snd, Scheme.SpecΓIdentity_app, Proj.pullbackAwayιIso_inv_fst_assoc, Scheme.IdealSheafData.inclusion_comp_assoc, Scheme.homeoOfIso_apply, pullbackSpecIso_inv_fst'_assoc, affineLocally_respectsIso, IsZariskiLocalAtSource.sigmaDesc, ExistsHomHomCompEqCompAux.h𝒰X, isIso_stalkMap_coprodSpec, Proj.pullbackAwayιIso_hom_awayι, instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite, isOpenImmersion_stableUnderBaseChange, Scheme.Opens.toSpecΓ_SpecMap_map_assoc, hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict, IsImmersion.instDiagonalScheme, Scheme.IdealSheafData.ker_fst_of_isClosedImmersion, Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, specializingMap_respectsIso, Scheme.OpenCover.restrict_f, Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, sourceLocalClosure.instRespectsIsoScheme, Scheme.OpenCover.iSup_opensRange, Scheme.GlueData.ι_isOpenImmersion, Scheme.Pullback.Triplet.specTensorTo_snd_assoc, Scheme.Cover.mkOfCovers_X, IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, IsOpenImmersion.hasLimit_cospan_forget_of_right, universallyClosed_isStableUnderBaseChange, Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc, FormallyUnramified.isOpenImmersion_diagonal, AffineTargetMorphismProperty.arrow_mk_iso_iff, smooth_isStableUnderBaseChange, IsFinite.instCompScheme, Scheme.kerAdjunction_counit_app, opensDiagramι_app, Scheme.Pullback.carrierEquiv_symm_snd, IsClosedImmersion.comp_iff, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization, isCompl_range_inl_inr, UniversallyClosed.out, universallyClosed_isStableUnderComposition, Scheme.pretopology_le_inf, ΓSpec.adjunction_unit_app, Scheme.Opens.toSpecΓ_top, universally_isLocalAtTarget, HasRingHomProperty.stableUnderComposition, HasRingHomProperty.isMultiplicative, Scheme.Pullback.openCoverOfRight_f, SurjectiveOnStalks.isEmbedding_pullback, AffineSpace.SpecIso_inv_appTop_coord, IsOpenImmersion.to_iso, AffineSpace.functor_obj_map, AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite, instSurjectiveCompScheme, Scheme.Hom.iInf_ker_openCover_map_comp, Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, specTargetImageFactorization_comp_assoc, instIsIsoSchemeMorphismRestrict, AffineSpace.map_reindex_assoc, instGeometricallyIrreducibleSndScheme, instIsMultiplicativeSchemeQuasiSeparated, IsLocalAtSource.comp, instRespectsIsoSchemeSurjective, instSubsingletonOverTerminalScheme, Scheme.AffineCover.cover_f, instIsOpenImmersionInrScheme, instHasInitialScheme, IsLocalIso.instIsStableUnderBaseChangeScheme, SurjectiveOnStalks.comp, Scheme.Cover.gluedCover_J, Scheme.stalkMap_congr_hom_assoc, Scheme.Hom.opensRange_pullbackFst, Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, pullbackRestrictIsoRestrict_hom_ι_assoc, Scheme.Cover.sigmaFunctor_obj, compactSpace_iff_quasiCompact, Scheme.mem_overGrothendieckTopology, UniversallyOpen.snd, Scheme.Modules.pseudofunctor_right_unitality, Scheme.Modules.pseudofunctor_mapComp_hom_τl, sourceLocalClosure.instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange, IsAffineOpen.isoSpec_inv_toSpecΓ, disjoint_opensRange_sigmaι, Scheme.comp_base_assoc, Scheme.stalkMap_id, isIso_iff_isOpenImmersion_and_surjective, IsAffineOpen.toSpecΓ_isoSpec_inv, AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty, Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map, quasiCompact_isStableUnderComposition, Scheme.Hom.comp_app_assoc, Scheme.comp_app, instIsStableUnderCompositionSchemeLocallyOfFinitePresentation, isIso_iff_isOpenImmersion, isOpenImmersion_isMultiplicative, AffineSpace.homOfVector_toSpecMvPoly_assoc, Scheme.Cover.glued_cover_cocycle_snd, Scheme.Hom.normalizationPullback_snd_assoc, Scheme.GlueData.ι_eq_iff, Scheme.Cover.trans_map, AffineSpace.comp_homOfVector, Scheme.openCoverOfIsOpenCover_X, ι_left_coprodIsoSigma_inv, instHasStrictInitialObjectsScheme, AffineSpace.isOpenMap_over, instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType_1, Scheme.isoSpec_inv_naturality_assoc, Spec.map_comp_assoc, IsImmersion.isImmersion_iff_exists, Scheme.homOfLE_homOfLE_assoc, IsLocalAtSource.respectsLeft_isOpenImmersion, instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec, isLocalIso_iff, Spec.preimage_comp_assoc, Scheme.Cover.toSigma_s₀, IsClosedImmersion.lift_fac, AffineSpace.hom_ext_iff, Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated, Scheme.singleton_mem_precoverage_iff, Scheme.IdealSheafData.glueDataObjMap_glueDataObjι_assoc, QuasiCompactCover.inst, Scheme.Pullback.tensorCongr_SpecTensorTo_assoc, QuasiCompactCover.instPullback₁Scheme, Scheme.isoSpec_Spec_hom, AffineScheme.forgetToScheme_full, Scheme.IdealSheafData.comapIso_inv_subschemeι_assoc, IsZariskiLocalAtTarget.coprodMap, IsFinite.instDescScheme, AffineSpace.map_toSpecMvPoly, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, instHasFiniteCoproductsScheme, AffineSpace.isPullback_map, Scheme.Hom.inl_normalizationCoprodIso_hom_fromNormalization_assoc, instIsMultiplicativeSchemeUniversallyInjective, nonempty_isColimit_cofanMk_of, AffineScheme.forgetToScheme_faithful, instQuasiCompactSndScheme, pullbackSpecIso_inv_fst, IsLocalAtTarget.descendsAlong, UniversallyInjective.respectsIso, HasAffineProperty.coprodDesc_affineAnd, IsFinite.instFstScheme, Scheme.Pullback.affine_affine_hasPullback, Scheme.grothendieckTopology_eq_inf, AffineSpace.homOfVector_over_assoc, stalkwise_respectsIso, Scheme.GlueData.openCover_X, morphismRestrict_comp, Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc, Scheme.isPullback_toSpecΓ_toSpecΓ, Scheme.Cover.LocallyDirected.trans_comp, Scheme.Hom.stalkMap_hom_inv, instIsMultiplicativeSchemeLocallyOfFiniteType, Scheme.restrictFunctorΓ_hom_app, Scheme.Cover.functorOfLocallyDirected_map, Scheme.stalkMap_congr_hom, Scheme.Modules.pseudofunctor_mapComp_hom_τr, Scheme.Γ_map_op, Scheme.Pullback.range_snd_comp, Scheme.directedAffineCover_X, Scheme.Cover.property_trans, instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, Scheme.Modules.restrictFunctorId_inv_app_app, Scheme.Opens.isoOfLE_hom_ι, IsClosedImmersion.isStableUnderBaseChange, Scheme.Opens.over_def, Scheme.Opens.fromSpecStalkOfMem_ι, Scheme.Modules.pushforwardComp_hom_app_app, Scheme.iso_inv_base_hom_base, Scheme.Hom.inl_normalizationCoprodIso_hom_fromNormalization, Scheme.toSpecΓ_isoSpec_inv, SpecToEquivOfLocalRing_apply_fst, Scheme.Hom.comp_apply, Scheme.Cover.sigma_X, Scheme.homOfLE_homOfLE, Proj.awayι_toSpecZero, opensDiagram_obj, Scheme.Cover.nonempty_of_nonempty, Scheme.instSmallPrecoverage, IsProper.stableUnderComposition, Scheme.toIso_inv_ι_assoc, Scheme.instFullOppositeIdealSheafDataOverSubschemeFunctor, isPullback_SpecMap_of_isPushout, instIsOpenImmersionMapScheme, Scheme.Hom.cover_f, Scheme.presieve₀_mem_qcPrecoverage_iff, sigmaι_eq_iff, opensCone_π_app, Scheme.Hom.resLE_id, isOpenImmersion_respectsIso, Scheme.isClosedUnderIsomorphisms_quasiCompactCover, Scheme.stalkMap_comp, Scheme.AffineZariskiSite.directedCover_X, IsPreimmersion.instMonoScheme, Scheme.Cover.ulift_f, Scheme.IdealSheafData.comapIso_inv_subschemeι, UniversallyOpen.fst, instIsRightAdjointCommRingCatOppositeSchemeΓ, Scheme.OpenCover.instIsOpenImmersionTrans, Scheme.IdealSheafData.glueDataObjMap_glueDataObjι, Scheme.Hom.comp_appIso, isIso_of_isEmpty, instIsStableUnderBaseChangeSchemeGeometricallyIntegral, IsOpenImmersion.range_pullback_to_base_of_left, instSurjectiveDescI₀SchemeF, over_def, IsIntegralHom.instFstScheme, Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc, Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, instLocallyOfFinitePresentationFstScheme, Scheme.Hom.stalkMap_inv_hom_assoc, isAffineHom_isStableUnderBaseChange, Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc, Scheme.IdealSheafData.inclusion_comp, Scheme.Γ_map, Scheme.Cover.pullbackCoverOver'_I₀, AffineScheme.forgetToScheme_map, Scheme.Cover.ulift_I₀, IsIntegralHom.instIsMultiplicativeScheme_1, isSeparated_iff, Proj.awayι_toSpecZero_assoc, Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization_assoc, HasRingHomProperty.inf, IsClosedImmersion.instIsMultiplicativeScheme, IsOpenImmersion.lift_fac_assoc, instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1, ValuativeCommSq.commSq, Scheme.residueFieldCongr_fromSpecResidueField, universallyInjective_eq_diagonal, Scheme.coprodPresheafObjIso_hom_snd, IsOpenImmersion.instHasOfPostcompPropertyScheme, coprodSpec_coprodMk, Scheme.instIsStableUnderBaseChangeJointlySurjectivePrecoverage, isAffine_affineScheme, Scheme.Hom.preimageIso_hom_ι, IsClosedImmersion.iff_isFinite_and_mono, Scheme.Cover.sigmaFunctor_map, UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMap, Scheme.isoOfEq_hom_ι_assoc, isIso_iff_isOpenImmersion_and_epi_base, instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion, Scheme.isoSpec_inv_naturality, IsAffineOpen.toSpecΓ_fromSpec_assoc, Scheme.Hom.ker_comp_of_isIso, Scheme.Pullback.openCoverOfRight_X, instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion, Scheme.Hom.id_appIso, Scheme.isoOfEq_inv_ι_assoc, Scheme.Hom.preimageIso_inv_ι_assoc, instQuasiSeparatedSndScheme, Scheme.Modules.pseudofunctor_mapId_hom_τr, Scheme.Cover.gluedCoverT'_snd_fst_assoc, Scheme.Hom.asFiberHom_fiberι, Scheme.IdealSheafData.subschemeFunctor_obj, specTargetImageFactorization_comp, Scheme.comp_appTop_assoc, universallyInjective_isStableUnderComposition, instHasColimitsOfShapeDiscreteSchemeOfSmall, IsFinite.instSndScheme, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, Scheme.Hom.resLE_comp_resLE_assoc, IsZariskiLocalAtSource.respectsLeft_isOpenImmersion, Scheme.AffineZariskiSite.directedCover_f, IsImmersion.instIsMultiplicativeScheme, instIsAffineObjOppositeCommRingCatSchemeSpec, AffineSpace.reindex_comp, AffineSpace.map_SpecMap, emptyIsInitial_to, instLocallyOfFiniteTypeSndScheme, Scheme.isoSpec_Spec, Scheme.GlueData.oneHypercover_p₂, instGeometricallyIntegralFstScheme, isOpenImmersion_eq_inf, Scheme.Pullback.Triplet.specTensorTo_base_fst, Surjective.comp_iff, instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall, Proj.fromOfGlobalSections_toSpecZero, Scheme.iso_hom_base_inv_base, AffineSpace.SpecIso_inv_over_assoc, sourceLocalClosure.instContainsIdentitiesScheme, AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass, sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange, Scheme.stalkMap_hom_inv, IsClosedImmersion.eq_inf, sourceAffineLocally_respectsIso, Scheme.monObjAsOverPullback_mul, isClosedMap_isStableUnderComposition, HasAffineProperty.instRespectsIsoScheme, toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, instHasTerminalScheme, Scheme.Modules.pseudofunctor_obj_obj, IsClosedImmersion.isIso_lift, targetAffineLocally_affineAnd_eq_affineLocally, Scheme.Hom.comp_preimage, Scheme.kerFunctor_map, IsZariskiLocalAtSource.iff_of_openCover, Scheme.stalkMap_hom_inv_apply, AffineSpace.reindex_comp_assoc, Scheme.Hom.iInf_ker_openCover_map_comp_apply, Surjective.instSndScheme, Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization, pullbackSpecIso_inv_snd_assoc, AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass, Scheme.Cover.pushforwardIso_f, Scheme.isoOfEq_rfl, Scheme.inv_appTop, isPullback_Spec_map_pushout, IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated, Scheme.Hom.quasiFiniteAt_iff, IsProper.comp_iff, instIsOpenImmersionInlScheme, universallyClosed_fst, Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc, instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType, Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AffineTargetMorphismProperty.cancel_right_of_respectsIso, Scheme.fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom, IsOpenImmersion.hasPullback_of_right, Scheme.instIsOverFstOverInferInstanceOverClassId, IsImmersion.instFstScheme, AffineSpace.toSpecMvPolyIntEquiv_apply, Scheme.Cover.pullbackCoverOver_f, Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, Scheme.Pullback.openCoverOfBase_X, isOpenImmersion_sigmaDesc, IsOpenImmersion.isoOfRangeEq_hom_fac, coprodSpec_inr_assoc, Scheme.instIsStableUnderSupQcPrecoverage, AffineSpace.functor_obj_obj, IsClosedImmersion.Spec_iff, Scheme.Cover.toPresieveOver_le_arrows_iff, isPreimmersion_eq_inf, Scheme.Hom.comp_toLRSHom, AffineSpace.map_id, Scheme.Pullback.openCoverOfBase'_f, instIsOpenImmersionMapWalkingSpanSchemeSpan, AffineSpace.isIntegralHom_over_iff_isEmpty, pullbackSpecIso_inv_fst_assoc, Scheme.Pullback.ofPointTensor_SpecTensorTo, Scheme.Hom.id_base, AffineSpace.functor_map_app, UniversallyOpen.eq, IsOpenImmersion.range_pullback_snd_of_left, instIsMultiplicativeSchemeLocallyQuasiFinite, Scheme.instIsIsoSubschemeιBotIdealSheafData, Scheme.Cover.gluedCover_f, isProper_eq, ΓSpec.adjunction_homEquiv_apply, UniversallyOpen.universally_isOpenMap, Scheme.PartialMap.isOver_iff_eq_restrict, Scheme.Opens.isoOfLE_inv_ι, Scheme.Hom.ι_toNormalization_assoc, instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, Flat.comp, Scheme.Cover.Hom.sigma_h₀, Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, Scheme.isoSpec_inv_toSpecΓ_assoc, Proj.fromOfGlobalSections_morphismRestrict, Scheme.Cover.LocallyDirected.trans_id, Scheme.Hom.isoImage_inv_ι, AffineSpace.map_comp_assoc, Scheme.isSeparated_iff_isClosedImmersion_prod_lift, Scheme.GlueData.ι_isoCarrier_inv, IsFinite.instIsMultiplicativeScheme, Scheme.Cover.toSigma_h₀, universallyOpen_iff, Scheme.IdealSheafData.range_glueDataObjι, Scheme.Hom.isoImage_inv_ι_assoc, locallyOfFinitePresentation_isStableUnderBaseChange, Scheme.Modules.pushforwardId_hom_app_app, pullbackRestrictIsoRestrict_hom_ι, Scheme.Hom.ker_comp, Scheme.coprodPresheafObjIso_hom_fst, ExistsHomHomCompEqCompAux.ha, IsOpenImmersion.range_pullback_to_base_of_right, Scheme.IdealSheafData.comapIso_hom_snd, UniversallyClosed.universally_isClosedMap, IsLocalAtTarget.iff_of_openCover, Scheme.instHasIsosQcPrecoverage, smoothOfRelativeDimension_comp, Scheme.directedAffineCover_trans, instIsStableUnderCompositionSchemeLocallyOfFiniteType, instQuasiCompactFstScheme, Scheme.coverOfIsIso_X, isCompl_opensRange_inl_inr, universallyClosed_eq_universallySpecializing, Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, IsLocalIso.instIsMultiplicativeScheme, IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1, Scheme.Cover.LocallyDirected.property_trans, instHasOfPostcompPropertySchemeIsProperIsSeparated, instIsOpenImmersionSigmaSpec, topologically_respectsIso, ExistsHomHomCompEqCompAux.hab, Proj.basicOpenToSpec_SpecMap_awayMap_assoc, toSpecΓ_SpecMap_ΓSpecIso_inv, HasRingHomProperty.isStableUnderBaseChange, AffineSpace.homOfVector_over, Scheme.Hom.inv_appTop, Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, Scheme.PartialMap.restrict_hom, FormallyUnramified.instIsMultiplicativeScheme, Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, Scheme.Cover.ColimitGluingData.prop_trans, Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc, Scheme.qcCoverFamily_property, IsProper.instIsMultiplicativeScheme, pullbackSpecIso_hom_fst, IsProper.eq_valuativeCriterion, Scheme.Pullback.base_affine_hasPullback, locallyOfFinitePresentation_comp, Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition, IsClosedImmersion.eq_isFinite_inf_mono, quasiSeparated_iff, AffineSpace.reindex_over_assoc, Scheme.IdealSheafData.comapIso_hom_fst_assoc, Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop, QuasiCompactCover.instSumScheme_1, IsSeparated.stableUnderComposition, instIsAffineTerminalScheme, Spec.map_comp, Scheme.AffineZariskiSite.PreservesLocalization.isLocallyDirected, instIsStableUnderBaseChangeSchemeGeometrically, isIso_of_isClosedImmersion_of_surjective, instIsMultiplicativeSchemeUniversallyClosed, Scheme.Cover.gluedCoverT'_fst_snd_assoc, instIsOpenImmersionAppOverSchemeOpensDiagramι, Scheme.Pullback.range_snd, Scheme.Hom.stalkMap_comp, Scheme.SpecΓIdentity_inv_app, Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, Scheme.Cover.coconeOfLocallyDirected_pt, instLocallyOfFinitePresentationSndScheme, UniversallyClosed.eq_valuativeCriterion, Scheme.Cover.exists_eq, Scheme.ofArrows_mem_precoverage_iff, isClosedImmersion_equalizer_ι_left, Scheme.Cover.ColimitGluingData.trans_app_left, instRespectsIsoSchemeTopologicallyInjective, IsSeparated.instCompScheme, FormallyUnramified.instIsStableUnderBaseChangeScheme, Spec.homEquiv_apply, Scheme.AffineCover.cover_X, instLocallyOfFiniteTypeFstScheme, Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology, AffineSpace.isoOfIsAffine_hom_appTop, Etale.etale_isStableUnderBaseChange, coprodSpec_inl_assoc, Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, Proj.pullbackAwayιIso_hom_awayι_assoc, Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, Scheme.isoSpec_Spec_inv, Spec.map_eqToHom, Scheme.affineBasisCover_obj, Scheme.Hom.comp_toLRSHom_assoc, Scheme.Cover.ColimitGluingData.transitionMap_comp, sigmaOpenCover_I₀, Scheme.Cover.Hom.sigma_s₀, isomorphisms_eq_isOpenImmersion_inf_surjective, Scheme.topIso_hom, instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec, Scheme.Hom.map_resLE, Scheme.Cover.sigma_I₀, Scheme.instEtaleF, IsPreimmersion.instSndScheme, Scheme.isSeparated_iff, Scheme.inv_hom_apply, Proj.SpecMap_awayMap_awayι, basicOpenIsoSpecAway_inv_homOfLE_assoc, SurjectiveOnStalks.instIsMultiplicativeScheme, IsClosedImmersion.iff_isProper_and_mono, Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange, Scheme.Cover.pushforwardIso_I₀, sourceLocalClosure.instIsStableUnderBaseChangeScheme, Scheme.comp_toLRSHom, ι_sigmaSpec_assoc, instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc, isPullback_morphismRestrict, instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, isPullback_inr_inr_coprodMap, Scheme.OpenCover.finiteSubcover_X, instIsAffineHomCompScheme, Scheme.Pullback.range_fst, IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, instIsMultiplicativeSchemeIsDominant, instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, instRespectsIsoSchemeTargetAffineLocallyOfToProperty, AffineSpace.isoOfIsAffine_hom, instIsClosedImmersionFstScheme, AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget, Scheme.Hom.resLE_comp_ι_assoc, smoothOfRelativeDimension_isStableUnderBaseChange, geometrically_inf, Scheme.Hom.ι_fromNormalization_assoc, Scheme.Cover.trans_comp, instMonoCoprodScheme, Scheme.emptyTo_c_app, Scheme.stalkMap_inv_hom_apply, basicOpenIsoSpecAway_inv_homOfLE, Scheme.Hom.map_resLE_assoc, IsLocalIso.exists_isOpenImmersion, Scheme.Hom.comp_base_assoc, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, coprodSpec_inl, Scheme.GlueData.oneHypercover_X, IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty, Scheme.IdealSheafData.subSchemeCover_map_inclusion, Scheme.Modules.conjugateEquiv_pullbackId_hom, QuasiCompactCover.singleton, Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, ΓSpec.adjunction_homEquiv_symm_apply, Scheme.Pullback.openCoverOfLeftRight_I₀, IsAffineOpen.isoSpec_hom_apply, Scheme.Modules.conjugateEquiv_pullbackComp_inv, Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology, IsFinite.eq_isProper_inf_isAffineHom, quasiSeparatedSpace_iff_quasiSeparated, Scheme.Hom.resLE_comp_ι, Scheme.Hom.liftCoborder_ι_assoc, targetAffineLocally_affineAnd_le, IsAffine.affine, Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, Scheme.IdealSheafData.inclusion_id_assoc, instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat, Etale.instHasOfPostcompPropertyScheme, Scheme.Pullback.Triplet.ofPoint_s, QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, Scheme.coverOfIsIso_f, Spec.map_inv, Scheme.Pullback.instHasPullback, Scheme.Modules.pseudofunctor_left_unitality, Scheme.Hom.isoOpensRange_inv_comp_assoc, Scheme.Modules.pseudofunctor_associativity_assoc, Scheme.instHasPullbacksIsOpenImmersion, Scheme.Hom.cover_I₀, pullbackSpecIso_hom_base_assoc, IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, Scheme.Cover.gluedCoverT'_snd_snd, universally_isZariskiLocalAtSource, instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, isPullback_SpecMap_pushout, Scheme.Opens.instIsOverι, Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc, Scheme.IdealSheafData.comapIso_hom_fst, AffineSpace.homOverEquiv_apply, pullbackRestrictIsoRestrict_inv_fst_assoc, Scheme.GlueData.ι_isoLocallyRingedSpace_inv, Scheme.IdealSheafData.map_id, Scheme.iso_inv_base_hom_base_apply, Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, Scheme.Hom.asFiberHom_fiberToSpecResidueField, Scheme.Modules.pseudofunctor_mapComp_inv_τl, locallyOfFiniteType_comp, Scheme.Pullback.Triplet.exists_preimage, Scheme.comp_appTop, Scheme.Hom.stalkMap_hom_inv_apply, IsZariskiLocalAtTarget.iff_of_openCover, instIsLocallyNoetherianXScheme, sigmaOpenCover_f, topologically_isStableUnderComposition, AffineSpace.over_over, Scheme.stalkMap_inv_hom, Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage, Etale.etale_comp, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, isLocallyArtinian_iff_openCover, Scheme.comp_base_apply, SpecMap_residueFieldIsoBase_inv, Scheme.AffineOpenCover.openCover_I₀, Scheme.PartialMap.isOver_iff, AffineSpace.toSpecMvPolyIntEquiv_comp, SpecMap_residueFieldIsoBase_inv_assoc, IsAffineOpen.isoSpec_hom_base_apply, Scheme.Hom.toNormalization_normalizationPullback_fst_assoc, AffineSpace.homOfVector_toSpecMvPoly, Scheme.OpenCover.restrict_I₀, QuasiSeparated.quasiCompact_diagonal, Proj.basicOpenIsoSpec_hom, pullbackSpecIso_hom_fst'_assoc, Scheme.Pullback.openCoverOfLeft_I₀, Scheme.GlueData.glue_condition_assoc, isIso_iff_stalk_iso, Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, Scheme.AffineZariskiSite.cocone_ι_app, geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms, IsAffineOpen.SpecMap_appLE_fromSpec_assoc, Scheme.forgetToLocallyRingedSpace_obj, QuasiCompactCover.homCover, instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat, IsAffineOpen.fromSpec_top, IsSchemeTheoreticallyDominant.pullbackFst, SpecToEquivOfLocalRing_symm_apply, Scheme.Hom.stalkMap_congr, Scheme.instIsOpenImmersionF, Flat.isIso_of_surjective_of_mono, Scheme.instFullEtaleOverForget, Scheme.affineOpenCover_f, pullbackSpecIso_inv_fst', Scheme.Cover.pullbackCoverOver'_f, Scheme.Hom.comp_appTop, IsOpenImmersion.opensRange_pullback_snd_of_left, IsAffineOpen.Spec_map_appLE_fromSpec, IsPreimmersion.instIsMultiplicativeScheme, Scheme.Cover.gluedCoverT'_fst_snd, IsZariskiLocalAtTarget.descendsAlong, IsPreimmersion.instFstScheme, IsAffineOpen.isLocalization_stalk', pullback_of_geometrically', instHasOfPostcompPropertySchemeIsAffineHomIsSeparated, IsSeparated.instIsMultiplicativeScheme, Scheme.IdealSheafData.glueDataObjHom_comp_assoc, IsImmersion.instLiftSchemeId, UniversallyOpen.instIsStableUnderCompositionScheme, universally_isZariskiLocalAtTarget, Scheme.Hom.appLE_comp_appLE_assoc, Scheme.Hom.liftCoborder_ι, Scheme.canonicallyOverPullback_over, Scheme.mem_smallGrothendieckTopology, Scheme.Modules.pseudofunctor_left_unitality_assoc, Flat.instIsStableUnderCompositionScheme, instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, pullbackRestrictIsoRestrict_hom_morphismRestrict, Scheme.IdealSheafData.glueDataObjHom_comp, Scheme.GlueData.oneHypercover_I₀, Scheme.Cover.pushforwardIso_X, nonempty_isColimit_binaryCofanMk_of_isCompl, instRespectsIsoSchemeTopologicallyIsClosedMap, Scheme.Hom.inl_toNormalization_normalizationCoprodIso_inv_assoc, Scheme.IdealSheafData.inclusion_id, spread_out_unique_of_isGermInjective, IsAffineOpen.Spec_map_appLE_fromSpec_assoc, instIsIsoSchemeCoprodSpec, Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, Scheme.kerFunctor_obj, diagonal_Spec_map, instQuasiSeparatedFstScheme, Scheme.Hom.stalkMap_congr_assoc, IsOpenImmersion.opensRange_pullback_fst_of_right, Scheme.Modules.pseudofunctor_mapId_hom_τl, Scheme.Cover.add_toPreZeroHypercover, IsPreimmersion.instIsStableUnderBaseChangeScheme, universally_isLocalAtSource, Scheme.AffineZariskiSite.cocone_pt, isEmpty_pullback_sigmaι_of_ne, instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange, Scheme.stalkMap_inv_hom_assoc, IsOpenImmersion.hasPullback_of_left, Scheme.Spec_obj, IsFinite.instIsStableUnderCompositionScheme, IsIntegralHom.instDescScheme, HasAffineProperty.affineAnd_le_isAffineHom, AffineScheme.forgetToScheme_obj, instIsMultiplicativeSchemeIsAffineHom, ExistsHomHomCompEqCompAux.hb, IsAffineOpen.fromSpec_toSpecΓ_assoc, Scheme.Hom.comp_image, IsOpenImmersion.range_pullbackFst, Scheme.appLE_comp_appLE, Scheme.affineBasisCover_map_range, Scheme.Hom.resLE_comp_resLE, IsLocalAtSource.iff_of_iSup_eq_top, Scheme.Cover.map_prop, ΓSpec_adjunction_homEquiv_eq, Scheme.Cover.LocallyDirected.w, IsSeparated.instRespectsIsoScheme, Scheme.Modules.pushforwardCongr_inv_app_app, AffineTargetMorphismProperty.respectsIso_of, SurjectiveOnStalks.stableUnderBaseChange, Scheme.grothendieckTopology_cover, Scheme.Hom.isoImage_hom_ι, Flat.isStableUnderBaseChange, Flat.instSndScheme, AffineSpace.SpecIso_inv_over, Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, Scheme.Hom.toNormalization_fromNormalization, instRespectsIsoSchemeTopologicallyGeneralizingMap, Scheme.Cover.Over.isOver_map, Scheme.iso_hom_base_inv_base_apply, Scheme.toIso_inv_ι, IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, Scheme.Spec_map, Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom, Scheme.Hom.opensRange_comp_of_isIso, instRespectsSchemeSmoothIsOpenImmersion, Scheme.Hom.inv_image, isomorphisms_eq_stalkwise, Scheme.homOfLE_ι_assoc, Scheme.IsSeparated.isSeparated_terminal_from, UniversallyInjective.isStableUnderBaseChange, instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian, Scheme.residueFieldCongr_fromSpecResidueField_assoc, Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv_assoc, IsIntegralHom.instIsStableUnderBaseChangeScheme, Scheme.instIsClosedImmersionLiftIdOfIsSeparated, IsOpenImmersion.le_monomorphisms, Scheme.Cover.mkOfCovers_f, Scheme.Hom.normalizationPullback_snd, Scheme.Hom.opensRange_comp, IsFinite.eq_inf, HasAffineProperty.affineAnd_containsIdentities, Scheme.Hom.ι_fromNormalization, Scheme.Hom.comp_base, exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, IsIntegralHom.instIsMultiplicativeScheme, Scheme.mem_pretopology_iff, affineLocally_le, IsAffineOpen.isCompactOpenCovered, Scheme.IdealSheafData.comap_comp, instLocallyQuasiFiniteCompScheme, GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, Scheme.residueFieldMap_id, Scheme.GlueData.openCover_I₀, Proj.homOfLE_toBasicOpenOfGlobalSections_ι, Scheme.GlueData.oneHypercover_f, instIsStableUnderBaseChangeSchemeGeometricallyReduced, Scheme.restrictFunctor_obj_left, isLocallyNoetherian_iff_openCover, Scheme.IdealSheafData.subschemeMap_subschemeι_assoc, instGeometricallyIrreducibleFstScheme, AffineSpace.isoOfIsAffine_inv_over, IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget, FormallyUnramified.instIsStableUnderCompositionScheme, instSmoothSndScheme, Scheme.Hom.stalkMap_id, universallyClosed_iff, Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace, Scheme.instIsStableUnderBaseChangeQcPrecoverage, Scheme.zariskiPrecoverage_le_qcPrecoverage, IsPreimmersion.comp_iff, pullbackSpecIso_hom_fst', Scheme.IdealSheafData.glueDataObjι_ι, IsImmersion.instSndScheme, IsOpenImmersion.isoOfRangeEq_hom_fac_assoc, instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, Scheme.monObjAsOverPullback_one, instIsOverHomOfLE, Scheme.Modules.pseudofunctor_map_r, isPullback_Spec_map_isPushout, AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass, Scheme.restrictFunctor_map_left, Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, Scheme.comp_app_assoc, Scheme.Pullback.Triplet.ofPoint_y, IsAffineOpen.SpecMap_appLE_fromSpec, AffineSpace.comp_homOfVector_assoc, Scheme.Hom.appLE_comp_appLE, Scheme.GlueData.oneHypercover_Y, isIso_of_isOpenImmersion_of_opensRange_eq_top, Scheme.Cover.ColimitGluingData.functor_map, Scheme.Modules.restrictFunctorId_hom_app_app, Scheme.SpecMap_stalkMap_fromSpecStalk, instIsIsoSchemeMapOfCommRingCat, AffineTargetMorphismProperty.cancel_left_of_respectsIso, IsAffineOpen.isoSpec_hom, IsImmersion.isImmersion_iff_exists_of_quasiCompact, isPullback_opens_inf_le, Scheme.Γ_obj_op, Scheme.Hom.stalkMap_inv_hom_apply, Scheme.Cover.intersectionOfLocallyDirected_f, quasiCompactCover_iff, Scheme.Pullback.forget_comparison_surjective, Scheme.Hom.isoImage_hom_ι_assoc, Scheme.inv_base_hom_base_assoc, Scheme.Hom.stalkMap_hom_inv_assoc, Scheme.Modules.pseudofunctor_mapComp_inv_τr, IsLocalAtSource.sigmaDesc, Scheme.GlueData.oneHypercover_p₁, Scheme.PartialMap.compHom_hom, Scheme.Pullback.openCoverOfLeft_f, IsSeparated.comp_iff, spread_out_of_isGermInjective, Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, Scheme.OpenCover.restrict_X, UniversallyOpen.instCompScheme, pullbackSpecIso_hom_snd, Scheme.Hom.comp_appTop_assoc, instSmoothFstScheme, Scheme.Cover.mem_pretopology, universallyClosed_respectsIso, instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1, IsDominant.comp_iff, Scheme.Hom.quasiFiniteAt_comp_iff, instIsDominantCompScheme, IsFinite.instContainsIdentitiesScheme, Scheme.isEmpty_pullback, IsIntegralHom.instCompScheme, Scheme.coe_homeoOfIso, UniversallyOpen.instRespectsIsoScheme, Scheme.openCoverBasicOpenTop_f, pointEquivClosedPoint_symm_apply_coe, Scheme.Cover.gluedCoverT'_fst_fst_assoc, Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected, Scheme.Cover.functorOfLocallyDirectedHomBase_app, IsIntegralHom.eq_universallyClosed_inf_isAffineHom, IsPreimmersion.comp, AffineSpace.reindex_id, Scheme.GlueData.ι_jointly_surjective, quasiSeparated_isStableUnderComposition, Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, IsZariskiLocalAtSource.comp, IsProper.instRespectsIsoScheme, IsFinite.instHasOfPostcompPropertySchemeIsSeparated, instIsZariskiLocalAtTargetDiagonalScheme, Scheme.stalkClosedPointTo_comp, pointsPi_surjective, Scheme.pretopology_eq_inf, Scheme.Opens.toSpecΓ_SpecMap_appLE, IsAffineOpen.fromSpec_toSpecΓ, Scheme.Cover.ColimitGluingData.functor_obj, initial_isEmpty, Scheme.pullbackComparison_forget_surjective, Scheme.residueFieldMap_comp, Scheme.isoSpec_image_zeroLocus, Scheme.IdealSheafData.subschemeMap_subschemeι, Scheme.comp_coeBase, quasiSeparated_isStableUnderBaseChange, Scheme.Spec_stalkClosedPointTo_fromSpecStalk, IsSeparated.instFstScheme, IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, IsOpenImmersion.isoOfRangeEq_inv_fac, Scheme.Pullback.openCoverOfLeftRight_X, Scheme.mem_toGrothendieck_smallPretopology, Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop, Scheme.Hom.stalkMap_inv_hom, isSmoothOfRelativeDimension_isStableUnderBaseChange, Scheme.Hom.inv_app, Scheme.Hom.isoOpensRange_inv_comp, Scheme.restrictFunctor_obj_hom, IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, Scheme.instFaithfulEtaleOverForget, Scheme.IdealSheafData.subschemeFunctor_map, IsOpenImmersion.hasLimit_cospan_forget_of_left', instIsAffinePullbackSchemeOfIsAffineHom, Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField, Scheme.pretopology_cover, Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace, Scheme.isAffine_affineCover, Scheme.AffineZariskiSite.directedCover_I₀, IsSeparated.instSndScheme, IsOpenImmersion.instSndScheme, Scheme.Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField, universallyClosed_eq, coprodMk_inr, Scheme.AffineOpenCover.openCover_X, Scheme.isoOfEq_hom, QuasiCompactCover.exists_isAffineOpen_of_isCompact, Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, quasiSeparatedSpace_iff_quasiCompact_prod_lift, Scheme.Hom.liftQuotient_comp_assoc, Scheme.Pullback.exists_preimage_pullback, IsAffineOpen.isoSpec_inv_ι, Scheme.subcanonical_zariskiTopology, IsOpenImmersion.mono, isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed, IsAffineOpen.isoSpec_hom_appTop, IsImmersion.comp_iff, instHasFiniteCoproductsOverSchemeTopMorphismProperty, IsOpenImmersion.comp_lift, essImage_Spec, IsOpenImmersion.lift_fac, pullbackSpecIso_hom_fst_assoc, IsOpenImmersion.instFstScheme, ValuativeCriterion.eq, instRespectsIsoSchemeTopologicallyIsOpenMap, instRespectsIsoSchemeTopologicallyIsEmbedding, Scheme.Modules.pseudofunctor_mapId_inv_τl, Scheme.Modules.pseudofunctor_associativity, Scheme.Hom.eqToHom_app, Scheme.Cover.sigma_f, Scheme.id_app, IsClosedImmersion.isIso_iff_ker_eq_bot, Scheme.Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField, IsAffineOpen.toSpecΓ_fromSpec, Scheme.Modules.pseudofunctor_mapId_inv_τr, Scheme.RationalMap.isOver_iff, Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion, Scheme.Pullback.affine_hasPullback, Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap, Scheme.homOfLE_rfl, IsOpenImmersion.lift_app, sourceLocalClosure.instRespectsRightScheme, IsAffineOpen.isoSpec_inv_ι_assoc, UniversallyInjective.universally_injective, Scheme.IdealSheafData.map_ker, IsClosedImmersion.isIso_of_injective_of_isAffine, Scheme.Pullback.openCoverOfLeft_X, Scheme.stalkMap_congr, Spec.homEquiv_symm_apply, descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation, IsIntegralHom.comp_iff, Scheme.Cover.gluedCover_t', Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor, Scheme.Hom.stalkMap_congr_hom, geometrically_iff_of_isClosedUnderIsomorphisms, QuasiCompactCover.instPullback₂Scheme, Scheme.Pullback.diagonalCover_map, Scheme.inv_base_hom_base, AffineTargetMorphismProperty.diagonal_respectsIso, Scheme.Cover.ι_fromGlued, Scheme.Hom.inl_toNormalization_normalizationCoprodIso_inv, Scheme.Hom.inr_normalizationCoprodIso_hom_fromNormalization, Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine, Scheme.IdealSheafData.glueDataObjHom_id, sourceLocalClosure.le, pointOfClosedPoint_comp, instHasAffinePropertyDiagonalSchemeDiagonal, Scheme.Cover.mem_grothendieckTopology, Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, pullback_of_geometrically, Scheme.Opens.isoOfLE_inv_ι_assoc, universallyClosed_snd, QuasiCompactCover.instSumScheme, exists_etale_isCompl_of_quasiFiniteAt, morphismRestrict_id, instIsSchemeTheoreticallyDominantCompScheme, Spec.preimage_comp, Scheme.isAffine_affineOpenCover, Scheme.Hom.id_image, pullbackSpecIso_hom_snd_assoc
|
«term_⁻¹ᵁ_» 📖 | CompOp | — |
«termΓ(_,_)» 📖» "API Documentation") | CompOp | — |
| Name | Category | Theorems |
SpecΓIdentity 📖 | CompOp | 3 mathmath: SpecΓIdentity_hom_app, SpecΓIdentity_app, SpecΓIdentity_inv_app
|
algebra_section_section_basicOpen 📖 | CompOp | 5 mathmath: AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map
|
arrowStalkMapIsoOfEq 📖 | CompOp | — |
basicOpen 📖 | CompOp | 84 mathmath: Opens.ι_image_basicOpen, AlgebraicGeometry.Proj.fromOfGlobalSections_resLE, map_PrimeSpectrum_basicOpen_of_affine, mem_basicOpen', basicOpen_of_isUnit, AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AffineZariskiSite.generate_presieveOfSections, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, zeroLocus_singleton, preimage_basicOpen_top, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, Opens.ι_image_basicOpen_topIso_inv, AlgebraicGeometry.isBasis_basicOpen, basicOpen_le, Opens.toSpecΓ_preimage_basicOpen, zeroLocus_def, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, Hom.preimage_basicOpen_top, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, basicOpen_pow, evaluation_eq_zero_iff_notMem_basicOpen, basicOpen_add_le, Hom.preimage_basicOpen, basicOpen_res_eq, image_basicOpen, isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, basicOpen_one, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc, map_basicOpen, AlgebraicGeometry.isRetrocompact_basicOpen, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, basicOpen_appLE, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, affineBasicOpen_coe, basicOpen_mul, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, Opens.mem_basicOpen_toScheme, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, mem_basicOpen_top, Opens.ι_image_basicOpen', basicOpen_res, AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine, map_basicOpen_map, basicOpen_zero, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, mem_basicOpen'', AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.exists_basicOpen_le_affine_inter, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', basicOpen_restrict, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, preimage_basicOpen, basicOpen_eq_bot_iff_forall_evaluation_eq_zero, toSpecΓ_preimage_basicOpen, openCoverBasicOpenTop_f, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated, IsQuasiAffine.isBasis_basicOpen, AffineZariskiSite.basicOpen_coe, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen, IdealSheafData.map_ideal_basicOpen, mem_zeroLocus_iff, AlgebraicGeometry.instIsAffineHomιBasicOpen, evaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.isCompact_basicOpen, isNilpotent_iff_basicOpen_eq_bot_of_isCompact, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map, mem_basicOpen
|
delabAdjoinNotation 📖 | CompOp | — |
delabCoeFunAppNotation 📖 | CompOp | — |
delabCoeFunNotation 📖 | CompOp | — |
empty 📖 | CompOp | 2 mathmath: empty_carrier_carrier, empty_presheaf
|
forget 📖 | CompOp | 78 mathmath: coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.coprodSpec_apply, Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc, AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec, Hom.inr_toNormalization_normalizationCoprodIso_inv, AlgebraicGeometry.instIsAffineSigmaObjScheme, AlgebraicGeometry.sigmaOpenCover_X, AlgebraicGeometry.ι_right_coprodIsoSigma_inv, AlgebraicGeometry.ι_sigmaSpec, AlgebraicGeometry.coprodSpec_inr, AlgebraicGeometry.instIsIsoSchemeSigmaSpecOfFinite, Hom.toNormalization_inr_normalizationCoprodIso_hom, forget_map, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.Flat.instDescScheme, coprodPresheafObjIso_hom_snd_assoc, forget_obj, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.instIsAffineHomDescScheme, AlgebraicGeometry.isPullback_inl_inl_coprodMap, AlgebraicGeometry.instIsAffineCoprodScheme, AlgebraicGeometry.Surjective.sigmaDesc_of_union_range_eq_univ, Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc, AlgebraicGeometry.isIso_stalkMap_coprodSpec, GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, AlgebraicGeometry.isCompl_range_inl_inr, AlgebraicGeometry.instIsOpenImmersionInrScheme, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.ι_left_coprodIsoSigma_inv, AlgebraicGeometry.IsZariskiLocalAtTarget.coprodMap, AlgebraicGeometry.IsFinite.instDescScheme, Hom.inl_normalizationCoprodIso_hom_fromNormalization_assoc, AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd, Hom.inl_normalizationCoprodIso_hom_fromNormalization, AlgebraicGeometry.instIsOpenImmersionMapScheme, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.instSurjectiveDescI₀SchemeF, Hom.inr_normalizationCoprodIso_hom_fromNormalization_assoc, coprodPresheafObjIso_hom_snd, AlgebraicGeometry.coprodSpec_coprodMk, AlgebraicGeometry.instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion, Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization, AlgebraicGeometry.instIsOpenImmersionInlScheme, AlgebraicGeometry.isOpenImmersion_sigmaDesc, AlgebraicGeometry.coprodSpec_inr_assoc, IsLocallyDirected.instIsLocallyDirectedWidePushoutShapeCompForgetOfIsOpenImmersionMap, coprodPresheafObjIso_hom_fst, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1, AlgebraicGeometry.instIsOpenImmersionSigmaSpec, Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc, AffineZariskiSite.PreservesLocalization.isLocallyDirected, AlgebraicGeometry.coprodSpec_inl_assoc, AlgebraicGeometry.sigmaOpenCover_I₀, AlgebraicGeometry.ι_sigmaSpec_assoc, AlgebraicGeometry.isPullback_inr_inr_coprodMap, AlgebraicGeometry.coprodSpec_inl, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc, AlgebraicGeometry.sigmaOpenCover_f, Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, Hom.inl_toNormalization_normalizationCoprodIso_inv_assoc, AlgebraicGeometry.instIsIsoSchemeCoprodSpec, AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne, AlgebraicGeometry.IsIntegralHom.instDescScheme, Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, Hom.toNormalization_inl_normalizationCoprodIso_hom, Hom.inr_toNormalization_normalizationCoprodIso_inv_assoc, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, Pullback.forget_comparison_surjective, AlgebraicGeometry.IsLocalAtSource.sigmaDesc, isLocallyDirected_of_equifibered_of_injective, pullbackComparison_forget_surjective, AlgebraicGeometry.coprodMk_inr, Hom.inl_toNormalization_normalizationCoprodIso_inv, Hom.inr_normalizationCoprodIso_hom_fromNormalization
|
forgetToLocallyRingedSpace 📖 | CompOp | 14 mathmath: AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right', forgetToLocallyRingedSpace_map, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, Γ_def, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right, IsLocallyDirected.instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace, fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom, forgetToLocallyRingedSpace_obj, AlgebraicGeometry.IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, instFullLocallyRingedSpaceForgetToLocallyRingedSpace, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left', instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace
|
forgetToTop 📖 | CompOp | 7 mathmath: forgetToTop_map, forgetToTop_obj, AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall, GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, AlgebraicGeometry.isomorphisms_eq_stalkwise
|
forgetToTop_obj_eq_coe 📖 | MathDef | — |
forget_obj_eq_coe 📖 | MathDef | — |
fullyFaithfulForgetToLocallyRingedSpace 📖 | CompOp | 1 mathmath: fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom
|
hasCoeToTopCat 📖 | CompOp | — |
homeoOfIso 📖 | CompOp | 4 mathmath: homeoOfIso_symm, coe_homeoOfIso_symm, homeoOfIso_apply, coe_homeoOfIso
|
instCategory 📖 | CompOp | 1348 mathmath: AlgebraicGeometry.AffineSpace.not_isIntegralHom, Hom.resLE_map_assoc, AlgebraicGeometry.Surjective.instFstScheme, AlgebraicGeometry.AffineSpace.map_Spec_map, GlueData.oneHypercover_I₁, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIrreducible, coprodPresheafObjIso_hom_fst_assoc, Hom.toPartialMap_hom, AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', map_PrimeSpectrum_basicOpen_of_affine, bot_mem_grothendieckTopology, Modules.pseudofunctor_map_adj, coverOfIsIso_I₀, AlgebraicGeometry.IsImmersion.isStableUnderBaseChange, AlgebraicGeometry.instLocallyQuasiFiniteSndScheme, isoOfEq_inv, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Spec.map_eq_id, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc, AffineOpenCover.openCover_f, Modules.pushforwardId_inv_app_app, AlgebraicGeometry.IsClosedImmersion.instIsIsoSchemeToImage, AlgebraicGeometry.AffineSpace.map_reindex, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, Pullback.Triplet.specTensorTo_fst, Hom.opensRange_pullbackSnd, Cover.pullbackCoverOver_X, AlgebraicGeometry.IsProper.instCompScheme, Cover.gluedCoverT'_snd_snd_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, Spec_map_stalkMap_fromSpecStalk, Cover.LocallyDirected.directed, AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, PartialMap.ext_iff, AlgebraicGeometry.instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated, AlgebraicGeometry.pointOfClosedPoint_comp_assoc, isEmpty_pullback_iff, AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.IsSeparated.isStableUnderBaseChange, Hom.quasiFiniteLocus_comp, AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral, AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom_1, IdealSheafData.glueDataObjHom_ι_assoc, AlgebraicGeometry.instIsLocallyArtinianXScheme, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc, AlgebraicGeometry.coprodSpec_apply, RingHom.IsStableUnderBaseChange.pullback_fst_appTop, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc, AffineCover.cover_I₀, Hom.toNormalization_normalizationPullback_fst, AlgebraicGeometry.instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right', AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec, AlgebraicGeometry.Etale.instFstScheme, AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.ΓSpec.isIso_adjunction_counit, AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.injective_isStableUnderComposition, affineBasisCover_is_basis, AlgebraicGeometry.instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion, Opens.toSpecΓ_naturality, AlgebraicGeometry.instLocallyQuasiFiniteFstScheme, Opens.toSpecΓ_SpecMap_presheaf_map_top, Pullback.openCoverOfLeftRight_f, comp_toLRSHom_assoc, restrictFunctorΓ_inv_app, Hom.inr_toNormalization_normalizationCoprodIso_inv, mem_grothendieckTopology_iff, Pullback.Triplet.ofPoint_x, overGrothendieckTopology_eq_toGrothendieck_overPretopology, AlgebraicGeometry.universallyClosedTypeComp, AlgebraicGeometry.quasiSeparated_comp, AlgebraicGeometry.HasAffineProperty.affineAnd_le_affineAnd, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc, Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.morphismRestrict_ι_assoc, fromSpecStalk_toSpecΓ_assoc, Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.sourceLocalClosure.instIsMultiplicativeSchemeOfIsStableUnderBaseChange, AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal, AlgebraicGeometry.instIsAffineSigmaObjScheme, zariskiTopology_le_etaleTopology, AlgebraicGeometry.isIso_SpecMap_iff, zariskiTopology_eq, Cover.iUnion_range, AlgebraicGeometry.IsDominant.respectsIso, AlgebraicGeometry.QuasiCompactCover.instCoverOfIsIso, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.Spec.map_surjective, AlgebraicGeometry.IsProper.instFstScheme, AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf, AlgebraicGeometry.instFinitaryExtensiveScheme, AlgebraicGeometry.pointsPi_surjective_of_isAffine, AlgebraicGeometry.isOpenImmersion_isStableUnderComposition, Cover.glued_cover_cocycle_fst, instIsStableUnderCompositionQcPrecoverage, AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme, AlgebraicGeometry.sigmaOpenCover_X, AlgebraicGeometry.GeometricallyIrreducible.comp, Hom.iUnion_support_ker_openCover_map_comp, AlgebraicGeometry.UniversallyOpen.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.diagonal_SpecMap, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso, inv_app, Pullback.openCoverOfBase_I₀, Hom.id_appTop, AlgebraicGeometry.ι_right_coprodIsoSigma_inv, AlgebraicGeometry.ι_sigmaSpec, Cover.instIsIsoFromGlued, Hom.le_ker_comp, AlgebraicGeometry.Spec.map_injective, AlgebraicGeometry.coprodSpec_inr, AlgebraicGeometry.IsOpenImmersion.comp_lift_assoc, AlgebraicGeometry.IsProper.instSndScheme, OpenCover.finiteSubcover_f, AlgebraicGeometry.instIsIsoSchemeSigmaSpecOfFinite, Spec_map_stalkSpecializes_fromSpecStalk, Pullback.openCoverOfBase_f, AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion, ideal_ker_le_ker_ΓSpecIso_inv_comp, Cover.pullbackCoverOver'_X, stalkMap_congr_assoc, Pullback.openCoverOfRight_I₀, Opens.toSpecΓ_SpecMap_map, isoSpec_inv_toSpecΓ, Pullback.SpecTensorTo_SpecOfPoint, AlgebraicGeometry.UniversallyInjective.iff_diagonal, AlgebraicGeometry.instIsStableUnderCompositionSchemeSmooth, hom_inv_apply, AlgebraicGeometry.pointsPi_injective, Hom.instIsIsoToNormalizationOfIsIntegralHom, instHasPullbacksPrecoverageOfHasPullbacks, ι_toIso_inv, AlgebraicGeometry.instIsMultiplicativeSchemeQuasiCompact, instIsOverFromSpecStalkOfMem, AlgebraicGeometry.isPullback_opens_inf, Cover.functorOfLocallyDirected_obj, Hom.preimageIso_hom_ι_assoc, isoOfEq_inv_ι, openCoverOfIsOpenCover_I₀, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰S, Hom.toNormalization_inr_normalizationCoprodIso_hom, AlgebraicGeometry.UniversallyOpen.instIsMultiplicativeScheme, AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange, AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange, Cover.glued_cover_cocycle, Pullback.instHasPullbacks, IdealSheafData.glueDataObjHom_ι, affineOpenCover_I₀, AlgebraicGeometry.isImmersion_eq_inf, Cover.gluedCover_t, SpecΓIdentity_hom_app, AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange, preimage_comp, AlgebraicGeometry.instIsZariskiLocalAtTargetMonomorphismsScheme, Hom.stalkMap_congr_hom_assoc, quasiCompactCover_shrink_iff, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, Pullback.Triplet.isPullback_SpecMap_tensor, forget_map, AlgebraicGeometry.sigmaMk_mk, Pullback.Triplet.specTensorTo_base_snd, Hom.isOver_iff, PartialMap.fromSpecStalkOfMem_compHom, AlgebraicGeometry.affineAnd_respectsIso, AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.Flat.instDescScheme, Cover.pullbackCoverOver_I₀, AlgebraicGeometry.instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant, AlgebraicGeometry.AffineSpace.map_over_assoc, IdealSheafData.inclusion_subschemeι_assoc, AlgebraicGeometry.IsClosedImmersion.comp, Modules.pseudofunctor_map_l, instIsClosedImmersionιOfIsSeparated, Cover.gluedCover_U, mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId, Pullback.tensorCongr_SpecTensorTo, AlgebraicGeometry.IsSeparated.eq_valuativeCriterion, Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.instGeometricallyReducedSndScheme, AlgebraicGeometry.instCoproductsOfShapeDisjointSchemeOfSmall, AlgebraicGeometry.IsImmersion.comp, Hom.toNormalization_fromNormalization_assoc, AlgebraicGeometry.Flat.epi_of_flat_of_surjective, forgetToTop_map, AlgebraicGeometry.UniversallyOpen.out, AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms, bot_mem_precoverage, AlgebraicGeometry.IsImmersion.instιScheme, AlgebraicGeometry.isSmooth_isStableUnderBaseChange, coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.AffineScheme.mk_obj, isoSpec_hom, ι_toIso_inv_assoc, Hom.id_preimage, Modules.pseudofunctor_right_unitality_assoc, Hom.toImage_imageι, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, AlgebraicGeometry.HasAffineProperty.diagonal_iff, forget_obj, eqToHom_c_app, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated, AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe, forgetToTop_obj, affineOpenCover_idx, Opens.isoOfLE_hom_ι_assoc, Hom.fromNormalization_preimage, AlgebraicGeometry.IsIntegralHom.instSndScheme, toSpecΓ_naturality_assoc, Pullback.Triplet.snd_SpecTensorTo_apply, Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.LocallyQuasiFinite.comp_iff, AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackSnd, AlgebraicGeometry.IsFinite.comp_iff, AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion, Cover.ColimitGluingData.cocone_ι_transitionMap, Pullback.Triplet.specTensorTo_fst_assoc, isoOfEq_hom_ι, AlgebraicGeometry.IsAffineHom.comp_iff, AlgebraicGeometry.AffineScheme.forgetToScheme_preservesLimits, AlgebraicGeometry.HasRingHomProperty.containsIdentities, presieve₀_mem_precoverage_iff, comp_base, AlgebraicGeometry.IsClosedImmersion.lift_fac_assoc, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top, isoSpec_hom_naturality, homOfLE_ι, toSpecΓ_isoSpec_inv_assoc, Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, Hom.resLE_map, Cover.mkOfCovers_I₀, Hom.comp_app, AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme, AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion, IdealSheafData.range_glueDataObjι_ι_eq_support_inter, Pullback.left_affine_comp_pullback_hasPullback, hom_base_inv_base, AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition, AlgebraicGeometry.IsLocalAtSource.iff_of_openCover, GlueData.instHasMulticoequalizerDiagram, forgetToLocallyRingedSpace_map, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, toSpecΓ_naturality, AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeLocallyQuasiFinite, Hom.ι_toNormalization, AlgebraicGeometry.geometrically_eq_universally, AlgebraicGeometry.instGeometricallyIntegralSndScheme, AlgebraicGeometry.Spec.faithful, AlgebraicGeometry.Spec.preimage_id, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, homeoOfIso_symm, Cover.ColimitGluingData.transitionCocone_pt, comp_coeBase_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource, AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.IsProper.isStableUnderBaseChange, AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left, IdealSheafData.inclusion_subschemeι, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.IsClosedImmersion.respectsIso, Opens.toSpecΓ_naturality_assoc, GlueData.openCover_f, AlgebraicGeometry.instSmoothOfRelativeDimensionOfNatNatCompScheme, instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.instIsMultiplicativeSchemeSurjective, Hom.id_app, Γ_obj, Opens.fromSpecStalkOfMem_ι_assoc, AlgebraicGeometry.instIsAffineXSchemeAffineCover, kerAdjunction_unit_app, Hom.liftQuotient_comp, Pullback.carrierEquiv_symm_fst, AlgebraicGeometry.instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, Cover.ColimitGluingData.transitionMap_id, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc, Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.instIsAffineHomDescScheme, IdealSheafData.comapIso_hom_snd_assoc, Hom.cover_X, directedAffineCover_f, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, AlgebraicGeometry.Flat.instFstScheme, AlgebraicGeometry.instIsOverTerminalScheme, Opens.toSpecΓ_SpecMap_presheaf_map_assoc, IdealSheafData.comap_id, Pullback.range_fst_comp, AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.quasiCompact_isStableUnderBaseChange, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc, isoSpec_hom_naturality_assoc, AlgebraicGeometry.pullbackSpecIso_inv_snd, AlgebraicGeometry.IsImmersion.instMapDescScheme, isoSpec_inv_image_zeroLocus, IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall, AlgebraicGeometry.HasAffineProperty.affineAnd_eq_of_propertyIsLocal, AlgebraicGeometry.quasiCompact_comp, AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective, AlgebraicGeometry.Etale.instSndScheme, AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, AlgebraicGeometry.IsOpenImmersion.isIso, Cover.gluedCover_V, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, hom_base_inv_base_assoc, AlgebraicGeometry.isPullback_inl_inl_coprodMap, AlgebraicGeometry.IsFinite.eq_proper_inf_locallyQuasiFinite, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AlgebraicGeometry.AffineSpace.map_comp, over_def, Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.IsOpenImmersion.instπWalkingCospanSchemeCospanOne, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap, Cover.coconeOfLocallyDirected_ι, AlgebraicGeometry.Flat.instIsMultiplicativeScheme, Cover.ι_fromGlued_assoc, AlgebraicGeometry.universallyInjective_iff, AlgebraicGeometry.instHasFiniteLimitsScheme, GlueData.glue_condition, GlueData.f_open, OpenCover.isOpenCover_opensRange, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, Cover.ulift_X, openCoverOfIsOpenCover_f, AlgebraicGeometry.instIsAffineCoprodScheme, Pullback.Triplet.Spec_map_tensor_isPullback, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, id_appTop, Cover.gluedCoverT'_fst_fst, AlgebraicGeometry.pullbackSpecIso_hom_base, Cover.covers, AlgebraicGeometry.IsOpenImmersion.comp, AlgebraicGeometry.smooth_comp, AlgebraicGeometry.ValuativeCriterion.Existence.eq, isCommMonObj_asOver_pullback, AlgebraicGeometry.QuasiCompactCover.exists_hom, GlueData.isOpen_iff, AlgebraicGeometry.Surjective.sigmaDesc_of_union_range_eq_univ, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, fromSpecStalk_toSpecΓ, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenEmbedding, isMonHom_fst_id_right, AlgebraicGeometry.IsLocalIso.eq_iInf, AlgebraicGeometry.ValuativeCriterion.Existence.stableUnderBaseChange, Spec_map_stalkMap_fromSpecStalk_assoc, PartialMap.equiv_toPartialMap_iff_of_isSeparated, AlgebraicGeometry.Etale.instIsMultiplicativeScheme, AlgebraicGeometry.isInitial_iff_isEmpty, AlgebraicGeometry.AffineSpace.reindex_over, IdealSheafData.subschemeCover_map_subschemeι, Cover.gluedCoverT'_snd_fst, AlgebraicGeometry.AffineSpace.map_over, isAffine_affineBasisCover, Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.topologically_iso_le, Cover.trans_id, AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp, Cover.exists_lift_trans_eq, Hom.toImage_imageι_assoc, AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyQuasiFinite, AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact, GlueData.instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedEmbedding, AlgebraicGeometry.instGeometricallyReducedFstScheme, Hom.preimage_smoothLocus_eq, coe_homeoOfIso_symm, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, stalkMap_hom_inv_assoc, AlgebraicGeometry.universallyInjective_eq, AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι, id.base, Γ_def, Hom.isoOpensRange_hom_ι_assoc, AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact, AlgebraicGeometry.Spec.full, Pullback.Triplet.specTensorTo_snd, directedAffineCover_I₀, AlgebraicGeometry.opensDiagram_map, Hom.isoOpensRange_hom_ι, AlgebraicGeometry.instHasOfPrecompPropertySchemeSurjective, AlgebraicGeometry.morphismRestrict_ι, Modules.restrictFunctorComp_hom_app_app, Hom.preimageIso_inv_ι, SpecMap_stalkSpecializes_fromSpecStalk, descResidueField_fromSpecResidueField, Cover.RelativeGluingData.equifibered, AlgebraicGeometry.Spec.map_preimage_unop, IdealSheafData.map_comp, AlgebraicGeometry.instIsClosedImmersionSndScheme, Modules.restrictFunctorComp_inv_app_app, Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, AlgebraicGeometry.IsOpenImmersion.isPullback_lift_id, AlgebraicGeometry.IsLocalIso.le_of_isLocalAtSource, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd, SpecΓIdentity_app, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc, IdealSheafData.inclusion_comp_assoc, homeoOfIso_apply, AlgebraicGeometry.pullbackSpecIso_inv_fst'_assoc, AlgebraicGeometry.affineLocally_respectsIso, AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite, AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange, Opens.toSpecΓ_SpecMap_map_assoc, AlgebraicGeometry.hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict, AlgebraicGeometry.IsImmersion.instDiagonalScheme, IdealSheafData.ker_fst_of_isClosedImmersion, GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, AlgebraicGeometry.specializingMap_respectsIso, OpenCover.restrict_f, instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.sourceLocalClosure.instRespectsIsoScheme, OpenCover.iSup_opensRange, GlueData.ι_isOpenImmersion, Pullback.Triplet.specTensorTo_snd_assoc, Cover.mkOfCovers_X, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right, AlgebraicGeometry.universallyClosed_isStableUnderBaseChange, Pullback.ofPointTensor_SpecTensorTo_assoc, AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal, AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.smooth_isStableUnderBaseChange, AlgebraicGeometry.IsFinite.instCompScheme, kerAdjunction_counit_app, AlgebraicGeometry.opensDiagramι_app, Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.IsClosedImmersion.comp_iff, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization, AlgebraicGeometry.isCompl_range_inl_inr, AlgebraicGeometry.UniversallyClosed.out, AlgebraicGeometry.universallyClosed_isStableUnderComposition, pretopology_le_inf, AlgebraicGeometry.ΓSpec.adjunction_unit_app, Opens.toSpecΓ_top, AlgebraicGeometry.universally_isLocalAtTarget, AlgebraicGeometry.HasRingHomProperty.stableUnderComposition, AlgebraicGeometry.HasRingHomProperty.isMultiplicative, Pullback.openCoverOfRight_f, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.IsOpenImmersion.to_iso, AlgebraicGeometry.AffineSpace.functor_obj_map, AlgebraicGeometry.AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite, AlgebraicGeometry.instSurjectiveCompScheme, Hom.iInf_ker_openCover_map_comp, AffineZariskiSite.restrictIsoSpec_hom_app, AlgebraicGeometry.specTargetImageFactorization_comp_assoc, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.AffineSpace.map_reindex_assoc, AlgebraicGeometry.instGeometricallyIrreducibleSndScheme, AlgebraicGeometry.instIsMultiplicativeSchemeQuasiSeparated, AlgebraicGeometry.IsLocalAtSource.comp, AlgebraicGeometry.instRespectsIsoSchemeSurjective, AlgebraicGeometry.instSubsingletonOverTerminalScheme, AffineCover.cover_f, AlgebraicGeometry.instIsOpenImmersionInrScheme, AlgebraicGeometry.instHasInitialScheme, AlgebraicGeometry.IsLocalIso.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.SurjectiveOnStalks.comp, Cover.gluedCover_J, stalkMap_congr_hom_assoc, Hom.opensRange_pullbackFst, Cover.ColimitGluingData.transitionCocone_ι_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, Cover.sigmaFunctor_obj, AlgebraicGeometry.compactSpace_iff_quasiCompact, mem_overGrothendieckTopology, AlgebraicGeometry.UniversallyOpen.snd, Modules.pseudofunctor_right_unitality, Modules.pseudofunctor_mapComp_hom_τl, AlgebraicGeometry.sourceLocalClosure.instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.disjoint_opensRange_sigmaι, comp_base_assoc, stalkMap_id, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_surjective, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty, Hom.instIsIsoNormalizationPullbackOfSmooth, Opens.toSpecΓ_SpecMap_presheaf_map, AlgebraicGeometry.quasiCompact_isStableUnderComposition, Hom.comp_app_assoc, comp_app, AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFinitePresentation, AlgebraicGeometry.isIso_iff_isOpenImmersion, AlgebraicGeometry.isOpenImmersion_isMultiplicative, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc, Cover.glued_cover_cocycle_snd, Hom.normalizationPullback_snd_assoc, GlueData.ι_eq_iff, Cover.trans_map, AlgebraicGeometry.AffineSpace.comp_homOfVector, openCoverOfIsOpenCover_X, AlgebraicGeometry.ι_left_coprodIsoSigma_inv, AlgebraicGeometry.instHasStrictInitialObjectsScheme, AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType_1, isoSpec_inv_naturality_assoc, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.IsImmersion.isImmersion_iff_exists, homOfLE_homOfLE_assoc, AlgebraicGeometry.IsLocalAtSource.respectsLeft_isOpenImmersion, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec, AlgebraicGeometry.isLocalIso_iff, AlgebraicGeometry.Spec.preimage_comp_assoc, Cover.toSigma_s₀, AlgebraicGeometry.IsClosedImmersion.lift_fac, AlgebraicGeometry.AffineSpace.hom_ext_iff, SpecMap_stalkMap_fromSpecStalk_assoc, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated, singleton_mem_precoverage_iff, IdealSheafData.glueDataObjMap_glueDataObjι_assoc, AlgebraicGeometry.QuasiCompactCover.inst, Pullback.tensorCongr_SpecTensorTo_assoc, AlgebraicGeometry.QuasiCompactCover.instPullback₁Scheme, isoSpec_Spec_hom, AlgebraicGeometry.AffineScheme.forgetToScheme_full, IdealSheafData.comapIso_inv_subschemeι_assoc, AlgebraicGeometry.IsZariskiLocalAtTarget.coprodMap, AlgebraicGeometry.IsFinite.instDescScheme, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, AlgebraicGeometry.instHasFiniteCoproductsScheme, AlgebraicGeometry.AffineSpace.isPullback_map, Hom.inl_normalizationCoprodIso_hom_fromNormalization_assoc, AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyInjective, AlgebraicGeometry.nonempty_isColimit_cofanMk_of, AlgebraicGeometry.AffineScheme.forgetToScheme_faithful, AlgebraicGeometry.instQuasiCompactSndScheme, AlgebraicGeometry.pullbackSpecIso_inv_fst, AlgebraicGeometry.IsLocalAtTarget.descendsAlong, AlgebraicGeometry.UniversallyInjective.respectsIso, AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd, AlgebraicGeometry.IsFinite.instFstScheme, Pullback.affine_affine_hasPullback, grothendieckTopology_eq_inf, AlgebraicGeometry.AffineSpace.homOfVector_over_assoc, AlgebraicGeometry.stalkwise_respectsIso, GlueData.openCover_X, AlgebraicGeometry.morphismRestrict_comp, SpecMap_stalkSpecializes_fromSpecStalk_assoc, isPullback_toSpecΓ_toSpecΓ, Cover.LocallyDirected.trans_comp, Hom.stalkMap_hom_inv, AlgebraicGeometry.instIsMultiplicativeSchemeLocallyOfFiniteType, restrictFunctorΓ_hom_app, Cover.functorOfLocallyDirected_map, stalkMap_congr_hom, Modules.pseudofunctor_mapComp_hom_τr, Γ_map_op, Pullback.range_snd_comp, directedAffineCover_X, Cover.property_trans, AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, Modules.restrictFunctorId_inv_app_app, Opens.isoOfLE_hom_ι, AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange, Opens.over_def, Opens.fromSpecStalkOfMem_ι, Modules.pushforwardComp_hom_app_app, iso_inv_base_hom_base, Hom.inl_normalizationCoprodIso_hom_fromNormalization, toSpecΓ_isoSpec_inv, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, Hom.comp_apply, Cover.sigma_X, homOfLE_homOfLE, AlgebraicGeometry.Proj.awayι_toSpecZero, AlgebraicGeometry.opensDiagram_obj, Cover.nonempty_of_nonempty, instSmallPrecoverage, AlgebraicGeometry.IsProper.stableUnderComposition, toIso_inv_ι_assoc, instFullOppositeIdealSheafDataOverSubschemeFunctor, AlgebraicGeometry.isPullback_SpecMap_of_isPushout, AlgebraicGeometry.instIsOpenImmersionMapScheme, Hom.cover_f, presieve₀_mem_qcPrecoverage_iff, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.opensCone_π_app, Hom.resLE_id, AlgebraicGeometry.isOpenImmersion_respectsIso, isClosedUnderIsomorphisms_quasiCompactCover, stalkMap_comp, AffineZariskiSite.directedCover_X, AlgebraicGeometry.IsPreimmersion.instMonoScheme, Cover.ulift_f, IdealSheafData.comapIso_inv_subschemeι, AlgebraicGeometry.UniversallyOpen.fst, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeSchemeΓ, OpenCover.instIsOpenImmersionTrans, IdealSheafData.glueDataObjMap_glueDataObjι, Hom.comp_appIso, AlgebraicGeometry.isIso_of_isEmpty, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIntegral, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.instSurjectiveDescI₀SchemeF, AlgebraicGeometry.over_def, AlgebraicGeometry.IsIntegralHom.instFstScheme, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc, Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, AlgebraicGeometry.instLocallyOfFinitePresentationFstScheme, Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.isAffineHom_isStableUnderBaseChange, Opens.toSpecΓ_SpecMap_appLE_assoc, IdealSheafData.inclusion_comp, Γ_map, Cover.pullbackCoverOver'_I₀, AlgebraicGeometry.AffineScheme.forgetToScheme_map, Cover.ulift_I₀, AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme_1, AlgebraicGeometry.isSeparated_iff, AlgebraicGeometry.Proj.awayι_toSpecZero_assoc, Hom.inr_normalizationCoprodIso_hom_fromNormalization_assoc, AlgebraicGeometry.HasRingHomProperty.inf, AlgebraicGeometry.IsClosedImmersion.instIsMultiplicativeScheme, AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc, AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1, AlgebraicGeometry.ValuativeCommSq.commSq, residueFieldCongr_fromSpecResidueField, AlgebraicGeometry.universallyInjective_eq_diagonal, coprodPresheafObjIso_hom_snd, AlgebraicGeometry.IsOpenImmersion.instHasOfPostcompPropertyScheme, AlgebraicGeometry.coprodSpec_coprodMk, instIsStableUnderBaseChangeJointlySurjectivePrecoverage, AlgebraicGeometry.isAffine_affineScheme, Hom.preimageIso_hom_ι, AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono, Cover.sigmaFunctor_map, AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMap, isoOfEq_hom_ι_assoc, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, AlgebraicGeometry.instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion, isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, Hom.ker_comp_of_isIso, Pullback.openCoverOfRight_X, AlgebraicGeometry.instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion, Hom.id_appIso, isoOfEq_inv_ι_assoc, Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.instQuasiSeparatedSndScheme, Modules.pseudofunctor_mapId_hom_τr, Cover.gluedCoverT'_snd_fst_assoc, Hom.asFiberHom_fiberι, IdealSheafData.subschemeFunctor_obj, AlgebraicGeometry.specTargetImageFactorization_comp, comp_appTop_assoc, AlgebraicGeometry.universallyInjective_isStableUnderComposition, AlgebraicGeometry.instHasColimitsOfShapeDiscreteSchemeOfSmall, AlgebraicGeometry.IsFinite.instSndScheme, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, Hom.resLE_comp_resLE_assoc, AlgebraicGeometry.IsZariskiLocalAtSource.respectsLeft_isOpenImmersion, AffineZariskiSite.directedCover_f, AlgebraicGeometry.IsImmersion.instIsMultiplicativeScheme, AlgebraicGeometry.instIsAffineObjOppositeCommRingCatSchemeSpec, AlgebraicGeometry.AffineSpace.reindex_comp, AlgebraicGeometry.AffineSpace.map_SpecMap, AlgebraicGeometry.emptyIsInitial_to, AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme, isoSpec_Spec, GlueData.oneHypercover_p₂, AlgebraicGeometry.instGeometricallyIntegralFstScheme, AlgebraicGeometry.isOpenImmersion_eq_inf, Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.Surjective.comp_iff, AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero, iso_hom_base_inv_base, AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc, AlgebraicGeometry.sourceLocalClosure.instContainsIdentitiesScheme, AlgebraicGeometry.AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass, AlgebraicGeometry.sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange, stalkMap_hom_inv, AlgebraicGeometry.IsClosedImmersion.eq_inf, AlgebraicGeometry.sourceAffineLocally_respectsIso, monObjAsOverPullback_mul, AlgebraicGeometry.isClosedMap_isStableUnderComposition, AlgebraicGeometry.HasAffineProperty.instRespectsIsoScheme, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.instHasTerminalScheme, Modules.pseudofunctor_obj_obj, AlgebraicGeometry.IsClosedImmersion.isIso_lift, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, Hom.comp_preimage, kerFunctor_map, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, stalkMap_hom_inv_apply, AlgebraicGeometry.AffineSpace.reindex_comp_assoc, Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.Surjective.instSndScheme, Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, AlgebraicGeometry.AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass, Cover.pushforwardIso_f, isoOfEq_rfl, inv_appTop, AlgebraicGeometry.isPullback_Spec_map_pushout, AlgebraicGeometry.IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated, Hom.quasiFiniteAt_iff, AlgebraicGeometry.IsProper.comp_iff, AlgebraicGeometry.instIsOpenImmersionInlScheme, AlgebraicGeometry.universallyClosed_fst, Spec_map_stalkSpecializes_fromSpecStalk_assoc, AlgebraicGeometry.instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType, Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso, fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom, AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right, instIsOverFstOverInferInstanceOverClassId, AlgebraicGeometry.IsImmersion.instFstScheme, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, Cover.pullbackCoverOver_f, descResidueField_stalkClosedPointTo_fromSpecResidueField, Pullback.openCoverOfBase_X, AlgebraicGeometry.isOpenImmersion_sigmaDesc, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac, AlgebraicGeometry.coprodSpec_inr_assoc, instIsStableUnderSupQcPrecoverage, AlgebraicGeometry.AffineSpace.functor_obj_obj, AlgebraicGeometry.IsClosedImmersion.Spec_iff, Cover.toPresieveOver_le_arrows_iff, AlgebraicGeometry.isPreimmersion_eq_inf, Hom.comp_toLRSHom, AlgebraicGeometry.AffineSpace.map_id, Pullback.openCoverOfBase'_f, AlgebraicGeometry.instIsOpenImmersionMapWalkingSpanSchemeSpan, AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty, AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc, Pullback.ofPointTensor_SpecTensorTo, Hom.id_base, AlgebraicGeometry.AffineSpace.functor_map_app, AlgebraicGeometry.UniversallyOpen.eq, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.instIsMultiplicativeSchemeLocallyQuasiFinite, instIsIsoSubschemeιBotIdealSheafData, Cover.gluedCover_f, AlgebraicGeometry.isProper_eq, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, AlgebraicGeometry.UniversallyOpen.universally_isOpenMap, PartialMap.isOver_iff_eq_restrict, Opens.isoOfLE_inv_ι, Hom.ι_toNormalization_assoc, AlgebraicGeometry.instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Flat.comp, Cover.Hom.sigma_h₀, Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, Cover.LocallyDirected.trans_id, Hom.isoImage_inv_ι, AlgebraicGeometry.AffineSpace.map_comp_assoc, isSeparated_iff_isClosedImmersion_prod_lift, GlueData.ι_isoCarrier_inv, AlgebraicGeometry.IsFinite.instIsMultiplicativeScheme, Cover.toSigma_h₀, AlgebraicGeometry.universallyOpen_iff, IdealSheafData.range_glueDataObjι, Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange, Modules.pushforwardId_hom_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, Hom.ker_comp, coprodPresheafObjIso_hom_fst, AlgebraicGeometry.ExistsHomHomCompEqCompAux.ha, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, IdealSheafData.comapIso_hom_snd, AlgebraicGeometry.UniversallyClosed.universally_isClosedMap, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, instHasIsosQcPrecoverage, AlgebraicGeometry.smoothOfRelativeDimension_comp, directedAffineCover_trans, AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType, AlgebraicGeometry.instQuasiCompactFstScheme, coverOfIsIso_X, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.universallyClosed_eq_universallySpecializing, Pullback.Triplet.fst_SpecTensorTo_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.IsLocalIso.instIsMultiplicativeScheme, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1, Cover.LocallyDirected.property_trans, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsProperIsSeparated, AlgebraicGeometry.instIsOpenImmersionSigmaSpec, AlgebraicGeometry.topologically_respectsIso, AlgebraicGeometry.ExistsHomHomCompEqCompAux.hab, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange, AlgebraicGeometry.AffineSpace.homOfVector_over, Hom.inv_appTop, AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, PartialMap.restrict_hom, AlgebraicGeometry.FormallyUnramified.instIsMultiplicativeScheme, AffineZariskiSite.opensRange_relativeGluingData_map, Cover.ColimitGluingData.prop_trans, Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc, qcCoverFamily_property, AlgebraicGeometry.IsProper.instIsMultiplicativeScheme, AlgebraicGeometry.pullbackSpecIso_hom_fst, AlgebraicGeometry.IsProper.eq_valuativeCriterion, Pullback.base_affine_hasPullback, AlgebraicGeometry.locallyOfFinitePresentation_comp, instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition, AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono, AlgebraicGeometry.quasiSeparated_iff, AlgebraicGeometry.AffineSpace.reindex_over_assoc, IdealSheafData.comapIso_hom_fst_assoc, IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop, AlgebraicGeometry.QuasiCompactCover.instSumScheme_1, AlgebraicGeometry.IsSeparated.stableUnderComposition, AlgebraicGeometry.instIsAffineTerminalScheme, AlgebraicGeometry.Spec.map_comp, AffineZariskiSite.PreservesLocalization.isLocallyDirected, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometrically, AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective, AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyClosed, Cover.gluedCoverT'_fst_snd_assoc, AlgebraicGeometry.instIsOpenImmersionAppOverSchemeOpensDiagramι, Pullback.range_snd, Hom.stalkMap_comp, SpecΓIdentity_inv_app, Pullback.diagonalCoverDiagonalRange_eq_top_of_injective, Cover.coconeOfLocallyDirected_pt, AlgebraicGeometry.instLocallyOfFinitePresentationSndScheme, AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion, Cover.exists_eq, ofArrows_mem_precoverage_iff, AlgebraicGeometry.isClosedImmersion_equalizer_ι_left, Cover.ColimitGluingData.trans_app_left, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyInjective, AlgebraicGeometry.IsSeparated.instCompScheme, AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.Spec.homEquiv_apply, AffineCover.cover_X, AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme, jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Etale.etale_isStableUnderBaseChange, AlgebraicGeometry.coprodSpec_inl_assoc, Opens.fromSpecStalkOfMem_toSpecΓ, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, isoSpec_Spec_inv, AlgebraicGeometry.Spec.map_eqToHom, affineBasisCover_obj, Hom.comp_toLRSHom_assoc, Cover.ColimitGluingData.transitionMap_comp, AlgebraicGeometry.sigmaOpenCover_I₀, Cover.Hom.sigma_s₀, AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective, topIso_hom, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec, Hom.map_resLE, Cover.sigma_I₀, instEtaleF, AlgebraicGeometry.IsPreimmersion.instSndScheme, isSeparated_iff, inv_hom_apply, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, AlgebraicGeometry.SurjectiveOnStalks.instIsMultiplicativeScheme, AlgebraicGeometry.IsClosedImmersion.iff_isProper_and_mono, instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange, Cover.pushforwardIso_I₀, AlgebraicGeometry.sourceLocalClosure.instIsStableUnderBaseChangeScheme, comp_toLRSHom, AlgebraicGeometry.ι_sigmaSpec_assoc, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, IdealSheafData.subSchemeCover_map_inclusion_assoc, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, AlgebraicGeometry.isPullback_inr_inr_coprodMap, OpenCover.finiteSubcover_X, AlgebraicGeometry.instIsAffineHomCompScheme, Pullback.range_fst, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, AlgebraicGeometry.instIsMultiplicativeSchemeIsDominant, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, AlgebraicGeometry.instRespectsIsoSchemeTargetAffineLocallyOfToProperty, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.instIsClosedImmersionFstScheme, AlgebraicGeometry.AffineTargetMorphismProperty.isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget, Hom.resLE_comp_ι_assoc, AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange, AlgebraicGeometry.geometrically_inf, Hom.ι_fromNormalization_assoc, Cover.trans_comp, AlgebraicGeometry.instMonoCoprodScheme, stalkMap_inv_hom_apply, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, Hom.map_resLE_assoc, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, Hom.comp_base_assoc, OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, AlgebraicGeometry.coprodSpec_inl, GlueData.oneHypercover_X, AlgebraicGeometry.IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty, IdealSheafData.subSchemeCover_map_inclusion, Modules.conjugateEquiv_pullbackId_hom, AlgebraicGeometry.QuasiCompactCover.singleton, Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, Pullback.openCoverOfLeftRight_I₀, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, Modules.conjugateEquiv_pullbackComp_inv, smallGrothendieckTopology_eq_toGrothendieck_smallPretopology, AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, Hom.resLE_comp_ι, Hom.liftCoborder_ι_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_le, AlgebraicGeometry.IsAffine.affine, Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, IdealSheafData.inclusion_id_assoc, AlgebraicGeometry.instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat, AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme, Pullback.Triplet.ofPoint_s, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, coverOfIsIso_f, AlgebraicGeometry.Spec.map_inv, Pullback.instHasPullback, Modules.pseudofunctor_left_unitality, Hom.isoOpensRange_inv_comp_assoc, Modules.pseudofunctor_associativity_assoc, instHasPullbacksIsOpenImmersion, Hom.cover_I₀, AlgebraicGeometry.pullbackSpecIso_hom_base_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, Cover.gluedCoverT'_snd_snd, AlgebraicGeometry.universally_isZariskiLocalAtSource, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, AlgebraicGeometry.isPullback_SpecMap_pushout, Opens.instIsOverι, Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization_assoc, IdealSheafData.comapIso_hom_fst, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, GlueData.ι_isoLocallyRingedSpace_inv, IdealSheafData.map_id, iso_inv_base_hom_base_apply, Opens.fromSpecStalkOfMem_toSpecΓ_assoc, Hom.asFiberHom_fiberToSpecResidueField, Modules.pseudofunctor_mapComp_inv_τl, AlgebraicGeometry.locallyOfFiniteType_comp, Pullback.Triplet.exists_preimage, comp_appTop, Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.instIsLocallyNoetherianXScheme, AlgebraicGeometry.sigmaOpenCover_f, AlgebraicGeometry.topologically_isStableUnderComposition, AlgebraicGeometry.AffineSpace.over_over, stalkMap_inv_hom, instIsLocalAtTargetIsomorphismsZariskiPrecoverage, AlgebraicGeometry.Etale.etale_comp, OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, AlgebraicGeometry.isLocallyArtinian_iff_openCover, comp_base_apply, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv, AffineOpenCover.openCover_I₀, PartialMap.isOver_iff, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, Hom.toNormalization_normalizationPullback_fst_assoc, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly, OpenCover.restrict_I₀, AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom, AlgebraicGeometry.pullbackSpecIso_hom_fst'_assoc, Pullback.openCoverOfLeft_I₀, GlueData.glue_condition_assoc, AlgebraicGeometry.isIso_iff_stalk_iso, instIsOverMapStalkMapOverInferInstanceOverClass, AffineZariskiSite.cocone_ι_app, AlgebraicGeometry.geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc, forgetToLocallyRingedSpace_obj, AlgebraicGeometry.QuasiCompactCover.homCover, AlgebraicGeometry.instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.fromSpec_top, AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackFst, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, Hom.stalkMap_congr, instIsOpenImmersionF, AlgebraicGeometry.Flat.isIso_of_surjective_of_mono, instFullEtaleOverForget, affineOpenCover_f, AlgebraicGeometry.pullbackSpecIso_inv_fst', Cover.pullbackCoverOver'_f, Hom.comp_appTop, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec, AlgebraicGeometry.IsPreimmersion.instIsMultiplicativeScheme, Cover.gluedCoverT'_fst_snd, AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong, AlgebraicGeometry.IsPreimmersion.instFstScheme, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk', AlgebraicGeometry.pullback_of_geometrically', AlgebraicGeometry.instHasOfPostcompPropertySchemeIsAffineHomIsSeparated, AlgebraicGeometry.IsSeparated.instIsMultiplicativeScheme, IdealSheafData.glueDataObjHom_comp_assoc, AlgebraicGeometry.IsImmersion.instLiftSchemeId, AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionScheme, AlgebraicGeometry.universally_isZariskiLocalAtTarget, Hom.appLE_comp_appLE_assoc, Hom.liftCoborder_ι, canonicallyOverPullback_over, mem_smallGrothendieckTopology, Modules.pseudofunctor_left_unitality_assoc, AlgebraicGeometry.Flat.instIsStableUnderCompositionScheme, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, IdealSheafData.glueDataObjHom_comp, GlueData.oneHypercover_I₀, Cover.pushforwardIso_X, AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap, Hom.inl_toNormalization_normalizationCoprodIso_inv_assoc, IdealSheafData.inclusion_id, AlgebraicGeometry.spread_out_unique_of_isGermInjective, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc, AlgebraicGeometry.instIsIsoSchemeCoprodSpec, AffineZariskiSite.PreservesLocalization.opensRange_map, kerFunctor_obj, AlgebraicGeometry.diagonal_Spec_map, AlgebraicGeometry.instQuasiSeparatedFstScheme, Hom.stalkMap_congr_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, Modules.pseudofunctor_mapId_hom_τl, Cover.add_toPreZeroHypercover, AlgebraicGeometry.IsPreimmersion.instIsStableUnderBaseChangeScheme, AlgebraicGeometry.universally_isLocalAtSource, AffineZariskiSite.cocone_pt, AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange, stalkMap_inv_hom_assoc, AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left, Spec_obj, AlgebraicGeometry.IsFinite.instIsStableUnderCompositionScheme, AlgebraicGeometry.IsIntegralHom.instDescScheme, AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom, AlgebraicGeometry.AffineScheme.forgetToScheme_obj, AlgebraicGeometry.instIsMultiplicativeSchemeIsAffineHom, AlgebraicGeometry.ExistsHomHomCompEqCompAux.hb, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, Hom.comp_image, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, appLE_comp_appLE, affineBasisCover_map_range, Hom.resLE_comp_resLE, AlgebraicGeometry.IsLocalAtSource.iff_of_iSup_eq_top, Cover.map_prop, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, Cover.LocallyDirected.w, AlgebraicGeometry.IsSeparated.instRespectsIsoScheme, Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_of, AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange, grothendieckTopology_cover, Hom.isoImage_hom_ι, AlgebraicGeometry.Flat.isStableUnderBaseChange, AlgebraicGeometry.Flat.instSndScheme, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, Hom.toNormalization_fromNormalization, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyGeneralizingMap, Cover.Over.isOver_map, iso_hom_base_inv_base_apply, toIso_inv_ι, AlgebraicGeometry.IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, Spec_map, Hom.toNormalization_inl_normalizationCoprodIso_hom, Hom.opensRange_comp_of_isIso, AlgebraicGeometry.instRespectsSchemeSmoothIsOpenImmersion, Hom.inv_image, AlgebraicGeometry.isomorphisms_eq_stalkwise, homOfLE_ι_assoc, IsSeparated.isSeparated_terminal_from, AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange, AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian, residueFieldCongr_fromSpecResidueField_assoc, Hom.inr_toNormalization_normalizationCoprodIso_inv_assoc, AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme, instIsClosedImmersionLiftIdOfIsSeparated, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms, Cover.mkOfCovers_f, Hom.normalizationPullback_snd, Hom.opensRange_comp, AlgebraicGeometry.IsFinite.eq_inf, AlgebraicGeometry.HasAffineProperty.affineAnd_containsIdentities, Hom.ι_fromNormalization, Hom.comp_base, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme, mem_pretopology_iff, AlgebraicGeometry.affineLocally_le, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, IdealSheafData.comap_comp, AlgebraicGeometry.instLocallyQuasiFiniteCompScheme, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, residueFieldMap_id, GlueData.openCover_I₀, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι, GlueData.oneHypercover_f, AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyReduced, restrictFunctor_obj_left, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, IdealSheafData.subschemeMap_subschemeι_assoc, AlgebraicGeometry.instGeometricallyIrreducibleFstScheme, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget, AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme, AlgebraicGeometry.instSmoothSndScheme, Hom.stalkMap_id, AlgebraicGeometry.universallyClosed_iff, instFullLocallyRingedSpaceForgetToLocallyRingedSpace, instIsStableUnderBaseChangeQcPrecoverage, zariskiPrecoverage_le_qcPrecoverage, AlgebraicGeometry.IsPreimmersion.comp_iff, AlgebraicGeometry.pullbackSpecIso_hom_fst', IdealSheafData.glueDataObjι_ι, AlgebraicGeometry.IsImmersion.instSndScheme, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac_assoc, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, monObjAsOverPullback_one, AlgebraicGeometry.instIsOverHomOfLE, Modules.pseudofunctor_map_r, AlgebraicGeometry.isPullback_Spec_map_isPushout, AlgebraicGeometry.AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass, restrictFunctor_map_left, Hom.SpecMap_residueFieldMap_fromSpecResidueField, comp_app_assoc, Pullback.Triplet.ofPoint_y, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, Hom.appLE_comp_appLE, GlueData.oneHypercover_Y, AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top, Cover.ColimitGluingData.functor_map, Modules.restrictFunctorId_hom_app_app, SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat, AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.IsImmersion.isImmersion_iff_exists_of_quasiCompact, AlgebraicGeometry.isPullback_opens_inf_le, Γ_obj_op, Hom.stalkMap_inv_hom_apply, Cover.intersectionOfLocallyDirected_f, AlgebraicGeometry.quasiCompactCover_iff, Pullback.forget_comparison_surjective, Hom.isoImage_hom_ι_assoc, inv_base_hom_base_assoc, Hom.stalkMap_hom_inv_assoc, Modules.pseudofunctor_mapComp_inv_τr, AlgebraicGeometry.IsLocalAtSource.sigmaDesc, GlueData.oneHypercover_p₁, PartialMap.compHom_hom, Pullback.openCoverOfLeft_f, AlgebraicGeometry.IsSeparated.comp_iff, AlgebraicGeometry.spread_out_of_isGermInjective, Pullback.Triplet.ofPoint_SpecTensorTo, OpenCover.restrict_X, AlgebraicGeometry.UniversallyOpen.instCompScheme, AlgebraicGeometry.pullbackSpecIso_hom_snd, Hom.comp_appTop_assoc, AlgebraicGeometry.instSmoothFstScheme, Cover.mem_pretopology, AlgebraicGeometry.universallyClosed_respectsIso, AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1, AlgebraicGeometry.IsDominant.comp_iff, Hom.quasiFiniteAt_comp_iff, AlgebraicGeometry.instIsDominantCompScheme, AlgebraicGeometry.IsFinite.instContainsIdentitiesScheme, isEmpty_pullback, AlgebraicGeometry.IsIntegralHom.instCompScheme, coe_homeoOfIso, AlgebraicGeometry.UniversallyOpen.instRespectsIsoScheme, openCoverBasicOpenTop_f, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, Cover.gluedCoverT'_fst_fst_assoc, OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected, Cover.functorOfLocallyDirectedHomBase_app, AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom, AlgebraicGeometry.IsPreimmersion.comp, AlgebraicGeometry.AffineSpace.reindex_id, GlueData.ι_jointly_surjective, AlgebraicGeometry.quasiSeparated_isStableUnderComposition, AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.IsZariskiLocalAtSource.comp, AlgebraicGeometry.IsProper.instRespectsIsoScheme, AlgebraicGeometry.IsFinite.instHasOfPostcompPropertySchemeIsSeparated, AlgebraicGeometry.instIsZariskiLocalAtTargetDiagonalScheme, stalkClosedPointTo_comp, AlgebraicGeometry.pointsPi_surjective, pretopology_eq_inf, Opens.toSpecΓ_SpecMap_appLE, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, Cover.ColimitGluingData.functor_obj, AlgebraicGeometry.initial_isEmpty, pullbackComparison_forget_surjective, residueFieldMap_comp, isoSpec_image_zeroLocus, IdealSheafData.subschemeMap_subschemeι, comp_coeBase, AlgebraicGeometry.quasiSeparated_isStableUnderBaseChange, Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsSeparated.instFstScheme, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac, Pullback.openCoverOfLeftRight_X, mem_toGrothendieck_smallPretopology, IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop, Hom.stalkMap_inv_hom, AlgebraicGeometry.isSmoothOfRelativeDimension_isStableUnderBaseChange, Hom.inv_app, Hom.isoOpensRange_inv_comp, restrictFunctor_obj_hom, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, instFaithfulEtaleOverForget, IdealSheafData.subschemeFunctor_map, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left', AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom, Hom.Spec_map_residueFieldMap_fromSpecResidueField, pretopology_cover, instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace, isAffine_affineCover, AffineZariskiSite.directedCover_I₀, AlgebraicGeometry.IsSeparated.instSndScheme, AlgebraicGeometry.IsOpenImmersion.instSndScheme, Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField, AlgebraicGeometry.universallyClosed_eq, AlgebraicGeometry.coprodMk_inr, AffineOpenCover.openCover_X, isoOfEq_hom, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, Hom.asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, Hom.liftQuotient_comp_assoc, Pullback.exists_preimage_pullback, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, subcanonical_zariskiTopology, AlgebraicGeometry.IsOpenImmersion.mono, AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.IsImmersion.comp_iff, AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty, AlgebraicGeometry.IsOpenImmersion.comp_lift, AlgebraicGeometry.essImage_Spec, AlgebraicGeometry.IsOpenImmersion.lift_fac, AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc, AlgebraicGeometry.IsOpenImmersion.instFstScheme, AlgebraicGeometry.ValuativeCriterion.eq, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsEmbedding, Modules.pseudofunctor_mapId_inv_τl, Modules.pseudofunctor_associativity, Hom.eqToHom_app, Cover.sigma_f, id_app, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot, Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, Modules.pseudofunctor_mapId_inv_τr, RationalMap.isOver_iff, AffineZariskiSite.PreservesLocalization.isOpenImmersion, Pullback.affine_hasPullback, PartialMap.fromSpecStalkOfMem_toPartialMap, homOfLE_rfl, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.sourceLocalClosure.instRespectsRightScheme, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.UniversallyInjective.universally_injective, IdealSheafData.map_ker, AlgebraicGeometry.IsClosedImmersion.isIso_of_injective_of_isAffine, Pullback.openCoverOfLeft_X, stalkMap_congr, AlgebraicGeometry.Spec.homEquiv_symm_apply, AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation, AlgebraicGeometry.IsIntegralHom.comp_iff, Cover.gluedCover_t', Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor, Hom.stalkMap_congr_hom, AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms, AlgebraicGeometry.QuasiCompactCover.instPullback₂Scheme, Pullback.diagonalCover_map, inv_base_hom_base, AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso, Cover.ι_fromGlued, Hom.inl_toNormalization_normalizationCoprodIso_inv, Hom.inr_normalizationCoprodIso_hom_fromNormalization, Pullback.isAffine_of_isAffine_isAffine_isAffine, IdealSheafData.glueDataObjHom_id, AlgebraicGeometry.sourceLocalClosure.le, AlgebraicGeometry.pointOfClosedPoint_comp, AlgebraicGeometry.instHasAffinePropertyDiagonalSchemeDiagonal, Cover.mem_grothendieckTopology, Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, AlgebraicGeometry.pullback_of_geometrically, Opens.isoOfLE_inv_ι_assoc, AlgebraicGeometry.universallyClosed_snd, AlgebraicGeometry.QuasiCompactCover.instSumScheme, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.instIsSchemeTheoreticallyDominantCompScheme, AlgebraicGeometry.Spec.preimage_comp, isAffine_affineOpenCover, Hom.id_image, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc
|
instCoeFunHomForallCarrierCarrierCommRingCat 📖 | CompOp | — |
instCoeSortType 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | 4 mathmath: emptyTo_base, AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme, AlgebraicGeometry.emptyIsInitial_to, emptyTo_c_app
|
instPreorderCarrierCarrierCommRingCat 📖 | CompOp | 3 mathmath: height_of_isClosed, AlgebraicGeometry.AffineSpace.spec_le_iff, le_iff_specializes
|
instUniqueCarrierCarrierCommRingCatSpecOf 📖 | CompOp | 1 mathmath: default_asIdeal
|
sheaf 📖 | CompOp | 1 mathmath: AlgebraicGeometry.Spec_sheaf
|
toLocallyRingedSpace 📖 | CompOp | 1107 mathmath: 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, AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton, fromSpecStalk_closedPoint, coprodPresheafObjIso_hom_fst_assoc, Hom.toPartialMap_hom, AlgebraicGeometry.irreducibleSpace_of_isIntegral, height_of_isClosed, map_PrimeSpectrum_basicOpen_of_affine, isoOfEq_inv, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, zeroLocus_iInf, Modules.pushforwardId_inv_app_app, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, Hom.opensRange_pullbackSnd, AffineZariskiSite.instFaithfulOpensToOpensFunctor, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, Spec_map_stalkMap_fromSpecStalk, Hom.image_preimage_eq_opensRange_inter, Cover.LocallyDirected.directed, Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace, IsQuasiAffine.toIsImmersion, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, Hom.denseRange, isEmpty_pullback_iff, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, Hom.quasiFiniteLocus_comp, app_eq, Hom.closePoints_subset_preimage_closedPoints, support_nilradical, AlgebraicGeometry.opensCone_pt, zeroLocus_empty_eq_univ, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.morphismRestrict_base_coe, Hom.fiberHomeo_apply, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral, AlgebraicGeometry.IsAffineOpen.map_fromSpec, affineBasisCover_is_basis, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, Opens.toSpecΓ_naturality, Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.range_eq_range_of_surjective, comp_toLRSHom_assoc, restrictFunctorΓ_inv_app, Cover.isOpenMap_fromGlued, Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, Pullback.Triplet.ofPoint_x, 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, Hom.stalkMap_congr_point, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, fromSpecStalk_toSpecΓ_assoc, Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, Modules.pushforward_obj_obj, Hom.range_fiberι, Hom.preimage_bot, Cover.iUnion_range, mem_basicOpen', AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, Hom.mem_opensRange, zeroLocus_eq_univ_iff_subset_nilradical, Opens.topIso_inv, SpecToEquivOfField_eq_iff, AlgebraicGeometry.isCompact_iff_exists, Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Spec_presheaf, RationalMap.dense_domain, AlgebraicGeometry.HasRingHomProperty.stalkMap, Hom.resLE_eq_morphismRestrict, Hom.iUnion_support_ker_openCover_map_comp, inv_app, Hom.id_appTop, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, AlgebraicGeometry.image_morphismRestrict_preimage, IdealSheafData.gc, emptyTo_base, zeroLocus_mul, OpenCover.finiteSubcover_f, AlgebraicGeometry.SpecMap_preimage_basicOpen, ideal_ker_le_ker_ΓSpecIso_inv_comp, stalkMap_congr_assoc, AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, isoSpec_inv_toSpecΓ, Pullback.SpecTensorTo_SpecOfPoint, hom_inv_apply, Hom.range_asFiberHom, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, Hom.tendsto_cofinite_cofinite, ι_toIso_inv, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.noetherianSpace_of_isAffine, Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne, Modules.Hom.zero_app, IdealSheafData.equivOfIsAffine_symm_apply, congr_app, IdealSheafData.ideal_mul, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, Opens.stalkIso_inv, SpecΓIdentity_hom_app, AlgebraicGeometry.locallyQuasiFinite_iff, preimage_comp, Hom.stalkMap_congr_hom_assoc, Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, IdealSheafData.support_mul, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.IsFinite.instMorphismRestrict, Pullback.Triplet.isPullback_SpecMap_tensor, forget_map, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, Pullback.Triplet.specTensorTo_base_snd, isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.functionField_isScalarTower, Modules.toOpen_fromTildeΓ_app, Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, exists_germ_injective, forgetToTop_map, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, Cover.instIsIsoCommRingCatStalkMapFromGlued, Hom.preimage_top, coprodPresheafObjIso_hom_snd_assoc, Hom.toNormalization_app_preimage, Pullback.carrierEquiv_eq_iff, Hom.toImage_app_injective, isoSpec_hom, AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat, ι_toIso_inv_assoc, Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.instQuasiCompactMorphismRestrict, forget_obj, 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, forgetToTop_obj, AlgebraicGeometry.IsOpenImmersion.isOpen_range, affineOpenCover_idx, Hom.fromNormalization_preimage, toSpecΓ_naturality_assoc, Pullback.Triplet.snd_SpecTensorTo_apply, Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, compactSpace_of_isAffine, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, AlgebraicGeometry.IsIntegralHom.isIntegral_app, ker_ideal_of_isPullback_of_isOpenImmersion, presieve₀_mem_precoverage_iff, comp_base, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.isIso_iff_isIso_stalkMap, Hom.image_iSup₂, isoSpec_hom_naturality, zeroLocus_singleton, AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme, toSpecΓ_isoSpec_inv_assoc, Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.IsImmersion.instMorphismRestrict, Hom.isDiscrete_preimage_singleton, Hom.comp_app, IdealSheafData.range_glueDataObjι_ι_eq_support_inter, hom_base_inv_base, AlgebraicGeometry.isNoetherian_iff, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, toSpecΓ_naturality, Hom.quasiFiniteLocus_eq_top, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.IsNoetherian.toCompactSpace, AlgebraicGeometry.IsIntegral.nonempty, Hom.ι_toNormalization, IdealSheafData.ideal_pow, AlgebraicGeometry.IsNoetherian.noetherianSpace, range_fromSpecStalk, homeoOfIso_symm, comp_coeBase_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace, Hom.congr_app, Hom.preimage_iSup, Hom.toPartialMap_domain, AlgebraicGeometry.coprodMk_inl, Opens.toSpecΓ_naturality_assoc, Pullback.Triplet.hy, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, Hom.id_app, Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop, Pullback.carrierEquiv_symm_fst, Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Proj.mem_basicOpen, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, preimage_basicOpen_top, ΓSpecIso_inv, Hom.app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.quasiCompact_over_affine_iff, Pullback.range_fst_comp, Hom.coequifibered_normalizationDiagramMap, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace, isoSpec_hom_naturality_assoc, isoSpec_inv_image_zeroLocus, IdealSheafData.range_glueDataObjι_ι, germToFunctionField_injective, Hom.isIso_base, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', hom_base_inv_base_assoc, 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, Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.isBasis_preimage_isAffineOpen, Cover.isOpenEmbedding_fromGlued, Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.affineLocally_iff_affineOpens_le, fromSpecStalk_appTop, OpenCover.isOpenCover_opensRange, Modules.toPresheaf_obj, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, Hom.isCompact_preimage_singleton, Opens.toScheme_presheaf_obj, Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, IdealSheafData.vanishingIdeal_ideal, Pullback.Triplet.Spec_map_tensor_isPullback, id_appTop, Cover.covers, Spec_map_presheaf_map_eqToHom, Opens.toSpecΓ_appTop_assoc, Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, stalkMap_congr_point_assoc, GlueData.isOpen_iff, 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, Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.isInitial_iff_isEmpty, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, Γevaluation_naturality_apply, basicOpen_le, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, Modules.isSheaf, Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, Cover.exists_lift_trans_eq, zeroLocus_def, stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, Hom.preimage_smoothLocus_eq, AlgebraicGeometry.tilde.isoTop_hom, coe_homeoOfIso_symm, AlgebraicGeometry.IsArtinianScheme.finite, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, stalkMap_hom_inv_assoc, ModuleCat.Tilde.toOpen_res, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, IdealSheafData.mem_supportSet_iff, id.base, IdealSheafData.range_subschemeι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme, Opens.toSpecΓ_appTop, IdealSheafData.mem_support_iff, IdealSheafData.le_support_iff_le_vanishingIdeal, Hom.isClosedMap, Hom.isLocallyClosed_range, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, residue_descResidueField, AlgebraicGeometry.Γ_restrict_isLocalization, Hom.appIso_inv_app_presheafMap, Opens.toScheme_carrier, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, Modules.restrictFunctorComp_hom_app_app, Hom.preimageIso_inv_ι, descResidueField_fromSpecResidueField, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Hom.apply_mem_image_iff, Hom.asFiberHom_apply, Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.Proj.basicOpen_mul, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, homeoOfIso_apply, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, IdealSheafData.le_ofIdeals_iff, Hom.preimage_basicOpen_top, Modules.restrict_map, PartialMap.restrict_id, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.AffineSpace.spec_le_iff, IsLocallyDirected.homOfLE_tAux, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat, Opens.exists_toScheme, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, instIsOverMapResidueFieldMapOverInferInstanceOverClass, OpenCover.iSup_opensRange, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat, Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, Pullback.carrierEquiv_symm_snd, IdealSheafData.coe_support_ofIdealTop, IdealSheafData.support_antitone, Hom.isIso_toLRSHom, component_nontrivial, AlgebraicGeometry.isCompl_range_inl_inr, zeroLocus_iInf_of_nonempty, AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, basicOpen_pow, Opens.toSpecΓ_top, AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace, Hom.ker_apply, IdealSheafData.ideal_comap_of_isOpenImmersion, Pullback.range_map, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, Hom.isSpectralMap, IdealSheafData.support_eq_top_iff, AlgebraicGeometry.mem_range_iff_of_surjective, AffineZariskiSite.restrictIsoSpec_hom_app, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, Modules.toPresheaf_map, Hom.appIso_inv_app, Hom.liftCoborder_preimage, stalkMap_congr_hom_assoc, Hom.opensRange_pullbackFst, IdealSheafData.mem_supportSet_iff_mem_support, zeroLocus_radical, Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.compactSpace_iff_quasiCompact, AffineZariskiSite.presieveOfSections_surjective, Opens.ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.disjoint_opensRange_sigmaι, comp_base_assoc, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, stalkMap_id, Spec.residue_residueFieldIso_hom_assoc, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, Hom.appIso_inv_naturality, basicOpen_add_le, Hom.comp_app_assoc, comp_app, Hom.finite_app, AlgebraicGeometry.isIso_iff_isOpenImmersion, AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, GlueData.ι_eq_iff, Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, Hom.appIso_hom', zeroLocus_inf, AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.surjective_iff, 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, SpecMap_stalkMap_fromSpecStalk_assoc, Hom.preimage_basicOpen, singleton_mem_precoverage_iff, IdealSheafData.subschemeι_app, AlgebraicGeometry.IsLocallyArtinian.discreteTopology, Hom.isOpenMap, PartialMap.equiv_iff_of_isSeparated, isoSpec_Spec_hom, basicOpen_res_eq, Pullback.Triplet.hx, Hom.isAffineOpen_iff_of_isOpenImmersion, Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, image_basicOpen, AlgebraicGeometry.tilde.isIso_toOpen_top, instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.IsProper.instMorphismRestrict, isPullback_toSpecΓ_toSpecΓ, Hom.genericPoint_mem_smoothLocus_of_perfectField, instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, AlgebraicGeometry.IsArtinianScheme.toCompactSpace, ΓSpecIso_naturality, Hom.stalkMap_hom_inv, IdealSheafData.support_comap, restrictFunctorΓ_hom_app, stalkMap_congr_hom, Modules.restrictFunctorCongr_hom_app_app, IdealSheafData.vanishingIdeal_sup, Pullback.range_snd_comp, Modules.restrictFunctorId_inv_app_app, Modules.pushforwardComp_hom_app_app, AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField, iso_inv_base_hom_base, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.range_eq_univ, toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, Hom.comp_apply, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, Modules.mapPresheaf_app, Hom.isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Proj.basicOpen_mono, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, residueFieldCongr_trans, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.pointOfClosedPoint_apply, toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', Hom.isEmbedding, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.opensCone_π_app, toSpecΓ_appTop, Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, IdealSheafData.support_eq_bot_iff, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton, stalkMap_comp, residue_surjective, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, Hom.comp_appIso, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing, basicOpen_one, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.over_def, Modules.Hom.id_app, IdealSheafData.map_vanishingIdeal, Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, Hom.appIso_inv_app_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, Hom.ker_eq_top_iff_isEmpty, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, Cover.ulift_I₀, Modules.Hom.isIso_iff_isIso_app, Hom.residueFieldMap_congr, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, Opens.ι_appTop, Modules.Hom.comp_app, Hom.map_mem_image_iff, IdealSheafData.support_iSup, coprodPresheafObjIso_hom_snd, map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, AlgebraicGeometry.coprodSpec_coprodMk, IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.isRetrocompact_basicOpen, Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, Hom.injective, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, AlgebraicGeometry.quasiSeparatedSpace_of_isAffine, isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, AlgebraicGeometry.Spec_carrier, AlgebraicGeometry.isArtinianScheme_iff, Hom.id_appIso, empty_carrier_carrier, AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology, Hom.preimageIso_inv_ι_assoc, Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.isAffineHom_iff, Hom.asFiberHom_fiberι, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, comp_appTop_assoc, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, local_affine, AlgebraicGeometry.Proj.basicOpen_one, IdealSheafData.ideal_top, AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, IsLocallyDirected.ι_eq_ι_iff, isoSpec_Spec, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.compactSpace_iff_exists, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible, Hom.preimage_sup, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, Spec.algebraMap_residueFieldIso_inv, iso_hom_base_inv_base, stalkMap_congr_point, eq_zeroLocus_of_isClosed_of_isAffine, Opens.ι_preimage_self, stalkMap_hom_inv, residueFieldCongr_refl, toSpecΓ_image_zeroLocus, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, Hom.image_iSup, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, Hom.comp_preimage, Modules.instIsIsoAbApp, Hom.naturality_assoc, IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, stalkMap_hom_inv_apply, Hom.iInf_ker_openCover_map_comp_apply, Hom.isOpen_quasiFiniteAt, inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, Hom.quasiFiniteAt_iff, AlgebraicGeometry.morphismRestrict_appTop, Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.Proj.isBasis_basicOpen, descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, Hom.comp_toLRSHom, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.geometricallyIrreducible_iff, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, Hom.fiberι_asFiber, AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, default_asIdeal, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, Hom.id_base, IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, Modules.Hom.sub_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AffineCover.covers, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, Hom.ι_toNormalization_assoc, Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsFinite.finite_preimage_singleton, AlgebraicGeometry.IsLocalAtTarget.restrict, Hom.fromNormalization_app_assoc, isoSpec_inv_toSpecΓ_assoc, IdealSheafData.ideal_iInf, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, Hom.isoImage_inv_ι, GlueData.ι_isoCarrier_inv, IdealSheafData.range_glueDataObjι, Hom.isoImage_inv_ι_assoc, Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, ker_morphismRestrict_ideal, Modules.pushforwardId_hom_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, coprodPresheafObjIso_hom_fst, toOpen_eq, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, 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, Pullback.Triplet.fst_SpecTensorTo_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, Modules.Hom.add_app, IdealSheafData.isClosed_supportSet, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.isBasis_affine_open, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, Hom.inv_appTop, AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.Spec_zeroLocus, basicOpen_mul, ΓSpecIso_inv_naturality, IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, zeroLocus_biInf_of_nonempty, AlgebraicGeometry.Flat.stalkMap, Pullback.range_snd, Hom.stalkMap_comp, SpecΓIdentity_inv_app, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType, Cover.exists_eq, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, ofArrows_mem_precoverage_iff, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom, IsLocallyDirected.ι_jointly_surjective, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.IsPreimmersion.base_embedding, 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, Hom.isClosedEmbedding, Hom.comp_toLRSHom_assoc, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, Opens.forall_toScheme, topIso_hom, AlgebraicGeometry.Proj.awayMap_awayToSection, Hom.finite_preimage_singleton, AlgebraicGeometry.finite_appTop_of_universallyClosed, AffineZariskiSite.toOpens_mono, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, inv_hom_apply, AlgebraicGeometry.instIsPreimmersionFromSpecStalk, AlgebraicGeometry.IsIntegralHom.integral_app, residue_residueFieldMap_assoc, IdealSheafData.support_map, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.specTargetImageFactorization_app_injective, comp_toLRSHom, IsGermInjectiveAt.cond, IdealSheafData.zeroLocus_inter_subset_supportSet, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, Hom.preimage_inf, AlgebraicGeometry.isPullback_morphismRestrict, IdealSheafData.map_ideal', residue_residueFieldCongr, Hom.appIso_hom, OpenCover.finiteSubcover_X, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, Pullback.range_fst, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, residue_residueFieldMap, IdealSheafData.ideal_sup, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, Hom.ι_fromNormalization_assoc, emptyTo_c_app, stalkMap_inv_hom_apply, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact, IsQuasiAffine.toCompactSpace, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, Opens.mem_basicOpen_toScheme, Hom.comp_base_assoc, AlgebraicGeometry.affineAnd_apply, SpecMap_residue_apply, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, Hom.image_le_opensRange, AlgebraicGeometry.noetherianSpace_of_isAffineOpen, 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, instIsPreimmersionMapResidue, Hom.mem_smoothLocus, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, AlgebraicGeometry.instSmoothMorphismRestrict, IdealSheafData.ideal_mono, empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, Opens.ι_app_self, zeroLocus_span, IdealSheafData.ideal_iSup, Hom.naturality, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, Hom.image_injective, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.Spec_toLocallyRingedSpace, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, IdealSheafData.vanishingIdeal_top, AlgebraicGeometry.Proj.basicOpen_zero, AlgebraicGeometry.formallyUnramified_iff, Pullback.Triplet.ofPoint_s, mem_basicOpen_top, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.isClosedImmersion_iff, Opens.ι_image_basicOpen', AlgebraicGeometry.Spec_closedPoint, Hom.range_subset_ker_support, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, Hom.finite_preimage, Opens.ι_apply, Modules.instFullPresheafOfModulesToPresheafOfModules, Hom.dense_smoothLocus_of_perfectField, AlgebraicGeometry.quasiCompact_iff_compactSpace, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, GlueData.ι_isoLocallyRingedSpace_inv, basicOpen_res, iso_inv_base_hom_base_apply, Hom.continuous, Hom.asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.Smooth.exists_isStandardSmooth, Pullback.Triplet.exists_preimage, comp_appTop, Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.Surjective.surj, IdealSheafData.radical_ideal, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AffineZariskiSite.mem_grothendieckTopology, stalkMap_inv_hom, comp_base_apply, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, IdealSheafData.ideal_inf, Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.IsDominant.denseRange, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Flat.iff_flat_stalkMap, IdealSheafData.subschemeι_app_surjective, preimage_zeroLocus, AlgebraicGeometry.isIso_iff_stalk_iso, instIsOverMapStalkMapOverInferInstanceOverClass, AffineZariskiSite.cocone_ι_app, forgetToLocallyRingedSpace_obj, Hom.smoothLocus_eq_top, AlgebraicGeometry.Spec.map_base, IdealSheafData.coe_support_inter, AlgebraicGeometry.compactSpace_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.fromSpec_top, Hom.support_ker, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, Hom.homeomorph_apply, Hom.stalkMap_congr, Hom.isIso_toPshHom, IdealSheafData.support_top, map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, Hom.comp_appTop, AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier, germ_stalkClosedPointTo_Spec, basicOpen_zero, Hom.surjective, residue_residueFieldCongr_assoc, 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.isAffineOpen_bot, IsLocallyDirected.V_self, Opens.ι_image_le, Hom.stalkMap_congr_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, mem_basicOpen'', AlgebraicGeometry.stalkClosedPointIso_inv, AffineZariskiSite.cocone_pt, AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne, stalkMap_inv_hom_assoc, Cover.RelativeGluingData.preimage_toBase_eq_range_ι, AlgebraicGeometry.tilde.toOpen_map_app_assoc, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, 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, Cover.instEpiTopCatBaseCommRingCatFromGlued, affineBasisCover_map_range, residue_descResidueField_assoc, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, Opens.ι_app, Hom.QuasiFiniteAt.isClopen_singleton_asFiber, Modules.pushforwardCongr_inv_app_app, IdealSheafData.supportSet_inter, AlgebraicGeometry.instIsPreimmersionAsFiberHom, AlgebraicGeometry.locallyOfFinitePresentation_iff, Hom.isoImage_hom_ι, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, AlgebraicGeometry.quasiCompact_iff_spectral, iso_hom_base_inv_base_apply, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, toIso_inv_ι, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, Hom.instIsIsoCommRingCatApp, residueFieldCongr_trans_hom, Hom.opensRange_comp_of_isIso, Hom.inv_image, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, Hom.opensRange_comp, Hom.ι_fromNormalization, Hom.comp_base, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.genericPoint_eq_bot_of_affine, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, IdealSheafData.coe_support_vanishingIdeal, Γevaluation_naturality, AlgebraicGeometry.IsSeparated.instMorphismRestrict, PartialMap.dense_domain, AlgebraicGeometry.basicOpen_eq_bot_iff, Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, Hom.appIso_inv_app_apply, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, restrictFunctor_obj_left, AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, Hom.stalkMap_id, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, IdealSheafData.ideal_biInf, isLocalHom_stalkClosedPointTo, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', basicOpen_restrict, IdealSheafData.support_bot, Hom.opensRange_of_isIso, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, preimage_basicOpen, Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff, restrictFunctor_map_left, Hom.SpecMap_residueFieldMap_fromSpecResidueField, affineOpenCover_X, comp_app_assoc, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, Pullback.Triplet.ofPoint_y, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, PartialMap.le_domain_toRationalMap, Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, Opens.ι_image_top, Hom.toImage_app, range_fromSpecResidueField, Modules.restrictFunctorId_hom_app_app, SpecMap_stalkMap_fromSpecStalk, zeroLocus_isClosed, AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, Modules.Hom.app_smul, Γ_obj_op, Hom.stalkMap_inv_hom_apply, 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, isBasis_affineOpens, Hom.fiberToSpecResidueField_apply, inv_base_hom_base_assoc, Opens.topIso_hom, Hom.stalkMap_hom_inv_assoc, IdealSheafData.support_sup, IsLocallyDirected.homOfLE_tAux_assoc, Pullback.Triplet.ofPoint_SpecTensorTo, OpenCover.restrict_X, zeroLocus_univ, JointlySurjective.exists_eq, Hom.image_le_image_iff, Hom.comp_appTop_assoc, AlgebraicGeometry.AffineSpace.map_appTop_coord, toSpecΓ_preimage_basicOpen, residueFieldCongr_trans_hom_assoc, Hom.app_appIso_inv, AlgebraicGeometry.isIso_fromTildeΓ_iff, residueFieldCongr_inv, coe_homeoOfIso, Hom.normalizationObjIso_hom_val, openCoverBasicOpenTop_f, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, Hom.appLE_eq_app, RationalMap.mem_domain, IdealSheafData.support_sSup, AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.spec_punit_isEmpty, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian, AlgebraicGeometry.isReduced_stalk_of_isReduced, image_preimage_eq_of_isPullback, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, GlueData.ι_jointly_surjective, IdealSheafData.vanishingIdeal_iSup, IdealSheafData.strictMono_ideal, codisjoint_zeroLocus, PartialMap.restrict_id_hom, stalkClosedPointTo_comp, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.initial_isEmpty, residueFieldMap_comp, AlgebraicGeometry.Etale.instMorphismRestrict, isoSpec_image_zeroLocus, Hom.fiberι_fiberHomeo_symm, comp_coeBase, IdealSheafData.ideal_map_of_isAffineHom, Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, Modules.pushforward_map_app, mem_toGrothendieck_smallPretopology, Hom.stalkMap_inv_hom, AlgebraicGeometry.coe_opensRestrict_apply_coe, AffineZariskiSite.presieveOfSections_eq_ofArrows, Hom.inv_app, localRingHom_comp_stalkIso, restrictFunctor_obj_hom, AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian, Hom.app_injective, Modules.inv_app, Hom.Spec_map_residueFieldMap_fromSpecResidueField, Opens.toSpecΓ_preimage_zeroLocus, Cover.fromGlued_open_map, AlgebraicGeometry.coprodMk_inr, instEpiCommRingCatResidue, Hom.isProperMap, isoOfEq_hom, le_iff_specializes, Hom.asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, Spec.residue_residueFieldIso_hom, IdealSheafData.vanishingIdeal_sSup, AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, IdealSheafData.map_ideal_basicOpen, AffineZariskiSite.toOpensFunctor_obj, localRingHom_comp_stalkIso_apply, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, Hom.isOpen_smoothLocus, mem_zeroLocus_iff, Hom.fromNormalization_app, AlgebraicGeometry.Spec_stalkClosedPointIso, Opens.ι_base_apply, Hom.eqToHom_app, AlgebraicGeometry.instIsAffineHomιBasicOpen, id_app, AlgebraicGeometry.flat_iff, zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, residueFieldCongr_symm, PartialMap.fromSpecStalkOfMem_toPartialMap, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, homOfLE_rfl, fromSpecResidueField_apply, AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, Hom.coe_opensRange, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, IdealSheafData.le_def, stalkMap_congr, AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, Hom.stalkMap_congr_hom, inv_base_hom_base, IdealSheafData.vanishingIdeal_bot, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.quasiSeparated_over_affine_iff, IdealSheafData.subschemeι_apply, IdealSheafData.supportSet_eq_iInter_zeroLocus, Modules.map_smul, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, affineBasicOpen_le, Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.Spec.map_app, Spec_fromSpecStalk, Cover.fromGlued_injective, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.Spec.map_base_apply, AlgebraicGeometry.morphismRestrict_id, Hom.stalkMap_surjective, AlgebraicGeometry.tilde.toOpen_map_app, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, Hom.id_image, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
|
zeroLocus 📖 | CompOp | 47 mathmath: zeroLocus_iInf, zeroLocus_empty_eq_univ, zeroLocus_eq_univ_iff_subset_nilradical, zeroLocus_mul, isoSpec_inv_preimage_zeroLocus, zeroLocus_biInf, zeroLocus_iUnion, zeroLocus_singleton, IdealSheafData.mem_support_iff_of_mem, isoSpec_inv_image_zeroLocus, IdealSheafData.range_glueDataObjι_ι, zeroLocus_setMul, toSpecΓ_preimage_zeroLocus, zeroLocus_mono, zeroLocus_def, IdealSheafData.mem_supportSet_iff, IdealSheafData.mem_support_iff, IdealSheafData.coe_support_ofIdealTop, zeroLocus_iInf_of_nonempty, zeroLocus_radical, zeroLocus_map, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, zeroLocus_inf, zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, eq_zeroLocus_of_isClosed_of_isAffine, toSpecΓ_image_zeroLocus, AlgebraicGeometry.Spec_zeroLocus, IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, zeroLocus_biInf_of_nonempty, IdealSheafData.supportSet_subset_zeroLocus, IdealSheafData.zeroLocus_inter_subset_supportSet, zeroLocus_span, preimage_zeroLocus, IdealSheafData.coe_support_inter, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, IdealSheafData.mem_supportSet_iff_of_mem, IdealSheafData.supportSet_inter, zeroLocus_isClosed, image_zeroLocus, zeroLocus_univ, codisjoint_zeroLocus, isoSpec_image_zeroLocus, Opens.toSpecΓ_preimage_zeroLocus, mem_zeroLocus_iff, zeroLocus_map_of_eq, IdealSheafData.supportSet_eq_iInter_zeroLocus
|
Γ 📖 | CompOp | 24 mathmath: AlgebraicGeometry.ΓSpec.isIso_adjunction_counit, restrictFunctorΓ_inv_app, AlgebraicGeometry.preservesColimit_Γ, AlgebraicGeometry.instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj, SpecΓIdentity_hom_app, Γ_obj, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.ΓSpec.adjunction_counit_app, Γ_def, SpecΓIdentity_app, AlgebraicGeometry.ΓSpec.adjunction_unit_app, restrictFunctorΓ_hom_app, Γ_map_op, AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeSchemeΓ, Γ_map, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, SpecΓIdentity_inv_app, AlgebraicGeometry.preservesLimit_rightOp_Γ, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, Γ_obj_op, AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone
|
ΓSpecIso 📖 | CompOp | 64 mathmath: ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, germ_stalkClosedPointTo, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, ideal_ker_le_ker_ΓSpecIso_inv_comp, SpecΓIdentity_hom_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, ΓSpecIso_inv, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, fromSpecStalk_appTop, Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.ΓSpec.adjunction_counit_app, Opens.toSpecΓ_appTop, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.ΓSpecIso_obj_hom, SpecΓIdentity_app, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, isoSpec_Spec_hom, ΓSpecIso_naturality, AlgebraicGeometry.germ_stalkClosedPointIso_hom, toSpecΓ_appTop, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, isoSpec_Spec, Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, toOpen_eq, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.Spec_zeroLocus, ΓSpecIso_inv_naturality, SpecΓIdentity_inv_app, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, isoSpec_Spec_inv, germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, fromSpecStalk_app, Spec.algebraMap_residueFieldIso_inv_assoc, germ_stalkClosedPointTo_Spec, AlgebraicGeometry.basicOpen_eq_of_affine, ΓSpecIso_naturality_assoc, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, Spec_fromSpecStalk
|
| Name | Category | Theorems |
app 📖 | CompOp | 116 mathmath: AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, germ_stalkMap_assoc, app_invApp'_assoc, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, toNormalization_app_preimage, toImage_app_injective, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, comp_app, ι_toNormalization, AlgebraicGeometry.Scheme.comp_appLE, congr_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, id_app, germ_stalkMap_apply, app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, app_surjective, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, appIso_inv_app_presheafMap, app_eq, comp_appLE, ker_apply, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, appIso_inv_app, comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, finite_app, AlgebraicGeometry.Scheme.evaluation_naturality, ideal_ker_le, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, preimage_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, app_invApp', comp_appLE_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.evaluation_naturality_apply, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, appIso_inv_app_assoc, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, AlgebraicGeometry.Scheme.homOfLE_app, naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, isIso_app, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, ι_toNormalization_assoc, fromNormalization_app_assoc, AlgebraicGeometry.Scheme.stalkMap_germ_apply, instIsIsoCommRingCatAppObjOpensOpensFunctor, germ_stalkMap, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, isIntegral_app, app_eq_appLE, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.IsIntegralHom.integral_app, appIso_hom, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.evaluation_naturality_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.Scheme.Opens.ι_app_self, naturality, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.Scheme.Opens.ι_app, instIsIsoCommRingCatApp, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, appIso_inv_app_apply, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.morphismRestrict_app, toImage_app, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, app_appIso_inv, normalizationObjIso_hom_val, appLE_eq_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, inv_app, app_injective, AlgebraicGeometry.Scheme.stalkMap_germ, AlgebraicGeometry.Scheme.comp_appLE_assoc, fromNormalization_app, eqToHom_app, AlgebraicGeometry.Scheme.id_app, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.Spec.map_app
|
appLE 📖 | CompOp | 92 mathmath: AlgebraicGeometry.Etale.etale_appLE, AlgebraicGeometry.LocallyQuasiFinite.quasiFinite_appLE, AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, formallyUnramified_appLE, appLE_map', smooth_appLE, AlgebraicGeometry.Scheme.comp_appLE, AlgebraicGeometry.Scheme.ofRestrict_appLE, QuasiFiniteAt.quasiFiniteAt, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.HasRingHomProperty.iff_of_iSup_eq_top, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE, AlgebraicGeometry.Spec.map_appLE, finitePresentation_appLE, AlgebraicGeometry.morphismRestrict_appLE, comp_appLE, AlgebraicGeometry.FormallyUnramified.formallyUnramified_of_affine_subset, AlgebraicGeometry.formallySmooth_stalkMap_iff, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, AlgebraicGeometry.HasRingHomProperty.appLE, map_appLE_assoc, map_appLE'_assoc, AlgebraicGeometry.smooth_iff, appIso_hom', appLE_appIso_inv, comp_appLE_assoc, AlgebraicGeometry.morphismRestrict_app', appLE_map_assoc, appIso_inv_appLE_assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, etale_appLE, appLE_congr, AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE, appLE_appIso_inv_assoc, AlgebraicGeometry.Scheme.homOfLE_appLE, AlgebraicGeometry.Scheme.basicOpen_appLE, AlgebraicGeometry.Flat.flat_of_affine_subset, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, app_eq_appLE, map_appLE', AlgebraicGeometry.Flat.flat_appLE, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE, finiteType_appLE, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, AlgebraicGeometry.smoothOfRelativeDimension_iff, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE, appLE_appIso_inv_apply, appLE_map'_assoc, AlgebraicGeometry.formallyUnramified_iff, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, AlgebraicGeometry.isIso_pushoutSection_iff, AlgebraicGeometry.Smooth.smooth_appLE, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset, appLE_comp_appLE_assoc, AlgebraicGeometry.etale_iff, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, AlgebraicGeometry.Scheme.Opens.ι_appLE, AlgebraicGeometry.Scheme.appLE_comp_appLE, resLE_appLE, AlgebraicGeometry.locallyOfFinitePresentation_iff, map_appLE, AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, flat_appLE, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, appLE_comp_appLE, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, appLE_map, normalizationObjIso_hom_val, appLE_eq_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.comp_appLE_assoc, AlgebraicGeometry.flat_iff, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map, appIso_inv_appLE, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
|
appTop 📖 | CompOp | 71 mathmath: AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, id_appTop, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.ΓSpecIso_obj_hom, preimage_basicOpen_top, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.Γ_map_op, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.Scheme.Γ_map, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, inv_appTop, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.finite_appTop_of_universallyClosed, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, comp_appTop, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, comp_appTop_assoc, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
|
arrowStalkMapIsoOfEq 📖 | CompOp | — |
copyBase 📖 | CompOp | 1 mathmath: copyBase_eq
|
homeomorph 📖 | CompOp | 1 mathmath: homeomorph_apply
|
stalkMap 📖 | CompOp | 76 mathmath: germ_stalkMap_assoc, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, AlgebraicGeometry.surjectiveOnStalks_iff, stalkMap_congr_point, AlgebraicGeometry.HasRingHomProperty.stalkMap, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, stalkMap_congr_hom_assoc, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.IsAffineOpen.stalkMap_injective, germ_stalkMap_apply, stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, AlgebraicGeometry.formallySmooth_stalkMap_iff, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.stalkMap_id, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, stalkMap_hom_inv, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.Scheme.stalkMap_comp, stalkMap_inv_hom_assoc, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, stalkSpecializes_stalkMap_apply, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective, AlgebraicGeometry.Scheme.stalkMap_germ_apply, germ_stalkMap, AlgebraicGeometry.stalkMap_injective_of_isAffine, AlgebraicGeometry.Flat.stalkMap, stalkMap_comp, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, mem_smoothLocus, stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, stalkMap_congr, stalkMap_congr_assoc, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, stalkMap_id, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, stalkMap_inv_hom_apply, stalkMap_hom_inv_assoc, instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, stalkMap_inv_hom, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.stalkMap_germ, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, isOpen_smoothLocus, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.stalkMap_congr, stalkMap_congr_hom, stalkMap_surjective
|
toLRSHom 📖 | CompOp | 24 mathmath: AlgebraicGeometry.Scheme.comp_toLRSHom_assoc, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base, AlgebraicGeometry.Scheme.forgetToTop_map, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_map, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.morphismRestrict_appLE, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, isIso_toLRSHom, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, id_appIso, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom, comp_toLRSHom, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, comp_toLRSHom_assoc, AlgebraicGeometry.Scheme.comp_toLRSHom, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk', AlgebraicGeometry.Scheme.Opens.ι_appLE, opensRange_comp_of_isIso, inv_image, opensRange_of_isIso, id_image
|
toLRSHom' 📖 | CompOp | 560 mathmath: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_resLE, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, opensRange_pullbackSnd, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, image_preimage_eq_opensRange_inter, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.QuasiCompact.isCompact_preimage, app_invApp'_assoc, denseRange, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, closePoints_subset_preimage_closedPoints, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.morphismRestrict_base_coe, fiberHomeo_apply, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.range_eq_range_of_surjective, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.morphismRestrict_ι_assoc, stalkMap_congr_point, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, range_fiberι, preimage_bot, AlgebraicGeometry.Scheme.Cover.iUnion_range, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, mem_opensRange, AlgebraicGeometry.isCompact_iff_exists, AlgebraicGeometry.HasRingHomProperty.stalkMap, resLE_eq_morphismRestrict, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.Scheme.emptyTo_base, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, AlgebraicGeometry.SpecMap_preimage_basicOpen, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, AlgebraicGeometry.Scheme.hom_inv_apply, range_asFiberHom, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, tendsto_cofinite_cofinite, preimage_le_preimage_of_le, stalkSpecializes_stalkMap, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint, preimageIso_hom_ι_assoc, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.Scheme.preimage_comp, stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.IsPreimmersion.isEmbedding, SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, toNormalization_app_preimage, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, toImage_app_injective, id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset, image_preimage_le, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc, fromNormalization_preimage, iSup_preimage_eq_top, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, AlgebraicGeometry.Scheme.comp_base, image_preimage_eq_opensRange_inf, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.IsImmersion.instMorphismRestrict, isDiscrete_preimage_singleton, comp_app, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.Scheme.hom_base_inv_base, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, ι_toNormalization, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.Scheme.comp_coeBase_assoc, congr_app, preimage_iSup, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.hy, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, asFiberHom_fiberι_assoc, AlgebraicGeometry.Scheme.preimage_basicOpen_top, app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.Scheme.opensRange_homOfLE, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, isIso_base, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Scheme.hom_base_inv_base_assoc, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, preimage_image_eq, quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, isCompact_preimage_singleton, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, mem_preimage, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, isConstructible_preimage, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, preimage_smoothLocus_eq, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.id.base, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme, isClosedMap, isLocallyClosed_range, AlgebraicGeometry.opensDiagram_map, appIso_inv_app_presheafMap, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, app_eq, AlgebraicGeometry.morphismRestrict_ι, preimageIso_inv_ι, apply_mem_image_iff, asFiberHom_apply, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.homeoOfIso_apply, preimage_basicOpen_top, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.isCompl_range_inl_inr, ker_apply, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, isSpectralMap, AlgebraicGeometry.mem_range_iff_of_surjective, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, isLocallyConstructible_image, appIso_inv_app, liftCoborder_preimage, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, opensRange_pullbackFst, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.Scheme.comp_base_assoc, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, finite_app, AlgebraicGeometry.isIso_iff_isOpenImmersion, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.exists_preimage_eq, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, ideal_ker_le, appIso_hom', AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.surjective_iff, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, preimage_basicOpen, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, isOpenMap, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, app_invApp', stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.IsProper.instMorphismRestrict, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, stalkMap_hom_inv, AlgebraicGeometry.Scheme.IdealSheafData.support_comap, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι, AlgebraicGeometry.Scheme.iso_inv_base_hom_base, AlgebraicGeometry.range_eq_univ, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, comp_apply, isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.pointOfClosedPoint_apply, AlgebraicGeometry.morphismRestrict_app', isEmbedding, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AlgebraicGeometry.Scheme.stalkMap_comp, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, appIso_inv_app_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, residueFieldMap_congr, map_mem_image_iff, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, AlgebraicGeometry.coprodSpec_coprodMk, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, injective, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, preimageIso_inv_ι_assoc, AlgebraicGeometry.isAffineHom_iff, asFiberHom_fiberι, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.compactSpace_iff_exists, preimage_sup, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Scheme.iso_hom_base_inv_base, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.Scheme.homOfLE_app, comp_preimage, naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, isIso_app, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, stalkSpecializes_stalkMap_apply, AlgebraicGeometry.morphismRestrict_appTop, exists_mem_and_isIso_morphismRestrict_toNormalization, preimage_opensRange, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, fiberι_asFiber, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, id_base, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.AffineCover.covers, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι, ι_toNormalization_assoc, Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsFinite.finite_preimage_singleton, AlgebraicGeometry.IsLocalAtTarget.restrict, fromNormalization_app_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, preimage_iSup_eq_top, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, isIntegral_app, app_eq_appLE, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.Flat.stalkMap, AlgebraicGeometry.Scheme.Pullback.range_snd, stalkMap_comp, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective, AlgebraicGeometry.IsPreimmersion.base_embedding, coe_image, coe_preimage, isClosedEmbedding, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.IsFinite.finite_app, finite_preimage_singleton, AlgebraicGeometry.Scheme.inv_hom_apply, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_map, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, preimage_inf, AlgebraicGeometry.isPullback_morphismRestrict, appIso_hom, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, comp_base_assoc, AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, mem_smoothLocus, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, naturality, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.isClosedImmersion_iff, AlgebraicGeometry.Spec_closedPoint, range_subset_ker_support, finite_preimage, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply, continuous, asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, isConstructible_image, stalkMap_hom_inv_apply, AlgebraicGeometry.Surjective.surj, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.Scheme.comp_base_apply, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.IsDominant.denseRange, AlgebraicGeometry.Scheme.homOfLE_base, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.Spec.map_base, support_ker, homeomorph_apply, stalkMap_congr, isIso_toPshHom, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, preimage_mono, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, surjective, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.isFinite_iff, stalkMap_congr_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, AlgebraicGeometry.Scheme.Opens.ι_app, QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.instIsPreimmersionAsFiberHom, isCompact_preimage, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, instIsIsoCommRingCatApp, inv_image, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, comp_base, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.IsSeparated.instMorphismRestrict, appIso_inv_app_apply, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, AlgebraicGeometry.morphismRestrict_app, toImage_app, AlgebraicGeometry.Scheme.range_fromSpecResidueField, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, stalkMap_inv_hom_apply, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.image_zeroLocus, fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.inv_base_hom_base_assoc, stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.Scheme.JointlySurjective.exists_eq, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, app_appIso_inv, AlgebraicGeometry.Scheme.coe_homeoOfIso, normalizationObjIso_hom_val, appLE_eq_app, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback, instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.residueFieldMap_comp, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, fiberι_fiberHomeo_symm, AlgebraicGeometry.Scheme.comp_coeBase, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, stalkMap_inv_hom, inv_app, isQuasiSeparated_preimage, app_injective, Spec_map_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, AlgebraicGeometry.coprodMk_inr, isProperMap, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen, isOpen_smoothLocus, fromNormalization_app, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Opens.ι_base_apply, eqToHom_app, isDiscrete_preimage, AlgebraicGeometry.Scheme.homOfLE_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, AlgebraicGeometry.Scheme.fromSpecResidueField_apply, coe_opensRange, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, stalkMap_congr_hom, AlgebraicGeometry.Scheme.inv_base_hom_base, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Cover.fromGlued_injective, AlgebraicGeometry.Spec.map_base_apply, AlgebraicGeometry.morphismRestrict_id, stalkMap_surjective, AlgebraicGeometry.Scheme.toSpecΓ_base
|