CommRingCat

📁 Source: Mathlib/Topology/Sheaves/CommRingCat.lean

Statistics

Metric	Count
Definitions CommRingCat, SubmonoidPresheaf, localizationPresheaf, obj, toLocalizationPresheaf, algebra_section_stalk, instAlgebraCarrierObjOppositeOpensCarrierCommRingCatLocalizationPresheaf, instEpiCommRingCatToTotalQuotientPresheaf, instInhabitedSubmonoidPresheaf, submonoidPresheafOfStalk, toTotalQuotientPresheaf, totalQuotientPresheaf, objSupIsoProdEqLocus, commRingYoneda, continuousFunctions, map, pullback, instAddHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instCommRingHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instIntCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instMulHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instNatCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instNegHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instOneHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instPowHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrierNat, instSMulIntHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instSMulNatHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instSubHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, instZeroHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier, presheafToTopCommRing	30
Theorems map, toLocalizationPresheaf_app, epi_toLocalizationPresheaf, instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, instMonoCommRingCatToTotalQuotientPresheafPresheaf, restrictOpenCommRingCat_apply, stalk_open_algebraMap, submonoidPresheafOfStalk_obj, objSupIsoProdEqLocus_hom_fst, objSupIsoProdEqLocus_hom_snd, objSupIsoProdEqLocus_inv_eq_iff, objSupIsoProdEqLocus_inv_fst, objSupIsoProdEqLocus_inv_snd	13
Total	43

TopCat

Definitions

Name	Category	Theorems
commRingYoneda 📖	CompOp	—
continuousFunctions 📖	CompOp	—
instAddHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instCommRingHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instIntCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instMulHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instNatCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instNegHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instOneHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instPowHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrierNat 📖	CompOp	—
instSMulIntHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instSMulNatHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instSubHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
instZeroHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier 📖	CompOp	—
presheafToTopCommRing 📖	CompOp	—

TopCat.Presheaf

Definitions

Name	Category	Theorems
SubmonoidPresheaf 📖	CompData	—
algebra_section_stalk 📖	CompOp	4 math math: AlgebraicGeometry.functionField_isScalarTower, stalk_open_algebraMap, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk'
instAlgebraCarrierObjOppositeOpensCarrierCommRingCatLocalizationPresheaf 📖	CompOp	1 math math: instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf
instEpiCommRingCatToTotalQuotientPresheaf 📖	CompOp	—
instInhabitedSubmonoidPresheaf 📖	CompOp	—
submonoidPresheafOfStalk 📖	CompOp	1 math math: submonoidPresheafOfStalk_obj
toTotalQuotientPresheaf 📖	CompOp	1 math math: instMonoCommRingCatToTotalQuotientPresheafPresheaf
totalQuotientPresheaf 📖	CompOp	1 math math: instMonoCommRingCatToTotalQuotientPresheafPresheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_toLocalizationPresheaf 📖	mathematical	—	CategoryTheory.Epi TopCat.Presheaf CommRingCat CommRingCat.instCategory TopCat.instCategoryPresheaf SubmonoidPresheaf.localizationPresheaf SubmonoidPresheaf.toLocalizationPresheaf	—	CategoryTheory.NatTrans.epi_of_epi_app Localization.epi'
instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf 📖	mathematical	—	IsLocalization CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CommRing.toCommSemiring CommRingCat.commRing SubmonoidPresheaf.obj SubmonoidPresheaf.localizationPresheaf instAlgebraCarrierObjOppositeOpensCarrierCommRingCatLocalizationPresheaf	—	Localization.isLocalization
instMonoCommRingCatToTotalQuotientPresheafPresheaf 📖	mathematical	—	CategoryTheory.Mono TopCat.Presheaf CommRingCat CommRingCat.instCategory TopCat.instCategoryPresheaf TopCat.Sheaf.presheaf totalQuotientPresheaf toTotalQuotientPresheaf	—	CategoryTheory.NatTrans.mono_of_mono_app CategoryTheory.ConcreteCategory.mono_of_injective CommRingCat.Colimits.hasColimits_commRingCat IsLocalization.injective Localization.isLocalization nonZeroDivisorsRight_eq_nonZeroDivisors section_ext CommRingCat.FilteredColimits.forget_preservesFilteredColimits CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.mem_iInf map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
restrictOpenCommRingCat_apply 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	restrictOpen CommRingCat CommRingCat.instCategory RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE	—	—
stalk_open_algebraMap 📖	mathematical	—	algebraMap CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory Opposite.op stalk CommRingCat.Colimits.hasColimits_commRingCat SetLike.instMembership TopologicalSpace.Opens.instSetLike CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring algebra_section_stalk CommRingCat.Hom.hom germ	—	CommRingCat.Colimits.hasColimits_commRingCat
submonoidPresheafOfStalk_obj 📖	mathematical	—	SubmonoidPresheaf.obj submonoidPresheafOfStalk iInf Submonoid CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing SetLike.instMembership TopologicalSpace.Opens.instSetLike Opposite.unop Submonoid.instInfSet Submonoid.comap stalk CommRingCat.Colimits.hasColimits_commRingCat RingHom Opposite.op RingHom.instFunLike CommRingCat.Hom.hom germ	—	CommRingCat.Colimits.hasColimits_commRingCat

TopCat.Presheaf.SubmonoidPresheaf

Definitions

Name	Category	Theorems
localizationPresheaf 📖	CompOp	3 math math: TopCat.Presheaf.epi_toLocalizationPresheaf, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, toLocalizationPresheaf_app
obj 📖	CompOp	4 math math: map, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, toLocalizationPresheaf_app, TopCat.Presheaf.submonoidPresheafOfStalk_obj
toLocalizationPresheaf 📖	CompOp	2 math math: TopCat.Presheaf.epi_toLocalizationPresheaf, toLocalizationPresheaf_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	—	Submonoid CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Preorder.toLE Submonoid.instPartialOrder obj Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass CommRingCat.Hom.hom CategoryTheory.Functor.map	—	—
toLocalizationPresheaf_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory localizationPresheaf toLocalizationPresheaf CommRingCat.ofHom CommRingCat.carrier Localization CategoryTheory.Functor.obj CommRing.toCommMonoid CommRingCat.commRing obj OreLocalization.instCommRing OreLocalization.oreSetComm algebraMap CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.instAlgebra Algebra.id	—	—

TopCat.Sheaf

Definitions

Name	Category	Theorems
objSupIsoProdEqLocus 📖	CompOp	5 math math: objSupIsoProdEqLocus_hom_fst, objSupIsoProdEqLocus_inv_snd, objSupIsoProdEqLocus_hom_snd, objSupIsoProdEqLocus_inv_eq_iff, objSupIsoProdEqLocus_inv_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
objSupIsoProdEqLocus_hom_fst 📖	mathematical	—	CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op Subring Prod.instRing CommRing.toRing CommRingCat.commRing SetLike.instMembership Subring.instSetLike RingHom.eqLocus SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CommSemiring.toSemiring CommRing.toCommSemiring RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE inf_le_left RingHom.fst inf_le_right RingHom.snd DFunLike.coe SemilatticeSup.toMax Lattice.toSemilatticeSup CommRingCat.of Subring.toCommRing Prod.instCommRing CategoryTheory.ConcreteCategory.hom RingHom RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Iso.hom objSupIsoProdEqLocus SemilatticeSup.toPartialOrder le_sup_left	—	CategoryTheory.ConcreteCategory.congr_hom inf_le_left inf_le_right CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
objSupIsoProdEqLocus_hom_snd 📖	mathematical	—	CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op Subring Prod.instRing CommRing.toRing CommRingCat.commRing SetLike.instMembership Subring.instSetLike RingHom.eqLocus SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CommSemiring.toSemiring CommRing.toCommSemiring RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE inf_le_left RingHom.fst inf_le_right RingHom.snd DFunLike.coe SemilatticeSup.toMax Lattice.toSemilatticeSup CommRingCat.of Subring.toCommRing Prod.instCommRing CategoryTheory.ConcreteCategory.hom RingHom RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Iso.hom objSupIsoProdEqLocus SemilatticeSup.toPartialOrder le_sup_right	—	CategoryTheory.ConcreteCategory.congr_hom inf_le_left inf_le_right CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
objSupIsoProdEqLocus_inv_eq_iff 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice SemilatticeInf.toMin Lattice.toSemilatticeInf	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE CommRingCat.of Subring Prod.instRing CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.eqLocus RingHom.comp Ring.toSemiring CommRingCat.Hom.hom inf_le_left RingHom.fst inf_le_right RingHom.snd Subring.toCommRing Prod.instCommRing CategoryTheory.Iso.inv objSupIsoProdEqLocus	—	inf_le_left inf_le_right le_sup_left objSupIsoProdEqLocus_inv_fst le_sup_right objSupIsoProdEqLocus_inv_snd LE.le.trans eq_of_locally_eq₂ CommRingCat.hasLimits CommRingCat.forgetReflectIsos CommRingCat.forget_preservesLimits inf_sup_right le_inf le_rfl
objSupIsoProdEqLocus_inv_fst 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SemilatticeSup.toPartialOrder CategoryTheory.homOfLE le_sup_left CommRingCat.of Subring Prod.instRing CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.eqLocus SemilatticeInf.toMin Lattice.toSemilatticeInf RingHom.comp Ring.toSemiring CommRingCat.Hom.hom inf_le_left RingHom.fst inf_le_right RingHom.snd Subring.toCommRing Prod.instCommRing CategoryTheory.Iso.inv objSupIsoProdEqLocus	—	inf_le_left inf_le_right CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
objSupIsoProdEqLocus_inv_snd 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SemilatticeSup.toPartialOrder CategoryTheory.homOfLE le_sup_right CommRingCat.of Subring Prod.instRing CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.eqLocus SemilatticeInf.toMin Lattice.toSemilatticeInf RingHom.comp Ring.toSemiring CommRingCat.Hom.hom inf_le_left RingHom.fst inf_le_right RingHom.snd Subring.toCommRing Prod.instCommRing CategoryTheory.Iso.inv objSupIsoProdEqLocus	—	inf_le_left inf_le_right CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp

TopCat.continuousFunctions

Definitions

Name	Category	Theorems
map 📖	CompOp	—
pullback 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
CommRingCat 📖	CompData	1633 math math: CommRingCat.tensorProd_map_right, AlgebraicGeometry.Scheme.toSpecΓ_apply, PresheafOfModules.Monoidal.tensorObj_obj, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, smoothSheafCommRing.ι_forgetStalk_inv, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.irreducibleSpace_of_isIntegral, AlgebraicGeometry.Scheme.height_of_isClosed, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, CommRingCat.forget₂Ring_preservesLimitsOfSize, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, AlgebraicGeometry.Scheme.isoOfEq_inv, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, AlgebraicGeometry.Spec.toPresheafedSpace_obj, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Spec.map_eq_id, AlgebraicGeometry.Scheme.zeroLocus_iInf, AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_comp, AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor, AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace, RingHom.isStableUnderCobaseChange_toMorphismProperty_iff, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, CommRingCat.instFullRingCatForget₂RingHomCarrierCarrier, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace, AlgebraicGeometry.LocallyRingedSpace.Γ_def, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, CommRingCat.forget_preservesLimitsOfSize, AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.isAffineOpen_top, CommRingCat.forgetReflectIsos, AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans_hom, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints, AlgebraicGeometry.Scheme.support_nilradical, AlgebraicGeometry.opensCone_pt, Localization.epi', AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ, AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.StructureSheaf.comap_id, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, CommRingCat.pushoutCocone_pt, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral, AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec, AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.ΓSpec.isIso_adjunction_counit, AlgebraicGeometry.Spec_Γ_naturality, smoothSheafCommRing.nonunits_stalk, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, AlgebraicGeometry.AffineScheme.Spec_faithful, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.range_eq_range_of_surjective, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.preservesColimit_Γ, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, AlgebraicGeometry.StructureSheaf.comap_comp, AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, CommRingCat.commRingCat_hasStrictTerminalObjects, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, AlgebraicGeometry.Scheme.Hom.range_fiberι, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.Cover.iUnion_range, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.mem_basicOpen', AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.Spec.map_surjective, AlgebraicGeometry.Scheme.Hom.mem_opensRange, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.Scheme.SpecToEquivOfField_eq_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.pow_apply, AlgebraicGeometry.isCompact_iff_exists, CommRingCat.id_apply, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Spec_presheaf, AlgebraicGeometry.Scheme.RationalMap.dense_domain, AlgebraicGeometry.HasRingHomProperty.stalkMap, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.homMk_toHom, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.LocallyRingedSpace.id_toShHom', AlgebraicGeometry.Scheme.Hom.id_appTop, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, smoothSheafCommRing.ι_evalHom_apply, CommRingCat.HomTopology.instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.Scheme.IdealSheafData.gc, AlgebraicGeometry.Scheme.emptyTo_base, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.Scheme.zeroLocus_mul, AlgebraicGeometry.Spec.map_injective, AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.StructureSheaf.comap_id', AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.SpecMap_preimage_basicOpen, CommRingCat.mkUnder_ext_iff, CommRingCat.free_obj_coe, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, smoothSheafCommRing.eval_germ, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, AlgebraicGeometry.Scheme.hom_inv_apply, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, AlgebraicGeometry.Scheme.Hom.range_asFiberHom, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite, AlgebraicGeometry.Scheme.ι_toIso_inv, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, CommAlgCat.forget₂_commRingCat_obj, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.Spec.sheafedSpaceObj_carrier, AlgebraicGeometry.noetherianSpace_of_isAffine, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, CommRingCat.forget_obj, AlgebraicGeometry.IsClosedImmersion.base_closed, AlgebraicGeometry.quasiCompact_iff, PresheafOfModules.Derivation.d_map, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.ValuativeCriterion.Existence.instIsLocalHomCarrierRingHomHomHomCommRingCat, CommRingCat.free_map_coe, AlgebraicGeometry.StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc, AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatOpRightOpΓ, CommRingCat.toAlgHom_comp, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, smoothSheafCommRing.instLocalRing_stalk, AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.Scheme.preimage_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.IdealSheafData.support_mul, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatRightOpΓ, AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.sigmaMk_mk, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_toSheafedSpace, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, AlgebraicGeometry.Spec.locallyRingedSpaceMap_id, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace, CommRingCat.coyoneda_map_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, AlgebraicGeometry.IsPreimmersion.isEmbedding, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', AlgebraicGeometry.functionField_isScalarTower, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, CommRingCat.ofHom_id, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.Scheme.forgetToTop_map, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, AlgebraicGeometry.Proj.one_apply, AlgebraicGeometry.AffineScheme.mk_obj, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.forget_obj, AlgebraicGeometry.Scheme.eqToHom_c_app, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.Scheme.forgetToTop_obj, CommRingCat.pushoutCocone_inl, AlgebraicGeometry.IsOpenImmersion.isOpen_range, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, CommRingCat.coyoneda_obj_obj_carrier, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, CommRingCat.isFinitelyPresentable_hom, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.compactSpace_of_isAffine, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_iUnion, CommRingCat.hasLimit, AlgebraicGeometry.IsReduced.component_reduced, CommRingCat.coyoneda_obj_map, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, PresheafOfModules.Derivation.postcomp_d_apply, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, AlgebraicGeometry.Scheme.comp_base, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, PresheafOfModules.Derivation.d_one, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.StructureSheaf.comap_const, AlgebraicGeometry.Scheme.Hom.image_iSup₂, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.zeroLocus_singleton, AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.component_nontrivial, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, CommRingCat.HomTopology.continuous_precomp, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.Proj.sub_apply, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, PresheafOfModules.Derivation.d_mul, AlgebraicGeometry.Scheme.hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.isNoetherian_iff, CommRingCat.Under.preservesFiniteLimits_of_flat, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.IsNoetherian.toCompactSpace, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, AlgebraicGeometry.IsIntegral.nonempty, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.StructureSheaf.comap_apply, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.Spec.faithful, AlgebraicGeometry.Spec.preimage_id, AlgebraicGeometry.IsNoetherian.noetherianSpace, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.Scheme.homeoOfIso_symm, AlgebraicGeometry.Scheme.comp_coeBase_assoc, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, CommRingCat.hasLimitsOfShape, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.Scheme.Hom.toPartialMap_domain, AlgebraicGeometry.coprodMk_inl, AlgebraicGeometry.RingedSpace.zeroLocus_isClosed, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.hy, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Hom.id_app, AlgebraicGeometry.Scheme.Γ_obj, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, AlgHom.toUnder_comp, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Proj.mem_basicOpen, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, CommRingCat.pushoutCocone_inr, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, Localization.epi, AlgebraicGeometry.quasiCompact_over_affine_iff, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, AlgebraicGeometry.ΓSpec.adjunction_counit_app', AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.Scheme.germToFunctionField_injective, AlgebraicGeometry.Scheme.Hom.isIso_base, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.Spec.topMap_id, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', AlgebraicGeometry.Scheme.hom_base_inv_base_assoc, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, PresheafOfModules.Monoidal.tensorObj_map_tmul, AlgebraicGeometry.Scheme.zeroLocus_setMul, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, AlgebraicGeometry.Scheme.Opens.nonempty_iff, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, commAlgCatEquivUnder_functor_obj, TopCat.Presheaf.stalk_open_algebraMap, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.Scheme.Hom.app_surjective, AlgebraicGeometry.coe_opensRestrict_symm_apply, smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.RingedSpace.basicOpen_pow, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Modules.toPresheaf_obj, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, CommRingCat.coproductCocone_inl, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, CommRingCat.Under.instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.AffineScheme.Γ_preservesLimits, CommRingCat.Colimits.cocone_naturality, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, smoothSheafCommRing.forgetStalk_inv_comp_eval, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, AlgebraicGeometry.Spec.toLocallyRingedSpace_obj, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, CommRingCat.HomTopology.precompHomeomorph_apply, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.isInitial_iff_isEmpty, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, CommRingCat.Under.instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier, AlgebraicGeometry.IsImmersion.isLocallyClosed_range, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.basicOpen_le, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.Scheme.Modules.isSheaf, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, smoothSheafCommRing.forgetStalk_inv_comp_eval_apply, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.Scheme.zeroLocus_def, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, smoothSheafCommRing.isUnit_stalk_iff, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.tilde.isoTop_hom, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, AlgebraicGeometry.IsArtinianScheme.finite, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, ModuleCat.Tilde.toOpen_res, CommRingCat.isPushout_tensorProduct, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, AlgebraicGeometry.Scheme.id.base, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, AlgebraicGeometry.Scheme.Γ_def, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.Spec.full, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, CommRingCat.mkUnder_hom, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Scheme.residue_descResidueField, smoothSheafCommRing.ι_evalHom, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Opens.toScheme_carrier, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, AlgEquiv.toUnder_trans, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, CommRingCat.instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι, AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_apply, AlgebraicGeometry.LocallyRingedSpace.stalkMap_id, AlgebraicGeometry.Spec.map_preimage_unop, RingEquiv.toCommRingCatIso_inv, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, CommRingCat.HomTopology.isEmbedding_pushout, AlgebraicGeometry.ΓSpecIso_obj_hom, CommRingCat.coproductCocone_inr, AlgebraicGeometry.Scheme.SpecΓIdentity_app, AlgebraicGeometry.Proj.basicOpen_mul, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.homeoOfIso_apply, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, CommRingCat.forget_map, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, CommRingCat.isPushout_of_isPushout, AlgebraicGeometry.Scheme.Modules.restrict_map, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, AlgebraicGeometry.Scheme.PartialMap.restrict_id, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.AffineSpace.spec_le_iff, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, smoothSheafCommRing.evalHom_germ, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, AlgebraicGeometry.HasRingHomProperty.iff_appLE, PresheafOfModules.Derivation.congr_d, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.Opens.exists_toScheme, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.HasAffineProperty.restrict, CommRingCat.Under.tensorProdEqualizer_ι, AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.opensDiagramι_app, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, AlgebraicGeometry.Scheme.IdealSheafData.support_antitone, AlgebraicGeometry.Scheme.component_nontrivial, AlgebraicGeometry.isCompl_range_inl_inr, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.ΓSpec.adjunction_unit_app, AlgebraicGeometry.Scheme.basicOpen_pow, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, AlgebraicGeometry.LocallyRingedSpace.comp_base, AlgebraicGeometry.IsLocallyNoetherian.quasiSeparatedSpace, AlgebraicGeometry.Scheme.Hom.ker_apply, CommRingCat.Under.instPreservesFiniteProductsUnderPushout, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, CommRingCat.toAlgHom_id, AlgebraicGeometry.Scheme.Hom.isSpectralMap, CommRingCat.HomTopology.instT2SpaceHomOfCarrier, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, AlgebraicGeometry.mem_range_iff_of_surjective, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans, AlgebraicGeometry.Scheme.Modules.toPresheaf_map, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, RingEquiv.toCommRingCatIso_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, CommRingCat.hom_comp, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, CommRingCat.hasLimitsOfSize, CommRingCat.HomTopology.precompHomeomorph_symm_apply, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support, AlgebraicGeometry.Scheme.zeroLocus_radical, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, CommRingCat.mkUnder_right, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.compactSpace_iff_quasiCompact, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, AlgebraicGeometry.RingedSpace.basicOpen_le, CommRingCat.HomTopology.isClosedEmbedding_hom, AlgebraicGeometry.Scheme.Opens.ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.Scheme.comp_base_assoc, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.Scheme.stalkMap_id, AlgebraicGeometry.LocallyRingedSpace.comp_toShHom, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, CommRingCat.hom_inv_apply, AlgebraicGeometry.LocallyRingedSpace.restrict_carrier, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.isIso_iff_isOpenImmersion, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.Spec.sheafedSpaceMap_comp, AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.Scheme.zeroLocus_inf, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', AlgebraicGeometry.AffineSpace.isOpenMap_over, AlgebraicGeometry.surjective_iff, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, CommRingCat.epi_iff_tmul_eq_tmul, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.Spec.toPresheafedSpace_map_op, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec, AlgebraicGeometry.isLocalIso_iff, AlgebraicGeometry.Spec.preimage_comp_assoc, AlgebraicGeometry.AffineSpace.hom_ext_iff, CommRingCat.forget₂CommSemiRing_preservesLimits, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.stalkMap_toStalk, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.IsLocallyArtinian.discreteTopology, AlgebraicGeometry.Scheme.Hom.isOpenMap, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, AlgEquiv.toUnder_inv_right_apply, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc, CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, AlgebraicGeometry.Scheme.Pullback.Triplet.hx, AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.tilde.isIso_toOpen_top, AlgebraicGeometry.Scheme.instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.Hom.prop, TopCat.Presheaf.SubmonoidPresheaf.map, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.Spec.fromSpecStalk_eq', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced, CommRingCat.commMon_forget₂_obj_coe, AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, CommRingCat.toAlgHom_apply, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, AlgebraicGeometry.IsProper.instMorphismRestrict, CommRingCat.HomTopology.isEmbedding_hom, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.IsArtinianScheme.toCompactSpace, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, TopCat.Presheaf.instMonoCommRingCatToTotalQuotientPresheafPresheaf, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, AlgebraicGeometry.Scheme.IdealSheafData.support_comap, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, CommRingCat.epi_iff_epi, CommRingCat.hasLimits, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup, AlgebraicGeometry.Scheme.Γ_map_op, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, smoothSheafCommRing.ι_forgetStalk_inv_apply, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField, AlgebraicGeometry.Scheme.iso_inv_base_hom_base, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.range_eq_univ, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.opensDiagram_obj, CommRingCat.coproductCocone_pt, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, AlgebraicGeometry.Proj.basicOpen_mono, CommRingCat.monoidAlgebra_map, AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, AlgebraicGeometry.Scheme.residueFieldCongr_trans, AlgebraicGeometry.Spec.map_apply, CommRingCat.forgetToRingCat_obj, CommRingCat.Colimits.cocone_naturality_components, AlgebraicGeometry.pointOfClosedPoint_apply, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Spec.toSheafedSpace_obj, AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.sigmaι_eq_iff, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.Scheme.toSpecΓ_appTop, TopCat.Presheaf.epi_toLocalizationPresheaf, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton, AlgebraicGeometry.Scheme.stalkMap_comp, smoothSheafCommRing.eval_surjective, AlgebraicGeometry.Scheme.residue_surjective, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeSchemeΓ, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing, AlgebraicGeometry.Scheme.basicOpen_one, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.over_def, AlgebraicGeometry.Scheme.Modules.Hom.id_app, AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, smoothSheafCommRing.forgetStalk_hom_comp_evalHom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.Γ_map, AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, AlgebraicGeometry.AffineScheme.forgetToScheme_map, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, AlgebraicGeometry.Scheme.Cover.ulift_I₀, CommRingCat.FilteredColimits.forget_preservesFilteredColimits, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, IsLocalization.epi, CommRingCat.moduleCatExtendScalarsPseudofunctor_obj, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply, commAlgCatEquivUnder_counitIso, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans_hom_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, AlgebraicGeometry.Scheme.Opens.ι_appTop, AlgebraicGeometry.Scheme.Modules.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, RingHom.surjective_iff_epi_and_finite, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, CommRingCat.isPushout_iff_isPushout, AlgebraicGeometry.coprodSpec_coprodMk, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Proj.zero_apply, PresheafOfModules.Derivation'.d_app, AlgebraicGeometry.isAffine_affineScheme, AlgebraicGeometry.isRetrocompact_basicOpen, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, AlgebraicGeometry.quasiSeparatedSpace_of_isAffine, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, AlgebraicGeometry.Spec_carrier, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, AlgebraicGeometry.isArtinianScheme_iff, AlgebraicGeometry.Scheme.Hom.id_appIso, AlgebraicGeometry.Scheme.empty_carrier_carrier, smoothSheafCommRing.ι_forgetStalk_inv_assoc, AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, AlgebraicGeometry.Scheme.local_affine, AlgebraicGeometry.Proj.basicOpen_one, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace, commAlgCatEquivUnder_inverse_obj_carrier, AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, ModuleCat.Derivation.d_map, AlgebraicGeometry.instIsAffineObjOppositeCommRingCatSchemeSpec, CommRingCat.Under.instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, CommRingCat.ofHom_apply, AlgebraicGeometry.Scheme.isoSpec_Spec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, AlgebraicGeometry.compactSpace_iff_exists, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible, AlgebraicGeometry.Scheme.Hom.preimage_sup, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.Scheme.iso_hom_base_inv_base, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgHom.toUnder_right, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.residueFieldCongr_refl, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.Scheme.Hom.image_iSup, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.isImmersion_iff, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d, AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, AlgEquiv.toUnder_hom_right_apply, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, CommRingCat.HomTopology.continuous_apply, AlgebraicGeometry.Scheme.Hom.isOpen_quasiFiniteAt, preservesFilteredColimits_coyoneda, AlgebraicGeometry.Scheme.inv_appTop, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.isPullback_Spec_map_pushout, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff, AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, CommRingCat.forget_map_apply, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, commAlgCatEquivUnder_unitIso, CommRingCat.isFinitelyPresentable_under, AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, AlgebraicGeometry.Proj.isBasis_basicOpen, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, CommRingCat.forget₂Ring_preservesLimits, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.geometricallyIrreducible_iff, AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Flat.generalizingMap, AlgebraicGeometry.Scheme.Hom.fiberι_asFiber, AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.Scheme.default_asIdeal, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.Hom.id_base, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map, AlgebraicGeometry.AffineScheme.Spec_essSurj, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.isPreimmersion_iff, AlgebraicGeometry.Scheme.AffineCover.covers, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, CommRingCat.equalizer_ι_isLocalHom', AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsFinite.finite_preimage_singleton, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, AlgebraicGeometry.IsLocalAtTarget.restrict, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, CommRingCat.FilteredColimits.forget₂Ring_preservesFilteredColimits, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom, RingHom.surjective_of_epi_of_finite, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, localization_unit_isIso, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.Scheme.toOpen_eq, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, AlgebraicGeometry.Spec.toSheafedSpace_map, AlgebraicGeometry.Scheme.Modules.restrict_obj, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, AlgebraicGeometry.isCompl_opensRange_inl_inr, TopCat.Presheaf.restrictOpenCommRingCat_apply, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ, AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, AlgebraicGeometry.Scheme.Modules.Hom.add_app, PresheafOfModules.Derivation.d_app, AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.isBasis_affine_open, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, CommRingCat.coproductCoconeIsColimit_desc, AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine, AlgebraicGeometry.isIntegralHom_iff, AlgebraicGeometry.RingedSpace.basicOpen_res_eq, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, PresheafOfModules.Monoidal.tensorHom_app, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map, AlgebraicGeometry.Spec.topMap_comp, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, CommRingCat.tensorProdIsoPushout_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc, CommRingCat.inv_hom_apply, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, AlgebraicGeometry.Flat.stalkMap, AlgebraicGeometry.Scheme.Pullback.range_snd, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_base, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType, AlgebraicGeometry.StructureSheaf.algebraMap_germ, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.preservesLimit_rightOp_Γ, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit, PresheafOfModules.Derivation'.app_apply, CommRingCat.comp_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, AlgebraicGeometry.Spec.homEquiv_apply, AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.IsPreimmersion.base_embedding, RingHom.toMorphismProperty_respectsIso_iff, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, smoothSheafCommRing.ι_forgetStalk_hom_apply, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, AlgebraicGeometry.instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, AlgebraicGeometry.Spec.map_eqToHom, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, AlgebraicGeometry.Scheme.Opens.forall_toScheme, smoothSheafCommRing.ι_forgetStalk_hom_assoc, AlgebraicGeometry.Scheme.topIso_hom, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton, AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec, AlgebraicGeometry.finite_appTop_of_universallyClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.Scheme.inv_hom_apply, AlgebraicGeometry.instIsPreimmersionFromSpecStalk, AlgebraicGeometry.IsIntegralHom.integral_app, commAlgCatEquivUnder_inverse_map, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, CommRingCat.coyonedaUnique_inv_app_hom_apply, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.Spec_fromSpecStalk', AlgebraicGeometry.Scheme.IdealSheafData.support_map, AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.ΓSpec.right_triangle, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', AlgebraicGeometry.Scheme.residue_residueFieldCongr, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, AlgebraicGeometry.Scheme.Pullback.range_fst, CommRingCat.Under.instPreservesFiniteProductsUnderTensorProd, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, AlgebraicGeometry.LocallyRingedSpace.isLocalRing, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.StructureSheaf.stalkAlgebra_map, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base, CommRingCat.equalizer_ι_isLocalHom, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact, AlgebraicGeometry.Scheme.IsQuasiAffine.toCompactSpace, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.Scheme.Hom.comp_base_assoc, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, preservesColimit_coyoneda_of_finitePresentation, AlgebraicGeometry.Scheme.Hom.image_le_opensRange, AlgebraicGeometry.noetherianSpace_of_isAffineOpen, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, AlgebraicGeometry.smoothOfRelativeDimension_iff, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE, AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.Spec_Γ_naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.Scheme.empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, AlgebraicGeometry.ΓSpec.toSpecΓ_of, AlgebraicGeometry.Scheme.zeroLocus_span, AlgebraicGeometry.StructureSheaf.toOpen_germ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated, AlgebraicGeometry.Scheme.Hom.image_injective, CommRingCat.HomTopology.isHomeomorph_precomp, AlgebraicGeometry.Proj.stalkIso'_germ, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, CommRingCat.Colimits.hasColimits_commRingCat, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top, AlgebraicGeometry.Proj.basicOpen_zero, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.formallyUnramified_iff, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, AlgebraicGeometry.Scheme.mem_basicOpen_top, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, CommRingCat.coyonedaUnique_hom_app_hom_apply, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.Spec.map_inv, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.isClosedImmersion_iff, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_base, AlgebraicGeometry.Spec_closedPoint, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.isPullback_SpecMap_pushout, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.Hom.finite_preimage, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField, AlgebraicGeometry.quasiCompact_iff_compactSpace, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, AlgebraicGeometry.Scheme.comp_appTop, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, smoothSheafCommRing.ι_evalHom_assoc, AlgebraicGeometry.Surjective.surj, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, CommRingCat.instIsRightAdjointOppositeObjFunctorTypeYoneda, CommRingCat.Under.equalizerFork_ι, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.Spec.toPresheafedSpace_obj_op, AlgebraicGeometry.Scheme.comp_base_apply, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv_assoc, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, smoothSheafCommRing.ι_forgetStalk_hom, AlgebraicGeometry.IsDominant.denseRange, AlgebraicGeometry.Spec.sheafedSpaceMap_id, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top, AlgebraicGeometry.Spec.map_base, AlgebraicGeometry.Scheme.instIsOverMapHomCommRingCatResidueFieldCongr, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.compactSpace_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.fromSpec_top, AlgebraicGeometry.Scheme.Hom.support_ker, commAlgCatEquivUnder_functor_map, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, CommRingCat.piFan_pt, AlgebraicGeometry.Scheme.Hom.homeomorph_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.Scheme.Hom.isIso_toPshHom, AlgebraicGeometry.Scheme.IdealSheafData.support_top, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.Scheme.Hom.comp_appTop, AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier, CommRingCat.instIsLeftAdjointCommMonCatUnderMonoidAlgebra, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.Scheme.Hom.surjective, AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, CommRingCat.monoidAlgebra_obj, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.LocallyRingedSpace.comp_toHom, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, AlgebraicGeometry.etale_iff, CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom, AlgebraicGeometry.isAffineOpen_bot, AlgebraicGeometry.Scheme.IsLocallyDirected.V_self, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_id, AlgebraicGeometry.Scheme.Opens.ι_image_le, AlgebraicGeometry.Spec.toPresheafedSpace_map, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, AlgebraicGeometry.LocallyRingedSpace.forgetToTop_obj, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, AlgebraicGeometry.specTargetImageRingHom_surjective, AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Spec_obj, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, AlgebraicGeometry.tilde.toOpen_map_app_assoc, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_map, AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, AlgebraicGeometry.AffineScheme.forgetToScheme_obj, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, AlgebraicGeometry.Scheme.Hom.comp_image, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, CommRingCat.hom_id, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Spec.toLocallyRingedSpace_map, isLocalHom_of_iso, AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.residue_descResidueField_assoc, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Flat.isQuotientMap_of_surjective, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.instIsPreimmersionAsFiberHom, AlgebraicGeometry.locallyOfFinitePresentation_iff, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, AlgebraicGeometry.quasiCompact_iff_spectral, AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply, CommRingCat.commMon_forget₂_map, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.Scheme.toIso_inv_ι, AlgebraicGeometry.quasiCompact_iff_isSpectralMap, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.Scheme.Spec_map, AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField_assoc, CommRingCat.isLocalHom_comp, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.opensRange_comp, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Scheme.Hom.comp_base, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.genericPoint_eq_bot_of_affine, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.Scheme.residueFieldMap_id, AlgebraicGeometry.IsSeparated.instMorphismRestrict, AlgebraicGeometry.Scheme.PartialMap.dense_domain, AlgebraicGeometry.basicOpen_eq_bot_iff, AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, localization_unit_isIso', AlgebraicGeometry.Scheme.restrictFunctor_obj_left, isFinitelyPresentable, AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, AlgebraicGeometry.Scheme.Hom.stalkMap_id, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.Scheme.basicOpen_restrict, AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, AlgebraicGeometry.Scheme.IdealSheafData.support_bot, CommRingCat.ofHom_comp, AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq, CommRingCat.forget_preservesLimits, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, CommRingCat.forgetToRingCat_map_hom, AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Opens.ι_image_top, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.range_fromSpecResidueField, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.LocallyRingedSpace.id_toHom, AlgebraicGeometry.Scheme.zeroLocus_isClosed, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.Scheme.Γ_obj_op, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.mem_quasiFiniteLocus, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.isIso_toSpecΓ, AlgebraicGeometry.Proj.res_apply, AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.inv_base_hom_base_assoc, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, AlgebraicGeometry.StructureSheaf.toOpen_res, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, AlgebraicGeometry.Scheme.OpenCover.restrict_X, PresheafOfModules.germ_smul, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, AlgebraicGeometry.Scheme.JointlySurjective.exists_eq, AlgebraicGeometry.Scheme.Hom.image_le_image_iff, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, AlgebraicGeometry.AffineSpace.map_appTop_coord, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, CommRingCat.prodFan_pt, AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom_assoc, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.isIso_fromTildeΓ_iff, AlgebraicGeometry.Scheme.residueFieldCongr_inv, AlgebraicGeometry.Scheme.coe_homeoOfIso, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj, AlgebraicGeometry.Scheme.RationalMap.mem_domain, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, AlgebraicGeometry.spec_punit_isEmpty, AlgebraicGeometry.LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace, AlgebraicGeometry.isClosedMap_iff_specializingMap, AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian, AlgebraicGeometry.isReduced_stalk_of_isReduced, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, TopCat.Presheaf.submonoidPresheafOfStalk_obj, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, CommRingCat.Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.codisjoint_zeroLocus, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_obj, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, AlgebraicGeometry.Scheme.PartialMap.restrict_id_hom, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.map_injective_of_isIntegral, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.initial_isEmpty, AlgebraicGeometry.Proj.stalkIso'_symm_mk, AlgebraicGeometry.Scheme.residueFieldMap_comp, AlgebraicGeometry.Etale.instMorphismRestrict, CommAlgCat.forget₂_commRingCat_map, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm, AlgebraicGeometry.Scheme.comp_coeBase, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base, AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, AlgebraicGeometry.localRingHom_comp_stalkIso, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_inv_app, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.coe_opensRestrict_apply_coe, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Spec.toTop_obj_carrier, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian, AlgebraicGeometry.Scheme.Hom.app_injective, AlgebraicGeometry.Scheme.Modules.inv_app, AlgebraicGeometry.Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.AffineScheme.Spec_full, CommRingCat.preservesFilteredColimits_coyoneda, AlgebraicGeometry.coprodMk_inr, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, AlgebraicGeometry.Scheme.instEpiCommRingCatResidue, AlgebraicGeometry.Scheme.Hom.isProperMap, AlgebraicGeometry.Scheme.isoOfEq_hom, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_symm, AlgebraicGeometry.Scheme.le_iff_specializes, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc, AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj, CommRingCat.coproductCocone_ι, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_refl, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, CommRingCat.preservesColimit_coyoneda_of_finitePresentation, AlgebraicGeometry.essImage_Spec, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Scheme.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Spec_stalkClosedPointIso, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_inv, AlgebraicGeometry.Scheme.Opens.ι_base_apply, AlgebraicGeometry.Scheme.Hom.eqToHom_app, AlgebraicGeometry.instIsAffineHomιBasicOpen, AlgebraicGeometry.LocallyRingedSpace.preservesCoequalizer, AlgebraicGeometry.Scheme.id_app, AlgebraicGeometry.flat_iff, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.Scheme.residueFieldCongr_symm, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base_apply, AlgebraicGeometry.Scheme.homOfLE_rfl, AlgebraicGeometry.Scheme.fromSpecResidueField_apply, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, CommRingCat.instIsRightAdjointForgetRingHomCarrier, AlgebraicGeometry.Scheme.Hom.coe_opensRange, AlgebraicGeometry.quasiSeparatedSpace_iff_affine, AlgebraicGeometry.Scheme.IdealSheafData.le_def, AlgebraicGeometry.Scheme.stalkMap_congr, AlgebraicGeometry.Spec.homEquiv_symm_apply, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, CommRingCat.Under.equalizer_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, RingHom.IsStableUnderBaseChange.pushout_inl, AlgebraicGeometry.AffineScheme.ΓIsEquiv, AlgebraicGeometry.Scheme.inv_base_hom_base, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion, AlgebraicGeometry.quasiSeparated_over_affine_iff, CommRingCat.Under.equalizerFork'_ι, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.Scheme.affineBasicOpen_le, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, CommRingCat.isPushout_of_isLocalization, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf', AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom, AlgebraicGeometry.Scheme.Cover.fromGlued_injective, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.Spec.map_base_apply, AlgebraicGeometry.morphismRestrict_id, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right, AlgebraicGeometry.tilde.toOpen_map_app, AlgebraicGeometry.Spec.preimage_comp, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right, AlgebraicGeometry.Scheme.Hom.id_image, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth

---

← Back to Index