Documentation Verification Report

StructureSheaf

📁 Source: Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

Statistics

Metric	Count
Definitions `stalkIso'`, `toLocallyRingedSpace`, `toSheafedSpace`, `structureSheaf`, `IsFraction`, `commRingStructureSheafInTypeObj`, `isFractionPrelocal`, `isLocallyFraction`, `sectionsSubring`, `structurePresheafCompForget`, `structurePresheafInCommRing`, `structureSheafInType`, `homogeneousLocalizationToStalk`, `openToLocalization`, `sectionInBasicOpen`, `stalkToFiberRingHom`	16
Theorems `add_apply`, `ext`, `ext_iff`, `mul_apply`, `one_apply`, `pow_apply`, `res_apply`, `stalkIso'_germ`, `stalkIso'_symm_mk`, `sub_apply`, `zero_apply`, `add_mem'`, `mul_mem'`, `neg_mem'`, `one_mem'`, `zero_mem'`, `structurePresheafInCommRing_obj_carrier`, `germ_comp_stalkToFiberRingHom`, `homogeneousLocalizationToStalk_stalkToFiberRingHom`, `mem_basicOpen_den`, `stalkToFiberRingHom_germ`, `stalkToFiberRingHom_homogeneousLocalizationToStalk`	22
Total	38

AlgebraicGeometry

Definitions

Name	Category	Theorems
`homogeneousLocalizationToStalk` 📖	CompOp	2 math math: `stalkToFiberRingHom_homogeneousLocalizationToStalk`, `homogeneousLocalizationToStalk_stalkToFiberRingHom`
`openToLocalization` 📖	CompOp	1 math math: `germ_comp_stalkToFiberRingHom`
`sectionInBasicOpen` 📖	CompOp	1 math math: `Proj.stalkIso'_symm_mk`
`stalkToFiberRingHom` 📖	CompOp	4 math math: `stalkToFiberRingHom_homogeneousLocalizationToStalk`, `germ_comp_stalkToFiberRingHom`, `stalkToFiberRingHom_germ`, `homogeneousLocalizationToStalk_stalkToFiberRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`germ_comp_stalkToFiberRingHom` 📖	mathematical	`TopCat.carrier` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `ProjectiveSpectrum.Proj.structureSheaf` `Opposite.op` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `CommRingCat.of` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Ideal.primeCompl` `TopCat.Presheaf.germ` `stalkToFiberRingHom` `openToLocalization`	—	`AddSubgroupClass.toAddSubmonoidClass` `CategoryTheory.Limits.colimit.ι_desc` `CommRingCat.Colimits.hasColimits_commRingCat`
`homogeneousLocalizationToStalk_stalkToFiberRingHom` 📖	mathematical	—	`homogeneousLocalizationToStalk` `DFunLike.coe` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `TopCat.Sheaf.presheaf` `ProjectiveSpectrum.Proj.structureSheaf` `CommRingCat.of` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Ideal.primeCompl` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `stalkToFiberRingHom`	—	`AddSubgroupClass.toAddSubmonoidClass` `CommRingCat.Colimits.hasColimits_commRingCat` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `TopCat.Presheaf.germ_exist` `CommRingCat.FilteredColimits.forget_preservesFilteredColimits` `stalkToFiberRingHom_germ` `mem_basicOpen_den` `homogeneousLocalizationToStalk.eq_1` `Quotient.liftOn'_mk''` `TopCat.Presheaf.germ_ext` `HomogeneousLocalization.val_injective` `Proj.res_apply` `Localization.isLocalization` `HomogeneousLocalization.NumDenSameDeg.den_mem` `Localization.mk_eq_mk'`
`mem_basicOpen_den` 📖	mathematical	—	`TopCat.carrier` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `TopologicalSpace.Opens` `ProjectiveSpectrum` `ProjectiveSpectrum.zariskiTopology` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `ProjectiveSpectrum.basicOpen` `HomogeneousLocalization.NumDenSameDeg.deg` `Ideal.primeCompl` `Ring.toSemiring` `HomogeneousIdeal.toIdeal` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.NumDenSameDeg.den`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `ProjectiveSpectrum.mem_basicOpen` `HomogeneousLocalization.NumDenSameDeg.den_mem`
`stalkToFiberRingHom_germ` 📖	mathematical	`TopCat.carrier` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`DFunLike.coe` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `TopCat.Sheaf.presheaf` `ProjectiveSpectrum.Proj.structureSheaf` `CommRingCat.of` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Ideal.primeCompl` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `stalkToFiberRingHom` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `TopCat.Presheaf.germ` `TopCat.PrelocalPredicate.pred` `TopCat.LocalPredicate.toPrelocalPredicate` `ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CommRingCat.Colimits.hasColimits_commRingCat` `RingHom.ext_iff` `CommRingCat.hom_ext_iff` `germ_comp_stalkToFiberRingHom`
`stalkToFiberRingHom_homogeneousLocalizationToStalk` 📖	mathematical	—	`DFunLike.coe` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `TopCat.Sheaf.presheaf` `ProjectiveSpectrum.Proj.structureSheaf` `CommRingCat.of` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Ideal.primeCompl` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `stalkToFiberRingHom` `homogeneousLocalizationToStalk`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CommRingCat.Colimits.hasColimits_commRingCat` `Quotient.mk''_surjective` `mem_basicOpen_den` `homogeneousLocalizationToStalk.eq_1` `Quotient.liftOn'_mk''` `stalkToFiberRingHom_germ` `sectionInBasicOpen.eq_1`

AlgebraicGeometry.Proj

Definitions

Name	Category	Theorems
`stalkIso'` 📖	CompOp	5 math math: `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk`, `stalkIso'_germ`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ`, `stalkIso'_symm_mk`
`toLocallyRingedSpace` 📖	CompOp	24 math math: `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec`, `AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply`, `AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen`, `AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app`, `AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective`
`toSheafedSpace` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instAdd` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass`
`ext` 📖	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str`	—	—	`AddSubgroupClass.toAddSubmonoidClass`
`ext_iff` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str`	—	`AddSubgroupClass.toAddSubmonoidClass` `ext`
`mul_apply` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instMul` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass`
`one_apply` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `CommRingCat.commRing` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instOne` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass`
`pow_apply` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommRingCat.commRing` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.hasPow` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass`
`res_apply` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `TopologicalSpace.Opens.opensHom.instFunLike` `Quiver.Hom.unop`	—	`AddSubgroupClass.toAddSubmonoidClass`
`stalkIso'_germ` 📖	mathematical	`TopCat.carrier` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`DFunLike.coe` `RingEquiv` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `HomogeneousLocalization.instMul` `Nat.instAddCommMonoid` `Ideal.primeCompl` `Distrib.toAdd` `HomogeneousLocalization.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `stalkIso'` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ` `TopCat.PrelocalPredicate.pred` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop`	—	`AddSubgroupClass.toAddSubmonoidClass` `AlgebraicGeometry.stalkToFiberRingHom_germ`
`stalkIso'_symm_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `ProjectiveSpectrum.top` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `HomogeneousLocalization.instMul` `Nat.instAddCommMonoid` `Ideal.primeCompl` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `HomogeneousLocalization.instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `stalkIso'` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `ProjectiveSpectrum.basicOpen` `SetLike.instMembership` `HomogeneousLocalization.NumDenSameDeg.deg` `Ring.toSemiring` `HomogeneousLocalization.NumDenSameDeg.den` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ` `AlgebraicGeometry.mem_basicOpen_den` `AlgebraicGeometry.sectionInBasicOpen`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CommRingCat.Colimits.hasColimits_commRingCat`
`sub_apply` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `SubNegMonoid.toSub` `CommRingCat.commRing` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instSub` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass`
`zero_apply` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instZero` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass`

AlgebraicGeometry.ProjectiveSpectrum.Proj

Definitions

Name	Category	Theorems
`structureSheaf` 📖	CompOp	17 math math: `awayToSection_apply`, `AlgebraicGeometry.Proj.pow_apply`, `AlgebraicGeometry.Proj.mul_apply`, `AlgebraicGeometry.Proj.one_apply`, `awayToΓ_ΓToStalk`, `AlgebraicGeometry.Proj.sub_apply`, `AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk`, `AlgebraicGeometry.germ_comp_stalkToFiberRingHom`, `AlgebraicGeometry.Proj.zero_apply`, `AlgebraicGeometry.Proj.add_apply`, `AlgebraicGeometry.stalkToFiberRingHom_germ`, `AlgebraicGeometry.Proj.stalkIso'_germ`, `stalkMap_toSpec`, `awayToSection_germ`, `AlgebraicGeometry.Proj.res_apply`, `AlgebraicGeometry.Proj.stalkIso'_symm_mk`, `AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom`

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Definitions

Name	Category	Theorems
`IsFraction` 📖	MathDef	—
`commRingStructureSheafInTypeObj` 📖	CompOp	—
`isFractionPrelocal` 📖	CompOp	—
`isLocallyFraction` 📖	CompOp	13 math math: `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply`, `AlgebraicGeometry.Proj.pow_apply`, `AlgebraicGeometry.Proj.mul_apply`, `AlgebraicGeometry.Proj.one_apply`, `AlgebraicGeometry.Proj.sub_apply`, `AlgebraicGeometry.Proj.zero_apply`, `SectionSubring.one_mem'`, `AlgebraicGeometry.Proj.ext_iff`, `AlgebraicGeometry.Proj.add_apply`, `AlgebraicGeometry.stalkToFiberRingHom_germ`, `AlgebraicGeometry.Proj.stalkIso'_germ`, `SectionSubring.zero_mem'`, `AlgebraicGeometry.Proj.res_apply`
`sectionsSubring` 📖	CompOp	—
`structurePresheafCompForget` 📖	CompOp	—
`structurePresheafInCommRing` 📖	CompOp	1 math math: `structurePresheafInCommRing_obj_carrier`
`structureSheafInType` 📖	CompOp	1 math math: `structurePresheafInCommRing_obj_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`structurePresheafInCommRing_obj_carrier` 📖	mathematical	—	`CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CommRingCat` `CommRingCat.instCategory` `structurePresheafInCommRing` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `structureSheafInType`	—	`AddSubgroupClass.toAddSubmonoidClass`

AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem'` 📖	mathematical	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str`	`Pi.instAdd` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instAdd` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SetLike.mul_mem_graded` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `add_comm` `Submonoid.mul_mem` `HomogeneousLocalization.NumDenSameDeg.den_mem` `HomogeneousLocalization.val_add`
`mul_mem'` 📖	mathematical	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str`	`Pi.instMul` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instMul` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `SetLike.mul_mem_graded` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `Submonoid.mul_mem` `HomogeneousLocalization.NumDenSameDeg.den_mem` `HomogeneousLocalization.val_mul` `Localization.mk_mul`
`neg_mem'` 📖	mathematical	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str`	`Pi.instNeg` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instNeg` `AddSubgroupClass.toNegMemClass` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `AddSubgroupClass.toNegMemClass` `NegMemClass.neg_mem` `HomogeneousLocalization.NumDenSameDeg.den_mem` `HomogeneousLocalization.val_neg`
`one_mem'` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Pi.instOne` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instOne` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `SetLike.one_mem_graded` `SetLike.GradedMonoid.toGradedOne` `GradedRing.toGradedMonoid`
`zero_mem'` 📖	mathematical	—	`TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Pi.instZero` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `HomogeneousLocalization.instZero` `Nat.instAddCommMonoid` `Ideal.primeCompl`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `SetLike.one_mem_graded` `SetLike.GradedMonoid.toGradedOne` `GradedRing.toGradedMonoid`

---

← Back to Index