Basic

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

Statistics

Metric	Count
Definitions affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayToSection, awayι, basicOpen, basicOpenIsoAway, basicOpenIsoSpec, basicOpenToSpec, fromOfGlobalSections, openCoverOfISupEqTop, openCoverOfMapIrrelevantEqTop, openCoverOfMapIrreleventEqTop, pullbackAwayιIso, stalkIso, toBasicOpenOfGlobalSections, toSpecZero	16
Theorems SpecMap_awayMap_awayι, SpecMap_awayMap_awayι_assoc, awayMap_awayToSection, awayMap_awayToSection_assoc, awayι_preimage_basicOpen, awayι_toSpecZero, awayι_toSpecZero_assoc, basicOpenIsoAway_hom, basicOpenIsoSpec_hom, basicOpenIsoSpec_inv_ι, basicOpenIsoSpec_inv_ι_assoc, basicOpenToSpec_SpecMap_awayMap, basicOpenToSpec_SpecMap_awayMap_assoc, basicOpenToSpec_app_top, basicOpen_eq_iSup_proj, basicOpen_mono, basicOpen_mul, basicOpen_one, basicOpen_pow, basicOpen_zero, fromOfGlobalSections_morphismRestrict, fromOfGlobalSections_preimage_basicOpen, fromOfGlobalSections_resLE, fromOfGlobalSections_toSpecZero, fromOfGlobalSections_toSpecZero_assoc, homOfLE_toBasicOpenOfGlobalSections_ι, homOfLE_toBasicOpenOfGlobalSections_ι_assoc, iSup_basicOpen_eq_top, iSup_basicOpen_eq_top', instIsOpenImmersionAwayι, isAffineOpen_basicOpen, isBasis_basicOpen, mem_basicOpen, opensRange_awayι, pullbackAwayιIso_hom_SpecMap_awayMap_left, pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, pullbackAwayιIso_hom_SpecMap_awayMap_right, pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, pullbackAwayιIso_hom_awayι, pullbackAwayιIso_hom_awayι_assoc, pullbackAwayιIso_inv_fst, pullbackAwayιIso_inv_fst_assoc, pullbackAwayιIso_inv_snd, pullbackAwayιIso_inv_snd_assoc	44
Total	60

AlgebraicGeometry.Proj

Definitions

Name	Category	Theorems
affineOpenCover 📖	CompOp	—
affineOpenCoverOfIrrelevantLESpan 📖	CompOp	—
awayToSection 📖	CompOp	4 math math: awayMap_awayToSection_assoc, basicOpenIsoAway_hom, basicOpenToSpec_app_top, awayMap_awayToSection
awayι 📖	CompOp	19 math math: basicOpenIsoSpec_inv_ι_assoc, pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, pullbackAwayιIso_inv_snd_assoc, SpecMap_awayMap_awayι_assoc, pullbackAwayιIso_inv_fst, basicOpenIsoSpec_inv_ι, pullbackAwayιIso_inv_snd, pullbackAwayιIso_inv_fst_assoc, pullbackAwayιIso_hom_awayι, pullbackAwayιIso_hom_SpecMap_awayMap_right, pullbackAwayιIso_hom_SpecMap_awayMap_left, awayι_toSpecZero, awayι_toSpecZero_assoc, pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, opensRange_awayι, pullbackAwayιIso_hom_awayι_assoc, awayι_preimage_basicOpen, SpecMap_awayMap_awayι, instIsOpenImmersionAwayι
basicOpen 📖	CompOp	27 math math: awayMap_awayToSection_assoc, fromOfGlobalSections_resLE, basicOpenIsoSpec_inv_ι_assoc, basicOpenIsoAway_hom, basicOpenToSpec_app_top, isAffineOpen_basicOpen, mem_basicOpen, iSup_basicOpen_eq_top', basicOpenToSpec_SpecMap_awayMap, basicOpenIsoSpec_inv_ι, basicOpen_mul, basicOpen_mono, homOfLE_toBasicOpenOfGlobalSections_ι_assoc, basicOpen_one, opensRange_awayι, basicOpen_pow, basicOpen_eq_iSup_proj, isBasis_basicOpen, fromOfGlobalSections_morphismRestrict, basicOpenToSpec_SpecMap_awayMap_assoc, awayι_preimage_basicOpen, awayMap_awayToSection, basicOpen_zero, basicOpenIsoSpec_hom, homOfLE_toBasicOpenOfGlobalSections_ι, iSup_basicOpen_eq_top, fromOfGlobalSections_preimage_basicOpen
basicOpenIsoAway 📖	CompOp	1 math math: basicOpenIsoAway_hom
basicOpenIsoSpec 📖	CompOp	3 math math: basicOpenIsoSpec_inv_ι_assoc, basicOpenIsoSpec_inv_ι, basicOpenIsoSpec_hom
basicOpenToSpec 📖	CompOp	4 math math: basicOpenToSpec_app_top, basicOpenToSpec_SpecMap_awayMap, basicOpenToSpec_SpecMap_awayMap_assoc, basicOpenIsoSpec_hom
fromOfGlobalSections 📖	CompOp	5 math math: fromOfGlobalSections_resLE, fromOfGlobalSections_toSpecZero_assoc, fromOfGlobalSections_toSpecZero, fromOfGlobalSections_morphismRestrict, fromOfGlobalSections_preimage_basicOpen
openCoverOfISupEqTop 📖	CompOp	—
openCoverOfMapIrrelevantEqTop 📖	CompOp	—
openCoverOfMapIrreleventEqTop 📖	CompOp	—
pullbackAwayιIso 📖	CompOp	10 math math: pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, pullbackAwayιIso_inv_snd_assoc, pullbackAwayιIso_inv_fst, pullbackAwayιIso_inv_snd, pullbackAwayιIso_inv_fst_assoc, pullbackAwayιIso_hom_awayι, pullbackAwayιIso_hom_SpecMap_awayMap_right, pullbackAwayιIso_hom_SpecMap_awayMap_left, pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, pullbackAwayιIso_hom_awayι_assoc
stalkIso 📖	CompOp	—
toBasicOpenOfGlobalSections 📖	CompOp	4 math math: fromOfGlobalSections_resLE, homOfLE_toBasicOpenOfGlobalSections_ι_assoc, fromOfGlobalSections_morphismRestrict, homOfLE_toBasicOpenOfGlobalSections_ι
toSpecZero 📖	CompOp	10 math math: fromOfGlobalSections_toSpecZero_assoc, valuativeCriterion_existence, instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, isSeparated, awayι_toSpecZero, awayι_toSpecZero_assoc, fromOfGlobalSections_toSpecZero, instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat, instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_awayMap_awayι 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap awayι SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul Nat.instAddMonoid GradedRing.toGradedMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing LT.lt.trans_le Nat.instPreorder	—	AddSubgroupClass.toAddSubmonoidClass SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid LT.lt.trans_le awayι.eq_1 CategoryTheory.Iso.eq_inv_comp basicOpenIsoSpec_hom basicOpen_mono basicOpenToSpec_SpecMap_awayMap_assoc CategoryTheory.Iso.hom_inv_id_assoc AlgebraicGeometry.Scheme.homOfLE_ι
SpecMap_awayMap_awayι_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap AlgebraicGeometry.Proj awayι SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul Nat.instAddMonoid GradedRing.toGradedMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing LT.lt.trans_le Nat.instPreorder	—	AddSubgroupClass.toAddSubmonoidClass SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid LT.lt.trans_le CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' SpecMap_awayMap_awayι
awayMap_awayToSection 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	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 CommRingCat.ofHom HomogeneousLocalization.awayMap awayToSection CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.homOfLE basicOpen_mono Semigroup.toMul SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass CommRingCat.hom_ext basicOpen_mono RingHom.ext HomogeneousLocalization.val_injective HomogeneousLocalization.mk_surjective Localization.isLocalization ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.powers_le AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply CommRingCat.hom_ofHom Submonoid.mem_powers_iff Localization.mk_eq_mk' IsLocalization.map_mk' HomogeneousLocalization.NumDenSameDeg.den_mem Localization.mk_eq_mk_iff Localization.r_iff_exists one_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
awayMap_awayToSection_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	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 CommRingCat.ofHom HomogeneousLocalization.awayMap 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 CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.homOfLE basicOpen_mono Semigroup.toMul SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass basicOpen_mono CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' awayMap_awayToSection
awayι_preimage_basicOpen 📖	mathematical	SetLike.instMembership	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 AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' awayι basicOpen PrimeSpectrum.basicOpen HomogeneousLocalization.Away.isLocalizationElem	—	AddSubgroupClass.toAddSubmonoidClass TopologicalSpace.Opens.ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι pullbackAwayιIso_inv_fst Set.range_comp Set.range_eq_univ Homeomorph.surjective CategoryTheory.Iso.isIso_inv opensRange_awayι Set.image_univ AlgebraicGeometry.IsOpenImmersion.range_pullbackFst PrimeSpectrum.localization_away_comap_range HomogeneousLocalization.Away.isLocalization_mul LT.lt.ne'
awayι_toSpecZero 📖	mathematical	SetLike.instMembership	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj SetLike.GradeZero.instCommRing GradedRing.toGradedMonoid AddCommMonoid.toAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing awayι toSpecZero AlgebraicGeometry.Spec.map AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass HomogeneousLocalization CommRingCat.ofHom HomogeneousLocalization.fromZeroRingHom	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid basicOpen_one toSpecZero.eq_1 basicOpenToSpec.eq_1 awayι.eq_1 CategoryTheory.Category.assoc LE.le.trans_eq le_top AlgebraicGeometry.Scheme.isoOfEq_hom_ι AlgebraicGeometry.Scheme.homOfLE_ι Mathlib.Tactic.Reassoc.eq_whisker' AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc AlgebraicGeometry.Spec.map_comp
awayι_toSpecZero_assoc 📖	mathematical	SetLike.instMembership	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι SetLike.GradeZero.instCommRing GradedRing.toGradedMonoid AddCommMonoid.toAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing toSpecZero AlgebraicGeometry.Spec.map AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass HomogeneousLocalization CommRingCat.ofHom HomogeneousLocalization.fromZeroRingHom	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' awayι_toSpecZero
basicOpenIsoAway_hom 📖	mathematical	SetLike.instMembership	CategoryTheory.Iso.hom CommRingCat 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 basicOpenIsoAway awayToSection	—	AddSubgroupClass.toAddSubmonoidClass
basicOpenIsoSpec_hom 📖	mathematical	SetLike.instMembership	CategoryTheory.Iso.hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Proj basicOpen AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring basicOpenIsoSpec basicOpenToSpec	—	AddSubgroupClass.toAddSubmonoidClass
basicOpenIsoSpec_inv_ι 📖	mathematical	SetLike.instMembership	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Proj basicOpen CategoryTheory.Iso.inv basicOpenIsoSpec AlgebraicGeometry.Scheme.Opens.ι awayι	—	AddSubgroupClass.toAddSubmonoidClass
basicOpenIsoSpec_inv_ι_assoc 📖	mathematical	SetLike.instMembership	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Proj basicOpen CategoryTheory.Iso.inv basicOpenIsoSpec AlgebraicGeometry.Scheme.Opens.ι awayι	—	AddSubgroupClass.toAddSubmonoidClass CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' basicOpenIsoSpec_inv_ι
basicOpenToSpec_SpecMap_awayMap 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Proj basicOpen AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring basicOpenToSpec AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap AlgebraicGeometry.Scheme.homOfLE basicOpen_mono Semigroup.toMul SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass basicOpen_mono basicOpenToSpec.eq_1 CategoryTheory.Category.assoc AlgebraicGeometry.Spec.map_comp awayMap_awayToSection AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc
basicOpenToSpec_SpecMap_awayMap_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Proj basicOpen AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring basicOpenToSpec AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap AlgebraicGeometry.Scheme.homOfLE basicOpen_mono Semigroup.toMul SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass basicOpen_mono CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' basicOpenToSpec_SpecMap_awayMap
basicOpenToSpec_app_top 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.app AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Proj basicOpen AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring basicOpenToSpec Top.top AlgebraicGeometry.Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.ΓSpecIso awayToSection CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.Opens.topIso	—	AddSubgroupClass.toAddSubmonoidClass basicOpenToSpec.eq_1 AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι CategoryTheory.eqToHom_op AlgebraicGeometry.Scheme.Hom.comp_app AlgebraicGeometry.Scheme.toSpecΓ_appTop AlgebraicGeometry.Scheme.ΓSpecIso_naturality AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc
basicOpen_eq_iSup_proj 📖	mathematical	—	basicOpen iSup AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Proj ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing AddMonoidHom.instFunLike GradedRing.proj Nat.instAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	AddSubgroupClass.toAddSubmonoidClass ProjectiveSpectrum.basicOpen_eq_union_of_projection
basicOpen_mono 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Proj Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier basicOpen	—	AddSubgroupClass.toAddSubmonoidClass Eq.trans_le basicOpen_mul inf_le_left
basicOpen_mul 📖	mathematical	—	basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Proj SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	AddSubgroupClass.toAddSubmonoidClass ProjectiveSpectrum.basicOpen_mul
basicOpen_one 📖	mathematical	—	basicOpen AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Top.top AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Proj OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	AddSubgroupClass.toAddSubmonoidClass ProjectiveSpectrum.basicOpen_one
basicOpen_pow 📖	mathematical	—	basicOpen Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass ProjectiveSpectrum.basicOpen_pow
basicOpen_zero 📖	mathematical	—	basicOpen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Bot.bot AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Proj OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier HeytingAlgebra.toOrderBot	—	AddSubgroupClass.toAddSubmonoidClass ProjectiveSpectrum.basicOpen_zero
fromOfGlobalSections_morphismRestrict 📖	mathematical	Ideal.map CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ring.toSemiring CommRing.toRing RingHom.instFunLike HomogeneousIdeal.toIdeal AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommMonoid.toAddMonoid Nat.instAddCommMonoid HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule SetLike.instMembership	AlgebraicGeometry.morphismRestrict AlgebraicGeometry.Proj fromOfGlobalSections basicOpen CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.Scheme.basicOpen DFunLike.coe CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.isoOfEq fromOfGlobalSections_preimage_basicOpen toBasicOpenOfGlobalSections	—	AddSubgroupClass.toAddSubmonoidClass Nat.instCanonicallyOrderedAdd fromOfGlobalSections_preimage_basicOpen CategoryTheory.Iso.inv_comp_eq CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι Eq.ge CategoryTheory.Category.assoc AlgebraicGeometry.morphismRestrict_ι AlgebraicGeometry.Scheme.homOfLE_ι_assoc AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
fromOfGlobalSections_preimage_basicOpen 📖	mathematical	Ideal.map CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ring.toSemiring CommRing.toRing RingHom.instFunLike HomogeneousIdeal.toIdeal AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommMonoid.toAddMonoid Nat.instAddCommMonoid HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule SetLike.instMembership	AlgebraicGeometry.Proj TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromOfGlobalSections basicOpen AlgebraicGeometry.Scheme.basicOpen DFunLike.coe	—	AddSubgroupClass.toAddSubmonoidClass Nat.instCanonicallyOrderedAdd le_antisymm AlgebraicGeometry.Scheme.Cover.exists_eq AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage SetLike.mem_coe AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen TopologicalSpace.Opens.map_coe Set.mem_preimage Set.mem_of_subset_of_mem Set.image_subset_iff map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Localization.isLocalization Localization.mk_eq_mk' IsLocalization.map_mk' IsLocalization.mk'.congr_simp Ideal.pow_mem_of_mem Ideal.le_radical Ideal.mem_span_singleton_self AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway Eq.ge AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac AlgebraicGeometry.basicOpenIsoSpecAway.eq_1 AlgebraicGeometry.Scheme.Hom.comp_apply Function.Injective.mem_set_image Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding awayι_preimage_basicOpen AlgebraicGeometry.Scheme.homOfLE_base AlgebraicGeometry.morphismRestrict_base CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.Opens.opensRange_ι
fromOfGlobalSections_resLE 📖	mathematical	Ideal.map CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ring.toSemiring CommRing.toRing RingHom.instFunLike HomogeneousIdeal.toIdeal AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommMonoid.toAddMonoid Nat.instAddCommMonoid HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule SetLike.instMembership	AlgebraicGeometry.Scheme.Hom.resLE AlgebraicGeometry.Proj fromOfGlobalSections basicOpen AlgebraicGeometry.Scheme.basicOpen DFunLike.coe Eq.ge TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromOfGlobalSections_preimage_basicOpen toBasicOpenOfGlobalSections	—	AddSubgroupClass.toAddSubmonoidClass Nat.instCanonicallyOrderedAdd Eq.ge fromOfGlobalSections_preimage_basicOpen CategoryTheory.Iso.inv_comp_eq fromOfGlobalSections_morphismRestrict le_rfl AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict LE.le.trans AlgebraicGeometry.Scheme.Hom.map_resLE
fromOfGlobalSections_toSpecZero 📖	mathematical	Ideal.map CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ring.toSemiring CommRing.toRing RingHom.instFunLike HomogeneousIdeal.toIdeal AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommMonoid.toAddMonoid Nat.instAddCommMonoid HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Proj AlgebraicGeometry.Spec CommRingCat.of SetLike.instMembership SetLike.GradeZero.instCommRing GradedRing.toGradedMonoid fromOfGlobalSections toSpecZero AlgebraicGeometry.Scheme.toSpecΓ AlgebraicGeometry.Spec.map CommRingCat.ofHom RingHom.comp algebraMap SetLike.GradeZero.instAlgebraSubtypeMemOfNat Nat.instAddMonoid	—	AddSubgroupClass.toAddSubmonoidClass Nat.instCanonicallyOrderedAdd AlgebraicGeometry.Scheme.Cover.hom_ext GradedRing.toGradedMonoid AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Cover.glueMorphisms.congr_simp AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc basicOpenIsoSpec_inv_ι_assoc awayι_toSpecZero AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc RingHom.comp_assoc IsScalarTower.algebraMap_eq HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.map_comp
fromOfGlobalSections_toSpecZero_assoc 📖	mathematical	Ideal.map CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ring.toSemiring CommRing.toRing RingHom.instFunLike HomogeneousIdeal.toIdeal AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommMonoid.toAddMonoid Nat.instAddCommMonoid HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Proj fromOfGlobalSections AlgebraicGeometry.Spec CommRingCat.of SetLike.instMembership SetLike.GradeZero.instCommRing GradedRing.toGradedMonoid toSpecZero AlgebraicGeometry.Scheme.toSpecΓ AlgebraicGeometry.Spec.map CommRingCat.ofHom RingHom.comp algebraMap SetLike.GradeZero.instAlgebraSubtypeMemOfNat Nat.instAddMonoid	—	AddSubgroupClass.toAddSubmonoidClass Nat.instCanonicallyOrderedAdd GradedRing.toGradedMonoid CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromOfGlobalSections_toSpecZero
homOfLE_toBasicOpenOfGlobalSections_ι 📖	mathematical	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.basicOpen AlgebraicGeometry.Proj AlgebraicGeometry.Scheme.homOfLE basicOpen toBasicOpenOfGlobalSections AlgebraicGeometry.Scheme.Opens.ι	—	AddSubgroupClass.toAddSubmonoidClass LE.le.trans Eq.ge AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen le_rfl AlgebraicGeometry.Spec.map_comp AlgebraicGeometry.Scheme.Hom.map_resLE_assoc CategoryTheory.Category.assoc map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass PrimeSpectrum.basicOpen_mul AlgebraicGeometry.Scheme.Hom.resLE_map_assoc SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid LT.lt.trans_le SpecMap_awayMap_awayι Localization.isLocalization AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc CategoryTheory.Iso.inv_hom_id_assoc RingHom.ext isUnit_of_dvd_unit map_dvd IsLocalization.Away.algebraMap_isUnit HomogeneousLocalization.val_awayMap IsLocalization.ringHom_ext IsLocalization.map_eq IsLocalization.Away.awayToAwayRight_eq IsLocalization.Away.lift_eq
homOfLE_toBasicOpenOfGlobalSections_ι_assoc 📖	mathematical	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.basicOpen AlgebraicGeometry.Scheme.homOfLE AlgebraicGeometry.Proj basicOpen toBasicOpenOfGlobalSections AlgebraicGeometry.Scheme.Opens.ι	—	AddSubgroupClass.toAddSubmonoidClass CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_toBasicOpenOfGlobalSections_ι
iSup_basicOpen_eq_top 📖	mathematical	Ideal Ring.toSemiring CommRing.toRing Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule HomogeneousIdeal.toIdeal AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommMonoid.toAddMonoid Nat.instAddCommMonoid HomogeneousIdeal.irrelevant Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set.range	iSup AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Proj ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier basicOpen Top.top OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	AddSubgroupClass.toAddSubmonoidClass Nat.instCanonicallyOrderedAdd top_le_iff TopologicalSpace.Opens.mem_iSup ProjectiveSpectrum.not_irrelevant_le LE.le.trans Ideal.span_le Set.range_subset_iff
iSup_basicOpen_eq_top' 📖	mathematical	SetLike.instMembership Algebra.adjoin SetLike.GradeZero.instCommSemiring CommRing.toCommSemiring Nat.instAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid CommSemiring.toSemiring SetLike.GradeZero.instAlgebraSubtypeMemOfNat Set.range Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	iSup AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Proj ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier basicOpen	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid iSup_basicOpen_eq_top Nat.instCanonicallyOrderedAdd GradedRing.projZeroRingHom_apply GradedRing.proj_apply HomogeneousIdeal.mem_irrelevant_iff sub_zero Algebra.adjoin_induction DirectSum.decompose_of_mem_same sub_self ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass DirectSum.decompose_of_mem_ne Ideal.subset_span sub_eq_zero map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass add_sub_add_comm AddMemClass.add_mem AddSubmonoidClass.toAddMemClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Ideal.mul_mem_left Ideal.mul_mem_right Ideal.instIsTwoSided_1
instIsOpenImmersionAwayι 📖	mathematical	SetLike.instMembership	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.comp AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
isAffineOpen_basicOpen 📖	mathematical	SetLike.instMembership	AlgebraicGeometry.IsAffineOpen AlgebraicGeometry.Proj basicOpen	—	AddSubgroupClass.toAddSubmonoidClass instIsOpenImmersionAwayι opensRange_awayι AlgebraicGeometry.isAffineOpen_opensRange AlgebraicGeometry.isAffine_Spec
isBasis_basicOpen 📖	mathematical	—	TopologicalSpace.Opens.IsBasis TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Proj AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.range TopologicalSpace.Opens basicOpen	—	AddSubgroupClass.toAddSubmonoidClass Set.range_comp ProjectiveSpectrum.isTopologicalBasis_basic_opens
mem_basicOpen 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Proj AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier basicOpen HomogeneousIdeal Ring.toSemiring CommRing.toRing Nat.instAddMonoid HomogeneousIdeal.setLike ProjectiveSpectrum.asHomogeneousIdeal	—	AddSubgroupClass.toAddSubmonoidClass
opensRange_awayι 📖	mathematical	SetLike.instMembership	AlgebraicGeometry.Scheme.Hom.opensRange AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι instIsOpenImmersionAwayι basicOpen	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.comp AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso AlgebraicGeometry.Scheme.Hom.isIso_toLRSHom CategoryTheory.Iso.isIso_inv AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι AlgebraicGeometry.Scheme.Hom.opensRange_comp_of_isIso AlgebraicGeometry.Scheme.Opens.opensRange_ι
pullbackAwayιIso_hom_SpecMap_awayMap_left 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.hom pullbackAwayιIso AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap CategoryTheory.Limits.pullback.fst	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid LT.lt.trans_le pullbackAwayιIso_hom_awayι CategoryTheory.Category.assoc SpecMap_awayMap_awayι
pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.hom pullbackAwayιIso AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap CategoryTheory.Limits.pullback.fst	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackAwayιIso_hom_SpecMap_awayMap_left
pullbackAwayιIso_hom_SpecMap_awayMap_right 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.hom pullbackAwayιIso AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap mul_comm NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring CategoryTheory.Limits.pullback.snd	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι mul_comm CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono CategoryTheory.Limits.pullback.condition SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid LT.lt.trans_le pullbackAwayιIso_hom_awayι CategoryTheory.Category.assoc SpecMap_awayMap_awayι
pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.hom pullbackAwayιIso AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap mul_comm NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring CategoryTheory.Limits.pullback.snd	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι mul_comm CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackAwayιIso_hom_SpecMap_awayMap_right
pullbackAwayιIso_hom_awayι 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.hom pullbackAwayιIso SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul Nat.instAddMonoid GradedRing.toGradedMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing LT.lt.trans_le Nat.instPreorder CategoryTheory.Limits.pullback.fst	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι
pullbackAwayιIso_hom_awayι_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.hom pullbackAwayιIso SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul Nat.instAddMonoid GradedRing.toGradedMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing LT.lt.trans_le Nat.instPreorder CategoryTheory.Limits.pullback.fst	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid LT.lt.trans_le CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackAwayιIso_hom_awayι
pullbackAwayιIso_inv_fst 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Limits.pullback AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.inv pullbackAwayιIso CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι pullbackAwayιIso_hom_SpecMap_awayMap_left CategoryTheory.Iso.inv_hom_id_assoc
pullbackAwayιIso_inv_fst_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Limits.pullback AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.inv pullbackAwayιIso CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackAwayιIso_inv_fst
pullbackAwayιIso_inv_snd 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Limits.pullback AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.inv pullbackAwayιIso CategoryTheory.Limits.pullback.snd AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap mul_comm NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι mul_comm pullbackAwayιIso_hom_SpecMap_awayMap_right CategoryTheory.Iso.inv_hom_id_assoc
pullbackAwayιIso_inv_snd_assoc 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Limits.pullback AlgebraicGeometry.Proj awayι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι CategoryTheory.Iso.inv pullbackAwayιIso CategoryTheory.Limits.pullback.snd AlgebraicGeometry.Spec.map CommRingCat.ofHom HomogeneousLocalization.awayMap mul_comm NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionAwayι mul_comm CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackAwayιIso_inv_snd

---

← Back to Index