Basic

📁 Source: Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

Statistics

Metric	Count
Definitions algebra, instAlgebra, instMulSemiringAction, map, mapAut, mapEquiv	6
Theorems algebraMap_eq, algebraMap_residue, finite_of_finite, finite_of_module_finite, instIsScalarTower, instIsScalarTower_1, instLiesOverMaximalIdeal, lift_comp_residue, lift_residue_apply, mapAut_apply, mapEquiv_apply, mapEquiv_refl, mapEquiv_trans, map_comp, map_comp_residue, map_id, map_id_apply, map_map, map_residue, residue_smul, instFiniteResidueField, instIsLocalHomResidueFieldRingHomResidue, instIsScalarTowerResidueField, isLocalHom_residue, ker_residue, residue_def, residue_eq_zero_iff, residue_ne_zero_iff_isUnit, residue_surjective	29
Total	35

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteResidueField 📖	mathematical	—	Module.Finite ResidueField CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingResidueField Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field ResidueField.algebra	—	Module.Finite.of_surjective RingHomSurjective.ids instIsScalarTowerResidueField IsScalarTower.right Ideal.Quotient.mk_surjective Ideal.instIsTwoSided_1
instIsLocalHomResidueFieldRingHomResidue 📖	mathematical	—	IsLocalHom ResidueField RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike residue	—	Iff.not Ideal.Quotient.eq_zero_iff_mem isUnit_iff_ne_zero
instIsScalarTowerResidueField 📖	mathematical	—	IsScalarTower ResidueField Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field ResidueField.algebra	—	Ideal.Quotient.isScalarTower
isLocalHom_residue 📖	mathematical	—	IsLocalHom ResidueField RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike residue	—	instIsLocalHomResidueFieldRingHomResidue
ker_residue 📖	mathematical	—	RingHom.ker ResidueField RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field RingHom.instFunLike RingHom.instRingHomClass residue maximalIdeal	—	Ideal.mk_ker
residue_def 📖	mathematical	—	DFunLike.coe RingHom ResidueField Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field RingHom.instFunLike residue HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient maximalIdeal Ideal.Quotient.ring Ideal.instIsTwoSided_1	—	—
residue_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom ResidueField Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field RingHom.instFunLike residue MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingResidueField Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule maximalIdeal	—	RingHom.instRingHomClass RingHom.mem_ker ker_residue
residue_ne_zero_iff_isUnit 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
residue_surjective 📖	mathematical	—	ResidueField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ResidueField.field RingHom.instFunLike residue	—	Ideal.Quotient.mk_surjective

IsLocalRing.ResidueField

Definitions

Name	Category	Theorems
algebra 📖	CompOp	64 math math: PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.residueField_specComap, Ideal.exists_mem_span_singleton_map_residueField_eq, Ideal.ker_algebraMap_residueField, Polynomial.fiberEquivQuotient_tmul, Module.rankAtStalk_eq, instLiesOverFiberOfIsPrime, Ideal.algebraMap_quotient_residueField_mk, Algebra.QuasiFinite.instResidueField, instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Ideal.Fiber.lift_residueField_surjective, Ideal.algebraMap_residueField_surjective, IsLocalRing.map_tensorProduct_mk_eq_top, Ideal.ResidueField.ringHom_ext_iff, Ideal.surjectiveOnStalks_residueField, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, PrimeSpectrum.mem_image_comap_basicOpen, Ideal.ResidueField.liftₐ_comp_toAlgHom, Algebra.QuasiFinite.finite_fiber, Ideal.ResidueField.map_algebraMap, algebraMap_mk, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, Ideal.ResidueField.exists_smul_eq_tmul_one, PrimeSpectrum.residueField_comap, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, instLiesOverResidueFieldBotIdeal, IsLocalRing.split_injective_iff_lTensor_residueField_injective, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, algebraMap_eq, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace, instEssFiniteTypeResidueField, Ideal.ResidueField.algHom_ext_iff, Ideal.ResidueField.lift_algebraMap, isNilpotent_tensor_residueField_iff, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, Module.mem_support_iff_nontrivial_residueField_tensorProduct, instFiniteResidueField, instIsScalarTower, 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, IsLocalRing.subsingleton_tensorProduct, IsLocalRing.instFiniteResidueField, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Polynomial.residueFieldMapCAlgEquiv_symm_X, Ideal.algebraMap_residueField_eq_zero, Ideal.ResidueField.liftₐ_algebraMap, Algebra.QuasiFinite.instIsArtinianRingFiber, IsLocalRing.instIsScalarTowerResidueField, Polynomial.residueFieldMapCAlgEquiv_algebraMap, Ideal.Fiber.exists_smul_eq_one_tmul, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, Ideal.ResidueField.mapₐ_apply, PrimeSpectrum.nontrivial_iff_mem_rangeComap, Algebra.instFormallyUnramifiedResidueField
instAlgebra 📖	CompOp	25 math math: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, Algebra.instIsSeparableResidueFieldOfFormallyUnramified, algebraMap_residue, instIsAlgebraicResidueFieldOfIsIntegral, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, Algebra.WeaklyQuasiFiniteAt.finite_residueField, Algebra.FormallyUnramified.iff_map_maximalIdeal_eq, instEssFiniteTypeResidueField_1, Ideal.Fiber.lift_residueField_surjective, Algebra.instFiniteResidueFieldOfFormallyUnramified, Algebra.instFormallyUnramifiedResidueField_1, instIsSeparableResidueFieldOfQuotientIdeal, instIsScalarTower_1, Algebra.QuasiFinite.instFiniteResidueField, Algebra.isUnramifiedAt_iff_map_eq, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt, finite_of_module_finite, instIsScalarTower, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, Polynomial.residueFieldMapCAlgEquiv_symm_X, Algebra.isSeparable_residueField_iff, Polynomial.residueFieldMapCAlgEquiv_algebraMap, Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap, Polynomial.residueFieldMapCAlgEquiv_symm_C
instMulSemiringAction 📖	CompOp	1 math math: residue_smul
map 📖	CompOp	8 math math: map_comp, RingHom.EssFiniteType.residueFieldMap, map_comp_residue, mapEquiv_apply, map_map, map_residue, map_id, map_id_apply
mapAut 📖	CompOp	1 math math: mapAut_apply
mapEquiv 📖	CompOp	5 math math: mapEquiv_refl, mapEquiv_apply, mapEquiv_trans, mapAut_apply, mapEquiv.symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_eq 📖	mathematical	—	algebraMap IsLocalRing.ResidueField CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field algebra Algebra.id IsLocalRing.residue	—	—
algebraMap_residue 📖	mathematical	—	DFunLike.coe RingHom IsLocalRing.ResidueField Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield field DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap instAlgebra CommRing.toCommSemiring IsLocalRing.residue	—	—
finite_of_finite 📖	mathematical	—	Finite IsLocalRing.ResidueField	—	Module.finite_of_finite finite_of_module_finite
finite_of_module_finite 📖	mathematical	—	Module.Finite IsLocalRing.ResidueField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Algebra.toModule Semifield.toCommSemiring instAlgebra	—	Module.Finite.of_restrictScalars_finite instIsScalarTower IsScalarTower.left IsLocalRing.instFiniteResidueField
instIsScalarTower 📖	mathematical	—	IsScalarTower IsLocalRing.ResidueField Algebra.toSMul CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field algebra Semifield.toCommSemiring instAlgebra	—	Ideal.Quotient.isScalarTower_of_liesOver instLiesOverMaximalIdeal
instIsScalarTower_1 📖	mathematical	—	IsScalarTower IsLocalRing.ResidueField Algebra.toSMul Semifield.toCommSemiring Field.toSemifield field DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebra	—	IsScalarTower.of_algebraMap_eq IsLocalRing.residue_surjective
instLiesOverMaximalIdeal 📖	mathematical	—	Ideal.LiesOver CommRing.toCommSemiring CommSemiring.toSemiring IsLocalRing.maximalIdeal	—	RingHom.instRingHomClass List.TFAE.out IsLocalRing.local_hom_TFAE
lift_comp_residue 📖	mathematical	—	RingHom.comp IsLocalRing.ResidueField Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field lift IsLocalRing.residue	—	RingHom.ext
lift_residue_apply 📖	mathematical	—	DFunLike.coe RingHom IsLocalRing.ResidueField Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field RingHom.instFunLike lift CommSemiring.toSemiring CommRing.toCommSemiring IsLocalRing.residue	—	—
mapAut_apply 📖	mathematical	—	DFunLike.coe MonoidHom RingAut Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd IsLocalRing.ResidueField IsLocalRing.instCommRingResidueField MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup MonoidHom.instFunLike mapAut mapEquiv	—	—
mapEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv IsLocalRing.ResidueField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike mapEquiv RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field RingHom.instFunLike map RingHomClass.toRingHom CommSemiring.toSemiring CommRing.toCommSemiring	—	—
mapEquiv_refl 📖	mathematical	—	mapEquiv RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd IsLocalRing.ResidueField IsLocalRing.instCommRingResidueField	—	RingEquiv.toRingHom_injective map_id
mapEquiv_trans 📖	mathematical	—	mapEquiv RingEquiv.trans Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd IsLocalRing.ResidueField IsLocalRing.instCommRingResidueField	—	RingEquiv.toRingHom_injective map_comp RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass isLocalHom_toRingHom isLocalHom_equiv RingEquivClass.toMulEquivClass
map_comp 📖	mathematical	—	map RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.isLocalHom_comp IsLocalRing.ResidueField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field	—	Ideal.Quotient.ringHom_ext Ideal.instIsTwoSided_1 RingHom.isLocalHom_comp RingHom.ext
map_comp_residue 📖	mathematical	—	RingHom.comp IsLocalRing.ResidueField Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field map IsLocalRing.residue	—	—
map_id 📖	mathematical	—	map RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring isLocalHom_id IsLocalRing.ResidueField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field	—	Ideal.Quotient.ringHom_ext Ideal.instIsTwoSided_1 isLocalHom_id RingHom.ext
map_id_apply 📖	mathematical	—	DFunLike.coe RingHom IsLocalRing.ResidueField Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field RingHom.instFunLike map RingHom.id CommSemiring.toSemiring CommRing.toCommSemiring isLocalHom_id	—	DFunLike.congr_fun isLocalHom_id map_id
map_map 📖	mathematical	—	DFunLike.coe RingHom IsLocalRing.ResidueField Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field RingHom.instFunLike map RingHom.comp CommSemiring.toSemiring CommRing.toCommSemiring RingHom.isLocalHom_comp	—	DFunLike.congr_fun RingHom.isLocalHom_comp map_comp
map_residue 📖	mathematical	—	DFunLike.coe RingHom IsLocalRing.ResidueField Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field RingHom.instFunLike map CommSemiring.toSemiring CommRing.toCommSemiring IsLocalRing.residue	—	—
residue_smul 📖	mathematical	—	DFunLike.coe RingHom IsLocalRing.ResidueField Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield field RingHom.instFunLike IsLocalRing.residue SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Ring.toSemiring MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero instSMulZeroClass MulSemiringAction.toMulDistribMulAction instMulSemiringAction	—	—

---

← Back to Index