Documentation Verification Report

Functor

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

Statistics

Metric	Count
Definitions `comapStructureSheaf`, `comapStructureSheafFun`, `map`, `mapAffineOpenCover`, `sheafedSpaceMap`, `comap`, `comapFun`	7
Theorems `awayToSection_comp_appLE`, `awayToSection_comp_appLE_assoc`, `awayι_comp_map`, `awayι_comp_map_assoc`, `germ_map_sectionInBasicOpen`, `isLocallyFraction_comapStructureSheafFun`, `localRingHom_comp_stalkIso`, `localRingHom_comp_stalkIso_apply`, `mapAffineOpenCover_I₀`, `mapAffineOpenCover_f`, `map_comp`, `map_id`, `map_preimage_basicOpen`, `sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier`, `sheafedSpaceMap_hom_c_app_hom_apply_coe`, `val_sectionInBasicOpen_apply`, `ι_comp_map`, `comapFun_asHomogeneousIdeal`	18
Total	25

AlgebraicGeometry.Proj

Definitions

Name	Category	Theorems
`comapStructureSheaf` 📖	CompOp	—
`comapStructureSheafFun` 📖	CompOp	2 math math: `isLocallyFraction_comapStructureSheafFun`, `sheafedSpaceMap_hom_c_app_hom_apply_coe`
`map` 📖	CompOp	8 math math: `map_preimage_basicOpen`, `ι_comp_map`, `awayι_comp_map_assoc`, `map_comp`, `map_id`, `awayToSection_comp_appLE`, `awayToSection_comp_appLE_assoc`, `awayι_comp_map`
`mapAffineOpenCover` 📖	CompOp	2 math math: `mapAffineOpenCover_I₀`, `mapAffineOpenCover_f`
`sheafedSpaceMap` 📖	CompOp	5 math math: `sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier`, `germ_map_sectionInBasicOpen`, `sheafedSpaceMap_hom_c_app_hom_apply_coe`, `localRingHom_comp_stalkIso_apply`, `localRingHom_comp_stalkIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`awayToSection_comp_appLE` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map` `SetLike.instMembership`	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CommRingCat.of` `HomogeneousLocalization.Away` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Proj` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `basicOpen` `DFunLike.coe` `GradedRingHom` `GradedRingHom.instFunLike` `awayToSection` `AlgebraicGeometry.Scheme.Hom.appLE` `map` `CommRingCat.ofHom` `HomogeneousLocalization.Away.map`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `CommRingCat.hom_ext` `RingHom.ext` `HomogeneousLocalization.Away.mk_surjective` `Graded.map_mem` `GradedRingHom.instGradedFunLike` `HomogeneousLocalization.val_injective` `HomogeneousLocalization.NumDenSameDeg.den_mem` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `GradedRingHom.instRingHomClass`
`awayToSection_comp_appLE_assoc` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map` `SetLike.instMembership`	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CommRingCat.of` `HomogeneousLocalization.Away` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Proj` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `basicOpen` `awayToSection` `DFunLike.coe` `GradedRingHom` `GradedRingHom.instFunLike` `AlgebraicGeometry.Scheme.Hom.appLE` `map` `CommRingCat.ofHom` `HomogeneousLocalization.Away.map`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `awayToSection_comp_appLE`
`awayι_comp_map` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map` `SetLike.instMembership`	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Spec` `CommRingCat.of` `HomogeneousLocalization.Away` `DFunLike.coe` `GradedRingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GradedRingHom.instFunLike` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgebraicGeometry.Proj` `awayι` `GradedRingHom.map_mem` `map` `AlgebraicGeometry.Spec.map` `CommRingCat.ofHom` `HomogeneousLocalization.Away.map`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `GradedRingHom.map_mem` `awayι.eq_1` `CategoryTheory.Category.assoc` `le_rfl` `ι_comp_map` `CategoryTheory.Iso.inv_comp_eq` `CategoryTheory.Iso.eq_comp_inv` `AlgebraicGeometry.ext_to_Spec` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `LE.le.trans` `basicOpenToSpec_app_top` `CategoryTheory.eqToHom_op` `AlgebraicGeometry.Scheme.Hom.resLE_app_top` `AlgebraicGeometry.Scheme.Hom.appLE_map` `AlgebraicGeometry.Scheme.Hom.map_appLE` `CategoryTheory.Iso.inv_hom_id_assoc` `awayToSection_comp_appLE` `AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc` `CategoryTheory.eqToHom_map_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`awayι_comp_map_assoc` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map` `SetLike.instMembership`	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Spec` `CommRingCat.of` `HomogeneousLocalization.Away` `DFunLike.coe` `GradedRingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GradedRingHom.instFunLike` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgebraicGeometry.Proj` `awayι` `GradedRingHom.map_mem` `map` `AlgebraicGeometry.Spec.map` `CommRingCat.ofHom` `HomogeneousLocalization.Away.map`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `GradedRingHom.map_mem` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `awayι_comp_map`
`germ_map_sectionInBasicOpen` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `toSheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `CategoryTheory.InducedCategory.Hom.hom` `AlgebraicGeometry.SheafedSpace` `AlgebraicGeometry.PresheafedSpace` `AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces` `sheafedSpaceMap` `Opposite.unop` `ProjectiveSpectrum.top` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ProjectiveSpectrum.basicOpen` `SetLike.instMembership` `HomogeneousLocalization.NumDenSameDeg.deg` `Ideal.primeCompl` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HomogeneousIdeal.toIdeal` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ContinuousMap` `ProjectiveSpectrum` `ProjectiveSpectrum.zariskiTopology` `ContinuousMap.instFunLike` `AlgebraicGeometry.ProjectiveSpectrum.comap` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.NumDenSameDeg.den` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ` `AlgebraicGeometry.mem_basicOpen_den` `TopCat` `TopCat.instCategory` `TopCat.instConcreteCategoryContinuousMapCarrier` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward` `CategoryTheory.NatTrans.app` `AlgebraicGeometry.PresheafedSpace.Hom.c` `AlgebraicGeometry.sectionInBasicOpen` `GradedRingHom` `GradedRingHom.instFunLike` `HomogeneousLocalization.NumDenSameDeg.den_mem` `HomogeneousLocalization.NumDenSameDeg.map` `Submonoid.comap` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `GradedRingHom.instRingHomClass` `le_rfl` `Submonoid` `Submonoid.instPartialOrder`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.mem_basicOpen_den`
`isLocallyFraction_comapStructureSheafFun` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map` `Set` `ProjectiveSpectrum` `Set.instHasSubset` `TopologicalSpace.Opens.carrier` `ProjectiveSpectrum.zariskiTopology` `Set.preimage` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `AlgebraicGeometry.ProjectiveSpectrum.comap` `TopCat.PrelocalPredicate.pred` `ProjectiveSpectrum.top` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction`	`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` `comapStructureSheafFun`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.val_injective` `HomogeneousLocalization.NumDenSameDeg.den_mem` `GradedRingHom.instRingHomClass` `RingHom.instRingHomClass` `HomogeneousLocalization.val_localRingHom`
`localRingHom_comp_stalkIso` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Proj` `AlgebraicGeometry.PresheafedSpace.presheaf` `DFunLike.coe` `ContinuousMap` `ProjectiveSpectrum` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ProjectiveSpectrum.zariskiTopology` `ContinuousMap.instFunLike` `AlgebraicGeometry.ProjectiveSpectrum.comap` `CommRingCat.of` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Ideal.primeCompl` `CategoryTheory.Iso.hom` `stalkIso` `CommRingCat.ofHom` `HomogeneousLocalization.localRingHom` `Ideal` `CategoryTheory.Iso.inv` `AlgebraicGeometry.PresheafedSpace.Hom.stalkMap` `toSheafedSpace` `CategoryTheory.InducedCategory.Hom.hom` `AlgebraicGeometry.SheafedSpace` `AlgebraicGeometry.PresheafedSpace` `AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces` `sheafedSpaceMap`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `CommRingCat.Colimits.hasColimits_commRingCat` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CategoryTheory.Iso.eq_inv_comp` `CategoryTheory.Iso.comp_inv_eq` `CommRingCat.hom_ext` `RingHom.ext` `HomogeneousLocalization.val_injective` `HomogeneousLocalization.mk_surjective` `GradedRingHom.instRingHomClass` `HomogeneousLocalization.NumDenSameDeg.den_mem` `HomogeneousLocalization.val_localRingHom` `RingHom.instRingHomClass` `AlgebraicGeometry.mem_basicOpen_den` `AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `le_rfl` `germ_map_sectionInBasicOpen` `stalkIso'_germ`
`localRingHom_comp_stalkIso_apply` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`DFunLike.coe` `RingHom` `HomogeneousLocalization.AtPrime` `HomogeneousIdeal.toIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Proj` `AlgebraicGeometry.PresheafedSpace.presheaf` `Semiring.toNonAssocSemiring` `CommRingCat.of` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Nat.instAddCommMonoid` `Ideal.primeCompl` `CommRingCat.commRing` `RingHom.instFunLike` `CategoryTheory.ConcreteCategory.hom` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.Iso.inv` `stalkIso` `ContinuousMap` `ProjectiveSpectrum` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ProjectiveSpectrum.zariskiTopology` `ContinuousMap.instFunLike` `AlgebraicGeometry.ProjectiveSpectrum.comap` `HomogeneousLocalization.localRingHom` `Ideal` `CategoryTheory.Iso.hom` `AlgebraicGeometry.PresheafedSpace.Hom.stalkMap` `toSheafedSpace` `CategoryTheory.InducedCategory.Hom.hom` `AlgebraicGeometry.SheafedSpace` `AlgebraicGeometry.PresheafedSpace` `AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces` `sheafedSpaceMap`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `CommRingCat.Colimits.hasColimits_commRingCat` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `CategoryTheory.comp_apply` `Mathlib.Tactic.Elementwise.hom_elementwise` `localRingHom_comp_stalkIso`
`mapAffineOpenCover_I₀` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`AlgebraicGeometry.Scheme.AffineCover.I₀` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Proj` `mapAffineOpenCover` `affineOpenCover`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd`
`mapAffineOpenCover_f` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`AlgebraicGeometry.Scheme.AffineCover.f` `AlgebraicGeometry.IsOpenImmersion` `AlgebraicGeometry.Proj` `mapAffineOpenCover` `awayι` `DFunLike.coe` `GradedRingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GradedRingHom.instFunLike` `SetLike.instMembership` `PNat.val` `PNat`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd`
`map_comp` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`map` `GradedRingHom.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HomogeneousIdeal.irrelevant_le_map_comp` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Proj`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `AlgebraicGeometry.Scheme.Cover.hom_ext` `HomogeneousIdeal.irrelevant_le_map_comp` `awayι_comp_map` `HomogeneousLocalization.Away.map_comp` `AlgebraicGeometry.Spec.map_comp` `CategoryTheory.Category.assoc` `GradedRingHom.map_mem` `Graded.map_mem` `GradedRingHom.instGradedFunLike` `awayι_comp_map_assoc`
`map_id` 📖	mathematical	—	`map` `GradedRingHom.id` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CategoryTheory.CategoryStruct.id` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Proj`	—	`AddSubgroupClass.toAddSubmonoidClass` `AlgebraicGeometry.Scheme.Cover.hom_ext` `GradedRingHom.map_mem` `CategoryTheory.Category.comp_id` `HomogeneousLocalization.Away.map_id` `AlgebraicGeometry.Spec.map_id` `CategoryTheory.Category.id_comp` `awayι_comp_map`
`map_preimage_basicOpen` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.Proj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `map` `basicOpen` `DFunLike.coe` `GradedRingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GradedRingHom.instFunLike`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd`
`sheafedSpaceMap_hom_base_hom_apply_asHomogeneousIdeal_carrier` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`SetLike.coe` `HomogeneousSubmodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Nat.instAddMonoid` `GradedRing.toDecomposition` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `HomogeneousSubmodule.setLike` `ProjectiveSpectrum.asHomogeneousIdeal` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `ContinuousMap` `ProjectiveSpectrum` `ProjectiveSpectrum.zariskiTopology` `ContinuousMap.instFunLike` `TopCat.Hom.hom` `TopCat.of` `AlgebraicGeometry.PresheafedSpace.Hom.base` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `toSheafedSpace` `CategoryTheory.InducedCategory.Hom.hom` `AlgebraicGeometry.SheafedSpace` `AlgebraicGeometry.PresheafedSpace` `AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces` `sheafedSpaceMap` `Set.preimage` `GradedRingHom` `GradedRingHom.instFunLike` `HomogeneousIdeal`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd`
`sheafedSpaceMap_hom_c_app_hom_apply_coe` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`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` `Opposite.op` `CategoryTheory.Functor.obj` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `toSheafedSpace` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `TopCat.ofHom` `ProjectiveSpectrum` `ProjectiveSpectrum.zariskiTopology` `AlgebraicGeometry.ProjectiveSpectrum.comap` `DFunLike.coe` `RingHom` `CommRingCat.carrier` `Opposite` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `Opens.grothendieckTopology` `AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf` `Semiring.toNonAssocSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.Hom.hom` `CommRingCat.of` `CategoryTheory.types` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.commRingStructureSheafInTypeObj` `CategoryTheory.Functor.op` `CategoryTheory.NatTrans.app` `AlgebraicGeometry.PresheafedSpace.presheaf` `TopCat.Presheaf` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward` `AlgebraicGeometry.PresheafedSpace.Hom.c` `CategoryTheory.InducedCategory.Hom.hom` `AlgebraicGeometry.SheafedSpace` `AlgebraicGeometry.PresheafedSpace` `AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces` `sheafedSpaceMap` `comapStructureSheafFun`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal`
`val_sectionInBasicOpen_apply` 📖	mathematical	—	`HomogeneousLocalization.val` `Ideal.primeCompl` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HomogeneousIdeal.toIdeal` `Nat.instAddMonoid` `ProjectiveSpectrum.asHomogeneousIdeal` `TopCat.carrier` `ProjectiveSpectrum.top` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Opposite.unop` `Opposite.op` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `ProjectiveSpectrum.basicOpen` `HomogeneousLocalization.NumDenSameDeg.deg` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal` `HomogeneousLocalization.NumDenSameDeg.den` `TopCat.PrelocalPredicate.pred` `HomogeneousLocalization.AtPrime` `TopCat.LocalPredicate.toPrelocalPredicate` `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction` `AlgebraicGeometry.sectionInBasicOpen` `CommRing.toCommMonoid` `HomogeneousLocalization.NumDenSameDeg.num` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid.instSetLike` `ProjectiveSpectrum` `ProjectiveSpectrum.zariskiTopology`	—	`AddSubgroupClass.toAddSubmonoidClass` `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal`
`ι_comp_map` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Opens.toScheme` `AlgebraicGeometry.Proj` `basicOpen` `DFunLike.coe` `GradedRingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `GradedRingHom.instFunLike` `AlgebraicGeometry.Scheme.Opens.ι` `map` `CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `AlgebraicGeometry.Scheme.Hom.resLE` `le_rfl` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd` `le_rfl` `AlgebraicGeometry.Scheme.Hom.resLE_comp_ι`

AlgebraicGeometry.ProjectiveSpectrum

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	4 math math: `AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen`, `AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe`, `AlgebraicGeometry.Proj.localRingHom_comp_stalkIso_apply`, `AlgebraicGeometry.Proj.localRingHom_comp_stalkIso`
`comapFun` 📖	CompOp	1 math math: `comapFun_asHomogeneousIdeal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comapFun_asHomogeneousIdeal` 📖	mathematical	`HomogeneousIdeal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `HomogeneousIdeal.irrelevant` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `HomogeneousIdeal.map`	`ProjectiveSpectrum.asHomogeneousIdeal` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `comapFun` `HomogeneousIdeal.comap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid`	—	`AddSubgroupClass.toAddSubmonoidClass` `Nat.instCanonicallyOrderedAdd`

---

← Back to Index