Spec

📁 Source: Mathlib/AlgebraicGeometry/Spec.lean

Statistics

Metric	Count
Definitions Spec, SpecΓIdentity, Spec, Spec, locallyRingedSpaceMap, locallyRingedSpaceObj, sheafedSpaceMap, sheafedSpaceObj, toLocallyRingedSpace, toPresheafedSpace, toSheafedSpace, toTop, topMap, topObj, instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapValOpensCarrierTopStructureSheaf, toPushforwardStalk, toPushforwardStalkAlgHom, toSpecΓ	18
Theorems SpecΓIdentity_hom_app, SpecΓIdentity_inv_app, Spec, basicOpen_hom_ext, coe_toTop_map_hom_apply_asIdeal, locallyRingedSpaceMap_comp, locallyRingedSpaceMap_id, locallyRingedSpaceMap_toHom, locallyRingedSpaceObj_presheaf, locallyRingedSpaceObj_presheaf', locallyRingedSpaceObj_presheaf_map, locallyRingedSpaceObj_presheaf_map', locallyRingedSpaceObj_sheaf, locallyRingedSpaceObj_sheaf', locallyRingedSpaceObj_toSheafedSpace, sheafedSpaceMap_comp, sheafedSpaceMap_hom_base, sheafedSpaceMap_hom_c_app, sheafedSpaceMap_id, sheafedSpaceObj_carrier, sheafedSpaceObj_presheaf, toLocallyRingedSpace_map, toLocallyRingedSpace_obj, toPresheafedSpace_map, toPresheafedSpace_map_op, toPresheafedSpace_obj, toPresheafedSpace_obj_op, toSheafedSpace_map, toSheafedSpace_obj, toTop_obj_carrier, topMap_comp, topMap_id, topObj_forget, Spec_map_localization_isIso, Spec_Γ_naturality, Spec_Γ_naturality_assoc, algebraMap_pushforward_stalk, isLocalizedModule_toPushforwardStalkAlgHom, isLocalizedModule_toPushforwardStalkAlgHom_aux, toPushforwardStalkAlgHom_apply, toPushforwardStalk_comp, toPushforwardStalk_comp_assoc, isIso_SpecMap_stakMap_localization, isIso_toSpecΓ, localRingHom_comp_stalkIso, localRingHom_comp_stalkIso_apply, stalkMap_toStalk, stalkMap_toStalk_apply	48
Total	66

AlgebraicGeometry

Definitions

Name	Category	Theorems
Spec 📖	CompOp	486 math math: Scheme.toSpecΓ_apply, AffineSpace.map_Spec_map, IsPreimmersion.of_isLocalization, Scheme.ΓSpecIso_inv_naturality_assoc, Scheme.fromSpecStalk_closedPoint, Scheme.map_PrimeSpectrum_basicOpen_of_affine, IsAffineOpen.isoSpec_inv_appTop, Spec.map_eq_id, AffineSpace.map_toSpecMvPoly_assoc, IsAffineOpen.map_fromSpec_assoc, Scheme.Pullback.Triplet.specTensorTo_fst, Scheme.Spec_map_stalkMap_fromSpecStalk, Scheme.IsQuasiAffine.toIsImmersion, IsPreimmersion.mk_SpecMap, pointOfClosedPoint_comp_assoc, AffineSpace.isoOfIsAffine_inv, isCommMonObj_of_isProper_of_geometricallyIntegral, Proj.basicOpenIsoSpec_inv_ι_assoc, coprodSpec_apply, IsAffineOpen.map_fromSpec, Scheme.Opens.toSpecΓ_naturality, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, instIsNoetherianSpecOfIsNoetherianRingCarrier, Proj.fromOfGlobalSections_toSpecZero_assoc, AffineSpace.toSpecMvPolyIntEquiv_symm_apply, Scheme.fromSpecStalk_toSpecΓ_assoc, AffineSpace.SpecIso_hom_appTop, isIso_SpecMap_iff, Spec.map_surjective, isCompact_iff_exists, pointsPi_surjective_of_isAffine, Spec_presheaf, HasAffineProperty.SpecMap_iff_of_affineAnd, diagonal_SpecMap, ι_sigmaSpec, GeometricallyIrreducible.iff_geometricallyIrreducible_fiber, Spec.map_injective, coprodSpec_inr, Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul, instIsIsoSchemeSigmaSpecOfFinite, instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier, Scheme.Spec_map_stalkSpecializes_fromSpecStalk, SpecMap_preimage_basicOpen, Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, Scheme.Opens.toSpecΓ_SpecMap_map, Scheme.isoSpec_inv_toSpecΓ, Scheme.Pullback.SpecTensorTo_SpecOfPoint, pointsPi_injective, Scheme.Hom.range_asFiberHom, Scheme.basic_open_isOpenImmersion, isIso_ΓSpec_adjunction_unit_app_basicOpen, instIsReducedSpecOfIsReducedCarrier, instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor, Scheme.instIsOverFromSpecStalkOfMem, functionField_isFractionRing_of_affine, tilde.map_id, IsAffineOpen.fromSpecStalk_closedPoint, tilde.map_sub, Scheme.SpecΓIdentity_hom_app, Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, Scheme.Pullback.Triplet.specTensorTo_base_snd, Scheme.PartialMap.fromSpecStalkOfMem_compHom, Scheme.isoSpec_inv_preimage_zeroLocus, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Scheme.Modules.toOpen_fromTildeΓ_app, Scheme.Pullback.tensorCongr_SpecTensorTo, Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, instGeometricallyReducedFiberToSpecResidueField, Scheme.Pullback.carrierEquiv_eq_iff, Scheme.isoSpec_hom, IsAffineOpen.opensRange_fromSpec, Scheme.isOpenImmersion_SpecMap_localizationAway, SpecToEquivOfLocalRing_apply_snd_coe, Scheme.exists_affine_mem_range_and_range_subset, Proj.basicOpenToSpec_app_top, instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact, Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap, Scheme.toSpecΓ_naturality_assoc, Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, instAdditiveModuleCatCarrierModulesSpecOfFunctor, SpecMap_ΓSpecIso_hom, stalkwise_SpecMap_iff, Scheme.Pullback.Triplet.specTensorTo_fst_assoc, AffineSpace.isoOfIsAffine_inv_appTop_coord, AffineSpace.isoOfIsAffine_inv_over_assoc, Scheme.isoSpec_hom_naturality, IsPreimmersion.mk_Spec_map, Scheme.toSpecΓ_isoSpec_inv_assoc, Scheme.toSpecΓ_naturality, instIsArtinianSchemeSpecOfIsArtinianRingCarrier, pointEquivClosedPoint_apply_coe, Scheme.Hom.ι_toNormalization, Spec.preimage_id, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, Scheme.range_fromSpecStalk, Scheme.Opens.toSpecΓ_naturality_assoc, smooth_of_grpObj_of_isAlgClosed, IsAffineOpen.isoSpec_inv, Scheme.Opens.fromSpecStalkOfMem_ι_assoc, Scheme.AffineCover.map_prop, Scheme.Pullback.carrierEquiv_symm_fst, instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, Proj.pullbackAwayιIso_inv_snd_assoc, Scheme.Hom.asFiberHom_fiberι_assoc, Scheme.ΓSpecIso_inv, IsAffineOpen.basicOpen_fromSpec_app, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Proj.SpecMap_awayMap_awayι_assoc, Scheme.isoSpec_hom_naturality_assoc, pullbackSpecIso_inv_snd, Scheme.isoSpec_inv_image_zeroLocus, instGeometricallyIntegralFiberToSpecResidueField, Proj.pullbackAwayιIso_inv_fst, instFullModuleCatCarrierModulesSpecOfFunctor, SpecMap_ΓSpecIso_inv_toSpecΓ, Scheme.over_def, Scheme.toSpecΓ_preimage_zeroLocus, Proj.basicOpenToSpec_SpecMap_awayMap, Scheme.fromSpecStalk_appTop, Scheme.IdealSheafData.vanishingIdeal_ideal, Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, pullbackSpecIso_hom_base, Proj.valuativeCriterion_existence, IsPreimmersion.Spec_map_iff, Scheme.Spec_map_presheaf_map_eqToHom, Scheme.Opens.toSpecΓ_appTop_assoc, instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, Scheme.fromSpecStalk_toSpecΓ, Scheme.ker_toSpecΓ, IsAffineOpen.algebraMap_Spec_obj, Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, Scheme.IdealSheafData.subschemeCover_map_subschemeι, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, Scheme.Opens.toSpecΓ_preimage_basicOpen, Scheme.stalkClosedPointTo_fromSpecStalk, ΓSpec.adjunction_counit_app, tilde.isoTop_hom, Spec.map_id, ModuleCat.Tilde.toOpen_res, Proj.instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Proj.basicOpenIsoSpec_inv_ι, Scheme.Opens.toSpecΓ_appTop, Scheme.Pullback.Triplet.specTensorTo_snd, locallyQuasiFinite_iff_isFinite_fiber, ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, affine_isIntegral_iff, Scheme.SpecMap_stalkSpecializes_fromSpecStalk, Scheme.descResidueField_fromSpecResidueField, ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, Scheme.Hom.asFiberHom_apply, ΓSpecIso_obj_hom, Proj.isSeparated, Proj.pullbackAwayιIso_inv_snd, Proj.pullbackAwayιIso_inv_fst_assoc, Scheme.AffineOpenCover.instIsOpenImmersionF, pullbackSpecIso_inv_fst'_assoc, Spec.germ_stalkMapIso_hom_assoc, isIso_stalkMap_coprodSpec, Proj.pullbackAwayιIso_hom_awayι, AffineSpace.spec_le_iff, Scheme.Opens.toSpecΓ_SpecMap_map_assoc, Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, Scheme.Pullback.Triplet.specTensorTo_snd_assoc, tilde.functor_map, Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc, Scheme.Pullback.carrierEquiv_symm_snd, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, Scheme.Opens.toSpecΓ_top, AffineSpace.SpecIso_inv_appTop_coord, germ_stalkClosedPointIso_hom_assoc, Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, specTargetImageFactorization_comp_assoc, isOpenImmersion_SpecMap_iff_of_surjective, IsAffineOpen.isoSpec_inv_toSpecΓ, Scheme.Spec.residue_residueFieldIso_hom_assoc, IsAffineOpen.toSpecΓ_isoSpec_inv, tilde.map_comp_assoc, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map, IsAffineOpen.fromSpec_preimage_zeroLocus, AffineSpace.homOfVector_toSpecMvPoly_assoc, Scheme.Modules.toOpen_fromTildeΓ_app_assoc, Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, IsClosedImmersion.spec_of_quotient_mk, Scheme.affineOpenCoverOfSpanRangeEqTop_X_carrier, Scheme.isoSpec_inv_naturality_assoc, Spec.map_comp_assoc, IsAffineOpen.fromSpec_app_self, Spec.preimage_comp_assoc, Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, Scheme.Pullback.tensorCongr_SpecTensorTo_assoc, Scheme.isoSpec_Spec_hom, AffineSpace.map_toSpecMvPoly, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, tilde.isIso_toOpen_top, Spec.fromSpecStalk_eq', pullbackSpecIso_inv_fst, isLocallyNoetherian_Spec, Scheme.Pullback.affine_affine_hasPullback, IsClosedImmersion.Spec_map_residue, Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc, Scheme.isPullback_toSpecΓ_toSpecΓ, Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField, Scheme.ΓSpecIso_naturality, Scheme.Opens.fromSpecStalkOfMem_ι, germ_stalkClosedPointIso_hom, Scheme.toSpecΓ_isoSpec_inv, SpecToEquivOfLocalRing_apply_fst, Proj.awayι_toSpecZero, tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, Spec.map_apply, pointOfClosedPoint_apply, isPullback_SpecMap_of_isPushout, Scheme.toSpecΓ_appTop, instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing, over_def, IsAffineOpen.fromSpec_preimage_self, Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc, isClosed_singleton_iff_locallyOfFiniteType, Proj.awayι_toSpecZero_assoc, Spec_zeroLocus_eq_zeroLocus, ValuativeCommSq.commSq, Scheme.residueFieldCongr_fromSpecResidueField, coprodSpec_coprodMk, Scheme.IdealSheafData.opensRange_subschemeCover_map, Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf, Scheme.isoSpec_inv_naturality, IsAffineOpen.toSpecΓ_fromSpec_assoc, Spec_carrier, instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, IsAffineOpen.basicOpenSectionsToAffine_isIso, Scheme.Hom.asFiberHom_fiberι, specTargetImageFactorization_comp, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, AffineSpace.map_SpecMap, Scheme.isoSpec_Spec, Scheme.Pullback.Triplet.specTensorTo_base_fst, compactSpace_iff_exists, Scheme.preimage_opensRange_toSpecΓ, Proj.fromOfGlobalSections_toSpecZero, Scheme.Spec.algebraMap_residueFieldIso_inv, AffineSpace.SpecIso_inv_over_assoc, IsClosedImmersion.spec_of_surjective, Scheme.toSpecΓ_image_zeroLocus, instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier, toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, Proj.opensRange_awayι, IsAffineOpen.fromSpec_app_self_apply, pullbackSpecIso_inv_snd_assoc, isPullback_Spec_map_pushout, Scheme.Hom.quasiFiniteAt_iff, Scheme.IsGermInjective.Spec, Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc, Scheme.instIsPreimmersionFromSpecResidueField, instIsNoetherianSpecOfOfIsNoetherianRing, SurjectiveOnStalks.Spec_iff, ΓSpecIso_hom_stalkClosedPointIso_inv, AffineSpace.toSpecMvPolyIntEquiv_apply, Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, IsAffineOpen.fromSpec_preimage_basicOpen, coprodSpec_inr_assoc, IsClosedImmersion.Spec_iff, Spec.algebraMap_stalkIso_inv, stalkwise_Spec_map_iff, pullbackSpecIso_inv_fst_assoc, Scheme.Pullback.ofPointTensor_SpecTensorTo, Scheme.default_asIdeal, Scheme.AffineCover.covers, Proj.instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Scheme.Hom.ι_toNormalization_assoc, Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, Scheme.isLocalHom_stalkClosedPointTo', Scheme.isoSpec_inv_toSpecΓ_assoc, HasRingHomProperty.of_isLocalAtSource_of_isLocalAtTarget, IsAffineOpen.primeIdealOf_eq_map_closedPoint, Scheme.IdealSheafData.range_glueDataObjι, Scheme.toOpen_eq, instIsOpenImmersionMapOfHomForallEvalRingHom, Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, IsFinite.SpecMap_iff, instIsOpenImmersionSigmaSpec, Proj.basicOpenToSpec_SpecMap_awayMap_assoc, toSpecΓ_SpecMap_ΓSpecIso_inv, instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, pullbackSpecIso_hom_fst, HasRingHomProperty.isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget, Scheme.Pullback.base_affine_hasPullback, Spec_zeroLocus, Scheme.ΓSpecIso_inv_naturality, IsPreimmersion.SpecMap_iff, Spec.map_comp, Scheme.SpecΓIdentity_inv_app, Spec.homEquiv_apply, Scheme.AffineCover.cover_X, basicOpen_eq_of_affine', AffineSpace.isoOfIsAffine_hom_appTop, coprodSpec_inl_assoc, Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, Proj.pullbackAwayιIso_hom_awayι_assoc, instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, Scheme.isoSpec_Spec_inv, Spec.map_eqToHom, instFaithfulModuleCatCarrierModulesSpecOfFunctor, Scheme.affineBasisCover_obj, Proj.awayι_preimage_basicOpen, isClosed_singleton_iff_isClosedImmersion, finite_appTop_of_universallyClosed, instIsPreimmersionFromSpecStalk, Proj.SpecMap_awayMap_awayι, basicOpenIsoSpecAway_inv_homOfLE_assoc, tilde.map_add, Scheme.Spec_fromSpecStalk', specTargetImageFactorization_app_injective, ι_sigmaSpec_assoc, Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc, geometrically_iff_forall_fiberToSpecResidueField, HasRingHomProperty.Spec_iff, AffineSpace.isoOfIsAffine_hom, tilde.toOpen_res, tilde.toOpen_res_assoc, Scheme.Hom.ι_fromNormalization_assoc, basicOpenIsoSpecAway_inv_homOfLE, Scheme.SpecMap_residue_apply, tilde.isUnit_algebraMap_end_basicOpen, coprodSpec_inl, Scheme.IdealSheafData.subSchemeCover_map_inclusion, Spec.algebraMap_stalkIso_inv_assoc, Scheme.instIsPreimmersionMapResidue, GeometricallyIntegral.iff_geometricallyIntegral_fiber, IsAffineOpen.isoSpec_hom_apply, IsAffine.affine, IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, Spec_toLocallyRingedSpace, Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, Scheme.affineOpenCoverOfSpanRangeEqTop_idx, IsSeparated.instMap, IsAffineOpen.fromSpecStalk_isPreimmersion, IsAffineOpen.range_fromSpec, Spec.map_inv, Spec_closedPoint, IsIntegralHom.SpecMap_iff, pullbackSpecIso_hom_base_assoc, IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, isPullback_SpecMap_pushout, Scheme.Hom.dense_smoothLocus_of_perfectField, Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, Scheme.Hom.asFiberHom_fiberToSpecResidueField, Scheme.affineOpenCoverOfSpanRangeEqTop_f, AffineSpace.over_over, Scheme.fromSpecStalk_app, SpecMap_residueFieldIsoBase_inv, AffineSpace.toSpecMvPolyIntEquiv_comp, tilde.map_zero, SpecMap_residueFieldIsoBase_inv_assoc, IsAffineOpen.isoSpec_hom_base_apply, AffineSpace.homOfVector_toSpecMvPoly, Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, Proj.basicOpenIsoSpec_hom, pullbackSpecIso_hom_fst'_assoc, Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms, IsAffineOpen.SpecMap_appLE_fromSpec_assoc, Spec.map_base, Scheme.instIsOverMapHomCommRingCatResidueFieldCongr, IsAffineOpen.fromSpec_top, SpecToEquivOfLocalRing_symm_apply, geometrically_iff_of_commRing, pullbackSpecIso_inv_fst', instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier, IsAffineOpen.Spec_map_appLE_fromSpec, instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier, Scheme.germ_stalkClosedPointTo_Spec, pullback_of_geometrically', Scheme.SpecMap_presheaf_map_eqToHom, IsAffineOpen.fromSpec_image_basicOpen, instIsIntegralSpecOfIsDomainCarrier, flat_and_surjective_SpecMap_iff, IsAffineOpen.Spec_map_appLE_fromSpec_assoc, instIsIsoSchemeCoprodSpec, diagonal_Spec_map, tilde.functor_obj, stalkClosedPointIso_inv, Scheme.Spec_obj, tilde.toOpen_map_app_assoc, IsClosedImmersion.SpecMap_residue, basicOpen_eq_of_affine, Scheme.ΓSpecIso_naturality_assoc, IsAffineOpen.fromSpec_toSpecΓ_assoc, IsAffineOpen.fromSpec_image_zeroLocus, ΓSpec_adjunction_homEquiv_eq, instIsPreimmersionAsFiberHom, IsAffineOpen.isOpenImmersion_fromSpec, AffineSpace.SpecIso_inv_over, Scheme.residueFieldCongr_fromSpecResidueField_assoc, Scheme.Hom.ι_fromNormalization, genericPoint_eq_bot_of_affine, IsOpenImmersion.of_isLocalization, instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, tilde.map_comp, Spec.germ_stalkMapIso_hom, Proj.instIsOpenImmersionAwayι, Spec.fromSpecStalk_eq, AffineSpace.isoOfIsAffine_inv_over, Scheme.isLocalHom_stalkClosedPointTo, IsAffineOpen.fromSpec_preimage_basicOpen', pullbackSpecIso_hom_fst', Scheme.IdealSheafData.glueDataObjι_ι, IsAffineOpen.ΓSpecIso_hom_fromSpec_app, isPullback_Spec_map_isPushout, Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, IsAffineOpen.SpecMap_appLE_fromSpec, instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction, tilde.map_neg, Scheme.range_fromSpecResidueField, Scheme.SpecMap_stalkMap_fromSpecStalk, instIsIsoSchemeMapOfCommRingCat, IsAffineOpen.isoSpec_hom, Scheme.Hom.fiberToSpecResidueField_apply, spread_out_of_isGermInjective, Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, Scheme.isLocallyArtinianScheme_Spec, pullbackSpecIso_hom_snd, IsAffineOpen.fromSpec_app_of_le, Scheme.toSpecΓ_preimage_basicOpen, isIso_fromTildeΓ_iff, pointEquivClosedPoint_symm_apply_coe, tilde.map_id_assoc, Scheme.isArtinianScheme_Spec, spec_punit_isEmpty, Scheme.affineOpenCoverOfSpanRangeEqTop_I₀, Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Spec_sheaf, ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Scheme.stalkClosedPointTo_comp, pointsPi_surjective, Scheme.Opens.toSpecΓ_SpecMap_appLE, IsAffineOpen.fromSpec_toSpecΓ, Scheme.Spec_map_residue_apply, Scheme.isoSpec_image_zeroLocus, Scheme.Spec_stalkClosedPointTo_fromSpecStalk, instGeometricallyIrreducibleFiberToSpecResidueField, IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, isAffine_Spec, Scheme.localRingHom_comp_stalkIso, Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField, Scheme.Opens.toSpecΓ_preimage_zeroLocus, Scheme.Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField, Scheme.AffineOpenCover.openCover_X, Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, Scheme.Spec.residue_residueFieldIso_hom, IsAffineOpen.isoSpec_inv_ι, isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed, IsAffineOpen.isoSpec_hom_appTop, Scheme.localRingHom_comp_stalkIso_apply, instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, pullbackSpecIso_hom_fst_assoc, Spec_stalkClosedPointIso, Scheme.Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField, IsAffineOpen.toSpecΓ_fromSpec, Scheme.Pullback.affine_hasPullback, Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap, IsAffineOpen.fromSpec_primeIdealOf, Scheme.fromSpecResidueField_apply, HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget, IsAffineOpen.isoSpec_inv_ι_assoc, Spec.homEquiv_symm_apply, Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, geometrically_iff_of_isClosedUnderIsomorphisms, tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, affine_isReduced_iff, pointOfClosedPoint_comp, Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, isNoetherian_Spec, pullback_of_geometrically, IsAffineOpen.Spec_basicOpen, Spec.map_app, Scheme.Spec_fromSpecStalk, Spec.map_base_apply, tilde.toOpen_map_app, Spec.preimage_comp, IsAffineOpen.primeIdealOf_genericPoint, Scheme.toSpecΓ_base, pullbackSpecIso_hom_snd_assoc
toSpecΓ 📖	CompOp	8 math math: Spec_Γ_naturality, LocallyRingedSpace.Γ_Spec_left_triangle, Spec_Γ_naturality_assoc, ΓSpec.toSpecΓ_of, LocallyRingedSpace.SpecΓIdentity_hom_app, isIso_toSpecΓ, LocallyRingedSpace.SpecΓIdentity_inv_app, ΓSpec.toSpecΓ_unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Spec_map_localization_isIso 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite PresheafedSpace PresheafedSpace.categoryOfPresheafedSpaces Spec.toPresheafedSpace Opposite.op CommRingCat.of CommRingCat.carrier CommRingCat.commRing PresheafedSpace.presheaf DFunLike.coe Localization CommRing.toCommMonoid OreLocalization.instCommRing OreLocalization.oreSetComm TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.instAlgebra Algebra.id PresheafedSpace.Hom.stalkMap	—	isIso_SpecMap_stakMap_localization
Spec_Γ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite LocallyRingedSpace CategoryTheory.Category.opposite LocallyRingedSpace.instCategory LocallyRingedSpace.Γ Opposite.op Spec.toLocallyRingedSpace toSpecΓ CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CommRingCat.hom_ext RingHom.ext PrimeSpectrum.isPrime StructureSheaf.comap_apply Localization.localRingHom_to_map
Spec_Γ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite LocallyRingedSpace CategoryTheory.Category.opposite LocallyRingedSpace.instCategory LocallyRingedSpace.Γ Opposite.op Spec.toLocallyRingedSpace toSpecΓ CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Spec_Γ_naturality
isIso_SpecMap_stakMap_localization 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite PresheafedSpace PresheafedSpace.categoryOfPresheafedSpaces Spec.toPresheafedSpace Opposite.op CommRingCat.of CommRingCat.carrier CommRingCat.commRing PresheafedSpace.presheaf DFunLike.coe Localization CommRing.toCommMonoid OreLocalization.instCommRing OreLocalization.oreSetComm TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.instAlgebra Algebra.id PresheafedSpace.Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime localRingHom_comp_stalkIso CategoryTheory.ConcreteCategory.isIso_iff_bijective CommRingCat.forgetReflectIsos RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquivClass.toRingEquivClass Function.Bijective.comp AlgEquiv.bijective Ideal.IsPrime.under CategoryTheory.Iso.isIso_hom
isIso_toSpecΓ 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite LocallyRingedSpace CategoryTheory.Category.opposite LocallyRingedSpace.instCategory LocallyRingedSpace.Γ Opposite.op Spec.toLocallyRingedSpace toSpecΓ	—	CategoryTheory.ConcreteCategory.isIso_iff_bijective CommRingCat.forgetReflectIsos StructureSheaf.algebraMap_obj_top_bijective
localRingHom_comp_stalkIso 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.Top CommRingCat.commRing structurePresheafInCommRingCat PrimeSpectrum.comap CommRing.toCommSemiring CommRingCat.Hom.hom Localization.AtPrime PrimeSpectrum.asIdeal PrimeSpectrum.isPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid CommRingCat.ofHom RingEquiv.toRingHom Semiring.toNonAssocSemiring OreLocalization.instSemiring AlgEquiv.toRingEquiv StructureSheaf.instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat OreLocalization.instAlgebra Algebra.id AlgEquiv.symm StructureSheaf.stalkIso Localization.localRingHom Ideal PresheafedSpace.Hom.stalkMap SheafedSpace.toPresheafedSpace Spec.sheafedSpaceObj CategoryTheory.InducedCategory.Hom.hom SheafedSpace PresheafedSpace PresheafedSpace.categoryOfPresheafedSpaces Spec.sheafedSpaceMap	—	PrimeSpectrum.isPrime CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Iso.eq_inv_comp CategoryTheory.Iso.comp_inv_eq CommRingCat.hom_ext Localization.localRingHom_unique PrimeSpectrum.comap_asIdeal AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass RingHom.instRingHomClass AlgEquiv.commutes stalkMap_toStalk_apply
localRingHom_comp_stalkIso_apply 📖	mathematical	—	DFunLike.coe RingHom Localization.AtPrime CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing PrimeSpectrum.asIdeal PrimeSpectrum.isPrime TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.Top structurePresheafInCommRingCat Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instCommSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike IsLocalization.map OreLocalization.instAlgebra Algebra.id StructureSheaf.instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal RingHom.id RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd Ideal.comap CommRingCat.Hom.hom RingHom.instRingHomClass PrimeSpectrum.comap OreLocalization.instCommRing Localization.localRingHom Ideal RingEquiv OreLocalization.instSemiring EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm RingEquivClass.toRingEquiv AlgEquiv AlgEquiv.instEquivLike AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass StructureSheaf.stalkIso CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CommRingCat.of PresheafedSpace.Hom.stalkMap SheafedSpace.toPresheafedSpace Spec.sheafedSpaceObj CategoryTheory.InducedCategory.Hom.hom SheafedSpace PresheafedSpace PresheafedSpace.categoryOfPresheafedSpaces Spec.sheafedSpaceMap	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal RingHom.instRingHomClass AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise localRingHom_comp_stalkIso
stalkMap_toStalk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CommRingCat.commRing TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.Top structurePresheafInCommRingCat PrimeSpectrum.comap CommRing.toCommSemiring CommRingCat.Hom.hom PresheafedSpace.carrier SheafedSpace.toPresheafedSpace Spec.sheafedSpaceObj PresheafedSpace.presheaf StructureSheaf.toStalk PresheafedSpace.Hom.stalkMap CategoryTheory.InducedCategory.Hom.hom SheafedSpace PresheafedSpace PresheafedSpace.categoryOfPresheafedSpaces Spec.sheafedSpaceMap	—	CommRingCat.Colimits.hasColimits_commRingCat StructureSheaf.algebraMap_germ CategoryTheory.Category.assoc PresheafedSpace.stalkMap_germ Spec.sheafedSpaceMap_hom_c_app PrimeSpectrum.continuous_comap StructureSheaf.toOpen_comp_comap_assoc
stalkMap_toStalk_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.Top CommRingCat.commRing structurePresheafInCommRingCat PrimeSpectrum.comap CommRing.toCommSemiring CommRingCat.Hom.hom Spec.topObj CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology Spec.structureSheaf Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier PresheafedSpace.Hom.stalkMap SheafedSpace.toPresheafedSpace Spec.sheafedSpaceObj CategoryTheory.InducedCategory.Hom.hom SheafedSpace PresheafedSpace PresheafedSpace.categoryOfPresheafedSpaces Spec.sheafedSpaceMap CommRingCat.of StructureSheaf.toStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise stalkMap_toStalk

AlgebraicGeometry.AffineScheme

Definitions

Name	Category	Theorems
Spec 📖	CompOp	3 math math: Spec_faithful, Spec_essSurj, Spec_full

AlgebraicGeometry.LocallyRingedSpace

Definitions

Name	Category	Theorems
SpecΓIdentity 📖	CompOp	5 math math: AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.ΓSpec.right_triangle, SpecΓIdentity_hom_app, SpecΓIdentity_inv_app, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecΓIdentity_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommRingCat CommRingCat.instCategory CategoryTheory.Functor.comp Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.Spec.toLocallyRingedSpace Γ CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category SpecΓIdentity CategoryTheory.inv CategoryTheory.Functor.obj TopologicalSpace.Opens PrimeSpectrum CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing TopCat.str AlgebraicGeometry.Spec.topObj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.toSpecΓ AlgebraicGeometry.isIso_toSpecΓ	—	—
SpecΓIdentity_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommRingCat CommRingCat.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.Spec.toLocallyRingedSpace Γ CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category SpecΓIdentity AlgebraicGeometry.toSpecΓ	—	—

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
Spec 📖	CompOp	34 math math: AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec, AlgebraicGeometry.ΓSpec.isIso_adjunction_counit, SpecΓIdentity_hom_app, AlgebraicGeometry.AffineScheme.mk_obj, AlgebraicGeometry.Spec.faithful, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.Spec.full, AlgebraicGeometry.Spec.map_preimage_unop, SpecΓIdentity_app, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite, AlgebraicGeometry.ΓSpec.adjunction_unit_app, AffineZariskiSite.restrictIsoSpec_hom_app, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec, AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, AlgebraicGeometry.AffineScheme.forgetToScheme_map, AlgebraicGeometry.isAffine_affineScheme, AlgebraicGeometry.instIsAffineObjOppositeCommRingCatSchemeSpec, isoSpec_Spec, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AffineZariskiSite.PreservesLocalization.isLocallyDirected, SpecΓIdentity_inv_app, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, AffineZariskiSite.cocone_ι_app, AffineZariskiSite.cocone_pt, Spec_obj, AlgebraicGeometry.AffineScheme.forgetToScheme_obj, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, Spec_map, AlgebraicGeometry.essImage_Spec, AffineZariskiSite.PreservesLocalization.isOpenImmersion, AffineZariskiSite.restrictIsoSpec_inv_app

AlgebraicGeometry.Scheme.IsGermInjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Spec 📖	mathematical	CommRingCat.carrier Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	AlgebraicGeometry.Scheme.IsGermInjective AlgebraicGeometry.Spec	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime AlgebraicGeometry.basicOpen_eq_of_affine AlgebraicGeometry.IsAffineOpen.basicOpen AlgebraicGeometry.isAffineOpen_top AlgebraicGeometry.isAffine_Spec RingHom.instRingHomClass RingHom.injective_iff_ker_eq_bot RingHom.ker_eq_bot_iff_eq_zero AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen IsLocalization.exists_mk'_eq IsLocalization.map_eq_zero_iff AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk Mathlib.Tactic.Elementwise.hom_elementwise AlgebraicGeometry.StructureSheaf.algebraMap_germ RingHom.mem_ker Ideal.mul_unit_mem_iff_mem isUnit_of_invertible IsLocalization.mk'_eq_mul_mk'_one IsLocalization.mk'_eq_zero_iff

AlgebraicGeometry.Spec

Definitions

Name	Category	Theorems
locallyRingedSpaceMap 📖	CompOp	6 math math: locallyRingedSpaceMap_id, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', locallyRingedSpaceMap_comp, locallyRingedSpaceMap_toHom, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, toLocallyRingedSpace_map
locallyRingedSpaceObj 📖	CompOp	39 math math: AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, locallyRingedSpaceMap_id, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, locallyRingedSpaceObj_presheaf', AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, toLocallyRingedSpace_obj, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, locallyRingedSpaceObj_toSheafedSpace, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', locallyRingedSpaceMap_comp, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, locallyRingedSpaceMap_toHom, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_base, AlgebraicGeometry.Spec_toLocallyRingedSpace, locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, locallyRingedSpaceObj_presheaf, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, locallyRingedSpaceObj_sheaf, locallyRingedSpaceObj_sheaf'
sheafedSpaceMap 📖	CompOp	14 math math: AlgebraicGeometry.localRingHom_comp_stalkIso_apply, sheafedSpaceMap_comp, toPresheafedSpace_map_op, AlgebraicGeometry.stalkMap_toStalk, sheafedSpaceMap_hom_c_app, locallyRingedSpaceMap_toHom, AlgebraicGeometry.stalkMap_toStalk_apply, toSheafedSpace_map, sheafedSpaceMap_hom_base, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, sheafedSpaceMap_id, toPresheafedSpace_map, AlgebraicGeometry.localRingHom_comp_stalkIso
sheafedSpaceObj 📖	CompOp	19 math math: toPresheafedSpace_obj, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, sheafedSpaceObj_carrier, locallyRingedSpaceObj_toSheafedSpace, sheafedSpaceMap_comp, toPresheafedSpace_map_op, AlgebraicGeometry.stalkMap_toStalk, sheafedSpaceMap_hom_c_app, toSheafedSpace_obj, locallyRingedSpaceMap_toHom, AlgebraicGeometry.stalkMap_toStalk_apply, sheafedSpaceMap_hom_base, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, toPresheafedSpace_obj_op, sheafedSpaceMap_id, toPresheafedSpace_map, AlgebraicGeometry.localRingHom_comp_stalkIso, sheafedSpaceObj_presheaf
toLocallyRingedSpace 📖	CompOp	29 math math: AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.Spec_Γ_naturality, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', toLocallyRingedSpace_obj, 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.Scheme.local_affine, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit, AlgebraicGeometry.instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, AlgebraicGeometry.ΓSpec.right_triangle, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, AlgebraicGeometry.Spec_Γ_naturality_assoc, AlgebraicGeometry.ΓSpec.toSpecΓ_of, toLocallyRingedSpace_map, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.isIso_toSpecΓ, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_inv_app, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit
toPresheafedSpace 📖	CompOp	6 math math: toPresheafedSpace_obj, AlgebraicGeometry.Spec_map_localization_isIso, toPresheafedSpace_map_op, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, toPresheafedSpace_obj_op, toPresheafedSpace_map
toSheafedSpace 📖	CompOp	8 math math: AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, toSheafedSpace_obj, toSheafedSpace_map, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app
toTop 📖	CompOp	2 math math: coe_toTop_map_hom_apply_asIdeal, toTop_obj_carrier
topMap 📖	CompOp	10 math math: AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, topMap_id, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, sheafedSpaceMap_hom_c_app, topMap_comp, sheafedSpaceMap_hom_base, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk
topObj 📖	CompOp	17 math math: sheafedSpaceObj_carrier, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, topMap_id, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, sheafedSpaceMap_hom_c_app, AlgebraicGeometry.stalkMap_toStalk_apply, topMap_comp, coe_toTop_map_hom_apply_asIdeal, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, topObj_forget, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basicOpen_hom_ext 📖	—	AlgebraicGeometry.PresheafedSpace.Hom.base CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CommRingCat.of CommRingCat.carrier CommRingCat.commRing CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op PrimeSpectrum.basicOpen CommRing.toCommSemiring CategoryTheory.Functor.op TopologicalSpace.Opens.map AlgebraicGeometry.PrimeSpectrum.Top CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	—	AlgebraicGeometry.SheafedSpace.ext TopCat.Sheaf.hom_ext PrimeSpectrum.isBasis_basic_opens CategoryTheory.Epi.left_cancellation AlgebraicGeometry.StructureSheaf.to_basicOpen_epi CategoryTheory.Functor.congr_obj CategoryTheory.eqToHom_app CategoryTheory.Category.assoc
coe_toTop_map_hom_apply_asIdeal 📖	mathematical	—	SetLike.coe Submodule CommRingCat.carrier Opposite.unop CommRingCat CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike PrimeSpectrum.asIdeal DFunLike.coe ContinuousMap PrimeSpectrum PrimeSpectrum.zariskiTopology ContinuousMap.instFunLike TopCat.Hom.hom topObj CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CommRingCat.instCategory TopCat TopCat.instCategory toTop Set.preimage RingHom RingHom.instFunLike CommRingCat.Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Ideal	—	—
locallyRingedSpaceMap_comp 📖	mathematical	—	locallyRingedSpaceMap CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory locallyRingedSpaceObj	—	AlgebraicGeometry.LocallyRingedSpace.Hom.ext' locallyRingedSpaceMap_toHom sheafedSpaceMap_comp
locallyRingedSpaceMap_id 📖	mathematical	—	locallyRingedSpaceMap CategoryTheory.CategoryStruct.id CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory locallyRingedSpaceObj	—	AlgebraicGeometry.LocallyRingedSpace.Hom.ext' locallyRingedSpaceMap_toHom sheafedSpaceMap_id
locallyRingedSpaceMap_toHom 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.Hom.toHom locallyRingedSpaceObj locallyRingedSpaceMap CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj sheafedSpaceMap	—	—
locallyRingedSpaceObj_presheaf 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.presheaf CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace locallyRingedSpaceObj CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology structureSheaf	—	—
locallyRingedSpaceObj_presheaf' 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.presheaf CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace locallyRingedSpaceObj CommRingCat.of CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology structureSheaf	—	—
locallyRingedSpaceObj_presheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace locallyRingedSpaceObj TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier CommRingCat.commRing CategoryTheory.Sheaf.val Opens.grothendieckTopology structureSheaf	—	—
locallyRingedSpaceObj_presheaf_map' 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace locallyRingedSpaceObj CommRingCat.of TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.PrimeSpectrum.Top CategoryTheory.Sheaf.val Opens.grothendieckTopology structureSheaf	—	—
locallyRingedSpaceObj_sheaf 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.sheaf CommRingCat CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace locallyRingedSpaceObj structureSheaf CommRingCat.carrier CommRingCat.commRing	—	—
locallyRingedSpaceObj_sheaf' 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.sheaf CommRingCat CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace locallyRingedSpaceObj CommRingCat.of structureSheaf	—	—
locallyRingedSpaceObj_toSheafedSpace 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace locallyRingedSpaceObj sheafedSpaceObj	—	—
sheafedSpaceMap_comp 📖	mathematical	—	sheafedSpaceMap CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory sheafedSpaceObj	—	AlgebraicGeometry.SheafedSpace.ext topMap_comp TopCat.Presheaf.ext CommRingCat.hom_ext RingHom.ext CategoryTheory.NatTrans.comp_app sheafedSpaceMap_hom_c_app CategoryTheory.Functor.whiskerRight_app CategoryTheory.eqToHom_refl CategoryTheory.Functor.map_id AlgebraicGeometry.StructureSheaf.comap_comp
sheafedSpaceMap_hom_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces sheafedSpaceMap topMap	—	—
sheafedSpaceMap_hom_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj 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 topMap AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces sheafedSpaceMap CommRingCat.ofHom AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier CommRingCat.commRing CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.op TopologicalSpace.Opens.map AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id AlgebraicGeometry.StructureSheaf.comap CommRingCat.Hom.hom Opposite.unop topObj	—	—
sheafedSpaceMap_id 📖	mathematical	—	sheafedSpaceMap CategoryTheory.CategoryStruct.id CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory sheafedSpaceObj	—	AlgebraicGeometry.SheafedSpace.ext topMap_id TopCat.Presheaf.ext CommRingCat.hom_ext RingHom.ext TopologicalSpace.Opens.map_id_obj AlgebraicGeometry.StructureSheaf.comap_id CategoryTheory.Functor.map_id RingHomCompTriple.comp_apply RingHomCompTriple.ids AlgebraicGeometry.PresheafedSpace.id_c_app
sheafedSpaceObj_carrier 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj topObj	—	—
sheafedSpaceObj_presheaf 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.presheaf CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology structureSheaf	—	—
toLocallyRingedSpace_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory toLocallyRingedSpace locallyRingedSpaceMap Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
toLocallyRingedSpace_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory toLocallyRingedSpace locallyRingedSpaceObj Opposite.unop	—	—
toPresheafedSpace_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj Opposite.unop sheafedSpaceMap Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
toPresheafedSpace_map_op 📖	mathematical	—	CategoryTheory.Functor.map Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj sheafedSpaceMap	—	—
toPresheafedSpace_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj Opposite.unop	—	—
toPresheafedSpace_obj_op 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toPresheafedSpace Opposite.op AlgebraicGeometry.SheafedSpace.toPresheafedSpace sheafedSpaceObj	—	—
toSheafedSpace_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory toSheafedSpace sheafedSpaceMap Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
toSheafedSpace_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory toSheafedSpace sheafedSpaceObj Opposite.unop	—	—
toTop_obj_carrier 📖	mathematical	—	TopCat.carrier CategoryTheory.Functor.obj Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory TopCat TopCat.instCategory toTop PrimeSpectrum CommRingCat.carrier Opposite.unop CommRing.toCommSemiring CommRingCat.commRing	—	—
topMap_comp 📖	mathematical	—	topMap CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat TopCat.instCategory topObj	—	—
topMap_id 📖	mathematical	—	topMap CategoryTheory.CategoryStruct.id CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat TopCat.instCategory topObj	—	—
topObj_forget 📖	mathematical	—	CategoryTheory.ToType TopCat TopCat.instCategory ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier topObj PrimeSpectrum CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing	—	—

AlgebraicGeometry.StructureSheaf

Definitions

Name	Category	Theorems
instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapValOpensCarrierTopStructureSheaf 📖	CompOp	4 math math: toPushforwardStalkAlgHom_apply, isLocalizedModule_toPushforwardStalkAlgHom_aux, isLocalizedModule_toPushforwardStalkAlgHom, algebraMap_pushforward_stalk
toPushforwardStalk 📖	CompOp	3 math math: toPushforwardStalk_comp, toPushforwardStalk_comp_assoc, algebraMap_pushforward_stalk
toPushforwardStalkAlgHom 📖	CompOp	3 math math: toPushforwardStalkAlgHom_apply, isLocalizedModule_toPushforwardStalkAlgHom_aux, isLocalizedModule_toPushforwardStalkAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_pushforward_stalk 📖	mathematical	—	algebraMap CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.topObj CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.Spec.topMap CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf CommRing.toCommSemiring CommSemiring.toSemiring instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapValOpensCarrierTopStructureSheaf CommRingCat.Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct toPushforwardStalk	—	CommRingCat.Colimits.hasColimits_commRingCat
isLocalizedModule_toPushforwardStalkAlgHom 📖	mathematical	—	IsLocalizedModule CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.topObj CommRingCat.of CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.Spec.topMap CommRingCat.ofHom algebraMap CommSemiring.toSemiring CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapValOpensCarrierTopStructureSheaf Ideal.primeCompl PrimeSpectrum.asIdeal PrimeSpectrum.isPrime AlgHom.toLinearMap toPushforwardStalkAlgHom	—	IsLocalizedModule.mkOfAlgebra CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime algebraMap_pushforward_stalk toPushforwardStalk_comp IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map_units IsLocalization.to_stalk isLocalizedModule_toPushforwardStalkAlgHom_aux TopCat.Presheaf.germ_eq CommRingCat.FilteredColimits.forget_preservesFilteredColimits map_zero MonoidWithZeroHomClass.toZeroHomClass CommRingCat.comp_apply toPushforwardStalk.eq_1 RingHom.map_zero toPushforwardStalkAlgHom_apply TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open PrimeSpectrum.isTopologicalBasis_basic_opens TopologicalSpace.Opens.is_open' IsLocalization.to_basicOpen IsLocalization.mk'_one IsLocalization.mk'_eq_zero_iff Submonoid.instSubmonoidClass Submonoid.smul_def Algebra.smul_def SubmonoidClass.coe_pow map_pow
isLocalizedModule_toPushforwardStalkAlgHom_aux 📖	mathematical	—	CommRingCat.carrier Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing SetLike.instMembership Submonoid.instSetLike Ideal.primeCompl PrimeSpectrum.asIdeal PrimeSpectrum.isPrime TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.topObj CommRingCat.of CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.Spec.topMap CommRingCat.ofHom algebraMap CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Submonoid.smul Algebra.toSMul instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapValOpensCarrierTopStructureSheaf DFunLike.coe AlgHom AlgHom.funLike toPushforwardStalkAlgHom	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime TopCat.Presheaf.germ_exist CommRingCat.FilteredColimits.forget_preservesFilteredColimits TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open PrimeSpectrum.isTopologicalBasis_basic_opens TopologicalSpace.Opens.is_open' TopCat.Presheaf.germ_res_apply IsLocalization.surj IsLocalization.to_basicOpen Submonoid.instSubmonoidClass Submonoid.smul_def Algebra.smul_def algebraMap_pushforward_stalk toPushforwardStalk.eq_1 CommRingCat.comp_apply le_top map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_comm map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
toPushforwardStalkAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.topObj CommRingCat.of CommRingCat.commRing CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.Spec.topMap CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapValOpensCarrierTopStructureSheaf AlgHom.funLike toPushforwardStalkAlgHom RingHom Opposite CategoryTheory.Category.opposite CategoryTheory.types AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule Opposite.op PrimeSpectrum TopologicalSpace.Opens.map Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Semiring.toNonAssocSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id RingHom.instFunLike CommRingCat.Hom.hom' TopCat.Presheaf.germ AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	CommRingCat.Colimits.hasColimits_commRingCat
toPushforwardStalk_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.topObj CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.Spec.topMap CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf toPushforwardStalk CommRingCat.of AlgebraicGeometry.structurePresheafInCommRingCat TopCat.Presheaf.stalkFunctor AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.Spec.sheafedSpaceObj AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.Spec.sheafedSpaceMap AlgebraicGeometry.PresheafedSpace.presheaf toStalk CategoryTheory.Functor.map AlgebraicGeometry.PresheafedSpace.Hom.c	—	CommRingCat.Colimits.hasColimits_commRingCat toStalk.eq_1 CategoryTheory.Category.assoc TopCat.Presheaf.stalkFunctor_map_germ AlgebraicGeometry.Spec_Γ_naturality_assoc
toPushforwardStalk_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.topObj CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.Spec.topMap CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf toPushforwardStalk AlgebraicGeometry.structurePresheafInCommRingCat toStalk CategoryTheory.Functor.map TopCat.Presheaf.stalkFunctor AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.Spec.sheafedSpaceObj AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.Spec.sheafedSpaceMap AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.PresheafedSpace.Hom.c	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPushforwardStalk_comp

---

← Back to Index