ResidueField

📁 Source: Mathlib/AlgebraicGeometry/ResidueField.lean

Statistics

Metric	Count
Definitions residueFieldMap, residueFieldIso, SpecToEquivOfField, descResidueField, evaluation, fromSpecResidueField, instCanonicallyOverSpecResidueField, instFieldCarrierResidueField, instOverSpecResidueField, instUniqueCarrierCarrierCommRingCatSpecResidueField, residue, residueField, residueFieldCongr, Γevaluation	14
Theorems SpecMap_residueFieldMap_fromSpecResidueField, SpecMap_residueFieldMap_fromSpecResidueField_assoc, Spec_map_residueFieldMap_fromSpecResidueField, Spec_map_residueFieldMap_fromSpecResidueField_assoc, residueFieldMap_congr, algebraMap_residueFieldIso_inv, algebraMap_residueFieldIso_inv_assoc, residue_residueFieldIso_hom, residue_residueFieldIso_hom_assoc, SpecMap_residue_apply, SpecToEquivOfField_eq_iff, Spec_map_residue_apply, basicOpen_eq_bot_iff_forall_evaluation_eq_zero, descResidueField_fromSpecResidueField, descResidueField_stalkClosedPointTo_fromSpecResidueField, evaluation_eq_zero_iff_notMem_basicOpen, evaluation_naturality, evaluation_naturality_apply, evaluation_naturality_assoc, evaluation_ne_zero_iff_mem_basicOpen, fromSpecResidueField_apply, germ_residue, germ_residue_assoc, instEpiCommRingCatResidue, instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, instIsOverMapHomCommRingCatResidueFieldCongr, instIsOverMapResidueFieldMapOverInferInstanceOverClass, instIsPreimmersionFromSpecResidueField, instIsPreimmersionMapResidue, over_def, range_fromSpecResidueField, residueFieldCongr_fromSpecResidueField, residueFieldCongr_fromSpecResidueField_assoc, residueFieldCongr_inv, residueFieldCongr_refl, residueFieldCongr_symm, residueFieldCongr_trans, residueFieldCongr_trans_hom, residueFieldCongr_trans_hom_assoc, residueFieldMap_comp, residueFieldMap_id, residue_descResidueField, residue_descResidueField_assoc, residue_residueFieldCongr, residue_residueFieldCongr_assoc, residue_residueFieldMap, residue_residueFieldMap_assoc, residue_surjective, Γevaluation_naturality, Γevaluation_naturality_apply, Γevaluation_naturality_assoc	51
Total	65

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
SpecToEquivOfField 📖	CompOp	—
descResidueField 📖	CompOp	4 math math: residue_descResidueField, descResidueField_fromSpecResidueField, descResidueField_stalkClosedPointTo_fromSpecResidueField, residue_descResidueField_assoc
evaluation 📖	CompOp	7 math math: evaluation_eq_zero_iff_notMem_basicOpen, evaluation_naturality, evaluation_naturality_apply, evaluation_naturality_assoc, germ_residue_assoc, germ_residue, basicOpen_eq_bot_iff_forall_evaluation_eq_zero
fromSpecResidueField 📖	CompOp	27 math math: Pullback.Triplet.specTensorTo_fst, Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, Pullback.Triplet.specTensorTo_fst_assoc, Hom.asFiberHom_fiberι_assoc, over_def, Pullback.Triplet.specTensorTo_snd, descResidueField_fromSpecResidueField, Pullback.Triplet.specTensorTo_snd_assoc, Pullback.ofPointTensor_SpecTensorTo_assoc, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, residueFieldCongr_fromSpecResidueField, Hom.asFiberHom_fiberι, instIsPreimmersionFromSpecResidueField, descResidueField_stalkClosedPointTo_fromSpecResidueField, Pullback.ofPointTensor_SpecTensorTo, Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv_assoc, residueFieldCongr_fromSpecResidueField_assoc, Hom.SpecMap_residueFieldMap_fromSpecResidueField, range_fromSpecResidueField, Hom.Spec_map_residueFieldMap_fromSpecResidueField, Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField, Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField, fromSpecResidueField_apply
instCanonicallyOverSpecResidueField 📖	CompOp	1 math math: instIsOverMapResidueFieldMapOverInferInstanceOverClass
instFieldCarrierResidueField 📖	CompOp	2 math math: AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, Hom.fiberToSpecResidueField_apply
instOverSpecResidueField 📖	CompOp	3 math math: over_def, instIsOverMapResidueFieldMapOverInferInstanceOverClass, instIsOverMapHomCommRingCatResidueFieldCongr
instUniqueCarrierCarrierCommRingCatSpecResidueField 📖	CompOp	—
residue 📖	CompOp	19 math math: residue_descResidueField, Spec.residue_residueFieldIso_hom_assoc, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, residue_surjective, Spec.algebraMap_residueFieldIso_inv, residue_residueFieldMap_assoc, residue_residueFieldCongr, residue_residueFieldMap, SpecMap_residue_apply, instIsPreimmersionMapResidue, Spec.algebraMap_residueFieldIso_inv_assoc, residue_residueFieldCongr_assoc, germ_residue_assoc, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, residue_descResidueField_assoc, germ_residue, Spec_map_residue_apply, instEpiCommRingCatResidue, Spec.residue_residueFieldIso_hom
residueField 📖	CompOp	85 math math: Pullback.Triplet.specTensorTo_fst, SpecToEquivOfField_eq_iff, AlgebraicGeometry.GeometricallyIrreducible.iff_geometricallyIrreducible_fiber, Hom.range_asFiberHom, Pullback.Triplet.isPullback_SpecMap_tensor, Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.instGeometricallyReducedFiberToSpecResidueField, AlgebraicGeometry.instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact, Pullback.Triplet.specTensorTo_fst_assoc, Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, Hom.asFiberHom_fiberι_assoc, AlgebraicGeometry.instGeometricallyIntegralFiberToSpecResidueField, over_def, Pullback.Triplet.Spec_map_tensor_isPullback, Γevaluation_naturality_apply, Pullback.Triplet.specTensorTo_snd, AlgebraicGeometry.locallyQuasiFinite_iff_isFinite_fiber, residue_descResidueField, descResidueField_fromSpecResidueField, Hom.asFiberHom_apply, instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, instIsOverMapResidueFieldMapOverInferInstanceOverClass, Pullback.Triplet.specTensorTo_snd_assoc, Pullback.ofPointTensor_SpecTensorTo_assoc, Γevaluation_naturality_assoc, evaluation_eq_zero_iff_notMem_basicOpen, Spec.residue_residueFieldIso_hom_assoc, evaluation_naturality, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, residueFieldCongr_trans, evaluation_naturality_apply, residue_surjective, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, Hom.residueFieldMap_congr, residueFieldCongr_fromSpecResidueField, Hom.asFiberHom_fiberι, Spec.algebraMap_residueFieldIso_inv, residueFieldCongr_refl, instIsPreimmersionFromSpecResidueField, descResidueField_stalkClosedPointTo_fromSpecResidueField, Pullback.ofPointTensor_SpecTensorTo, Hom.Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, residue_residueFieldMap_assoc, AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField, residue_residueFieldCongr, residue_residueFieldMap, evaluation_naturality_assoc, SpecMap_residue_apply, instIsPreimmersionMapResidue, AlgebraicGeometry.GeometricallyIntegral.iff_geometricallyIntegral_fiber, Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, Hom.asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv_assoc, Spec.algebraMap_residueFieldIso_inv_assoc, instIsOverMapHomCommRingCatResidueFieldCongr, residue_residueFieldCongr_assoc, germ_residue_assoc, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, residue_descResidueField_assoc, AlgebraicGeometry.instIsPreimmersionAsFiberHom, residueFieldCongr_trans_hom, residueFieldCongr_fromSpecResidueField_assoc, germ_residue, Γevaluation_naturality, residueFieldMap_id, Hom.SpecMap_residueFieldMap_fromSpecResidueField, range_fromSpecResidueField, basicOpen_eq_bot_iff_forall_evaluation_eq_zero, Hom.fiberToSpecResidueField_apply, residueFieldCongr_trans_hom_assoc, residueFieldCongr_inv, Spec_map_residue_apply, residueFieldMap_comp, AlgebraicGeometry.instGeometricallyIrreducibleFiberToSpecResidueField, Hom.Spec_map_residueFieldMap_fromSpecResidueField, Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField, instEpiCommRingCatResidue, Hom.asFiberHom_fiberToSpecResidueField_assoc, Spec.residue_residueFieldIso_hom, Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField, residueFieldCongr_symm, fromSpecResidueField_apply
residueFieldCongr 📖	CompOp	16 math math: SpecToEquivOfField_eq_iff, Pullback.Triplet.isPullback_SpecMap_tensor, Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, Pullback.Triplet.Spec_map_tensor_isPullback, residueFieldCongr_trans, Hom.residueFieldMap_congr, residueFieldCongr_fromSpecResidueField, residueFieldCongr_refl, residue_residueFieldCongr, instIsOverMapHomCommRingCatResidueFieldCongr, residue_residueFieldCongr_assoc, residueFieldCongr_trans_hom, residueFieldCongr_fromSpecResidueField_assoc, residueFieldCongr_trans_hom_assoc, residueFieldCongr_inv, residueFieldCongr_symm
Γevaluation 📖	CompOp	3 math math: Γevaluation_naturality_apply, Γevaluation_naturality_assoc, Γevaluation_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_residue_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec residueField 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' AlgebraicGeometry.Spec.map residue IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf	—	IsLocalRing.PrimeSpectrum.comap_residue CommRingCat.Colimits.hasColimits_commRingCat
SpecToEquivOfField_eq_iff 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct residueField CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom residueFieldCongr	—	CategoryTheory.Category.id_comp
Spec_map_residue_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec residueField 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' AlgebraicGeometry.Spec.map residue IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf	—	SpecMap_residue_apply
basicOpen_eq_bot_iff_forall_evaluation_eq_zero 📖	mathematical	—	basicOpen Bot.bot Opens OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier HeytingAlgebra.toOrderBot DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op residueField SetLike.instMembership TopologicalSpace.Opens.instSetLike CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier evaluation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero
descResidueField_fromSpecResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain residueField AlgebraicGeometry.Spec.map descResidueField fromSpecResidueField TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat residue_descResidueField
descResidueField_stalkClosedPointTo_fromSpecResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace 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 Field.instIsLocalRing AlgebraicGeometry.Spec.map descResidueField stalkClosedPointTo isLocalHom_stalkClosedPointTo' fromSpecResidueField Semifield.toCommSemiring Field.toSemifield	—	Field.instIsLocalRing isLocalHom_stalkClosedPointTo' CommRingCat.Colimits.hasColimits_commRingCat descResidueField_fromSpecResidueField Spec_stalkClosedPointTo_fromSpecStalk
evaluation_eq_zero_iff_notMem_basicOpen 📖	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 CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op residueField CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier evaluation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing basicOpen	—	AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen
evaluation_naturality 📖	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 CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	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 residueField evaluation Hom.residueFieldMap TopologicalSpace.Opens.map Hom.app	—	AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality
evaluation_naturality_apply 📖	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 CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	residueField CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.residueFieldMap CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op evaluation TopologicalSpace.Opens.map Hom.app	—	AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply
evaluation_naturality_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 CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	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 residueField evaluation Hom.residueFieldMap TopologicalSpace.Opens.map Hom.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' evaluation_naturality
evaluation_ne_zero_iff_mem_basicOpen 📖	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	basicOpen	—	—
fromSpecResidueField_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec residueField 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' fromSpecResidueField	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf SpecMap_residue_apply fromSpecStalk_closedPoint
germ_residue 📖	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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat residueField TopCat.Presheaf.germ residue evaluation	—	CommRingCat.Colimits.hasColimits_commRingCat
germ_residue_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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite 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 residueField residue evaluation	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_residue
instEpiCommRingCatResidue 📖	mathematical	—	CategoryTheory.Epi CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf residueField residue	—	CategoryTheory.ConcreteCategory.epi_of_surjective CommRingCat.Colimits.hasColimits_commRingCat residue_surjective
instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace 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' Hom.residueFieldMap	—	CategoryTheory.Iso.isIso_hom CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap
instIsOverMapHomCommRingCatResidueFieldCongr 📖	mathematical	—	Hom.IsOver AlgebraicGeometry.Spec residueField AlgebraicGeometry.Spec.map CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory residueFieldCongr instOverSpecResidueField	—	AlgebraicGeometry.Spec.map_id CategoryTheory.Category.id_comp
instIsOverMapResidueFieldMapOverInferInstanceOverClass 📖	mathematical	—	Hom.IsOver AlgebraicGeometry.Spec residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace 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.residueFieldMap CategoryTheory.CanonicallyOverClass.instOverClass instCanonicallyOverSpecResidueField instOverSpecResidueField	—	Hom.SpecMap_residueFieldMap_fromSpecResidueField
instIsPreimmersionFromSpecResidueField 📖	mathematical	—	AlgebraicGeometry.IsPreimmersion AlgebraicGeometry.Spec residueField fromSpecResidueField	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.IsPreimmersion.comp_iff AlgebraicGeometry.instIsPreimmersionFromSpecStalk instIsPreimmersionMapResidue
instIsPreimmersionMapResidue 📖	mathematical	—	AlgebraicGeometry.IsPreimmersion AlgebraicGeometry.Spec residueField TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Spec.map residue	—	AlgebraicGeometry.IsPreimmersion.mk_SpecMap CommRingCat.Colimits.hasColimits_commRingCat Topology.IsClosedEmbedding.isEmbedding Ideal.instIsTwoSided_1 PrimeSpectrum.isClosedEmbedding_comap_of_surjective Ideal.Quotient.mk_surjective RingHom.surjectiveOnStalks_of_surjective
over_def 📖	mathematical	—	CategoryTheory.over AlgebraicGeometry.Scheme instCategory AlgebraicGeometry.Spec residueField CategoryTheory.OverClass instOverSpecResidueField fromSpecResidueField	—	—
range_fromSpecResidueField 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec residueField 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' fromSpecResidueField Set Set.instSingletonSet	—	AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier EuclideanDomain.toNontrivial fromSpecResidueField_apply
residueFieldCongr_fromSpecResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec residueField AlgebraicGeometry.Spec.map CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory residueFieldCongr fromSpecResidueField	—	AlgebraicGeometry.Spec.map_id CategoryTheory.Category.id_comp
residueFieldCongr_fromSpecResidueField_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec residueField AlgebraicGeometry.Spec.map CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory residueFieldCongr fromSpecResidueField	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' residueFieldCongr_fromSpecResidueField
residueFieldCongr_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory residueField residueFieldCongr CategoryTheory.Iso.hom TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace	—	—
residueFieldCongr_refl 📖	mathematical	—	residueFieldCongr refl TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv CategoryTheory.Iso.refl residueField	—	refl IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv
residueFieldCongr_symm 📖	mathematical	—	CategoryTheory.Iso.symm CommRingCat CommRingCat.instCategory residueField residueFieldCongr TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace	—	—
residueFieldCongr_trans 📖	mathematical	—	CategoryTheory.Iso.trans CommRingCat CommRingCat.instCategory residueField residueFieldCongr TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace	—	—
residueFieldCongr_trans_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory residueField CategoryTheory.Iso.hom residueFieldCongr TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace	—	—
residueFieldCongr_trans_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory residueField CategoryTheory.Iso.hom residueFieldCongr TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' residueFieldCongr_trans_hom
residueFieldMap_comp 📖	mathematical	—	Hom.residueFieldMap CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory CommRingCat CommRingCat.instCategory residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace 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.LocallyRingedSpace.residueFieldMap_comp
residueFieldMap_id 📖	mathematical	—	Hom.residueFieldMap CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory CommRingCat CommRingCat.instCategory residueField	—	AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_id
residue_descResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf residueField CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain residue descResidueField	—	CommRingCat.Colimits.hasColimits_commRingCat CommRingCat.hom_ext RingHom.ext
residue_descResidueField_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf residueField residue CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain descResidueField	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' residue_descResidueField
residue_residueFieldCongr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf residueField residue CategoryTheory.Iso.hom residueFieldCongr TopCat.Presheaf.stalkCongr Inseparable.of_eq TopCat.carrier TopCat.str	—	CommRingCat.Colimits.hasColimits_commRingCat Inseparable.of_eq CategoryTheory.Category.comp_id TopCat.Presheaf.stalkSpecializes_refl CategoryTheory.Category.id_comp
residue_residueFieldCongr_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf residueField residue CategoryTheory.Iso.hom residueFieldCongr TopCat.Presheaf.stalkCongr Inseparable.of_eq TopCat.carrier TopCat.str	—	CommRingCat.Colimits.hasColimits_commRingCat Inseparable.of_eq CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' residue_residueFieldCongr
residue_residueFieldMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace 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' residueField residue Hom.residueFieldMap Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap
residue_residueFieldMap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace 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' residueField residue Hom.residueFieldMap Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' residue_residueFieldMap
residue_surjective 📖	mathematical	—	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 residueField DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier residue	—	Ideal.Quotient.mk_surjective CommRingCat.Colimits.hasColimits_commRingCat
Γevaluation_naturality 📖	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 TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf 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 residueField DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' Γevaluation Hom.residueFieldMap Hom.appTop	—	AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality
Γevaluation_naturality_apply 📖	mathematical	—	DFunLike.coe residueField AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace 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' CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.residueFieldMap CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf 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 Γevaluation Hom.appTop	—	AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply
Γevaluation_naturality_assoc 📖	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 TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf 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 residueField DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' Γevaluation Hom.residueFieldMap Hom.appTop	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Γevaluation_naturality

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
residueFieldMap 📖	CompOp	24 math math: AlgebraicGeometry.Scheme.Pullback.Triplet.isPullback_SpecMap_tensor, SpecMap_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_map_tensor_isPullback, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, AlgebraicGeometry.Scheme.evaluation_naturality, AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType, AlgebraicGeometry.Scheme.evaluation_naturality_apply, residueFieldMap_congr, Spec_map_residueFieldMap_fromSpecResidueField_assoc, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.Scheme.evaluation_naturality_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, asFiberHom_fiberToSpecResidueField, AlgebraicGeometry.Scheme.Γevaluation_naturality, AlgebraicGeometry.Scheme.residueFieldMap_id, SpecMap_residueFieldMap_fromSpecResidueField, AlgebraicGeometry.Scheme.residueFieldMap_comp, Spec_map_residueFieldMap_fromSpecResidueField, asFiberHom_fiberToSpecResidueField_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_residueFieldMap_fromSpecResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' AlgebraicGeometry.Spec.map residueFieldMap AlgebraicGeometry.Scheme.fromSpecResidueField	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk AlgebraicGeometry.Spec.map_comp_assoc
SpecMap_residueFieldMap_fromSpecResidueField_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField DFunLike.coe ContinuousMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' AlgebraicGeometry.Spec.map residueFieldMap AlgebraicGeometry.Scheme.fromSpecResidueField	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' SpecMap_residueFieldMap_fromSpecResidueField
Spec_map_residueFieldMap_fromSpecResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' AlgebraicGeometry.Spec.map residueFieldMap AlgebraicGeometry.Scheme.fromSpecResidueField	—	SpecMap_residueFieldMap_fromSpecResidueField
Spec_map_residueFieldMap_fromSpecResidueField_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField DFunLike.coe ContinuousMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' AlgebraicGeometry.Spec.map residueFieldMap AlgebraicGeometry.Scheme.fromSpecResidueField	—	SpecMap_residueFieldMap_fromSpecResidueField_assoc
residueFieldMap_congr 📖	mathematical	—	residueFieldMap CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.Scheme.residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.residueFieldCongr	—	CategoryTheory.Category.id_comp

AlgebraicGeometry.Scheme.Spec

Definitions

Name	Category	Theorems
residueFieldIso 📖	CompOp	4 math math: residue_residueFieldIso_hom_assoc, algebraMap_residueFieldIso_inv, algebraMap_residueFieldIso_inv_assoc, residue_residueFieldIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_residueFieldIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CommRingCat.commRing Ideal.ResidueField PrimeSpectrum.asIdeal CommRing.toCommSemiring PrimeSpectrum.isPrime IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid AlgebraicGeometry.Scheme.residueField AlgebraicGeometry.Spec CommRingCat.ofHom algebraMap IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id CategoryTheory.Iso.inv residueFieldIso CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.Scheme.ΓSpecIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ AlgebraicGeometry.Scheme.residue	—	PrimeSpectrum.isPrime CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc
algebraMap_residueFieldIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CommRingCat.commRing Ideal.ResidueField PrimeSpectrum.asIdeal CommRing.toCommSemiring PrimeSpectrum.isPrime IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid CommRingCat.ofHom algebraMap IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id AlgebraicGeometry.Scheme.residueField AlgebraicGeometry.Spec CategoryTheory.Iso.inv residueFieldIso CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.Scheme.ΓSpecIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ AlgebraicGeometry.Scheme.residue	—	PrimeSpectrum.isPrime CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' algebraMap_residueFieldIso_inv
residue_residueFieldIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.residueField CommRingCat.of Ideal.ResidueField CommRingCat.carrier CommRingCat.commRing PrimeSpectrum.asIdeal CommRing.toCommSemiring PrimeSpectrum.isPrime IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid AlgebraicGeometry.Scheme.residue CategoryTheory.Iso.hom residueFieldIso AlgebraicGeometry.Spec.stalkIso CommRingCat.ofHom algebraMap OreLocalization.instCommSemiring IsLocalRing.ResidueField.algebra Algebra.id	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime
residue_residueFieldIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.residueField AlgebraicGeometry.Scheme.residue CommRingCat.of Ideal.ResidueField CommRingCat.carrier CommRingCat.commRing PrimeSpectrum.asIdeal CommRing.toCommSemiring PrimeSpectrum.isPrime IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid CategoryTheory.Iso.hom residueFieldIso AlgebraicGeometry.Spec.stalkIso CommRingCat.ofHom algebraMap OreLocalization.instCommSemiring IsLocalRing.ResidueField.algebra Algebra.id	—	PrimeSpectrum.isPrime CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' residue_residueFieldIso_hom

---

← Back to Index