LocallyRingedSpace

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

Statistics

Metric	Count
Definitions LocallyRingedSpace, stalkMap, toHom, toShHom, comp, empty, emptyIsInitial, emptyTo, forgetToSheafedSpace, forgetToTop, homMk, homOfSheafedSpaceHomOfIsIso, id, instCategory, instCoeSortType, instEmptyCollection, instInhabitedHom, instQuiver, instUniqueHomEmptyCollection, isoOfSheafedSpaceIso, ofRestrict, restrict, restrictStalkIso, restrictTopIso, toRingedSpace, toSheafedSpace, toTopCat, Γ, 𝒪	29
Theorems ext, ext', ext'_iff, ext_iff, prop, toShHom_mk, basicOpen_eq_bot_of_isNilpotent, basicOpen_zero, comp_base, comp_c, comp_c_app, comp_toHom, comp_toShHom, component_nontrivial, forgetToSheafedSpace_map, forgetToSheafedSpace_obj, forgetToTop_map, forgetToTop_obj, homMk_toHom, homOfSheafedSpaceHomOfIsIso_toHom, id_toHom, id_toShHom', instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace, instIsLocalRingCarrierStalkCommRingCatPresheaf, instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace, isLocalHomStalkMap, isLocalHomStalkMap', isLocalHomValStalkMap, isLocalRing, is_sheafedSpace_iso, iso_hom_base_inv_base, iso_hom_base_inv_base_apply, iso_inv_base_hom_base, iso_inv_base_hom_base_apply, ofRestrict_stalkMap_isIso, preimage_basicOpen, restrictStalkIso_hom_eq_germ, restrictStalkIso_hom_eq_germ_apply, restrictStalkIso_hom_eq_germ_assoc, restrictStalkIso_inv_eq_germ, restrictStalkIso_inv_eq_germ_apply, restrictStalkIso_inv_eq_germ_assoc, restrictStalkIso_inv_eq_ofRestrict, restrict_carrier, restrict_presheaf_map, restrict_presheaf_obj, 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, Γ_def, Γ_map, Γ_map_op, Γ_obj, Γ_obj_op	71
Total	100

AlgebraicGeometry

Definitions

Name	Category	Theorems
LocallyRingedSpace 📖	CompData	151 math math: LocallyRingedSpace.stalkMap_hom_inv_assoc, LocallyRingedSpace.residueFieldMap_comp, LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace, ΓSpec.locallyRingedSpaceAdjunction_counit_app, LocallyRingedSpace.Γ_def, LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, LocallyRingedSpace.IsOpenImmersion.lift_fac, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, IsOpenImmersion.hasLimit_cospan_forget_of_right', Spec_Γ_naturality, LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, Scheme.comp_toLRSHom_assoc, LocallyRingedSpace.instHasCoequalizers, LocallyRingedSpace.id_toShHom', LocallyRingedSpace.GlueData.ι_isOpenImmersion, LocallyRingedSpace.IsOpenImmersion.lift_fac_assoc, Spec.locallyRingedSpaceMap_id, LocallyRingedSpace.preservesColimits_forgetToSheafedSpace, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, LocallyRingedSpace.iso_inv_base_hom_base_apply, LocallyRingedSpace.Γ_obj_op, ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, LocallyRingedSpace.stalkMap_inv_hom, LocallyRingedSpace.stalkMap_congr, Scheme.forgetToLocallyRingedSpace_map, LocallyRingedSpace.Γ_Spec_left_triangle, instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, IsOpenImmersion.hasLimit_cospan_forget_of_left, LocallyRingedSpace.stalkMap_inv_hom_assoc, ΓSpec.adjunction_counit_app', ΓSpec.locallyRingedSpaceAdjunction_counit_app', LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, LocallyRingedSpace.stalkMap_congr_assoc, IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, Spec.toLocallyRingedSpace_obj, LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, LocallyRingedSpace.toΓSpec_continuous, Scheme.Γ_def, ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, LocallyRingedSpace.stalkMap_id, LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, LocallyRingedSpace.IsOpenImmersion.comp, IsOpenImmersion.hasLimit_cospan_forget_of_right, Scheme.Hom.isIso_toLRSHom, ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, LocallyRingedSpace.comp_base, LocallyRingedSpace.IsOpenImmersion.mono, LocallyRingedSpace.stalkMap_inv_hom_apply, LocallyRingedSpace.comp_toShHom, ΓSpec.left_triangle, ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace, Spec.locallyRingedSpaceMap_comp, LocallyRingedSpace.IsOpenImmersion.pullback_snd_of_left, LocallyRingedSpace.GlueData.ι_jointly_surjective, ΓSpec.isIso_locallyRingedSpaceAdjunction_counit, LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, LocallyRingedSpace.IsOpenImmersion.hasPullback_of_left, Scheme.local_affine, Scheme.IsLocallyDirected.instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace, instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ, LocallyRingedSpace.stalkMap_hom_inv, Scheme.fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom, LocallyRingedSpace.IsOpenImmersion.to_iso, LocallyRingedSpace.Γ_map, Scheme.Hom.comp_toLRSHom, ΓSpec.adjunction_homEquiv_apply, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, ProjectiveSpectrum.Proj.isIso_toSpec, LocallyRingedSpace.forgetToTop_map, ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, LocallyRingedSpace.instHasColimitsOfShapeDiscrete, LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, LocallyRingedSpace.toΓSpec_base, ΓSpec.locallyRingedSpaceAdjunction_unit, instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, Scheme.Hom.comp_toLRSHom_assoc, Scheme.comp_toLRSHom, ΓSpec.right_triangle, LocallyRingedSpace.iso_inv_base_hom_base, LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, ΓSpec.adjunction_homEquiv_symm_apply, LocallyRingedSpace.instHasCoequalizer, Spec_Γ_naturality_assoc, ΓSpec.toSpecΓ_of, LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion, LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, Scheme.GlueData.ι_isoLocallyRingedSpace_inv, LocallyRingedSpace.instHasColimits, LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, Scheme.forgetToLocallyRingedSpace_obj, LocallyRingedSpace.comp_toHom, LocallyRingedSpace.residueFieldMap_id, LocallyRingedSpace.forgetToTop_obj, LocallyRingedSpace.forgetToSheafedSpace_map, LocallyRingedSpace.Γ_map_op, Spec.toLocallyRingedSpace_map, Scheme.affineBasisCover_map_range, LocallyRingedSpace.stalkMap_congr_hom_assoc, IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, LocallyRingedSpace.SpecΓIdentity_hom_app, Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace, LocallyRingedSpace.toΓSpecMapBasicOpen_eq, LocallyRingedSpace.GlueData.f_open, Scheme.affineOpenCover_X, LocallyRingedSpace.toStalk_stalkMap_toΓSpec, LocallyRingedSpace.id_toHom, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, LocallyRingedSpace.toΓSpecCBasicOpens_app, isIso_toSpecΓ, LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, LocallyRingedSpace.toΓSpecCApp_spec, LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, LocallyRingedSpace.stalkMap_comp, LocallyRingedSpace.stalkMap_hom_inv_apply, LocallyRingedSpace.forgetToSheafedSpace_obj, LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, LocallyRingedSpace.IsOpenImmersion.pullback_fst_of_right, LocallyRingedSpace.iso_hom_base_inv_base, LocallyRingedSpace.SpecΓIdentity_inv_app, IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, IsOpenImmersion.hasLimit_cospan_forget_of_left', Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace, Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, LocallyRingedSpace.comp_c_app, LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, LocallyRingedSpace.IsOpenImmersion.hasPullback_of_right, LocallyRingedSpace.stalkMap_congr_hom, LocallyRingedSpace.preservesCoequalizer, LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, LocallyRingedSpace.iso_hom_base_inv_base_apply, LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft, ΓSpec.toSpecΓ_unop, LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, LocallyRingedSpace.toΓSpecCApp_iff, LocallyRingedSpace.comp_c, ΓSpec.locallyRingedSpaceAdjunction_counit, LocallyRingedSpace.Γ_obj, LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right

AlgebraicGeometry.LocallyRingedSpace

Definitions

Name	Category	Theorems
comp 📖	CompOp	—
empty 📖	CompOp	—
emptyIsInitial 📖	CompOp	—
emptyTo 📖	CompOp	—
forgetToSheafedSpace 📖	CompOp	31 math math: instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, Γ_def, IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, preservesColimits_forgetToSheafedSpace, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace, IsOpenImmersion.forgetToTop_preservesPullback_of_left, IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, GlueData.ι_isoSheafedSpace_inv_assoc, IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, IsOpenImmersion.forget_reflectsPullback_of_left, AlgebraicGeometry.ΓSpec.toSpecΓ_of, forgetToSheafedSpace_map, toΓSpecMapBasicOpen_eq, instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, forgetToSheafedSpace_obj, IsOpenImmersion.forget_reflectsPullback_of_right, toΓSpec_preimage_basicOpen_eq, preservesCoequalizer, GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, IsOpenImmersion.forget_preservesPullbackOfLeft, IsOpenImmersion.forget_preservesPullback_of_right
forgetToTop 📖	CompOp	2 math math: forgetToTop_map, forgetToTop_obj
homMk 📖	CompOp	1 math math: homMk_toHom
homOfSheafedSpaceHomOfIsIso 📖	CompOp	1 math math: homOfSheafedSpaceHomOfIsIso_toHom
id 📖	CompOp	—
instCategory 📖	CompOp	147 math math: stalkMap_hom_inv_assoc, residueFieldMap_comp, instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, Γ_def, IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, IsOpenImmersion.lift_fac, IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right', AlgebraicGeometry.Spec_Γ_naturality, notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.comp_toLRSHom_assoc, instHasCoequalizers, id_toShHom', GlueData.ι_isOpenImmersion, IsOpenImmersion.lift_fac_assoc, AlgebraicGeometry.Spec.locallyRingedSpaceMap_id, preservesColimits_forgetToSheafedSpace, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, toΓSpecSheafedSpace_app_eq, iso_inv_base_hom_base_apply, Γ_obj_op, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, stalkMap_inv_hom, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_map, Γ_Spec_left_triangle, AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left, stalkMap_inv_hom_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, AlgebraicGeometry.Spec.toLocallyRingedSpace_obj, coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, toΓSpec_continuous, AlgebraicGeometry.Scheme.Γ_def, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, stalkMap_id, GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, IsOpenImmersion.comp, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right, AlgebraicGeometry.Scheme.Hom.isIso_toLRSHom, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, comp_base, IsOpenImmersion.mono, stalkMap_inv_hom_apply, comp_toShHom, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace, AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp, IsOpenImmersion.pullback_snd_of_left, GlueData.ι_jointly_surjective, AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit, IsOpenImmersion.forgetToTop_preservesPullback_of_left, IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, IsOpenImmersion.hasPullback_of_left, AlgebraicGeometry.Scheme.local_affine, AlgebraicGeometry.Scheme.IsLocallyDirected.instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ, stalkMap_hom_inv, AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom, IsOpenImmersion.to_iso, Γ_map, AlgebraicGeometry.Scheme.Hom.comp_toLRSHom, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, forgetToTop_map, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, GlueData.ι_isoSheafedSpace_inv_assoc, instHasColimitsOfShapeDiscrete, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, toΓSpec_base, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit, AlgebraicGeometry.instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, AlgebraicGeometry.Scheme.Hom.comp_toLRSHom_assoc, AlgebraicGeometry.Scheme.comp_toLRSHom, AlgebraicGeometry.ΓSpec.right_triangle, iso_inv_base_hom_base, IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, IsOpenImmersion.forget_reflectsPullback_of_left, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, instHasCoequalizer, AlgebraicGeometry.Spec_Γ_naturality_assoc, AlgebraicGeometry.ΓSpec.toSpecΓ_of, IsOpenImmersion.pullback_to_base_isOpenImmersion, IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, instHasColimits, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_obj, comp_toHom, residueFieldMap_id, forgetToTop_obj, forgetToSheafedSpace_map, Γ_map_op, AlgebraicGeometry.Spec.toLocallyRingedSpace_map, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, toΓSpec_preimage_zeroLocus_eq, SpecΓIdentity_hom_app, AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace, toΓSpecMapBasicOpen_eq, GlueData.f_open, AlgebraicGeometry.Scheme.affineOpenCover_X, toStalk_stalkMap_toΓSpec, id_toHom, toΓSpecSheafedSpace_app_spec, toΓSpecCBasicOpens_app, AlgebraicGeometry.isIso_toSpecΓ, IsOpenImmersion.pullback_snd_isIso_of_range_subset, toΓSpecSheafedSpace_app_spec_assoc, toΓSpecCApp_spec, toΓSpecSheafedSpace_hom_c_app, instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, stalkMap_comp, stalkMap_hom_inv_apply, forgetToSheafedSpace_obj, IsOpenImmersion.forget_reflectsPullback_of_right, IsOpenImmersion.pullback_fst_of_right, iso_hom_base_inv_base, SpecΓIdentity_inv_app, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left', AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, comp_c_app, toΓSpec_preimage_basicOpen_eq, IsOpenImmersion.hasPullback_of_right, preservesCoequalizer, GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, iso_hom_base_inv_base_apply, IsOpenImmersion.instSndPullbackConeOfLeft, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, IsOpenImmersion.isoRestrict_inv_ofRestrict, toΓSpecCApp_iff, comp_c, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit, Γ_obj, IsOpenImmersion.forget_preservesPullbackOfLeft, IsOpenImmersion.forget_preservesPullback_of_right
instCoeSortType 📖	CompOp	—
instEmptyCollection 📖	CompOp	—
instInhabitedHom 📖	CompOp	—
instQuiver 📖	CompOp	6 math math: stalkMap_congr, stalkMap_congr_assoc, Γ_map, Γ_map_op, stalkMap_congr_hom_assoc, stalkMap_congr_hom
instUniqueHomEmptyCollection 📖	CompOp	—
isoOfSheafedSpaceIso 📖	CompOp	—
ofRestrict 📖	CompOp	10 math math: IsOpenImmersion.ofRestrict, ofRestrict_stalkMap_isIso, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, restrictStalkIso_inv_eq_ofRestrict, IsOpenImmersion.ofRestrict_invApp, IsOpenImmersion.isoRestrict_hom_ofRestrict, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, IsOpenImmersion.instOfRestrict, IsOpenImmersion.isoRestrict_inv_ofRestrict, IsOpenImmersion.ofRestrict_invApp_apply
restrict 📖	CompOp	47 math math: AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, restrict_presheaf_obj, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, restrictStalkIso_hom_eq_germ, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, IsOpenImmersion.ofRestrict, restrictStalkIso_inv_eq_germ_apply, restrict_carrier, restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.Scheme.local_affine, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, ofRestrict_stalkMap_isIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, restrict_presheaf_map, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, restrictStalkIso_inv_eq_ofRestrict, IsOpenImmersion.ofRestrict_invApp, IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, IsOpenImmersion.instOfRestrict, IsOpenImmersion.isoRestrict_inv_ofRestrict, IsOpenImmersion.ofRestrict_invApp_apply
restrictStalkIso 📖	CompOp	9 math math: restrictStalkIso_hom_eq_germ, restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, restrictStalkIso_inv_eq_germ_apply, restrictStalkIso_hom_eq_germ_apply, restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, restrictStalkIso_hom_eq_germ_assoc, restrictStalkIso_inv_eq_germ
restrictTopIso 📖	CompOp	—
toRingedSpace 📖	CompOp	11 math math: basicOpen_eq_bot_iff_forall_evaluation_eq_zero, basicOpen_zero, preimage_basicOpen, Γevaluation_eq_zero_iff_notMem_basicOpen, Γevaluation_ne_zero_iff_mem_basicOpen, toΓSpec_preimage_zeroLocus_eq, evaluation_ne_zero_iff_mem_basicOpen, basicOpen_eq_bot_of_isNilpotent, toΓSpecMapBasicOpen_eq, evaluation_eq_zero_iff_notMem_basicOpen, toΓSpec_preimage_basicOpen_eq
toSheafedSpace 📖	CompOp	1232 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.irreducibleSpace_of_isIntegral, AlgebraicGeometry.Scheme.height_of_isClosed, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, AlgebraicGeometry.Scheme.isoOfEq_inv, stalkMap_hom_inv_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.zeroLocus_iInf, AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, residueFieldMap_comp, AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Scheme.Hom.denseRange, restrict_presheaf_obj, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, AlgebraicGeometry.Scheme.support_nilradical, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral, AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.range_eq_range_of_surjective, notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff, restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, AlgebraicGeometry.Scheme.Hom.range_fiberι, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.Scheme.Hom.preimage_bot, restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.Cover.iUnion_range, IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.mem_basicOpen', AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.Scheme.Hom.mem_opensRange, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.Scheme.SpecToEquivOfField_eq_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.isCompact_iff_exists, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.Scheme.RationalMap.dense_domain, AlgebraicGeometry.HasRingHomProperty.stalkMap, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, homMk_toHom, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, AlgebraicGeometry.Scheme.inv_app, id_toShHom', AlgebraicGeometry.Scheme.Hom.id_appTop, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.Scheme.IdealSheafData.gc, AlgebraicGeometry.Scheme.emptyTo_base, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.Scheme.zeroLocus_mul, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.SpecMap_preimage_basicOpen, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, AlgebraicGeometry.Scheme.hom_inv_apply, AlgebraicGeometry.Scheme.Hom.range_asFiberHom, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite, AlgebraicGeometry.Scheme.ι_toIso_inv, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.noetherianSpace_of_isAffine, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.Scheme.preimage_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.IdealSheafData.support_mul, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_toSheafedSpace, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.Scheme.forgetToTop_map, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.forget_obj, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.Scheme.forgetToTop_obj, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, IsOpenImmersion.stalk_iso, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.compactSpace_of_isAffine, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_iUnion, AlgebraicGeometry.IsReduced.component_reduced, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, AlgebraicGeometry.Scheme.comp_base, Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.isIso_iff_isIso_stalkMap, stalkMap_inv_hom, AlgebraicGeometry.Scheme.Hom.image_iSup₂, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.zeroLocus_singleton, AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, component_nontrivial, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.Scheme.hom_base_inv_base, stalkMap_congr, AlgebraicGeometry.isNoetherian_iff, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.IsNoetherian.toCompactSpace, AlgebraicGeometry.IsIntegral.nonempty, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, Γ_Spec_left_triangle, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, AlgebraicGeometry.IsNoetherian.noetherianSpace, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.Scheme.homeoOfIso_symm, AlgebraicGeometry.Scheme.comp_coeBase_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.Scheme.Hom.toPartialMap_domain, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.hy, stalkMap_inv_hom_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Hom.id_app, AlgebraicGeometry.Scheme.Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Proj.mem_basicOpen, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.quasiCompact_over_affine_iff, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.Scheme.germToFunctionField_injective, AlgebraicGeometry.Scheme.Hom.isIso_base, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', AlgebraicGeometry.Scheme.hom_base_inv_base_assoc, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, AlgebraicGeometry.Scheme.zeroLocus_setMul, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AlgebraicGeometry.Scheme.Opens.nonempty_iff, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, HasCoequalizer.imageBasicOpen_image_open, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Modules.toPresheaf_obj, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, stalkMap_congr_assoc, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.isInitial_iff_isEmpty, isLocalHomStalkMap, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.basicOpen_le, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.Scheme.Modules.isSheaf, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.Scheme.zeroLocus_def, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.tilde.isoTop_hom, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.IsArtinianScheme.finite, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, ModuleCat.Tilde.toOpen_res, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, AlgebraicGeometry.Scheme.id.base, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Scheme.residue_descResidueField, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Opens.toScheme_carrier, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_apply, stalkMap_id, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.Proj.basicOpen_mul, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.homeoOfIso_apply, IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Modules.restrict_map, AlgebraicGeometry.Scheme.PartialMap.restrict_id, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.AffineSpace.spec_le_iff, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, residue_comp_residueFieldMap_eq_stalkMap_comp_residue, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.Opens.exists_toScheme, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.Scheme.IdealSheafData.support_antitone, AlgebraicGeometry.Scheme.component_nontrivial, AlgebraicGeometry.isCompl_range_inl_inr, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.Scheme.basicOpen_pow, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, comp_base, AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.isSpectralMap, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, AlgebraicGeometry.mem_range_iff_of_surjective, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.Modules.toPresheaf_map, restrictStalkIso_inv_eq_germ_apply, IsOpenImmersion.inv_invApp, stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support, AlgebraicGeometry.Scheme.zeroLocus_radical, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.compactSpace_iff_quasiCompact, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, AlgebraicGeometry.Scheme.Opens.ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.Scheme.comp_base_assoc, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.Scheme.stalkMap_id, comp_toShHom, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, AlgebraicGeometry.Spec.locallyRingedSpaceObj_toSheafedSpace, restrict_carrier, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.isIso_iff_isOpenImmersion, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.Scheme.zeroLocus_inf, AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.surjective_iff, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.isLocalIso_iff, AlgebraicGeometry.AffineSpace.hom_ext_iff, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.IsLocallyArtinian.discreteTopology, AlgebraicGeometry.Scheme.Hom.isOpenMap, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, Hom.ext_iff, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.tilde.isIso_toOpen_top, AlgebraicGeometry.Scheme.instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated, IsOpenImmersion.invApp_app, Hom.prop, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, IsOpenImmersion.app_invApp_assoc, IsOpenImmersion.app_invApp, AlgebraicGeometry.HasRingHomProperty.appTop, basicOpen_zero, AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.IsProper.instMorphismRestrict, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.IsArtinianScheme.toCompactSpace, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, AlgebraicGeometry.Scheme.IdealSheafData.support_comap, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField, AlgebraicGeometry.Scheme.iso_inv_base_hom_base, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.range_eq_univ, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Proj.basicOpen_mono, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, AlgebraicGeometry.Scheme.residueFieldCongr_trans, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.pointOfClosedPoint_apply, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton, AlgebraicGeometry.Scheme.stalkMap_comp, AlgebraicGeometry.Scheme.residue_surjective, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing, AlgebraicGeometry.Scheme.basicOpen_one, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.over_def, AlgebraicGeometry.Scheme.Modules.Hom.id_app, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, AlgebraicGeometry.Scheme.Cover.ulift_I₀, IsOpenImmersion.instIsIsoCommRingCatInvApp, Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.Modules.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, AlgebraicGeometry.coprodSpec_coprodMk, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.isRetrocompact_basicOpen, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, AlgebraicGeometry.quasiSeparatedSpace_of_isAffine, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, AlgebraicGeometry.Spec_carrier, AlgebraicGeometry.isArtinianScheme_iff, AlgebraicGeometry.Scheme.Hom.id_appIso, AlgebraicGeometry.Scheme.empty_carrier_carrier, AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, AlgebraicGeometry.Proj.basicOpen_one, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.Scheme.isoSpec_Spec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.compactSpace_iff_exists, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible, AlgebraicGeometry.Scheme.Hom.preimage_sup, ofRestrict_stalkMap_isIso, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.Scheme.iso_hom_base_inv_base, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.residueFieldCongr_refl, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.Scheme.Hom.image_iSup, evaluation_naturality, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.Scheme.Hom.isOpen_quasiFiniteAt, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff, isLocalHomStalkMap', stalkMap_hom_inv, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.Proj.isBasis_basicOpen, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, Γ_map, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.geometricallyIrreducible_iff, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, AlgebraicGeometry.Scheme.Hom.fiberι_asFiber, AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.Scheme.default_asIdeal, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.Hom.id_base, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, restrict_presheaf_map, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.AffineCover.covers, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsFinite.finite_preimage_singleton, AlgebraicGeometry.IsLocalAtTarget.restrict, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, forgetToTop_map, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, homOfSheafedSpaceHomOfIsIso_toHom, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, instIsLocalRingCarrierStalkCommRingCatPresheaf, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, AlgebraicGeometry.Scheme.Modules.restrict_obj, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.Scheme.Modules.Hom.add_app, AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.isBasis_affine_open, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, GlueData.ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.Scheme.Hom.inv_appTop, AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, AlgebraicGeometry.Flat.stalkMap, AlgebraicGeometry.Scheme.Pullback.range_snd, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, toΓSpec_base, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType, 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.basicOpen_eq_of_affine', AlgebraicGeometry.IsPreimmersion.base_embedding, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Scheme.Hom.coe_preimage, stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.forall_toScheme, AlgebraicGeometry.Scheme.topIso_hom, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, AlgebraicGeometry.finite_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.Scheme.inv_hom_apply, AlgebraicGeometry.instIsPreimmersionFromSpecStalk, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_map, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', AlgebraicGeometry.Scheme.residue_residueFieldCongr, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, isLocalRing, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, iso_inv_base_hom_base, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact, AlgebraicGeometry.Scheme.IsQuasiAffine.toCompactSpace, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.Scheme.Hom.comp_base_assoc, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, AlgebraicGeometry.Scheme.Hom.image_le_opensRange, AlgebraicGeometry.noetherianSpace_of_isAffineOpen, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, AlgebraicGeometry.smoothOfRelativeDimension_iff, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE, AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, AlgebraicGeometry.Scheme.empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, AlgebraicGeometry.Scheme.zeroLocus_span, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, AlgebraicGeometry.Scheme.Hom.image_injective, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, AlgebraicGeometry.Proj.basicOpen_zero, IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.formallyUnramified_iff, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.isClosedImmersion_iff, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', Γevaluation_naturality_assoc, AlgebraicGeometry.Spec_closedPoint, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, is_sheafedSpace_iso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.Hom.finite_preimage, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField, AlgebraicGeometry.quasiCompact_iff_compactSpace, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.Surjective.surj, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.Scheme.comp_base_apply, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.IsDominant.denseRange, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top, AlgebraicGeometry.Spec.map_base, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.compactSpace_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.fromSpec_top, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, AlgebraicGeometry.Scheme.Hom.homeomorph_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.Scheme.Hom.isIso_toPshHom, AlgebraicGeometry.Scheme.IdealSheafData.support_top, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.Scheme.Hom.comp_appTop, AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.Scheme.Hom.surjective, AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, HasCoequalizer.imageBasicOpen_image_preimage, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, comp_toHom, restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.etale_iff, AlgebraicGeometry.isAffineOpen_bot, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, AlgebraicGeometry.Scheme.Opens.ι_image_le, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, forgetToTop_obj, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, AlgebraicGeometry.tilde.toOpen_map_app_assoc, forgetToSheafedSpace_map, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.basicOpen_eq_of_affine, Γ_map_op, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, AlgebraicGeometry.Scheme.Hom.comp_image, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued, isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.residue_descResidueField_assoc, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.instIsPreimmersionAsFiberHom, AlgebraicGeometry.locallyOfFinitePresentation_iff, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, stalkMap_congr_hom_assoc, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.Scheme.toIso_inv_ι, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.opensRange_comp, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, toΓSpec_preimage_zeroLocus_eq, restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Scheme.Hom.comp_base, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.genericPoint_eq_bot_of_affine, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.IsSeparated.instMorphismRestrict, AlgebraicGeometry.Scheme.PartialMap.dense_domain, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, AlgebraicGeometry.Scheme.restrictFunctor_obj_left, AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.Scheme.Hom.stalkMap_id, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, Γevaluation_naturality, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.Scheme.basicOpen_restrict, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap, toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Opens.ι_image_top, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.range_fromSpecResidueField, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, id_toHom, AlgebraicGeometry.Scheme.zeroLocus_isClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.Scheme.Γ_obj_op, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.mem_quasiFiniteLocus, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc, evaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.inv_base_hom_base_assoc, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.Scheme.zeroLocus_univ, toΓSpecCApp_spec, AlgebraicGeometry.Scheme.JointlySurjective.exists_eq, AlgebraicGeometry.Scheme.Hom.image_le_image_iff, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom_assoc, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.isIso_fromTildeΓ_iff, AlgebraicGeometry.Scheme.residueFieldCongr_inv, AlgebraicGeometry.Scheme.coe_homeoOfIso, stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, AlgebraicGeometry.Scheme.RationalMap.mem_domain, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.spec_punit_isEmpty, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian, AlgebraicGeometry.isReduced_stalk_of_isReduced, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, stalkMap_comp, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.codisjoint_zeroLocus, forgetToSheafedSpace_obj, AlgebraicGeometry.Scheme.PartialMap.restrict_id_hom, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, evaluation_naturality_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.initial_isEmpty, AlgebraicGeometry.Scheme.residueFieldMap_comp, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm, AlgebraicGeometry.Scheme.comp_coeBase, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, iso_hom_base_inv_base, isLocalHomValStalkMap, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, stalkMap_congr_point, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.coe_opensRestrict_apply_coe, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian, AlgebraicGeometry.Scheme.Hom.app_injective, AlgebraicGeometry.Scheme.Modules.inv_app, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.coprodMk_inr, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, comp_c_app, AlgebraicGeometry.Scheme.instEpiCommRingCatResidue, AlgebraicGeometry.Scheme.Hom.isProperMap, AlgebraicGeometry.Scheme.isoOfEq_hom, AlgebraicGeometry.Scheme.le_iff_specializes, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, stalkMap_congr_hom, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Scheme.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Spec_stalkClosedPointIso, AlgebraicGeometry.Scheme.Opens.ι_base_apply, AlgebraicGeometry.Scheme.Hom.eqToHom_app, AlgebraicGeometry.instIsAffineHomιBasicOpen, AlgebraicGeometry.Scheme.id_app, AlgebraicGeometry.flat_iff, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.Scheme.residueFieldCongr_symm, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, iso_hom_base_inv_base_apply, AlgebraicGeometry.Scheme.homOfLE_rfl, AlgebraicGeometry.Scheme.fromSpecResidueField_apply, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, AlgebraicGeometry.Scheme.IdealSheafData.le_def, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, AlgebraicGeometry.Scheme.inv_base_hom_base, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion, AlgebraicGeometry.quasiSeparated_over_affine_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.Scheme.affineBasicOpen_le, IsOpenImmersion.isoRestrict_inv_ofRestrict, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, toΓSpecCApp_iff, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf', comp_c, Γ_obj, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.Scheme.Cover.fromGlued_injective, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.Spec.map_base_apply, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, AlgebraicGeometry.tilde.toOpen_map_app, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, AlgebraicGeometry.Scheme.Hom.id_image, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
toTopCat 📖	CompOp	35 math math: basicOpen_eq_bot_iff_forall_evaluation_eq_zero, IsOpenImmersion.inv_naturality, stalkMap_congr_point_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, stalkMap_congr, HasCoequalizer.imageBasicOpen_image_open, IsOpenImmersion.invApp_app_apply, stalkMap_congr_assoc, coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, toΓSpec_continuous, IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.inv_invApp, IsOpenImmersion.invApp_app, IsOpenImmersion.app_invApp_assoc, IsOpenImmersion.app_invApp, IsOpenImmersion.instIsIsoCommRingCatInvApp, AlgebraicGeometry.Scheme.local_affine, evaluation_naturality, IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, Γevaluation_eq_zero_iff_notMem_basicOpen, HasCoequalizer.imageBasicOpen_image_preimage, Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, evaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.Scheme.affineOpenCover_X, evaluation_naturality_assoc, toΓSpecCBasicOpens_app, evaluation_eq_zero_iff_notMem_basicOpen, toΓSpecSheafedSpace_hom_c_app, evaluation_naturality_apply, stalkMap_congr_point, comp_c_app, toΓSpec_preimage_basicOpen_eq, IsOpenImmersion.ofRestrict_invApp_apply
Γ 📖	CompOp	46 math math: AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, Γ_def, AlgebraicGeometry.Spec_Γ_naturality, notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, toΓSpecSheafedSpace_app_eq, Γ_obj_op, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, Γ_Spec_left_triangle, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, toΓSpec_continuous, AlgebraicGeometry.Scheme.Γ_def, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ, Γ_map, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, toΓSpec_base, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit, AlgebraicGeometry.ΓSpec.right_triangle, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, AlgebraicGeometry.Spec_Γ_naturality_assoc, Γ_map_op, toΓSpec_preimage_zeroLocus_eq, SpecΓIdentity_hom_app, toStalk_stalkMap_toΓSpec, toΓSpecSheafedSpace_app_spec, toΓSpecCBasicOpens_app, AlgebraicGeometry.isIso_toSpecΓ, toΓSpecSheafedSpace_app_spec_assoc, toΓSpecCApp_spec, toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, SpecΓIdentity_inv_app, toΓSpec_preimage_basicOpen_eq, toΓSpecCApp_iff, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit, Γ_obj
𝒪 📖	CompOp	2 math math: toΓSpecCBasicOpens_app, toΓSpecSheafedSpace_hom_c_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basicOpen_eq_bot_of_isNilpotent 📖	mathematical	IsNilpotent CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	AlgebraicGeometry.RingedSpace.basicOpen toRingedSpace Bot.bot AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot	—	eq_zero_of_zero_eq_one pow_zero basicOpen_zero AlgebraicGeometry.RingedSpace.basicOpen_pow
basicOpen_zero 📖	mathematical	—	AlgebraicGeometry.RingedSpace.basicOpen toRingedSpace CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing Bot.bot AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot	—	TopologicalSpace.Opens.ext Set.ext CommRingCat.Colimits.hasColimits_commRingCat map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isUnit_zero_iff zero_ne_one NeZero.one IsLocalRing.toNontrivial instIsLocalRingCarrierStalkCommRingCatPresheaf
comp_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace Hom.toHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier	—	—
comp_c 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.c CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace Hom.toHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.carrier TopCat.instCategoryPresheaf AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.Functor.map	—	—
comp_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace.Hom.c Opposite.op TopologicalSpace.Opens.map Opposite.unop toTopCat	—	—
comp_toHom 📖	mathematical	—	Hom.toHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace	—	—
comp_toShHom 📖	mathematical	—	Hom.toShHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory toSheafedSpace	—	—
component_nontrivial 📖	mathematical	—	Nontrivial CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op	—	RingHom.domain_nontrivial CommRingCat.Colimits.hasColimits_commRingCat IsLocalRing.toNontrivial instIsLocalRingCarrierStalkCommRingCatPresheaf
forgetToSheafedSpace_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.LocallyRingedSpace instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory forgetToSheafedSpace CategoryTheory.InducedCategory.homMk AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace Hom.toHom	—	—
forgetToSheafedSpace_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory forgetToSheafedSpace toSheafedSpace	—	—
forgetToTop_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.LocallyRingedSpace instCategory TopCat TopCat.instCategory forgetToTop AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.forget toSheafedSpace CategoryTheory.InducedCategory.homMk AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace Hom.toHom	—	—
forgetToTop_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace instCategory TopCat TopCat.instCategory forgetToTop AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.forget toSheafedSpace	—	—
homMk_toHom 📖	mathematical	—	Hom.toHom homMk CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace	—	CommRingCat.Colimits.hasColimits_commRingCat
homOfSheafedSpaceHomOfIsIso_toHom 📖	mathematical	—	Hom.toHom homOfSheafedSpaceHomOfIsIso CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace	—	—
id_toHom 📖	mathematical	—	Hom.toHom CategoryTheory.CategoryStruct.id AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.PresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace	—	—
id_toShHom' 📖	mathematical	—	Hom.toShHom CategoryTheory.CategoryStruct.id AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory toSheafedSpace	—	—
instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace 📖	mathematical	—	CategoryTheory.Functor.Faithful AlgebraicGeometry.LocallyRingedSpace instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory forgetToSheafedSpace	—	Hom.ext'
instIsLocalRingCarrierStalkCommRingCatPresheaf 📖	mathematical	—	IsLocalRing CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing	—	isLocalRing
instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms AlgebraicGeometry.LocallyRingedSpace instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory forgetToSheafedSpace	—	CategoryTheory.Iso.isIso_hom
isLocalHomStalkMap 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom Hom.stalkMap	—	Hom.prop
isLocalHomStalkMap' 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	isLocalHomStalkMap
isLocalHomValStalkMap 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom Hom.stalkMap	—	Hom.prop
isLocalRing 📖	mathematical	—	IsLocalRing CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing	—	—
is_sheafedSpace_iso 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory toSheafedSpace Hom.toShHom	—	CategoryTheory.Functor.map_isIso
iso_hom_base_inv_base 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.hom AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
iso_hom_base_inv_base_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.inv AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.hom	—	iso_hom_base_inv_base
iso_inv_base_hom_base 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.inv AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
iso_inv_base_hom_base_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.hom AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.inv	—	iso_inv_base_hom_base
ofRestrict_stalkMap_isIso 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf restrict AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom ofRestrict Hom.stalkMap	—	AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso CommRingCat.Colimits.hasColimits_commRingCat
preimage_basicOpen 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom AlgebraicGeometry.RingedSpace.basicOpen toRingedSpace DFunLike.coe Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	TopologicalSpace.Opens.ext Set.ext CommRingCat.Colimits.hasColimits_commRingCat SetLike.mem_coe AlgebraicGeometry.RingedSpace.mem_basicOpen stalkMap_germ_apply RingHom.isUnit_map isUnit_map_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isLocalHomValStalkMap
restrictStalkIso_hom_eq_germ 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace restrict CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ CategoryTheory.Iso.hom restrictStalkIso IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap Set Set.instMembership SetLike.coe	—	AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ CommRingCat.Colimits.hasColimits_commRingCat
restrictStalkIso_hom_eq_germ_apply 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace restrict AlgebraicGeometry.PresheafedSpace.presheaf CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Iso.hom restrictStalkIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap Set Set.instMembership SetLike.coe	—	AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply CommRingCat.Colimits.hasColimits_commRingCat
restrictStalkIso_hom_eq_germ_assoc 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace restrict CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ CategoryTheory.Iso.hom restrictStalkIso IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap Set Set.instMembership SetLike.coe	—	CommRingCat.Colimits.hasColimits_commRingCat Topology.IsOpenEmbedding.isOpenMap CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictStalkIso_hom_eq_germ
restrictStalkIso_inv_eq_germ 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat restrict TopCat.Presheaf.germ Set Set.instMembership SetLike.coe CategoryTheory.Iso.inv restrictStalkIso	—	AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ CommRingCat.Colimits.hasColimits_commRingCat
restrictStalkIso_inv_eq_germ_apply 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf restrict CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Iso.inv restrictStalkIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap TopCat.Presheaf.germ Set Set.instMembership SetLike.coe	—	Topology.IsOpenEmbedding.isOpenMap AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply CommRingCat.Colimits.hasColimits_commRingCat
restrictStalkIso_inv_eq_germ_assoc 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ Set Set.instMembership SetLike.coe restrict CategoryTheory.Iso.inv restrictStalkIso	—	CommRingCat.Colimits.hasColimits_commRingCat Topology.IsOpenEmbedding.isOpenMap CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictStalkIso_inv_eq_germ
restrictStalkIso_inv_eq_ofRestrict 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace restrict AlgebraicGeometry.PresheafedSpace.presheaf restrictStalkIso Hom.stalkMap ofRestrict	—	AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict CommRingCat.Colimits.hasColimits_commRingCat
restrict_carrier 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace restrict	—	—
restrict_presheaf_map 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace restrict AlgebraicGeometry.PresheafedSpace.carrier Opposite.op CategoryTheory.Functor.obj IsOpenMap.functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
restrict_presheaf_obj 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace restrict AlgebraicGeometry.PresheafedSpace.carrier Opposite.op IsOpenMap.functor Opposite.unop	—	—
stalkMap_comp 📖	mathematical	—	Hom.stalkMap CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom	—	AlgebraicGeometry.PresheafedSpace.stalkMap.comp CommRingCat.Colimits.hasColimits_commRingCat
stalkMap_congr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq toTopCat Quiver.Hom AlgebraicGeometry.LocallyRingedSpace instQuiver	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
stalkMap_congr_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq toTopCat Quiver.Hom AlgebraicGeometry.LocallyRingedSpace instQuiver	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkMap_congr
stalkMap_congr_hom 📖	mathematical	—	Hom.stalkMap CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom TopCat.Presheaf.stalkSpecializes specializes_of_eq Quiver.Hom AlgebraicGeometry.LocallyRingedSpace instQuiver	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.id_comp
stalkMap_congr_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq Quiver.Hom AlgebraicGeometry.LocallyRingedSpace instQuiver	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkMap_congr_hom
stalkMap_congr_point 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq toTopCat	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
stalkMap_congr_point_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq toTopCat	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkMap_congr_point
stalkMap_germ 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopologicalSpace.Opens toTopCat TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ Hom.stalkMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c TopologicalSpace.Opens.map	—	AlgebraicGeometry.PresheafedSpace.stalkMap_germ CommRingCat.Colimits.hasColimits_commRingCat
stalkMap_germ_apply 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopologicalSpace.Opens toTopCat TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom	TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.stalkMap CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ TopologicalSpace.Opens.map TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply CommRingCat.Colimits.hasColimits_commRingCat
stalkMap_germ_assoc 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopologicalSpace.Opens toTopCat TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ Hom.stalkMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c TopologicalSpace.Opens.map	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkMap_germ
stalkMap_hom_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.hom AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.inv Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq stalkMap_comp CategoryTheory.Iso.inv_hom_id stalkMap_congr_hom stalkMap_id CategoryTheory.Category.comp_id
stalkMap_hom_inv_apply 📖	mathematical	—	DFunLike.coe TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.inv AlgebraicGeometry.LocallyRingedSpace instCategory CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.stalkMap CategoryTheory.Iso.hom TopCat.Presheaf.stalkSpecializes specializes_of_eq	—	CommRingCat.Colimits.hasColimits_commRingCat DFunLike.congr_fun specializes_of_eq CommRingCat.hom_ext_iff stalkMap_hom_inv
stalkMap_hom_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.hom AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.inv Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkMap_hom_inv
stalkMap_id 📖	mathematical	—	Hom.stalkMap CategoryTheory.CategoryStruct.id AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf	—	AlgebraicGeometry.PresheafedSpace.stalkMap.id CommRingCat.Colimits.hasColimits_commRingCat
stalkMap_inv_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.inv AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.hom Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq stalkMap_comp CategoryTheory.Iso.hom_inv_id stalkMap_congr_hom stalkMap_id CategoryTheory.Category.comp_id
stalkMap_inv_hom_apply 📖	mathematical	—	DFunLike.coe TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.hom AlgebraicGeometry.LocallyRingedSpace instCategory CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.stalkMap CategoryTheory.Iso.inv TopCat.Presheaf.stalkSpecializes specializes_of_eq	—	CommRingCat.Colimits.hasColimits_commRingCat DFunLike.congr_fun specializes_of_eq CommRingCat.hom_ext_iff stalkMap_inv_hom
stalkMap_inv_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CategoryTheory.Iso.inv AlgebraicGeometry.LocallyRingedSpace instCategory CategoryTheory.Iso.hom Hom.stalkMap TopCat.Presheaf.stalkSpecializes specializes_of_eq	—	CommRingCat.Colimits.hasColimits_commRingCat specializes_of_eq CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkMap_inv_hom
stalkSpecializes_stalkMap 📖	mathematical	Specializes TopCat.carrier toTopCat TopCat.str	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom TopCat.Presheaf.stalkSpecializes ContinuousMap.map_specializes Hom.stalkMap CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier	—	AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap CommRingCat.Colimits.hasColimits_commRingCat
stalkSpecializes_stalkMap_apply 📖	mathematical	Specializes TopCat.carrier toTopCat TopCat.str	DFunLike.coe TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.stalkMap TopCat.Hom.hom TopCat.Presheaf.stalkSpecializes ContinuousMap.map_specializes	—	CommRingCat.Colimits.hasColimits_commRingCat DFunLike.congr_fun ContinuousMap.map_specializes CommRingCat.hom_ext_iff stalkSpecializes_stalkMap
stalkSpecializes_stalkMap_assoc 📖	mathematical	Specializes TopCat.carrier toTopCat TopCat.str	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom TopCat.Presheaf.stalkSpecializes ContinuousMap.map_specializes Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat ContinuousMap.map_specializes CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkSpecializes_stalkMap
Γ_def 📖	mathematical	—	Γ CategoryTheory.Functor.comp Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Functor.op forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.Γ	—	—
Γ_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Quiver.Hom.unop instQuiver AlgebraicGeometry.PresheafedSpace.Hom.c Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
Γ_map_op 📖	mathematical	—	CategoryTheory.Functor.map Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op Quiver.Hom.op instQuiver CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom AlgebraicGeometry.PresheafedSpace.Hom.c Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
Γ_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
Γ_obj_op 📖	mathematical	—	CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—

AlgebraicGeometry.LocallyRingedSpace.Hom

Definitions

Name	Category	Theorems
stalkMap 📖	CompOp	29 math math: AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.LocallyRingedSpace.stalkMap_id, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ
toHom 📖	CompOp	638 math math: 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, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.QuasiCompact.isCompact_preimage, AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc, AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.Scheme.Hom.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.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.range_fiberι, AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.Scheme.Cover.iUnion_range, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.Scheme.Hom.mem_opensRange, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.isCompact_iff_exists, AlgebraicGeometry.HasRingHomProperty.stalkMap, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.homMk_toHom, 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.ofRestrict_toLRSHom_base, AlgebraicGeometry.Scheme.hom_inv_apply, AlgebraicGeometry.Scheme.Hom.range_asFiberHom, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite, AlgebraicGeometry.Scheme.Hom.preimage_le_preimage_of_le, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.Scheme.preimage_comp, AlgebraicGeometry.Scheme.Hom.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.LocallyRingedSpace.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.forgetToTop_map, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base_apply, 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, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.Scheme.hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.Scheme.comp_coeBase_assoc, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, ext'_iff, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.hy, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Hom.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ι_ι, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.Scheme.Hom.isConstructible_preimage, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, 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, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.id.base, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_apply, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.homeoOfIso_apply, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, 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, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.LocallyRingedSpace.comp_base, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlgebraicGeometry.Scheme.Hom.isSpectralMap, AlgebraicGeometry.mem_range_iff_of_surjective, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.Scheme.comp_base_assoc, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.isIso_iff_isOpenImmersion, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.exists_preimage_eq, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.Hom.isOpenMap, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, AlgebraicGeometry.Scheme.Hom.app_invApp', AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, ext_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, prop, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.IsProper.instMorphismRestrict, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Hom.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.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.iso_inv_base_hom_base, AlgebraicGeometry.range_eq_univ, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.pointOfClosedPoint_apply, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, AlgebraicGeometry.coprodSpec_coprodMk, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι, AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.compactSpace_iff_exists, AlgebraicGeometry.Scheme.Hom.preimage_sup, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Scheme.iso_hom_base_inv_base, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, 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.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Hom.isIso_app, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, AlgebraicGeometry.Scheme.Hom.fiberι_asFiber, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.Hom.id_base, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.AffineCover.covers, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsFinite.finite_preimage_singleton, AlgebraicGeometry.IsLocalAtTarget.restrict, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom, 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, AlgebraicGeometry.Scheme.Hom.preimage_iSup_eq_top, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_base, 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, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, AlgebraicGeometry.Scheme.inv_hom_apply, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_map, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.Hom.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.LocallyRingedSpace.iso_inv_base_hom_base, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, AlgebraicGeometry.Scheme.Hom.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.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.Spec_closedPoint, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.Scheme.Hom.finite_preimage, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, AlgebraicGeometry.Scheme.Hom.isConstructible_image, AlgebraicGeometry.Scheme.Hom.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.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, 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, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.Scheme.Hom.homeomorph_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.Scheme.Hom.isIso_toPshHom, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.Hom.preimage_mono, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Hom.surjective, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.comp_toHom, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.Scheme.Hom.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.LocallyRingedSpace.forgetToSheafedSpace_map, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, 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, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.instIsPreimmersionAsFiberHom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Hom.isCompact_preimage, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.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.LocallyRingedSpace.Γevaluation_naturality, 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, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.range_fromSpecResidueField, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.LocallyRingedSpace.id_toHom, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.inv_base_hom_base_assoc, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.Scheme.coe_homeoOfIso, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.residueFieldMap_comp, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm, AlgebraicGeometry.Scheme.comp_coeBase, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage, AlgebraicGeometry.Scheme.Hom.app_injective, AlgebraicGeometry.Scheme.Hom.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, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, AlgebraicGeometry.Scheme.Hom.isProperMap, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Opens.ι_base_apply, AlgebraicGeometry.Scheme.Hom.eqToHom_app, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage, AlgebraicGeometry.Scheme.homOfLE_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base_apply, AlgebraicGeometry.Scheme.fromSpecResidueField_apply, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, AlgebraicGeometry.Scheme.inv_base_hom_base, AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion, 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.LocallyRingedSpace.comp_c, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Cover.fromGlued_injective, AlgebraicGeometry.Spec.map_base_apply, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, AlgebraicGeometry.Scheme.toSpecΓ_base
toShHom 📖	CompOp	21 math math: AlgebraicGeometry.LocallyRingedSpace.id_toShHom', toShHom_mk, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, AlgebraicGeometry.morphismRestrict_appLE, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, AlgebraicGeometry.LocallyRingedSpace.comp_toShHom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, AlgebraicGeometry.Scheme.Opens.ι_appLE, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	AlgebraicGeometry.PresheafedSpace.Hom.base CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toHom Quiver.Hom TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.c	—	—	CommRingCat.Colimits.hasColimits_commRingCat
ext' 📖	—	toHom	—	—	CommRingCat.Colimits.hasColimits_commRingCat
ext'_iff 📖	mathematical	—	toHom	—	ext'
ext_iff 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toHom Quiver.Hom TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.c	—	ext
prop 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base toHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	—
toShHom_mk 📖	mathematical	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	toShHom CategoryTheory.InducedCategory.homMk AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	CommRingCat.Colimits.hasColimits_commRingCat

---

← Back to Index