StructureSheaf

📁 Source: Mathlib/AlgebraicGeometry/StructureSheaf.lean

Statistics

Metric	Count
Definitions Top, structureSheaf, IsFraction, Localizations, comapFun, comap, comapFun, comapₗ, commRingCatStalkEquivModuleStalk, const, globalSectionsIso, instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat, instModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheaf, isFractionPrelocal, isLocallyFraction, openAlgebra, sectionsSubalgebra, sectionsSubalgebraSubmodule, sectionsSubmodule, stalkAlgebra, stalkIso, toOpen, toOpenₗ, toStalk, toStalkₗ, instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType, instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType, instCommRingObjOppositeOpensCarrierTopValStructureSheafInType, instModuleObjOppositeOpensCarrierTopValStructureSheafInType, instModuleObjOppositeOpensCarrierTopValStructureSheafInType_1, moduleStructurePresheaf, structurePresheafCompForget, structurePresheafInCommRingCat, structurePresheafInModuleCat, structureSheafInType	35
Theorems to_basicOpen, to_stalk, comapFun_mk, algebraMap_germ, algebraMap_germ_apply, algebraMap_germ_assoc, algebraMap_obj_top_bijective, algebraMap_self_map, comap_apply, comap_basicOpen, comap_comp, comap_const, comap_id, comap_id', comap_id_eq_map, comapₗ_const, comapₗ_eq_localRingHom, const_add, const_algebraMap, const_apply, const_congr, const_eq_const_of_smul_eq_smul, const_ext, const_mul, const_mul_cancel, const_mul_cancel', const_mul_rev, const_one, const_self, const_zero, exists_const, globalSectionsIso_hom, globalSectionsIso_inv, instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal, instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, isLocallyFraction_comapFun, res_apply, res_const, smul_const, stalkAlgebra_map, toOpen_comp_comap, toOpen_comp_comap_apply, toOpen_comp_comap_assoc, toOpen_germ, toOpen_res, toOpenₗ_eq_const, toOpenₗ_top_bijective, toStalk_stalkSpecializes, toStalk_stalkSpecializes_apply, toStalk_stalkSpecializes_assoc, to_basicOpen_epi, instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, structurePresheafInCommRingCat_obj_carrier, structurePresheafInModuleCat_obj_carrier, add_apply, mul_apply, smul_apply	60
Total	95

AlgebraicGeometry

Definitions

Name	Category	Theorems
instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType 📖	CompOp	11 math math: StructureSheaf.const_add, StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, StructureSheaf.smul_const, StructureSheaf.const_zero, structureSheafInType.add_apply, StructureSheaf.comapₗ_const, StructureSheaf.toOpenₗ_top_bijective, StructureSheaf.toOpenₗ_eq_const, StructureSheaf.comapₗ_eq_localRingHom, structureSheafInType.smul_apply
instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType 📖	CompOp	23 math math: ΓSpec.locallyRingedSpaceAdjunction_counit_app, StructureSheaf.globalSectionsIso_inv, instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, StructureSheaf.toPushforwardStalkAlgHom_apply, Scheme.ΓSpecIso_inv, ΓSpec.locallyRingedSpaceAdjunction_counit_app', StructureSheaf.algebraMap_self_map, ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, StructureSheaf.globalSectionsIso_hom, ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', StructureSheaf.algebraMap_obj_top_bijective, StructureSheaf.algebraMap_germ_assoc, StructureSheaf.algebraMap_germ, ΓSpec.toSpecΓ_of, StructureSheaf.toOpen_germ, StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, StructureSheaf.toOpen_res, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, LocallyRingedSpace.toΓSpecCApp_spec, StructureSheaf.algebraMap_germ_apply, ΓSpec.toSpecΓ_unop, LocallyRingedSpace.toΓSpecCApp_iff
instCommRingObjOppositeOpensCarrierTopValStructureSheafInType 📖	CompOp	32 math math: ΓSpec.locallyRingedSpaceAdjunction_counit_app, StructureSheaf.globalSectionsIso_inv, StructureSheaf.const_mul_rev, StructureSheaf.const_self, structureSheafInType.mul_apply, instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, StructureSheaf.toPushforwardStalkAlgHom_apply, Scheme.ΓSpecIso_inv, ΓSpec.locallyRingedSpaceAdjunction_counit_app', StructureSheaf.algebraMap_self_map, StructureSheaf.const_mul_cancel, ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, StructureSheaf.const_one, StructureSheaf.globalSectionsIso_hom, ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', Spec.sheafedSpaceMap_hom_c_app, StructureSheaf.algebraMap_obj_top_bijective, StructureSheaf.const_algebraMap, StructureSheaf.algebraMap_germ_assoc, StructureSheaf.algebraMap_germ, StructureSheaf.const_mul_cancel', ΓSpec.toSpecΓ_of, StructureSheaf.toOpen_germ, StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, StructureSheaf.toOpen_res, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, LocallyRingedSpace.toΓSpecCApp_spec, StructureSheaf.const_mul, StructureSheaf.algebraMap_germ_apply, ΓSpec.toSpecΓ_unop, LocallyRingedSpace.toΓSpecCApp_iff
instModuleObjOppositeOpensCarrierTopValStructureSheafInType 📖	CompOp	8 math math: StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, StructureSheaf.smul_const, StructureSheaf.comapₗ_const, StructureSheaf.toOpenₗ_top_bijective, StructureSheaf.toOpenₗ_eq_const, StructureSheaf.comapₗ_eq_localRingHom, structureSheafInType.smul_apply
instModuleObjOppositeOpensCarrierTopValStructureSheafInType_1 📖	CompOp	1 math math: instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType
moduleStructurePresheaf 📖	CompOp	2 math math: StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ
structurePresheafCompForget 📖	CompOp	—
structurePresheafInCommRingCat 📖	CompOp	22 math math: StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, localRingHom_comp_stalkIso_apply, StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal, StructureSheaf.toStalk_stalkSpecializes_assoc, StructureSheaf.toStalk_stalkSpecializes, stalkMap_toStalk, Spec.fromSpecStalk_eq', StructureSheaf.toStalk_stalkSpecializes_apply, stalkMap_toStalk_apply, StructureSheaf.algebraMap_germ_assoc, StructureSheaf.algebraMap_germ, StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, Scheme.Spec_fromSpecStalk', StructureSheaf.stalkAlgebra_map, StructureSheaf.toOpen_germ, StructureSheaf.toPushforwardStalk_comp, StructureSheaf.toPushforwardStalk_comp_assoc, structurePresheafInCommRingCat_obj_carrier, LocallyRingedSpace.toStalk_stalkMap_toΓSpec, localRingHom_comp_stalkIso, StructureSheaf.algebraMap_germ_apply
structurePresheafInModuleCat 📖	CompOp	1 math math: structurePresheafInModuleCat_obj_carrier
structureSheafInType 📖	CompOp	47 math math: ΓSpec.locallyRingedSpaceAdjunction_counit_app, StructureSheaf.globalSectionsIso_inv, StructureSheaf.const_mul_rev, StructureSheaf.const_self, StructureSheaf.const_add, structureSheafInType.mul_apply, StructureSheaf.exists_const, StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, StructureSheaf.toPushforwardStalkAlgHom_apply, Scheme.ΓSpecIso_inv, ΓSpec.locallyRingedSpaceAdjunction_counit_app', StructureSheaf.algebraMap_self_map, StructureSheaf.const_mul_cancel, ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, StructureSheaf.const_one, StructureSheaf.globalSectionsIso_hom, StructureSheaf.smul_const, ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', StructureSheaf.const_zero, Spec.sheafedSpaceMap_hom_c_app, StructureSheaf.algebraMap_obj_top_bijective, StructureSheaf.const_algebraMap, structureSheafInType.add_apply, StructureSheaf.comapₗ_const, StructureSheaf.algebraMap_germ_assoc, StructureSheaf.res_apply, StructureSheaf.algebraMap_germ, StructureSheaf.const_mul_cancel', StructureSheaf.toOpenₗ_top_bijective, ΓSpec.toSpecΓ_of, StructureSheaf.toOpen_germ, StructureSheaf.toOpenₗ_eq_const, StructureSheaf.res_const, structurePresheafInCommRingCat_obj_carrier, StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, StructureSheaf.comapₗ_eq_localRingHom, StructureSheaf.toOpen_res, structurePresheafInModuleCat_obj_carrier, LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, LocallyRingedSpace.toΓSpecCApp_spec, StructureSheaf.const_mul, structureSheafInType.smul_apply, StructureSheaf.algebraMap_germ_apply, ΓSpec.toSpecΓ_unop, LocallyRingedSpace.toΓSpecCApp_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType 📖	mathematical	—	IsScalarTower CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Algebra.toSMul Algebra.toModule Algebra.id instCommRingObjOppositeOpensCarrierTopValStructureSheafInType instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleObjOppositeOpensCarrierTopValStructureSheafInType_1 instModuleObjOppositeOpensCarrierTopValStructureSheafInType	—	IsScalarTower.of_algebraMap_smul IsScalarTower.algebraMap_smul IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1
structurePresheafInCommRingCat_obj_carrier 📖	mathematical	—	CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory structurePresheafInCommRingCat CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	—	—
structurePresheafInModuleCat_obj_carrier 📖	mathematical	—	ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder ModuleCat ModuleCat.moduleCategory structurePresheafInModuleCat CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology structureSheafInType	—	—

AlgebraicGeometry.PrimeSpectrum

Definitions

Name	Category	Theorems
Top 📖	CompOp	77 math math: AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, AlgebraicGeometry.StructureSheaf.comap_id, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, AlgebraicGeometry.StructureSheaf.comap_id', AlgebraicGeometry.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.structureSheafInType.mul_apply, AlgebraicGeometry.StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, ModuleCat.Tilde.toOpen_res, AlgebraicGeometry.Spec.map_appLE, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.StructureSheaf.const_one, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.stalkMap_toStalk, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, AlgebraicGeometry.Spec.fromSpecStalk_eq', AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply, AlgebraicGeometry.structureSheafInType.add_apply, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.StructureSheaf.res_apply, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, AlgebraicGeometry.Scheme.Spec_fromSpecStalk', AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, AlgebraicGeometry.StructureSheaf.stalkAlgebra_map, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, AlgebraicGeometry.ΓSpec.toSpecΓ_of, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, AlgebraicGeometry.StructureSheaf.toOpen_res, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.StructureSheaf.const_apply, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.structureSheafInType.smul_apply, AlgebraicGeometry.localRingHom_comp_stalkIso, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, AlgebraicGeometry.Spec.map_app

AlgebraicGeometry.Spec

Definitions

Name	Category	Theorems
structureSheaf 📖	CompOp	45 math math: AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, AlgebraicGeometry.StructureSheaf.comap_id, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.StructureSheaf.comap_comp, AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, AlgebraicGeometry.StructureSheaf.comap_id', AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, locallyRingedSpaceObj_presheaf', AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, AlgebraicGeometry.StructureSheaf.comap_const, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes, AlgebraicGeometry.StructureSheaf.comap_apply, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, map_appLE, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, AlgebraicGeometry.StructureSheaf.stalkAlgebra_map, locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, locallyRingedSpaceObj_presheaf, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, AlgebraicGeometry.StructureSheaf.toOpen_res, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.Spec_sheaf, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, locallyRingedSpaceObj_sheaf, locallyRingedSpaceObj_sheaf', sheafedSpaceObj_presheaf, map_app

AlgebraicGeometry.StructureSheaf

Definitions

Name	Category	Theorems
IsFraction 📖	MathDef	—
Localizations 📖	CompOp	8 math math: AlgebraicGeometry.structureSheafInType.mul_apply, comap_apply, AlgebraicGeometry.structureSheafInType.add_apply, res_apply, Localizations.comapFun_mk, comapₗ_eq_localRingHom, const_apply, AlgebraicGeometry.structureSheafInType.smul_apply
comap 📖	CompOp	13 math math: comap_id, comap_comp, toOpen_comp_comap_apply, comap_id', toOpen_comp_comap, comap_const, comap_apply, AlgebraicGeometry.Spec.map_appLE, toOpen_comp_comap_assoc, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, comap_id_eq_map, comap_basicOpen, AlgebraicGeometry.Spec.map_app
comapFun 📖	CompOp	1 math math: isLocallyFraction_comapFun
comapₗ 📖	CompOp	2 math math: comapₗ_const, comapₗ_eq_localRingHom
commRingCatStalkEquivModuleStalk 📖	CompOp	—
const 📖	CompOp	19 math math: const_mul_rev, const_self, const_add, exists_const, const_eq_const_of_smul_eq_smul, comap_const, const_congr, const_mul_cancel, const_one, smul_const, const_zero, const_algebraMap, comapₗ_const, const_mul_cancel', toOpenₗ_eq_const, res_const, const_ext, const_mul, const_apply
globalSectionsIso 📖	CompOp	2 math math: globalSectionsIso_inv, globalSectionsIso_hom
instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat 📖	CompOp	4 math math: instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal, AlgebraicGeometry.localRingHom_comp_stalkIso
instModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheaf 📖	CompOp	2 math math: instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ
isFractionPrelocal 📖	CompOp	—
isLocallyFraction 📖	CompOp	7 math math: AlgebraicGeometry.structureSheafInType.mul_apply, comap_apply, AlgebraicGeometry.structureSheafInType.add_apply, res_apply, comapₗ_eq_localRingHom, const_apply, AlgebraicGeometry.structureSheafInType.smul_apply
openAlgebra 📖	CompOp	7 math math: toOpen_comp_comap_apply, toOpen_comp_comap, to_basicOpen_epi, IsLocalization.to_basicOpen, toOpen_comp_comap_assoc, AlgebraicGeometry.Scheme.toOpen_eq, comap_basicOpen
sectionsSubalgebra 📖	CompOp	—
sectionsSubalgebraSubmodule 📖	CompOp	—
sectionsSubmodule 📖	CompOp	—
stalkAlgebra 📖	CompOp	2 math math: IsLocalization.to_stalk, stalkAlgebra_map
stalkIso 📖	CompOp	2 math math: AlgebraicGeometry.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.localRingHom_comp_stalkIso
toOpen 📖	CompOp	—
toOpenₗ 📖	CompOp	3 math math: instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, toOpenₗ_top_bijective, toOpenₗ_eq_const
toStalk 📖	CompOp	17 math math: AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, toStalk_stalkSpecializes_assoc, toStalk_stalkSpecializes, AlgebraicGeometry.stalkMap_toStalk, AlgebraicGeometry.Spec.fromSpecStalk_eq', toStalk_stalkSpecializes_apply, AlgebraicGeometry.stalkMap_toStalk_apply, algebraMap_germ_assoc, algebraMap_germ, AlgebraicGeometry.Scheme.Spec_fromSpecStalk', stalkAlgebra_map, toOpen_germ, toPushforwardStalk_comp, toPushforwardStalk_comp_assoc, AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, algebraMap_germ_apply
toStalkₗ 📖	CompOp	1 math math: instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_germ 📖	mathematical	TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Opposite.op AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.structurePresheafInCommRingCat CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType TopCat.Presheaf.germ toStalk	—	CommRingCat.Colimits.hasColimits_commRingCat le_top TopCat.Presheaf.germ_res
algebraMap_germ_apply 📖	mathematical	TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe RingHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Opposite.op CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.structurePresheafInCommRingCat Semiring.toNonAssocSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CommRingCat.of TopCat.Presheaf.germ algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType toStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise algebraMap_germ
algebraMap_germ_assoc 📖	mathematical	TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Opposite.op AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.structurePresheafInCommRingCat TopCat.Presheaf.germ toStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' algebraMap_germ
algebraMap_obj_top_bijective 📖	mathematical	—	Function.Bijective CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe RingHom Semiring.toNonAssocSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id RingHom.instFunLike algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	toOpenₗ_top_bijective
algebraMap_self_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id AlgebraicGeometry.Spec.structureSheaf CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType CategoryTheory.Functor.map	—	—
comap_apply 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Set.instHasSubset TopologicalSpace.Opens.carrier TopCat.str Set.preimage PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap	TopCat.PrelocalPredicate.pred Localizations Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring TopCat.LocalPredicate.toPrelocalPredicate isLocallyFraction Opposite.unop TopologicalSpace.Opens Opposite.op DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Semiring.toNonAssocSemiring CommRingCat.commRing RingHom.instFunLike comap Localization.AtPrime PrimeSpectrum.asIdeal SetLike.instMembership TopologicalSpace.Opens.instSetLike PrimeSpectrum.isPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Localization.localRingHom Ideal	—	comapₗ_eq_localRingHom
comap_basicOpen 📖	mathematical	—	comap PrimeSpectrum.basicOpen CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Eq.le TopologicalSpace.Opens PrimeSpectrum PrimeSpectrum.zariskiTopology PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder FrameHom TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap PrimeSpectrum.comap PrimeSpectrum.continuous_comap PrimeSpectrum.comap_basicOpen IsLocalization.map Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CommRingCat.commRing openAlgebra IsLocalization.to_basicOpen Submonoid Monoid.toMulOneClass Preorder.toLE Submonoid.instPartialOrder Submonoid.comap MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers_le Submonoid.mem_powers	—	IsLocalization.ringHom_ext IsLocalization.to_basicOpen Eq.le PrimeSpectrum.continuous_comap PrimeSpectrum.comap_basicOpen MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.powers_le Submonoid.mem_powers IsLocalization.map_comp toOpen_comp_comap
comap_comp 📖	mathematical	PrimeSpectrum CommRing.toCommSemiring TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike PrimeSpectrum.comap	comap RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CommRingCat.commRing	—	RingHom.ext PrimeSpectrum.isPrime comap_apply RingHom.instRingHomClass Localization.localRingHom_comp
comap_const 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Set.instHasSubset TopologicalSpace.Opens.carrier TopCat.str Set.preimage PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Ideal.primeCompl PrimeSpectrum.asIdeal PrimeSpectrum.isPrime	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CommRingCat.commRing RingHom.instFunLike comap const Ring.toAddCommGroup CommRing.toRing Semiring.toModule	—	PrimeSpectrum.isPrime comap_apply const_apply Localization.isLocalization RingHom.instRingHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Localization.le_comap_primeCompl_iff ge_of_eq Localization.mk_eq_mk' Localization.localRingHom_mk'
comap_id 📖	mathematical	—	comap RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.Hom.hom CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.leOfHom comap_id_eq_map CategoryTheory.eqToHom_op CategoryTheory.eqToHom_map
comap_id' 📖	mathematical	—	comap RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CommRingCat.commRing	—	comap_id
comap_id_eq_map 📖	mathematical	—	comap RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.leOfHom TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat.Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	RingHom.ext CategoryTheory.leOfHom PrimeSpectrum.isPrime comap_apply RingHom.instRingHomClass Ideal.comap_id Localization.localRingHom_id
comapₗ_const 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Set.instHasSubset TopologicalSpace.Opens.carrier TopCat.str Set.preimage PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen	DFunLike.coe LinearMap CommSemiring.toSemiring CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op AddCommGroup.toAddCommMonoid AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType LinearMap.instFunLike comapₗ const RingHom Semiring.toNonAssocSemiring RingHom.instFunLike HasSubset.Subset.trans Set.instIsTransSubset SetLike.coe TopologicalSpace.Opens.instSetLike Set.preimage_mono	—	HasSubset.Subset.trans Set.instIsTransSubset Set.preimage_mono PrimeSpectrum.isPrime RingHom.instRingHomClass
comapₗ_eq_localRingHom 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Set.instHasSubset TopologicalSpace.Opens.carrier TopCat.str Set.preimage PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap	TopCat.PrelocalPredicate.pred Localizations Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring TopCat.LocalPredicate.toPrelocalPredicate isLocallyFraction Opposite.unop TopologicalSpace.Opens Opposite.op DFunLike.coe LinearMap CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType AddCommGroup.toAddCommMonoid AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType LinearMap.instFunLike comapₗ RingHom.toSemilinearMap RingHom Localization.AtPrime PrimeSpectrum.asIdeal SetLike.instMembership TopologicalSpace.Opens.instSetLike PrimeSpectrum.isPrime Semiring.toNonAssocSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike Localization.localRingHom Ideal	—	PrimeSpectrum.isPrime IsScalarTower.left IsScalarTower.right LocalizedModule.induction_on RingHom.instRingHomClass Localization.isLocalization MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Localization.le_comap_primeCompl_iff ge_of_eq Localization.mk_eq_mk' Localization.localRingHom_mk'
const_add 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType const SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
const_algebraMap 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	const Ring.toAddCommGroup CommRing.toRing Algebra.toModule CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType	—	LocalizedModule.mk_eq one_smul Algebra.smul_def mul_one OreLocalization.one_def
const_apply 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike Ideal.primeCompl PrimeSpectrum.asIdeal PrimeSpectrum.isPrime	TopCat.PrelocalPredicate.pred AlgebraicGeometry.PrimeSpectrum.Top Localizations TopCat.LocalPredicate.toPrelocalPredicate isLocallyFraction Opposite.unop TopologicalSpace.Opens TopCat.carrier TopCat.str Opposite.op const TopologicalSpace.Opens.instSetLike AddCommGroup.toAddCommMonoid	—	PrimeSpectrum.isPrime
const_congr 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	const	—	—
const_eq_const_of_smul_eq_smul 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	const	—	One.instNonempty
const_ext 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	const	—	LocalizedModule.mk_eq One.instNonempty
const_mul 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Algebra.toModule CommSemiring.toSemiring Opposite.op Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType const	—	—
const_mul_cancel 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring Opposite.op Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id const	—	const_mul const_ext Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
const_mul_cancel' 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring Opposite.op Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id const	—	mul_comm const_mul_cancel
const_mul_rev 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring Opposite.op Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id const AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	const_mul mul_comm const_congr const_self
const_one 📖	mathematical	—	const Ring.toAddCommGroup CommRing.toRing Algebra.toModule CommRing.toCommSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType	—	PrimeSpectrum.basicOpen_one const.congr_simp map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass const_algebraMap
const_self 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	const Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id	—	const_algebraMap
const_zero 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	const NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType	—	OreLocalization.zero_oreDiv
exists_const 📖	mathematical	TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	const PrimeSpectrum.basicOpen CommRing.toCommSemiring le_rfl PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op PrimeSpectrum PrimeSpectrum.zariskiTopology Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct LE.le.hom	—	le_rfl TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open PrimeSpectrum.isBasis_basic_opens TopologicalSpace.Opens.is_open' PrimeSpectrum.basicOpen_mul LE.le.trans inf_le_left HasSubset.Subset.trans Set.instIsTransSubset LocalizedModule.mk_eq Submonoid.isScalarTower IsScalarTower.left one_smul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero
globalSectionsIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CommRingCat.commRing CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val 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 globalSectionsIso CommRingCat.ofHom CategoryTheory.types AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	—
globalSectionsIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory CommRingCat.of CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val 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 globalSectionsIso CommRingCat.ofHom CategoryTheory.types AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquiv.symm RingEquiv.ofBijective RingHom RingHom.instFunLike algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType algebraMap_obj_top_bijective	—	—
instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal 📖	mathematical	—	IsLocalization.AtPrime CommRing.toCommSemiring CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat CommRingCat.commRing instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat PrimeSpectrum.asIdeal PrimeSpectrum.isPrime	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime isLocalizedModule_iff_isLocalization' AddCommGrpCat.hasColimitsOfSize UnivLE.self RingHomCompTriple.ids RingHomInvPair.ids AddCommGrpCat.hasColimit Opposite.small UnivLE.small CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CommRingCat.FilteredColimits.forget₂Ring_preservesFilteredColimits RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForget₂RingHomCarrierAddMonoidHomCarrier CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom LinearMap.ext_ring map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.map_one IsLocalizedModule.of_linearEquiv instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ
instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen 📖	mathematical	—	IsLocalization.Away CommRing.toCommSemiring CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring Opposite.op PrimeSpectrum.basicOpen AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	isLocalizedModule_iff_isLocalization' instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ
instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring AddCommGrpCat.carrier TopCat.Presheaf.stalk Ab AddCommGrpCat.instCategory AddCommGrpCat.hasColimitsOfSize UnivLE.self AlgebraicGeometry.PrimeSpectrum.Top PresheafOfModules.presheaf TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory RingCat RingCat.instCategory AlgebraicGeometry.structurePresheafInCommRingCat CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat AlgebraicGeometry.moduleStructurePresheaf AddCommGroup.toAddCommMonoid AddCommGrpCat.str instModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheaf Ideal.primeCompl PrimeSpectrum.asIdeal PrimeSpectrum.isPrime toStalkₗ	—	AddCommGrpCat.hasColimitsOfSize UnivLE.self PrimeSpectrum.isPrime ModuleCat.hasColimitsOfSize RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext AddCommGrpCat.hasColimit Opposite.small UnivLE.small ModuleCat.HasColimit.instHasColimit ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier AddEquiv.eq_symm_apply CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom IsLocalizedModule.of_linearEquiv
instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op PrimeSpectrum.basicOpen AddCommGroup.toAddCommMonoid AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring toOpenₗ	—	IsScalarTower.left IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext PrimeSpectrum.le_basicOpen_pow IsLocalizedModule.of_linearEquiv localizedModuleIsLocalizedModule
instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf 📖	mathematical	—	IsScalarTower CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat AddCommGrpCat.carrier Ab AddCommGrpCat.instCategory AddCommGrpCat.hasColimitsOfSize UnivLE.self PresheafOfModules.presheaf TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat AlgebraicGeometry.moduleStructurePresheaf Algebra.toSMul instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier instModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheaf	—	IsScalarTower.of_algebraMap_smul CommRingCat.Colimits.hasColimits_commRingCat AddCommGrpCat.hasColimitsOfSize UnivLE.self
isLocallyFraction_comapFun 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Set.instHasSubset TopologicalSpace.Opens.carrier TopCat.str Set.preimage PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap TopCat.PrelocalPredicate.pred Localizations TopCat.LocalPredicate.toPrelocalPredicate isLocallyFraction	comapFun	—	Continuous.isOpen_preimage PrimeSpectrum.continuous_comap TopologicalSpace.Opens.is_open' RingHom.instRingHomClass PrimeSpectrum.isPrime
res_apply 📖	mathematical	—	TopCat.PrelocalPredicate.pred AlgebraicGeometry.PrimeSpectrum.Top Localizations TopCat.LocalPredicate.toPrelocalPredicate isLocallyFraction Opposite.unop TopologicalSpace.Opens TopCat.carrier TopCat.str Opposite.op CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Quiver.Hom SetLike.instMembership TopologicalSpace.Opens.instSetLike TopologicalSpace.Opens.opensHom.instFunLike	—	—
res_const 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op const	—	—
smul_const 📖	mathematical	TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PrimeSpectrum.basicOpen CommRing.toCommSemiring	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType const	—	—
stalkAlgebra_map 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top TopCat.Sheaf.presheaf AlgebraicGeometry.Spec.structureSheaf Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike algebraMap stalkAlgebra CommRingCat.of AlgebraicGeometry.structurePresheafInCommRingCat CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier toStalk	—	CommRingCat.Colimits.hasColimits_commRingCat
toOpen_comp_comap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CommRingCat.commRing DFunLike.coe FrameHom PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap PrimeSpectrum.comap PrimeSpectrum.continuous_comap CommRingCat.ofHom algebraMap CommSemiring.toSemiring openAlgebra comap Set Set.instMembership TopologicalSpace.Opens.carrier	—	CommRingCat.hom_ext PrimeSpectrum.continuous_comap RingHom.ext PrimeSpectrum.isPrime comap_apply Localization.localRingHom_to_map
toOpen_comp_comap_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op FrameHom PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap PrimeSpectrum.comap PrimeSpectrum.continuous_comap Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRingCat.commRing RingHom.instFunLike comap Set Set.instMembership TopologicalSpace.Opens.carrier algebraMap openAlgebra	—	PrimeSpectrum.continuous_comap CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toOpen_comp_comap
toOpen_comp_comap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op CommRingCat.commRing CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring openAlgebra DFunLike.coe FrameHom PrimeSpectrum PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap PrimeSpectrum.comap PrimeSpectrum.continuous_comap comap Set Set.instMembership TopologicalSpace.Opens.carrier	—	PrimeSpectrum.continuous_comap CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toOpen_comp_comap
toOpen_germ 📖	mathematical	TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Opposite.op AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.structurePresheafInCommRingCat CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType TopCat.Presheaf.germ toStalk	—	algebraMap_germ
toOpen_res 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id AlgebraicGeometry.Spec.structureSheaf CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType CategoryTheory.Functor.map	—	algebraMap_self_map
toOpenₗ_eq_const 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op AddCommGroup.toAddCommMonoid AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType LinearMap.instFunLike toOpenₗ const AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
toOpenₗ_top_bijective 📖	mathematical	—	Function.Bijective CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType LinearMap.instFunLike toOpenₗ	—	PrimeSpectrum.basicOpen_one Submonoid.powers_one instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ one_smul IsLocalizedModule.eq_iff_exists IsLocalizedModule.mk'_surjective IsLocalizedModule.mk'_one
toStalk_stalkSpecializes 📖	mathematical	Specializes PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.zariskiTopology	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat TopCat.Sheaf.presheaf AlgebraicGeometry.Spec.structureSheaf toStalk TopCat.Presheaf.stalkSpecializes	—	CommRingCat.Colimits.hasColimits_commRingCat Specializes.mem_open TopologicalSpace.Opens.isOpen CategoryTheory.Category.assoc TopCat.Presheaf.germ_stalkSpecializes
toStalk_stalkSpecializes_apply 📖	mathematical	Specializes PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.zariskiTopology	DFunLike.coe RingHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat TopCat.Sheaf.presheaf AlgebraicGeometry.Spec.structureSheaf Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier TopCat.Presheaf.stalkSpecializes CommRingCat.of toStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toStalk_stalkSpecializes
toStalk_stalkSpecializes_assoc 📖	mathematical	Specializes PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.zariskiTopology	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat toStalk TopCat.Sheaf.presheaf AlgebraicGeometry.Spec.structureSheaf TopCat.Presheaf.stalkSpecializes	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toStalk_stalkSpecializes
to_basicOpen_epi 📖	mathematical	—	CategoryTheory.Epi CommRingCat CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op PrimeSpectrum.basicOpen CommRing.toCommSemiring CommRingCat.commRing CommRingCat.ofHom algebraMap CommSemiring.toSemiring openAlgebra	—	CommRingCat.hom_ext IsLocalization.ringHom_ext IsLocalization.to_basicOpen CommRingCat.hom_ext_iff

AlgebraicGeometry.StructureSheaf.IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_basicOpen 📖	mathematical	—	IsLocalization.Away CommRing.toCommSemiring CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf Opposite.op PrimeSpectrum.basicOpen CommRingCat.commRing AlgebraicGeometry.StructureSheaf.openAlgebra	—	AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen
to_stalk 📖	mathematical	—	IsLocalization.AtPrime CommRing.toCommSemiring CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top TopCat.Sheaf.presheaf AlgebraicGeometry.Spec.structureSheaf CommRingCat.commRing AlgebraicGeometry.StructureSheaf.stalkAlgebra PrimeSpectrum.asIdeal PrimeSpectrum.isPrime	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime AlgebraicGeometry.StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal

AlgebraicGeometry.StructureSheaf.Localizations

Definitions

Name	Category	Theorems
comapFun 📖	CompOp	1 math math: comapFun_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comapFun_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.StructureSheaf.Localizations PrimeSpectrum.comap OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.primeCompl PrimeSpectrum.asIdeal OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommGroup.toAddCommMonoid Module.toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id LinearMap.instFunLike comapFun Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike RingHom RingHom.instFunLike PrimeSpectrum.isPrime	—	PrimeSpectrum.isPrime IsScalarTower.left IsScalarTower.right smulCommClass_self Module.End.isUnit_iff IsLocalizedModule.map_units localizedModuleIsLocalizedModule RingHom.instRingHomClass LinearMap.map_smulₛₗ Submonoid.smul_def LocalizedModule.mk_cancel LocalizedModule.mkLinearMap_apply IsLocalizedModule.lift_apply

AlgebraicGeometry.structureSheafInType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	TopCat.PrelocalPredicate.pred AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.StructureSheaf.Localizations TopCat.LocalPredicate.toPrelocalPredicate AlgebraicGeometry.StructureSheaf.isLocallyFraction Opposite.unop TopologicalSpace.Opens TopCat.carrier TopCat.str Opposite.op CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType SetLike.instMembership TopologicalSpace.Opens.instSetLike OreLocalization.instAdd MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Ideal.primeCompl PrimeSpectrum.asIdeal OreLocalization.oreSetComm CommSemiring.toCommMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—
mul_apply 📖	mathematical	—	TopCat.PrelocalPredicate.pred AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.StructureSheaf.Localizations Ring.toAddCommGroup CommRing.toRing Algebra.toModule CommRing.toCommSemiring CommSemiring.toSemiring TopCat.LocalPredicate.toPrelocalPredicate AlgebraicGeometry.StructureSheaf.isLocallyFraction Opposite.unop TopologicalSpace.Opens TopCat.carrier TopCat.str Opposite.op CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType SetLike.instMembership TopologicalSpace.Opens.instSetLike LocalizedModule.instCommRing Ideal.primeCompl PrimeSpectrum.asIdeal	—	—
smul_apply 📖	mathematical	—	TopCat.PrelocalPredicate.pred AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.StructureSheaf.Localizations TopCat.LocalPredicate.toPrelocalPredicate AlgebraicGeometry.StructureSheaf.isLocallyFraction Opposite.unop TopologicalSpace.Opens TopCat.carrier TopCat.str Opposite.op CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AlgebraicGeometry.instAddCommGroupObjOppositeOpensCarrierTopValStructureSheafInType DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid AlgebraicGeometry.instModuleObjOppositeOpensCarrierTopValStructureSheafInType SetLike.instMembership TopologicalSpace.Opens.instSetLike OreLocalization.instSMulOfIsScalarTower Ideal.primeCompl PrimeSpectrum.asIdeal OreLocalization.oreSetComm CommSemiring.toCommMonoid DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Algebra.toSMul Algebra.id IsScalarTower.left IsScalarTower.right	—	—

---

← Back to Index