Stalk

📁 Source: Mathlib/AlgebraicGeometry/Stalk.lean

Statistics

Metric	Count
Definitions fromSpecStalk, fromSpecStalkOfMem, fromSpecStalk, stalkClosedPointTo, SpecToEquivOfLocalRing, instCanonicallyOverSpecStalkCommRingCatPresheaf, instOverSpecStalkCommRingCatPresheaf, stalkClosedPointIso	8
Theorems fromSpecStalk_closedPoint, fromSpecStalk_eq, fromSpecStalk_eq_fromSpecStalk, fromSpecStalk_isPreimmersion, fromSpecStalkOfMem_toSpecΓ, fromSpecStalkOfMem_toSpecΓ_assoc, fromSpecStalkOfMem_ι, fromSpecStalkOfMem_ι_assoc, SpecMap_stalkMap_fromSpecStalk, SpecMap_stalkMap_fromSpecStalk_assoc, SpecMap_stalkSpecializes_fromSpecStalk, SpecMap_stalkSpecializes_fromSpecStalk_assoc, Spec_fromSpecStalk, Spec_fromSpecStalk', Spec_map_stalkMap_fromSpecStalk, Spec_map_stalkMap_fromSpecStalk_assoc, Spec_map_stalkSpecializes_fromSpecStalk, Spec_map_stalkSpecializes_fromSpecStalk_assoc, Spec_stalkClosedPointTo_fromSpecStalk, Spec_stalkClosedPointTo_fromSpecStalk_assoc, fromSpecStalk_app, fromSpecStalk_appTop, fromSpecStalk_closedPoint, fromSpecStalk_toSpecΓ, fromSpecStalk_toSpecΓ_assoc, germ_stalkClosedPointTo, germ_stalkClosedPointTo_Spec, germ_stalkClosedPointTo_Spec_fromSpecStalk, germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc, germ_stalkClosedPointTo_assoc, instIsOverFromSpecStalkOfMem, instIsOverMapStalkMapOverInferInstanceOverClass, instIsOverMapStalkSpecializesCommRingCatPresheaf, isLocalHom_stalkClosedPointTo, isLocalHom_stalkClosedPointTo', preimage_eq_top_of_closedPoint_mem, range_fromSpecStalk, stalkClosedPointTo_comp, stalkClosedPointTo_fromSpecStalk, fromSpecStalk_eq, fromSpecStalk_eq', SpecToEquivOfLocalRing_apply_fst, SpecToEquivOfLocalRing_apply_snd_coe, SpecToEquivOfLocalRing_eq_iff, SpecToEquivOfLocalRing_symm_apply, Spec_stalkClosedPointIso, germ_stalkClosedPointIso_hom, germ_stalkClosedPointIso_hom_assoc, instIsPreimmersionFromSpecStalk, over_def, stalkClosedPointIso_inv, ΓSpecIso_hom_stalkClosedPointIso_inv	52
Total	60

AlgebraicGeometry

Definitions

Name	Category	Theorems
SpecToEquivOfLocalRing 📖	CompOp	3 math math: SpecToEquivOfLocalRing_apply_snd_coe, SpecToEquivOfLocalRing_apply_fst, SpecToEquivOfLocalRing_symm_apply
instCanonicallyOverSpecStalkCommRingCatPresheaf 📖	CompOp	1 math math: Scheme.instIsOverMapStalkMapOverInferInstanceOverClass
instOverSpecStalkCommRingCatPresheaf 📖	CompOp	4 math math: Scheme.instIsOverFromSpecStalkOfMem, over_def, Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf, Scheme.instIsOverMapStalkMapOverInferInstanceOverClass
stalkClosedPointIso 📖	CompOp	5 math math: germ_stalkClosedPointIso_hom_assoc, germ_stalkClosedPointIso_hom, ΓSpecIso_hom_stalkClosedPointIso_inv, stalkClosedPointIso_inv, Spec_stalkClosedPointIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecToEquivOfLocalRing_apply_fst 📖	mathematical	—	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf IsLocalHom CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom DFunLike.coe Equiv Scheme Scheme.instCategory Spec EquivLike.toFunLike Equiv.instEquivLike SpecToEquivOfLocalRing CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' IsLocalRing.closedPoint	—	CommRingCat.Colimits.hasColimits_commRingCat
SpecToEquivOfLocalRing_apply_snd_coe 📖	mathematical	—	Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf DFunLike.coe Spec TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing IsLocalHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom Equiv Scheme Scheme.instCategory EquivLike.toFunLike Equiv.instEquivLike SpecToEquivOfLocalRing Scheme.stalkClosedPointTo	—	CommRingCat.Colimits.hasColimits_commRingCat
SpecToEquivOfLocalRing_eq_iff 📖	mathematical	—	Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf TopCat.carrier IsLocalHom CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom TopCat.Presheaf.stalkCongr	—	CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.id_comp
SpecToEquivOfLocalRing_symm_apply 📖	mathematical	—	DFunLike.coe Equiv TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf IsLocalHom CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom Scheme Scheme.instCategory Spec EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SpecToEquivOfLocalRing CategoryTheory.CategoryStruct.comp Spec.map Scheme.fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat
Spec_stalkClosedPointIso 📖	mathematical	—	Spec.map TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec PresheafedSpace.presheaf IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing CategoryTheory.Iso.inv stalkClosedPointIso Scheme.fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat stalkClosedPointIso_inv Spec.fromSpecStalk_eq'
germ_stalkClosedPointIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing TopCat.Presheaf.germ CategoryTheory.Iso.hom stalkClosedPointIso Scheme.Opens SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.ΓSpecIso	—	CommRingCat.Colimits.hasColimits_commRingCat ΓSpecIso_hom_stalkClosedPointIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
germ_stalkClosedPointIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing TopCat.Presheaf.germ CategoryTheory.Iso.hom stalkClosedPointIso Scheme.Opens SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.ΓSpecIso	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkClosedPointIso_hom
instIsPreimmersionFromSpecStalk 📖	mathematical	—	IsPreimmersion Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf Scheme.fromSpecStalk	—	IsAffineOpen.fromSpecStalk_isPreimmersion Scheme.instJointlySurjectivePrecoverage
over_def 📖	mathematical	—	CategoryTheory.over Scheme Scheme.instCategory Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf CategoryTheory.OverClass instOverSpecStalkCommRingCatPresheaf Scheme.fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat
stalkClosedPointIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec PresheafedSpace.presheaf IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing stalkClosedPointIso StructureSheaf.toStalk	—	CommRingCat.hom_ext CommRingCat.Colimits.hasColimits_commRingCat RingHom.ext AlgEquiv.commutes PrimeSpectrum.isPrime
ΓSpecIso_hom_stalkClosedPointIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing CategoryTheory.Iso.hom Scheme.ΓSpecIso CategoryTheory.Iso.inv stalkClosedPointIso TopCat.Presheaf.germ	—	CommRingCat.Colimits.hasColimits_commRingCat stalkClosedPointIso_inv CategoryTheory.Iso.eq_inv_comp

AlgebraicGeometry.IsAffineOpen

Definitions

Name	Category	Theorems
fromSpecStalk 📖	CompOp	4 math math: fromSpecStalk_closedPoint, fromSpecStalk_isPreimmersion, fromSpecStalk_eq, fromSpecStalk_eq_fromSpecStalk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSpecStalk_closedPoint 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopologicalSpace.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromSpecStalk IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf fromSpecStalk.eq_1 AlgebraicGeometry.Scheme.Hom.comp_apply primeIdealOf_eq_map_closedPoint fromSpec_primeIdealOf
fromSpecStalk_eq 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.Opens.isBasis_iff_nbhd AlgebraicGeometry.Scheme.isBasis_affineOpens LE.le.trans inf_le_left map_fromSpec AlgebraicGeometry.Scheme.Spec_map CategoryTheory.Functor.map_comp_assoc CategoryTheory.op_comp TopCat.Presheaf.germ_res Quiver.Hom.unop_op inf_le_right
fromSpecStalk_eq_fromSpecStalk 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	fromSpecStalk AlgebraicGeometry.Scheme.fromSpecStalk	—	fromSpecStalk_eq AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage
fromSpecStalk_isPreimmersion 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopologicalSpace.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike	AlgebraicGeometry.IsPreimmersion AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.IsPreimmersion.comp AlgebraicGeometry.IsPreimmersion.of_isLocalization PrimeSpectrum.isPrime isLocalization_stalk AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion isOpenImmersion_fromSpec

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
fromSpecStalk 📖	CompOp	32 math math: fromSpecStalk_closedPoint, Spec_map_stalkMap_fromSpecStalk, fromSpecStalk_toSpecΓ_assoc, Spec_map_stalkSpecializes_fromSpecStalk, range_fromSpecStalk, Opens.fromSpecStalkOfMem_ι_assoc, fromSpecStalk_appTop, fromSpecStalk_toSpecΓ, Spec_map_stalkMap_fromSpecStalk_assoc, stalkClosedPointTo_fromSpecStalk, SpecMap_stalkSpecializes_fromSpecStalk, descResidueField_fromSpecResidueField, SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.Spec.fromSpecStalk_eq', SpecMap_stalkSpecializes_fromSpecStalk_assoc, Opens.fromSpecStalkOfMem_ι, AlgebraicGeometry.over_def, Hom.quasiFiniteAt_iff, Spec_map_stalkSpecializes_fromSpecStalk_assoc, AlgebraicGeometry.instIsPreimmersionFromSpecStalk, Spec_fromSpecStalk', fromSpecStalk_app, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, AlgebraicGeometry.Spec.fromSpecStalk_eq, SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.spread_out_of_isGermInjective, Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.Spec_stalkClosedPointIso, PartialMap.fromSpecStalkOfMem_toPartialMap, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk, Spec_stalkClosedPointTo_fromSpecStalk_assoc, Spec_fromSpecStalk
stalkClosedPointTo 📖	CompOp	13 math math: germ_stalkClosedPointTo, germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc, germ_stalkClosedPointTo_Spec_fromSpecStalk, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, stalkClosedPointTo_fromSpecStalk, descResidueField_stalkClosedPointTo_fromSpecResidueField, isLocalHom_stalkClosedPointTo', germ_stalkClosedPointTo_assoc, germ_stalkClosedPointTo_Spec, isLocalHom_stalkClosedPointTo, stalkClosedPointTo_comp, Spec_stalkClosedPointTo_fromSpecStalk, Spec_stalkClosedPointTo_fromSpecStalk_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_stalkMap_fromSpecStalk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' AlgebraicGeometry.Spec.map Hom.stalkMap fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open isBasis_affineOpens Set.mem_univ isOpen_univ TopologicalSpace.Opens.is_open' AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk AlgebraicGeometry.IsAffineOpen.fromSpecStalk.eq_1 AlgebraicGeometry.Spec.map_comp_assoc Hom.germ_stalkMap TopCat.Presheaf.germ_res CategoryTheory.Category.assoc le_rfl Hom.app_eq_appLE LE.le.trans Hom.appLE_map AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec
SpecMap_stalkMap_fromSpecStalk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' AlgebraicGeometry.Spec.map Hom.stalkMap fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' SpecMap_stalkMap_fromSpecStalk
SpecMap_stalkSpecializes_fromSpecStalk 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map TopCat.Presheaf.stalkSpecializes fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open isBasis_affineOpens Set.mem_univ isOpen_univ Specializes.mem_open TopologicalSpace.Opens.is_open' AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk AlgebraicGeometry.IsAffineOpen.fromSpecStalk.eq_1 CategoryTheory.Category.assoc AlgebraicGeometry.Spec.map_comp TopologicalSpace.Opens.isOpen TopCat.Presheaf.germ_stalkSpecializes
SpecMap_stalkSpecializes_fromSpecStalk_assoc 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map TopCat.Presheaf.stalkSpecializes fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' SpecMap_stalkSpecializes_fromSpecStalk
Spec_fromSpecStalk 📖	mathematical	—	fromSpecStalk AlgebraicGeometry.Spec AlgebraicGeometry.Spec.map TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv ΓSpecIso TopCat.Presheaf.germ	—	AlgebraicGeometry.Spec.fromSpecStalk_eq
Spec_fromSpecStalk' 📖	mathematical	—	fromSpecStalk AlgebraicGeometry.Spec AlgebraicGeometry.Spec.map CommRingCat.of CommRingCat.carrier CommRingCat.commRing TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat AlgebraicGeometry.StructureSheaf.toStalk	—	AlgebraicGeometry.Spec.fromSpecStalk_eq'
Spec_map_stalkMap_fromSpecStalk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' AlgebraicGeometry.Spec.map Hom.stalkMap fromSpecStalk	—	SpecMap_stalkMap_fromSpecStalk
Spec_map_stalkMap_fromSpecStalk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' AlgebraicGeometry.Spec.map Hom.stalkMap fromSpecStalk	—	SpecMap_stalkMap_fromSpecStalk_assoc
Spec_map_stalkSpecializes_fromSpecStalk 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map TopCat.Presheaf.stalkSpecializes fromSpecStalk	—	SpecMap_stalkSpecializes_fromSpecStalk
Spec_map_stalkSpecializes_fromSpecStalk_assoc 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map TopCat.Presheaf.stalkSpecializes fromSpecStalk	—	SpecMap_stalkSpecializes_fromSpecStalk_assoc
Spec_stalkClosedPointTo_fromSpecStalk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.Spec.map stalkClosedPointTo fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open isBasis_affineOpens Set.mem_univ isOpen_univ Eq.ge preimage_eq_top_of_closedPoint_mem AlgebraicGeometry.isAffineOpen_top AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk AlgebraicGeometry.IsAffineOpen.fromSpecStalk.eq_1 AlgebraicGeometry.Spec.map_comp_assoc germ_stalkClosedPointTo LE.le.trans le_rfl Hom.app_eq_appLE Hom.appLE_map_assoc isoSpec_Spec_hom CategoryTheory.Iso.eq_inv_comp AlgebraicGeometry.IsAffineOpen.fromSpec_top
Spec_stalkClosedPointTo_fromSpecStalk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.Spec.map stalkClosedPointTo fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Spec_stalkClosedPointTo_fromSpecStalk
fromSpecStalk_app 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Hom.app AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf fromSpecStalk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' TopCat.Presheaf.germ Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv ΓSpecIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE le_top	—	CommRingCat.Colimits.hasColimits_commRingCat le_top TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open isBasis_affineOpens TopologicalSpace.Opens.is_open' AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk AlgebraicGeometry.IsAffineOpen.fromSpecStalk.eq_1 Hom.comp_app AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le TopCat.Presheaf.germ_res CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality TopCat.Presheaf.germ_res'_assoc TopCat.Presheaf.germ_res'
fromSpecStalk_appTop 📖	mathematical	—	Hom.appTop AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf fromSpecStalk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.Presheaf.germ CategoryTheory.Iso.inv ΓSpecIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE le_top	—	fromSpecStalk_app
fromSpecStalk_closedPoint 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' fromSpecStalk IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf	—	AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint instJointlySurjectivePrecoverage
fromSpecStalk_toSpecΓ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder fromSpecStalk toSpecΓ AlgebraicGeometry.Spec.map TopCat.Presheaf.germ	—	CommRingCat.Colimits.hasColimits_commRingCat toSpecΓ_naturality AlgebraicGeometry.SpecMap_ΓSpecIso_hom AlgebraicGeometry.Spec.map_comp le_top fromSpecStalk_appTop CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id ΓSpecIso_inv_naturality CategoryTheory.Category.assoc ΓSpecIso_naturality CategoryTheory.Iso.inv_hom_id_assoc
fromSpecStalk_toSpecΓ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf fromSpecStalk CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toSpecΓ AlgebraicGeometry.Spec.map TopCat.Presheaf.germ	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromSpecStalk_toSpecΓ
germ_stalkClosedPointTo 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe AlgebraicGeometry.Spec CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ stalkClosedPointTo TopologicalSpace.Opens.map Hom.app CategoryTheory.Iso.hom CategoryTheory.Iso.trans Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor.mapIso CategoryTheory.Iso.op CategoryTheory.eqToIso preimage_eq_top_of_closedPoint_mem ΓSpecIso	—	CommRingCat.Colimits.hasColimits_commRingCat preimage_eq_top_of_closedPoint_mem stalkClosedPointTo.eq_1 Hom.germ_stalkMap_assoc CategoryTheory.Iso.trans_hom CategoryTheory.Iso.eq_comp_inv CategoryTheory.Category.assoc AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv TopCat.Presheaf.germ_res
germ_stalkClosedPointTo_Spec 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' AlgebraicGeometry.Spec.map IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing TopCat.Presheaf.germ stalkClosedPointTo Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Iso.hom ΓSpecIso	—	CommRingCat.Colimits.hasColimits_commRingCat stalkClosedPointTo.eq_1 Hom.germ_stalkMap_assoc CategoryTheory.Iso.inv_comp_eq ΓSpecIso_inv_naturality_assoc AlgebraicGeometry.germ_stalkClosedPointIso_hom CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
germ_stalkClosedPointTo_Spec_fromSpecStalk 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe AlgebraicGeometry.Spec CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map fromSpecStalk IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ stalkClosedPointTo	—	CommRingCat.Colimits.hasColimits_commRingCat Hom.comp_apply AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf AlgebraicGeometry.Spec_closedPoint fromSpecStalk_closedPoint LE.le.trans preimage_eq_top_of_closedPoint_mem le_rfl le_top germ_stalkClosedPointTo fromSpecStalk_app Hom.app_eq_appLE CategoryTheory.Category.assoc Hom.appLE_map_assoc Hom.map_appLE_assoc ΓSpecIso_naturality CategoryTheory.Iso.inv_hom_id_assoc
germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe AlgebraicGeometry.Spec CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map fromSpecStalk IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ stalkClosedPointTo	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkClosedPointTo_Spec_fromSpecStalk
germ_stalkClosedPointTo_assoc 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe AlgebraicGeometry.Spec CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ stalkClosedPointTo TopologicalSpace.Opens.map Hom.app CategoryTheory.Iso.hom CategoryTheory.Iso.trans Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor.mapIso CategoryTheory.Iso.op CategoryTheory.eqToIso preimage_eq_top_of_closedPoint_mem ΓSpecIso	—	CommRingCat.Colimits.hasColimits_commRingCat preimage_eq_top_of_closedPoint_mem CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkClosedPointTo
instIsOverFromSpecStalkOfMem 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Hom.IsOver AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf Opens.toScheme Opens.fromSpecStalkOfMem AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf CategoryTheory.CanonicallyOverClass.toOverClass AlgebraicGeometry.Scheme instCategory Opens.instCanonicallyOverToScheme	—	CommRingCat.Colimits.hasColimits_commRingCat Opens.fromSpecStalkOfMem_ι
instIsOverMapStalkMapOverInferInstanceOverClass 📖	mathematical	—	Hom.IsOver AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.over AlgebraicGeometry.Scheme instCategory CategoryTheory.OverClass AlgebraicGeometry.Spec.map Hom.stalkMap CategoryTheory.CanonicallyOverClass.instOverClass AlgebraicGeometry.instCanonicallyOverSpecStalkCommRingCatPresheaf AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf	—	CommRingCat.Colimits.hasColimits_commRingCat SpecMap_stalkMap_fromSpecStalk
instIsOverMapStalkSpecializesCommRingCatPresheaf 📖	mathematical	Specializes TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Hom.IsOver AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map TopCat.Presheaf.stalkSpecializes AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf	—	CommRingCat.Colimits.hasColimits_commRingCat SpecMap_stalkSpecializes_fromSpecStalk
isLocalHom_stalkClosedPointTo 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe AlgebraicGeometry.Spec TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRing.toCommSemiring CommRingCat.commRing RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom stalkClosedPointTo	—	CommRingCat.Colimits.hasColimits_commRingCat CommRingCat.isLocalHom_comp isLocalHom_of_isIso CategoryTheory.Iso.isIso_hom Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap
isLocalHom_stalkClosedPointTo' 📖	mathematical	—	IsLocalHom CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe AlgebraicGeometry.Spec CommRingCat.of TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRing.toCommSemiring CommRingCat.commRing RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike CommRingCat.Hom.hom stalkClosedPointTo	—	isLocalHom_stalkClosedPointTo
preimage_eq_top_of_closedPoint_mem 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe AlgebraicGeometry.Spec CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing	CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsLocalRing.closed_point_mem_iff
range_fromSpecStalk 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' fromSpecStalk setOf Specializes AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	Set.ext CommRingCat.Colimits.hasColimits_commRingCat Specializes.trans AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf Specializes.map IsLocalRing.specializes_closedPoint Hom.continuous specializes_of_eq fromSpecStalk_closedPoint SpecMap_stalkSpecializes_fromSpecStalk
stalkClosedPointTo_comp 📖	mathematical	—	stalkClosedPointTo CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat stalkClosedPointTo.eq_1 Hom.stalkMap_comp CategoryTheory.Category.assoc
stalkClosedPointTo_fromSpecStalk 📖	mathematical	—	stalkClosedPointTo TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf fromSpecStalk CategoryTheory.Iso.hom DFunLike.coe AlgebraicGeometry.Spec TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing TopCat.Presheaf.stalkCongr	—	TopCat.Presheaf.stalk_hom_ext CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf Specializes.mem_open TopologicalSpace.Opens.isOpen TopCat.Presheaf.germ_stalkSpecializes AlgebraicGeometry.Spec.map_id CategoryTheory.Category.id_comp isLocalHom_of_isIso CategoryTheory.IsIso.id germ_stalkClosedPointTo_Spec_fromSpecStalk

AlgebraicGeometry.Scheme.Opens

Definitions

Name	Category	Theorems
fromSpecStalkOfMem 📖	CompOp	7 math math: AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem, fromSpecStalkOfMem_ι_assoc, fromSpecStalkOfMem_ι, fromSpecStalkOfMem_toSpecΓ, fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.spread_out_of_isGermInjective, AlgebraicGeometry.spread_out_of_isGermInjective'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSpecStalkOfMem_toSpecΓ 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf toScheme CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op fromSpecStalkOfMem toSpecΓ AlgebraicGeometry.Spec.map TopCat.Presheaf.germ	—	CommRingCat.Colimits.hasColimits_commRingCat fromSpecStalkOfMem.eq_1 toSpecΓ.eq_1 CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc AlgebraicGeometry.Spec.map_comp CategoryTheory.IsIso.comp_inv_eq CategoryTheory.Iso.inv_comp_eq AlgebraicGeometry.Scheme.Hom.germ_stalkMap instIsOpenImmersionι Set.image_preimage_subset ι_app topIso_hom CategoryTheory.Functor.map_comp_assoc le_top TopCat.Presheaf.germ_res
fromSpecStalkOfMem_toSpecΓ_assoc 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf toScheme fromSpecStalkOfMem CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op toSpecΓ AlgebraicGeometry.Spec.map TopCat.Presheaf.germ	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromSpecStalkOfMem_toSpecΓ
fromSpecStalkOfMem_ι 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf toScheme fromSpecStalkOfMem ι AlgebraicGeometry.Scheme.fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat AlgebraicGeometry.Spec.map_inv CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk
fromSpecStalkOfMem_ι_assoc 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf toScheme fromSpecStalkOfMem ι AlgebraicGeometry.Scheme.fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromSpecStalkOfMem_ι

AlgebraicGeometry.Spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromSpecStalk_eq 📖	mathematical	—	AlgebraicGeometry.Scheme.fromSpecStalk AlgebraicGeometry.Spec map TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.ΓSpecIso TopCat.Presheaf.germ	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.isAffineOpen_top AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk AlgebraicGeometry.IsAffineOpen.fromSpecStalk.eq_1 AlgebraicGeometry.IsAffineOpen.fromSpec_top AlgebraicGeometry.Scheme.isoSpec_Spec_inv map_comp
fromSpecStalk_eq' 📖	mathematical	—	AlgebraicGeometry.Scheme.fromSpecStalk AlgebraicGeometry.Spec map CommRingCat.of CommRingCat.carrier CommRingCat.commRing TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat AlgebraicGeometry.StructureSheaf.toStalk	—	fromSpecStalk_eq

---

← Back to Index