ResidueField

📁 Source: Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean

Statistics

Metric	Count
Definitions evaluation, instFieldCarrierResidueField, residueField, residueFieldMap, Γevaluation, ResidueField, ResidueField, ResidueField	8
Theorems basicOpen_eq_bot_iff_forall_evaluation_eq_zero, evaluation_eq_zero_iff_notMem_basicOpen, evaluation_naturality, evaluation_naturality_apply, evaluation_naturality_assoc, evaluation_ne_zero_iff_mem_basicOpen, residueFieldMap_comp, residueFieldMap_id, residue_comp_residueFieldMap_eq_stalkMap_comp_residue, Γevaluation_eq_zero_iff_notMem_basicOpen, Γevaluation_naturality, Γevaluation_naturality_apply, Γevaluation_naturality_assoc, Γevaluation_ne_zero_iff_mem_basicOpen	14
Total	22

AlgebraicGeometry.LocallyRingedSpace

Definitions

Name	Category	Theorems
evaluation 📖	CompOp	5 math math: basicOpen_eq_bot_iff_forall_evaluation_eq_zero, evaluation_naturality, evaluation_naturality_assoc, evaluation_eq_zero_iff_notMem_basicOpen, evaluation_naturality_apply
instFieldCarrierResidueField 📖	CompOp	—
residueField 📖	CompOp	12 math math: residueFieldMap_comp, basicOpen_eq_bot_iff_forall_evaluation_eq_zero, residue_comp_residueFieldMap_eq_stalkMap_comp_residue, Γevaluation_naturality_apply, evaluation_naturality, Γevaluation_naturality_assoc, Γevaluation_eq_zero_iff_notMem_basicOpen, residueFieldMap_id, Γevaluation_naturality, evaluation_naturality_assoc, evaluation_eq_zero_iff_notMem_basicOpen, evaluation_naturality_apply
residueFieldMap 📖	CompOp	9 math math: residueFieldMap_comp, residue_comp_residueFieldMap_eq_stalkMap_comp_residue, Γevaluation_naturality_apply, evaluation_naturality, Γevaluation_naturality_assoc, residueFieldMap_id, Γevaluation_naturality, evaluation_naturality_assoc, evaluation_naturality_apply
Γevaluation 📖	CompOp	4 math math: Γevaluation_naturality_apply, Γevaluation_naturality_assoc, Γevaluation_eq_zero_iff_notMem_basicOpen, Γevaluation_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basicOpen_eq_bot_iff_forall_evaluation_eq_zero 📖	mathematical	—	AlgebraicGeometry.RingedSpace.basicOpen toRingedSpace Bot.bot TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot DFunLike.coe CategoryTheory.Functor.obj Opposite toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op residueField toTopCat 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	—	eq_bot_iff AlgebraicGeometry.RingedSpace.basicOpen_le
evaluation_eq_zero_iff_notMem_basicOpen 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op residueField toTopCat 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 toRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.RingedSpace.basicOpen	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.RingedSpace.mem_basicOpen not_iff_not IsLocalRing.residue_ne_zero_iff_isUnit
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 toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op residueField toTopCat SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom TopologicalSpace.Opens.map evaluation residueFieldMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	CommRingCat.Colimits.hasColimits_commRingCat instIsLocalRingCarrierStalkCommRingCatPresheaf isLocalHomValStalkMap CategoryTheory.Category.assoc CommRingCat.hom_ext RingHom.ext CommRingCat.comp_apply IsLocalRing.ResidueField.map_residue stalkMap_germ_apply
evaluation_naturality_apply 📖	mathematical	—	DFunLike.coe residueField AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier residueFieldMap Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op toTopCat evaluation TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	evaluation_naturality
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 toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op residueField DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom SetLike.instMembership TopologicalSpace.Opens.instSetLike TopologicalSpace.Opens.map evaluation toTopCat residueFieldMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' evaluation_naturality
evaluation_ne_zero_iff_mem_basicOpen 📖	mathematical	—	TopCat.carrier toTopCat TopologicalSpace.Opens AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.RingedSpace.basicOpen TopCat.str	—	—
residueFieldMap_comp 📖	mathematical	—	residueFieldMap CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory CommRingCat CommRingCat.instCategory residueField DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom	—	CommRingCat.hom_ext CommRingCat.Colimits.hasColimits_commRingCat instIsLocalRingCarrierStalkCommRingCatPresheaf isLocalHomValStalkMap stalkMap_comp IsLocalRing.ResidueField.map.congr_simp IsLocalRing.ResidueField.map_comp
residueFieldMap_id 📖	mathematical	—	residueFieldMap CategoryTheory.CategoryStruct.id AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct instCategory CommRingCat CommRingCat.instCategory residueField	—	CommRingCat.hom_ext CommRingCat.Colimits.hasColimits_commRingCat instIsLocalRingCarrierStalkCommRingCatPresheaf isLocalHomValStalkMap stalkMap_id IsLocalRing.ResidueField.map.congr_simp IsLocalRing.ResidueField.map_id
residue_comp_residueFieldMap_eq_stalkMap_comp_residue 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CommRingCat.commRing IsLocalRing.ResidueField instIsLocalRingCarrierStalkCommRingCatPresheaf IsLocalRing.instCommRingResidueField residueField CommRingCat.ofHom IsLocalRing.residue residueFieldMap Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat instIsLocalRingCarrierStalkCommRingCatPresheaf CategoryTheory.Limits.hasColimitOfHasColimitsOfShape isLocalHomValStalkMap
Γevaluation_eq_zero_iff_notMem_basicOpen 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace 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 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 toTopCat toRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.RingedSpace.basicOpen	—	evaluation_eq_zero_iff_notMem_basicOpen
Γ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 toSheafedSpace 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 residueField DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Γevaluation residueFieldMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	evaluation_naturality
Γevaluation_naturality_apply 📖	mathematical	—	DFunLike.coe residueField AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom CommRingCat.carrier RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier residueFieldMap CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens 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 Γevaluation TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	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 toSheafedSpace 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 residueField DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom Γevaluation residueFieldMap TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Γevaluation_naturality
Γevaluation_ne_zero_iff_mem_basicOpen 📖	mathematical	—	TopCat.carrier toTopCat TopologicalSpace.Opens AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.RingedSpace.basicOpen Top.top toSheafedSpace TopCat.str OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	evaluation_ne_zero_iff_mem_basicOpen

Ideal

Definitions

Name	Category	Theorems
ResidueField 📖	CompOp	69 math math: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.residueField_specComap, exists_mem_span_singleton_map_residueField_eq, ker_algebraMap_residueField, Polynomial.fiberEquivQuotient_tmul, Module.rankAtStalk_eq, instLiesOverFiberOfIsPrime, instIsAlgebraicResidueFieldOfIsIntegral, algebraMap_quotient_residueField_mk, Algebra.QuasiFinite.instResidueField, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, Algebra.WeaklyQuasiFiniteAt.finite_residueField, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, instEssFiniteTypeResidueField_1, Fiber.lift_residueField_surjective, algebraMap_residueField_surjective, ResidueField.ringHom_ext_iff, instIsSeparableResidueFieldOfQuotientIdeal, surjectiveOnStalks_residueField, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, PrimeSpectrum.mem_image_comap_basicOpen, ResidueField.liftₐ_comp_toAlgHom, instIsAlgebraicQuotientIdealResidueField, Algebra.QuasiFinite.finite_fiber, Algebra.QuasiFinite.instFiniteResidueField, ResidueField.map_algebraMap, algebraMap_mk, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, ResidueField.exists_smul_eq_tmul_one, Algebra.isUnramifiedAt_iff_map_eq, PrimeSpectrum.residueField_comap, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, RingHom.SurjectiveOnStalks.residueFieldMap_bijective, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt, instLiesOverResidueFieldBotIdeal, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, instEssFiniteTypeResidueField, ResidueField.algHom_ext_iff, ResidueField.lift_algebraMap, isNilpotent_tensor_residueField_iff, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, Module.mem_support_iff_nontrivial_residueField_tensorProduct, instFiniteResidueField, injective_algebraMap_quotient_residueField, instIsScalarTowerQuotientIdealResidueField, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Polynomial.residueFieldMapCAlgEquiv_symm_X, Algebra.isSeparable_residueField_iff, algebraMap_residueField_eq_zero, bijective_algebraMap_quotient_residueField, ResidueField.liftₐ_algebraMap, Algebra.QuasiFinite.instIsArtinianRingFiber, Polynomial.residueFieldMapCAlgEquiv_algebraMap, Fiber.exists_smul_eq_one_tmul, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, ResidueField.mapₐ_apply, PrimeSpectrum.nontrivial_iff_mem_rangeComap, Polynomial.residueFieldMapCAlgEquiv_symm_C, instIsFractionRingQuotientIdealResidueField

IsLocalRing

Definitions

Name	Category	Theorems
ResidueField 📖	CompOp	75 math math: Algebra.instIsSeparableResidueFieldOfFormallyUnramified, ValuationSubring.coe_mem_principalUnitGroup_iff, ResidueField.algebraMap_residue, finrank_CotangentSpace_eq_one_iff, ker_residue, Polynomial.fiberEquivQuotient_tmul, Module.rankAtStalk_eq, finrank_cotangentSpace_eq_zero, PowerSeries.degree_weierstrassMod_lt, ResidueField.finite_of_finite, ResidueField.map_comp, instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap, RingHom.EssFiniteType.residueFieldMap, residue_eq_zero_iff, Algebra.IsUnramifiedAt.residueField, Algebra.FormallyUnramified.iff_map_maximalIdeal_eq, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, instIsLocalHomResidueFieldRingHomResidue, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Ideal.Fiber.lift_residueField_surjective, finrank_CotangentSpace_eq_one, finrank_cotangentSpace_eq_zero_iff, Algebra.instFiniteResidueFieldOfFormallyUnramified, map_tensorProduct_mk_eq_top, residue_def, ResidueField.map_comp_residue, Algebra.instFormallyUnramifiedResidueField_1, ResidueField.instIsScalarTower_1, ResidueField.mapEquiv_refl, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, finite_residueField_of_compactSpace, ResidueField.lift_comp_residue, PowerSeries.IsWeierstrassFactorization.natDegree_eq_toNat_order_map, instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing, Algebra.QuasiFinite.finite_fiber, ResidueField.mapEquiv_apply, ResidueField.map_map, ResidueField.map_residue, PrimeSpectrum.comap_residue, IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation, tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, ResidueField.map_id, PadicInt.toZMod_eq_residueField_comp_residue, ResidueField.map_id_apply, split_injective_iff_lTensor_residueField_injective, ResidueField.algebraMap_eq, finrank_cotangentSpace_le_one_iff, instIsScalarTowerResidueFieldCotangentSpace, ValuationSubring.surjective_unitGroupToResidueFieldUnits, ResidueField.mapEquiv_trans, ValuationSubring.principalUnitGroupEquiv_apply, ResidueField.finite_of_module_finite, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, isLocalHom_residue, IsDiscreteValuationRing.TFAE, ResidueField.mapAut_apply, ResidueField.instIsScalarTower, instIsScalarTowerQuotientIdealResidueField, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, CotangentSpace.span_image_eq_top_iff, ResidueField.residue_smul, subsingleton_tensorProduct, instFiniteResidueField, ValuationSubring.ker_unitGroupToResidueFieldUnits, WeierstrassCurve.isGoodReduction_iff_isElliptic_reduction, instIsScalarTowerResidueField, ResidueField.lift_residue_apply, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap, residue_surjective, ValuationSubring.principalUnitGroup_symm_apply, ResidueField.mapEquiv.symm, Algebra.instFormallyUnramifiedResidueField

Valued

Definitions

Name	Category	Theorems
ResidueField 📖	CompOp	3 math math: integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, integer.totallyBounded_iff_finite_residueField

---

← Back to Index