Scheme

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

Statistics

Metric	Count
Definitions Proj, carrier, asHomogeneousIdeal, asIdeal, tacticMem_tac, toFun, carrier, toFun, fromSpec, toSpec, awayToSection, awayToΓ, specStalkEquiv, toSpec, projIsoSpec, projIsoSpecTopComponent, «termProj|_»	17
Theorems add_mem, homogeneous, ne_top, prime, denom_notMem, relevant, smul_mem, zero_mem, mem_carrier_iff, mem_carrier_iff', mem_carrier_iff_of_mem, mem_carrier_iff_of_mem_mul, num_mem_carrier_iff, isPrime_carrier, mk_mem_carrier, preimage_basicOpen, toFun_asIdeal, fromSpec_toSpec, image_basicOpen_eq_basicOpen, toSpec_bijective, toSpec_fromSpec, toSpec_hom_apply_asIdeal, toSpec_injective, toSpec_preimage_basicOpen, toSpec_surjective, awayToSection_apply, awayToSection_germ, awayToΓ_ΓToStalk, isIso_toSpec, isLocalization_atPrime, mk_mem_toSpec_base_apply, stalkMap_toSpec, toOpen_toSpec_val_c_app, toOpen_toSpec_val_c_app_assoc, toSpec_base_apply_eq, toSpec_base_apply_eq_comap, toSpec_base_isIso, toSpec_preimage_basicOpen, toStalk_specStalkEquiv, toStalk_stalkMap_toSpec, toStalk_stalkMap_toSpec_assoc	41
Total	58

AlgebraicGeometry

Definitions

Name	Category	Theorems
Proj 📖	CompOp	50 math math: Proj.awayMap_awayToSection_assoc, Proj.fromOfGlobalSections_resLE, Proj.basicOpenIsoSpec_inv_ι_assoc, Proj.fromOfGlobalSections_toSpecZero_assoc, Proj.basicOpenIsoAway_hom, Proj.instIsSeparated, Proj.basicOpenToSpec_app_top, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, Proj.isAffineOpen_basicOpen, Proj.pullbackAwayιIso_inv_snd_assoc, Proj.mem_basicOpen, Proj.SpecMap_awayMap_awayι_assoc, Proj.pullbackAwayιIso_inv_fst, Proj.iSup_basicOpen_eq_top', Proj.basicOpenToSpec_SpecMap_awayMap, Proj.valuativeCriterion_existence, Proj.instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Proj.basicOpenIsoSpec_inv_ι, Proj.isSeparated, Proj.pullbackAwayιIso_inv_snd, Proj.pullbackAwayιIso_inv_fst_assoc, Proj.basicOpen_mul, Proj.pullbackAwayιIso_hom_awayι, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, Proj.awayι_toSpecZero, Proj.basicOpen_mono, Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc, Proj.awayι_toSpecZero_assoc, Proj.basicOpen_one, Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, Proj.fromOfGlobalSections_toSpecZero, Proj.opensRange_awayι, Proj.basicOpen_eq_iSup_proj, Proj.isBasis_basicOpen, Proj.instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Proj.fromOfGlobalSections_morphismRestrict, Proj.basicOpenToSpec_SpecMap_awayMap_assoc, Proj.pullbackAwayιIso_hom_awayι_assoc, Proj.awayι_preimage_basicOpen, Proj.awayMap_awayToSection, Proj.SpecMap_awayMap_awayι, Proj.basicOpen_zero, Proj.basicOpenIsoSpec_hom, Proj.homOfLE_toBasicOpenOfGlobalSections_ι, Proj.instIsOpenImmersionAwayι, Proj.iSup_basicOpen_eq_top, Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, Proj.fromOfGlobalSections_preimage_basicOpen
projIsoSpec 📖	CompOp	—
projIsoSpecTopComponent 📖	CompOp	—
«termProj|_» 📖	CompOp	—

AlgebraicGeometry.ProjIsoSpecTopComponent

Definitions

Name	Category	Theorems
fromSpec 📖	CompOp	—
toSpec 📖	CompOp	9 math math: toSpec_injective, toSpec_fromSpec, toSpec_hom_apply_asIdeal, toSpec_surjective, fromSpec_toSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, toSpec_preimage_basicOpen, toSpec.image_basicOpen_eq_basicOpen, toSpec_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSpec_toSpec 📖	mathematical	SetLike.instMembership	FromSpec.toFun DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier toSpec	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding ProjectiveSpectrum.ext HomogeneousIdeal.ext' SetLike.pow_mem_graded GradedRing.toGradedMonoid FromSpec.mem_carrier_iff_of_mem ToSpec.mk_mem_carrier Ideal.IsPrime.pow_mem_iff_mem ProjectiveSpectrum.isPrime
toSpec_bijective 📖	mathematical	SetLike.instMembership	Function.Bijective TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier toSpec	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding toSpec_injective toSpec_surjective
toSpec_fromSpec 📖	mathematical	SetLike.instMembership	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier toSpec FromSpec.toFun	—	AddSubgroupClass.toAddSubmonoidClass PrimeSpectrum.ext TopologicalSpace.Opens.isOpenEmbedding Ideal.ext HomogeneousLocalization.mk_surjective FromSpec.num_mem_carrier_iff ToSpec.mk_mem_carrier
toSpec_hom_apply_asIdeal 📖	mathematical	—	PrimeSpectrum.asIdeal CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing DFunLike.coe ContinuousMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Proj.toLocallyRingedSpace TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike ProjectiveSpectrum.basicOpen PrimeSpectrum instTopologicalSpaceSubtype PrimeSpectrum.zariskiTopology ContinuousMap.instFunLike TopCat.Hom.hom AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj toSpec ToSpec.carrier	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding
toSpec_injective 📖	mathematical	SetLike.instMembership	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier toSpec	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding fromSpec_toSpec
toSpec_preimage_basicOpen 📖	mathematical	—	Set.preimage TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier toSpec SetLike.coe PrimeSpectrum HomogeneousLocalization PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen ProjectiveSpectrum SetLike.instMembership ProjectiveSpectrum.zariskiTopology HomogeneousLocalization.NumDenSameDeg.deg HomogeneousLocalization.NumDenSameDeg.num	—	AddSubgroupClass.toAddSubmonoidClass ToSpec.preimage_basicOpen
toSpec_surjective 📖	mathematical	SetLike.instMembership	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier toSpec	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding Function.surjective_iff_hasRightInverse toSpec_fromSpec

AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec

Definitions

Name	Category	Theorems
carrier 📖	CompOp	6 math math: carrier.zero_mem, mem_carrier_iff', mem_carrier_iff, mem_carrier_iff_of_mem_mul, mem_carrier_iff_of_mem, num_mem_carrier_iff
tacticMem_tac 📖	CompOp	—
toFun 📖	CompOp	2 math math: AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_carrier_iff 📖	mathematical	SetLike.instMembership	Set Set.instMembership carrier HomogeneousLocalization Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Ideal CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid CommRingCat.commRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal Monoid.toNatPow DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Ring.toSemiring CommRing.toRing AddMonoidHom.instFunLike GradedRing.proj Nat.instAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	AddSubgroupClass.toAddSubmonoidClass
mem_carrier_iff' 📖	mathematical	SetLike.instMembership	Set Set.instMembership carrier Localization CommRing.toCommMonoid Submonoid.powers CommMonoid.toMonoid Localization.Away Set.image HomogeneousLocalization.Away DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.oreSetComm RingHom.instFunLike algebraMap HomogeneousLocalization.homogeneousLocalizationAlgebra setOf Ideal CommRingCat.carrier CommRingCat.of CommRingCat.commRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal Monoid.toNatPow AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidHom.instFunLike GradedRing.proj Nat.instAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Submonoid Monoid.toMulOneClass Submonoid.instSetLike	—	AddSubgroupClass.toAddSubmonoidClass mem_carrier_iff Set.mem_image HomogeneousLocalization.ext_iff_val HomogeneousLocalization.NumDenSameDeg.den_mem
mem_carrier_iff_of_mem 📖	mathematical	SetLike.instMembership	Set Set.instMembership carrier HomogeneousLocalization Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Ideal CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid CommRingCat.commRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal Monoid.toNatPow SetLike.pow_mem_graded Nat.instAddMonoid GradedRing.toGradedMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	AddSubgroupClass.toAddSubmonoidClass smul_eq_mul SetLike.pow_mem_graded GradedRing.toGradedMonoid SetLike.coe_mem mul_comm HomogeneousLocalization.val_injective DirectSum.decompose_of_mem_ne zero_pow LT.lt.ne' Localization.mk_zero HomogeneousLocalization.NumDenSameDeg.den_mem HomogeneousLocalization.val_zero ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass DirectSum.decompose_of_mem_same
mem_carrier_iff_of_mem_mul 📖	mathematical	SetLike.instMembership	Set Set.instMembership carrier HomogeneousLocalization Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Ideal CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid CommRingCat.commRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal CommMagma.toMul NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalCommSemiring.toNonUnitalNonAssocCommSemiring CommSemiring.toNonUnitalCommSemiring Nat.instCommSemiring mul_comm Monoid.toNatPow	—	AddSubgroupClass.toAddSubmonoidClass mul_comm SetLike.pow_mem_graded GradedRing.toGradedMonoid mem_carrier_iff_of_mem Ideal.IsPrime.pow_mem_iff_mem PrimeSpectrum.isPrime HomogeneousLocalization.val_injective Submonoid.instSubmonoidClass HomogeneousLocalization.NumDenSameDeg.den_mem pow_mul HomogeneousLocalization.val_pow Localization.mk_pow
num_mem_carrier_iff 📖	mathematical	SetLike.instMembership	Set Set.instMembership carrier HomogeneousLocalization.NumDenSameDeg.deg Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring HomogeneousLocalization.NumDenSameDeg.num HomogeneousLocalization Ideal CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid CommRingCat.commRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal	—	AddSubgroupClass.toAddSubmonoidClass HomogeneousLocalization.NumDenSameDeg.den_mem HomogeneousLocalization.subsingleton PrimeSpectrum.instIsEmptyOfSubsingleton DirectSum.degree_eq_of_mem_mem SetLike.pow_mem_graded GradedRing.toGradedMonoid smul_eq_mul mul_comm HomogeneousLocalization.val_injective mem_carrier_iff_of_mem_mul

AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier

Definitions

Name	Category	Theorems
asHomogeneousIdeal 📖	CompOp	1 math math: relevant
asIdeal 📖	CompOp	3 math math: denom_notMem, asIdeal.homogeneous, asIdeal.prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem 📖	mathematical	SetLike.instMembership Set Set.instMembership AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	AddSubgroupClass.toAddSubmonoidClass Ideal.IsPrime.mem_or_mem PrimeSpectrum.isPrime map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass add_pow Finset.sum_congr mul_comm add_smul SetLike.GradedMul.mul_mem SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid SetLike.pow_mem_graded SetLike.coe_mem smul_eq_mul HomogeneousLocalization.ext_iff_val HomogeneousLocalization.NumDenSameDeg.den_mem map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Localization.mk_sum HomogeneousLocalization.val_smul LT.lt.not_ge Finset.mem_range IsScalarTower.right HomogeneousLocalization.val_mul Localization.mk_mul mul_assoc pow_add add_comm le_of_not_ge Ideal.sum_mem nsmul_mem Submodule.addSubmonoidClass Ideal.zero_mem Ideal.mul_mem_left Ideal.mul_mem_right Ideal.instIsTwoSided_1
denom_notMem 📖	mathematical	SetLike.instMembership	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	AddSubgroupClass.toAddSubmonoidClass Ideal.IsPrime.ne_top PrimeSpectrum.isPrime Ideal.eq_top_iff_one HomogeneousLocalization.ext_iff_val HomogeneousLocalization.val_one HomogeneousLocalization.NumDenSameDeg.den_mem DirectSum.decompose_of_mem_same Localization.mk_eq_monoidOf_mk' Submonoid.LocalizationMap.mk'_self
relevant 📖	mathematical	SetLike.instMembership	HomogeneousIdeal Ring.toSemiring CommRing.toRing AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrderHomogeneousIdeal HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd asHomogeneousIdeal	—	AddSubgroupClass.toAddSubmonoidClass Nat.instCanonicallyOrderedAdd denom_notMem DirectSum.decompose_of_mem_ne LT.lt.ne'
smul_mem 📖	mathematical	SetLike.instMembership Set Set.instMembership AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier	Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	AddSubgroupClass.toAddSubmonoidClass DirectSum.Decomposition.inductionOn zero_smul zero_mem DirectSum.coe_decompose_mul_of_left_mem Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid SetLike.pow_mem_graded GradedRing.toGradedMonoid mul_comm SetLike.coe_mem HomogeneousLocalization.ext_iff_val HomogeneousLocalization.NumDenSameDeg.den_mem HomogeneousLocalization.val_mul mul_pow Localization.mk_mul pow_add Ideal.mul_mem_left zero_pow LT.lt.ne' map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass add_smul add_mem
zero_mem 📖	mathematical	SetLike.instMembership	Set Set.instMembership AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	AddSubgroupClass.toAddSubmonoidClass HomogeneousLocalization.ext_iff_val HomogeneousLocalization.NumDenSameDeg.den_mem HomogeneousLocalization.val_zero map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass zero_pow LT.lt.ne' Localization.mk_zero Submodule.zero_mem

AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homogeneous 📖	mathematical	SetLike.instMembership	Ideal.IsHomogeneous CommSemiring.toSemiring CommRing.toCommSemiring AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Nat.instAddMonoid AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal	—	AddSubgroupClass.toAddSubmonoidClass em DirectSum.decompose_coe DirectSum.of_eq_same DirectSum.decompose_of_mem_ne SetLike.coe_mem zero_pow LT.lt.ne' map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem
ne_top 📖	—	SetLike.instMembership	—	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem Submodule.mem_top
prime 📖	mathematical	SetLike.instMembership	Ideal.IsPrime CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal	—	AddSubgroupClass.toAddSubmonoidClass Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem Nat.instIsOrderedCancelAddMonoid homogeneous ne_top and_forall_ne HomogeneousLocalization.ext_iff_val HomogeneousLocalization.NumDenSameDeg.den_mem HomogeneousLocalization.val_zero DirectSum.decompose_of_mem_ne zero_pow LT.lt.ne' Localization.mk_zero Ideal.zero_mem Ideal.IsPrime.mem_or_mem PrimeSpectrum.isPrime DirectSum.decompose_of_mem_same SetLike.GradedMul.mul_mem SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid mul_pow pow_add HomogeneousLocalization.val_mul Localization.mk_mul Submonoid.mul_mem Localization.mk_eq_monoidOf_mk'

AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec

Definitions

Name	Category	Theorems
carrier 📖	CompOp	4 math math: AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, isPrime_carrier, mk_mem_carrier, toFun_asIdeal
toFun 📖	CompOp	2 math math: toFun_asIdeal, preimage_basicOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrime_carrier 📖	mathematical	—	Ideal.IsPrime HomogeneousLocalization.Away CommSemiring.toSemiring CommRing.toCommSemiring HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero carrier	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding Ideal.IsPrime.comap IsLocalization.isPrime_of_isPrime_disjoint Localization.isLocalization ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Ideal.disjoint_powers_iff_notMem Ideal.IsPrime.isRadical
mk_mem_carrier 📖	mathematical	—	HomogeneousLocalization Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Ideal HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule carrier HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike ProjectiveSpectrum.asHomogeneousIdeal TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Proj.toLocallyRingedSpace TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.instSetLike ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne HomogeneousLocalization.NumDenSameDeg.deg HomogeneousLocalization.NumDenSameDeg.num	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding carrier.eq_1 Ideal.mem_comap HomogeneousLocalization.algebraMap_apply HomogeneousLocalization.NumDenSameDeg.den_mem Localization.isLocalization Localization.mk_eq_mk' IsLocalization.mk'_eq_mul_mk'_one mul_comm Ideal.unit_mul_mem_iff_mem isUnit_of_invertible RingHom.instRingHomClass IsLocalization.comap_map_of_isPrime_disjoint ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Ideal.disjoint_powers_iff_notMem Ideal.IsPrime.isRadical
preimage_basicOpen 📖	mathematical	—	Set.preimage TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring toFun SetLike.coe PrimeSpectrum HomogeneousLocalization PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen ProjectiveSpectrum SetLike.instMembership ProjectiveSpectrum.zariskiTopology HomogeneousLocalization.NumDenSameDeg.deg HomogeneousLocalization.NumDenSameDeg.num	—	AddSubgroupClass.toAddSubmonoidClass Set.ext TopologicalSpace.Opens.isOpenEmbedding Iff.not mk_mem_carrier
toFun_asIdeal 📖	mathematical	—	PrimeSpectrum.asIdeal CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing toFun carrier	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding

AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_basicOpen_eq_basicOpen 📖	mathematical	SetLike.instMembership	Set.image TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec Set.preimage TopologicalSpace.Opens.instSetLike SetLike.coe ProjectiveSpectrum ProjectiveSpectrum.zariskiTopology DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike Equiv DirectSum AddSubmonoidClass.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EquivLike.toFunLike Equiv.instEquivLike DirectSum.decompose GradedRing.toDecomposition Nat.instAddMonoid Ring.toSemiring TopologicalSpace.Opens.carrier PrimeSpectrum PrimeSpectrum.zariskiTopology PrimeSpectrum.basicOpen Monoid.toNatPow SetLike.pow_mem_graded GradedRing.toGradedMonoid SetLike.coe_mem smul_eq_mul	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding Set.preimage_injective AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective SetLike.pow_mem_graded GradedRing.toGradedMonoid SetLike.coe_mem smul_eq_mul TopologicalSpace.Opens.carrier_eq_coe AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen ProjectiveSpectrum.basicOpen_pow Set.preimage_image_eq AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective

AlgebraicGeometry.ProjectiveSpectrum.Proj

Definitions

Name	Category	Theorems
awayToSection 📖	CompOp	2 math math: awayToSection_apply, awayToSection_germ
awayToΓ 📖	CompOp	5 math math: toOpen_toSpec_val_c_app_assoc, awayToΓ_ΓToStalk, toStalk_stalkMap_toSpec_assoc, toStalk_stalkMap_toSpec, toOpen_toSpec_val_c_app
specStalkEquiv 📖	CompOp	2 math math: toStalk_specStalkEquiv, stalkMap_toSpec
toSpec 📖	CompOp	13 math math: toStalk_specStalkEquiv, toSpec_preimage_basicOpen, toOpen_toSpec_val_c_app_assoc, isLocalization_atPrime, toStalk_stalkMap_toSpec_assoc, toStalk_stalkMap_toSpec, toSpec_base_apply_eq, toSpec_base_isIso, mk_mem_toSpec_base_apply, isIso_toSpec, stalkMap_toSpec, toSpec_base_apply_eq_comap, toOpen_toSpec_val_c_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
awayToSection_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 TopCat.PrelocalPredicate.pred HomogeneousLocalization.AtPrime TopCat.LocalPredicate.toPrelocalPredicate AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction DFunLike.coe RingHom CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology structureSheaf Semiring.toNonAssocSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom' awayToSection Localization CommRing.toCommMonoid OreLocalization.instCommSemiring OreLocalization.oreSetComm IsLocalization.map OreLocalization.instAlgebra Algebra.id Localization.isLocalization Ring.toSemiring ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal RingHom.id Submonoid Monoid.toMulOneClass Preorder.toLE Submonoid.instPartialOrder Submonoid.comap MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.instSetLike Submonoid.powers_le	—	AddSubgroupClass.toAddSubmonoidClass Localization.isLocalization ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.powers_le HomogeneousLocalization.mk_surjective HomogeneousLocalization.NumDenSameDeg.den_mem Localization.mk_eq_mk' IsLocalization.map_mk'
awayToSection_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 ProjectiveSpectrum.basicOpen	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 CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology structureSheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Sheaf.presheaf awayToSection TopCat.Presheaf.germ HomogeneousLocalization Ideal.primeCompl HomogeneousIdeal.toIdeal Nat.instAddMonoid ProjectiveSpectrum.asHomogeneousIdeal ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal CommRingCat.carrier CommRingCat.commRing CommRingCat.ofHom HomogeneousLocalization.mapId Submonoid Monoid.toMulOneClass Preorder.toLE Submonoid.instPartialOrder Submonoid.instSetLike Submonoid.powers_le CategoryTheory.Iso.inv HomogeneousLocalization.AtPrime RingEquiv.toCommRingCatIso AlgebraicGeometry.Proj.stalkIso'	—	AddSubgroupClass.toAddSubmonoidClass CommRingCat.hom_ext CommRingCat.Colimits.hasColimits_commRingCat ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Submonoid.powers_le RingHom.ext RingEquiv.eq_symm_apply AlgebraicGeometry.Proj.stalkIso'_germ
awayToΓ_ΓToStalk 📖	mathematical	—	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 AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Γ Opposite.op AlgebraicGeometry.LocallyRingedSpace.restrict TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf awayToΓ TopCat.Presheaf.Γgerm HomogeneousLocalization Ideal.primeCompl HomogeneousIdeal.toIdeal Nat.instAddMonoid ProjectiveSpectrum.asHomogeneousIdeal SetLike.instMembership TopologicalSpace.Opens.instSetLike ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal AlgebraicGeometry.LocallyRingedSpace.toTopCat CommRingCat.ofHom HomogeneousLocalization.mapId Submonoid Monoid.toMulOneClass Preorder.toLE Submonoid.instPartialOrder Submonoid.instSetLike Submonoid.powers_le CommRingCat.carrier ProjectiveSpectrum.top TopCat.Sheaf.presheaf structureSheaf CommRingCat.commRing CategoryTheory.Iso.inv HomogeneousLocalization.AtPrime RingEquiv.toCommRingCatIso AlgebraicGeometry.Proj.stalkIso' DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding CommRingCat.Colimits.hasColimits_commRingCat ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Submonoid.powers_le awayToΓ.eq_1 CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv TopCat.Presheaf.Γgerm.eq_1 Topology.IsOpenEmbedding.isOpenMap AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ TopCat.Presheaf.germ_res awayToSection_germ
isIso_toSpec 📖	mathematical	SetLike.instMembership	CategoryTheory.IsIso AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring toSpec	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_stalk_iso Homeomorph.isOpenEmbedding toSpec_base_isIso CommRingCat.Colimits.hasColimits_commRingCat ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal stalkMap_toSpec CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso
isLocalization_atPrime 📖	mathematical	SetLike.instMembership	IsLocalization HomogeneousLocalization.Away CommRing.toCommSemiring HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Ideal.primeCompl CommRingCat.carrier CommRingCat.of CommRingCat.commRing PrimeSpectrum.asIdeal DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec PrimeSpectrum.isPrime HomogeneousLocalization.AtPrime HomogeneousIdeal.toIdeal Ring.toSemiring Nat.instAddMonoid ProjectiveSpectrum.asHomogeneousIdeal ProjectiveSpectrum ProjectiveSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal RingHom.toAlgebra HomogeneousLocalization HomogeneousLocalization.mapId Submonoid Monoid.toMulOneClass Preorder.toLE Submonoid.instPartialOrder Submonoid.instSetLike Submonoid.powers_le	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding PrimeSpectrum.isPrime ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Submonoid.powers_le HomogeneousLocalization.mk_surjective IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid Iff.not mk_mem_toSpec_base_apply HomogeneousLocalization.val_injective HomogeneousLocalization.NumDenSameDeg.den_mem HomogeneousLocalization.val_mul Localization.isLocalization Localization.mk_eq_mk' IsLocalization.mk'_mul_mk'_eq_one' HomogeneousLocalization.val_one succ_nsmul' tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub mul_comm smul_eq_mul SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid SetLike.pow_mem_graded Submonoid.pow_mem Submonoid.mul_mem mul_mul_mul_comm pow_succ' mul_assoc IsLocalization.exists_of_eq Ideal.IsHomogeneous.mem_iff HomogeneousIdeal.isHomogeneous DirectSum.coe_decompose_mul_add_of_right_mem add_right_comm mul_left_comm pow_succ
mk_mem_toSpec_base_apply 📖	mathematical	—	HomogeneousLocalization Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Ideal CommRingCat.carrier CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid CommRingCat.commRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec HomogeneousIdeal Ring.toSemiring Nat.instAddMonoid HomogeneousIdeal.setLike ProjectiveSpectrum.asHomogeneousIdeal TopologicalSpace.Opens.instSetLike HomogeneousLocalization.NumDenSameDeg.deg HomogeneousLocalization.NumDenSameDeg.num	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier toSpec_base_apply_eq
stalkMap_toSpec 📖	mathematical	SetLike.instMembership	AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring toSpec CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top TopCat.Sheaf.presheaf AlgebraicGeometry.Spec.structureSheaf DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom HomogeneousLocalization.AtPrime HomogeneousIdeal.toIdeal Ring.toSemiring Nat.instAddMonoid ProjectiveSpectrum.asHomogeneousIdeal ProjectiveSpectrum ProjectiveSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Ideal.primeCompl AlgebraicGeometry.LocallyRingedSpace.toTopCat AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Iso.hom specStalkEquiv CommRingCat.carrier ProjectiveSpectrum.top structureSheaf CommRingCat.commRing CategoryTheory.Iso.inv RingEquiv.toCommRingCatIso AlgebraicGeometry.Proj.stalkIso' AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso	—	AddSubgroupClass.toAddSubmonoidClass CommRingCat.hom_ext CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.Opens.isOpenEmbedding ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal IsLocalization.ringHom_ext PrimeSpectrum.isPrime AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk RingHom.ext toStalk_stalkMap_toSpec Submonoid.powers_le awayToΓ_ΓToStalk toStalk_specStalkEquiv CategoryTheory.Category.assoc
toOpen_toSpec_val_c_app 📖	mathematical	—	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.Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.Spec.locallyRingedSpaceObj TopCat.Presheaf AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.ΓSpecIso Opposite.unop CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE le_top CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Γ AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace TopologicalSpace.Opens.map awayToΓ	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding le_top AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app
toOpen_toSpec_val_c_app_assoc 📖	mathematical	—	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.Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.ΓSpecIso AlgebraicGeometry.Spec.locallyRingedSpaceObj Opposite.unop CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE le_top TopCat.Presheaf AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Γ awayToΓ AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace TopologicalSpace.Opens.map	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding le_top CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toOpen_toSpec_val_c_app
toSpec_base_apply_eq 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Submonoid.powers_le HomogeneousLocalization.isLocalRing toSpec_base_apply_eq_comap PrimeSpectrum.ext Ideal.ext HomogeneousLocalization.mk_surjective HomogeneousLocalization.isUnit_iff_isUnit_val AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier HomogeneousLocalization.NumDenSameDeg.den_mem Localization.isLocalization Localization.mk_eq_mk' IsLocalization.AtPrime.isUnit_mk'_iff
toSpec_base_apply_eq_comap 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec PrimeSpectrum.comap HomogeneousLocalization Ideal.primeCompl HomogeneousIdeal.toIdeal Ring.toSemiring Nat.instAddMonoid ProjectiveSpectrum.asHomogeneousIdeal SetLike.instMembership TopologicalSpace.Opens.instSetLike ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal HomogeneousLocalization.mapId Submonoid Monoid.toMulOneClass Preorder.toLE Submonoid.instPartialOrder Submonoid.instSetLike Submonoid.powers_le IsLocalRing.closedPoint HomogeneousLocalization.AtPrime HomogeneousLocalization.isLocalRing	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Submonoid.powers_le HomogeneousLocalization.isLocalRing CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf awayToΓ_ΓToStalk CommRingCat.hom_comp PrimeSpectrum.comap_comp IsLocalRing.comap_closedPoint isLocalHom_of_isIso CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_inv
toSpec_base_isIso 📖	mathematical	SetLike.instMembership	CategoryTheory.IsIso TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding CategoryTheory.ConcreteCategory.hom_ext toSpec_base_apply_eq CategoryTheory.Iso.isIso_hom
toSpec_preimage_basicOpen 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Spec.locallyRingedSpaceObj CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec PrimeSpectrum.basicOpen CommRingCat.carrier CommRingCat.commRing DFunLike.coe FrameHom ProjectiveSpectrum ProjectiveSpectrum.zariskiTopology SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap continuous_subtype_val HomogeneousLocalization.NumDenSameDeg.deg HomogeneousLocalization.NumDenSameDeg.num	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.ext TopologicalSpace.Opens.isOpenEmbedding continuous_subtype_val toSpec_base_apply_eq AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen TopologicalSpace.Opens.map_coe
toStalk_specStalkEquiv 📖	mathematical	SetLike.instMembership	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of HomogeneousLocalization.Away CommRingCat.commRing HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Spec.locallyRingedSpaceObj CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec HomogeneousLocalization.AtPrime HomogeneousIdeal.toIdeal Ring.toSemiring Nat.instAddMonoid ProjectiveSpectrum.asHomogeneousIdeal ProjectiveSpectrum ProjectiveSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal Ideal.primeCompl AlgebraicGeometry.StructureSheaf.toStalk CategoryTheory.Iso.hom TopCat.Sheaf.presheaf AlgebraicGeometry.Spec.structureSheaf specStalkEquiv CommRingCat.ofHom HomogeneousLocalization HomogeneousLocalization.mapId Submonoid Monoid.toMulOneClass Preorder.toLE Submonoid.instPartialOrder Submonoid.instSetLike Submonoid.powers_le	—	AddSubgroupClass.toAddSubmonoidClass CommRingCat.hom_ext ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.Opens.isOpenEmbedding Submonoid.powers_le AlgHom.comp_algebraMap PrimeSpectrum.isPrime AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk isLocalization_atPrime
toStalk_stalkMap_toSpec 📖	mathematical	—	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.Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.ΓSpecIso AlgebraicGeometry.Spec.locallyRingedSpaceObj DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec TopCat.Presheaf.germ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Γ awayToΓ TopCat.Presheaf.Γgerm	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ le_top toOpen_toSpec_val_c_app_assoc
toStalk_stalkMap_toSpec_assoc 📖	mathematical	—	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.Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.ΓSpecIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.locallyRingedSpaceObj DFunLike.coe ContinuousMap AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.Proj.toLocallyRingedSpace TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat ProjectiveSpectrum.basicOpen AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toSpec TopCat.Presheaf.germ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Γ awayToΓ TopCat.Presheaf.Γgerm	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.isOpenEmbedding CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toStalk_stalkMap_toSpec

---

← Back to Index