Basic

📁 Source: Mathlib/RingTheory/Localization/AtPrime/Basic.lean

Statistics

Metric	Count
Definitions equivQuotMaximalIdeal, equivQuotientMapMaximalIdeal, orderIsoOfPrime, primeSpectrumOrderIso, instAlgebraOfLiesOver, mapPiEvalRingHom, localAlgHom, localRingHom, equivQuotMaximalIdealOfIsLocalization	9
Theorems of_isLocalization_of_disjoint, isPrime_map_of_isLocalizationAtPrime, under_map_of_isLocalizationAtPrime, coe_orderIsoOfPrime_apply_coe, coe_orderIsoOfPrime_symm_apply_coe, coe_primeSpectrumOrderIso_apply_coe_asIdeal, coe_primeSpectrumOrderIso_symm_apply_asIdeal, comap_map_eq_map, comap_map_of_isMaximal, comap_maximalIdeal, equivQuotMaximalIdeal_apply_mk, equivQuotMaximalIdeal_symm_apply_mk, faithfulSMul, isLocalRing, isMaximal_map, isPrime_map_of_liesOver, isUnit_mk'_iff, isUnit_to_map_iff, liesOver_maximalIdeal, map_eq_maximalIdeal, mk'_mem_maximal_iff, nontrivial, to_map_mem_maximal_iff, isDomain_of_atPrime, isDomain_of_local_atPrime, liesOver_of_isPrime_of_disjoint, subsingleton_primeSpectrum_of_mem_minimalPrimes, comap_maximalIdeal, eq_maximalIdeal_iff_comap_eq, instIsScalarTower, instIsScalarTower_1, isLocalRing, mapPiEvalRingHom_algebraMap_apply, mapPiEvalRingHom_bijective, mapPiEvalRingHom_comp_algebraMap, map_eq_maximalIdeal, instFaithfulSMulAtPrimeOfNoZeroDivisors, instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, isLocalHom_localRingHom, le_comap_primeCompl_iff, localAlgHom_apply, localRingHom_bijective_of_saturated_inf_eq_top, localRingHom_comp, localRingHom_id, localRingHom_mk', localRingHom_to_map, localRingHom_unique	47
Total	56

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrime_map_of_isLocalizationAtPrime 📖	mathematical	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	IsPrime map RingHom RingHom.instFunLike algebraMap	—	compl_compl instIsConcreteLE IsLocalization.isPrime_of_isPrime_disjoint
under_map_of_isLocalizationAtPrime 📖	mathematical	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	under map RingHom RingHom.instFunLike algebraMap	—	compl_compl instIsConcreteLE IsLocalization.comap_map_of_isPrime_disjoint

Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalization_of_disjoint 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring	—	RingHom.instRingHomClass Ideal.exists_le_maximal ne_top Ideal.comap_top IsLocalization.map_comap eq_of_le Ideal.IsPrime.ne_top Ideal.IsPrime.under isPrime' Ideal.comap_mono Ideal.under_def

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDomain_of_atPrime 📖	mathematical	—	IsDomain CommSemiring.toSemiring	—	isDomain_of_le_nonZeroDivisors Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors
isDomain_of_local_atPrime 📖	mathematical	—	IsDomain Localization.AtPrime CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid	—	isDomain_localization Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors
liesOver_of_isPrime_of_disjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid.instSetLike Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	Ideal.LiesOver Ideal.map RingHom RingHom.instFunLike algebraMap	—	Ideal.under_under RingHom.instRingHomClass Ideal.under_def comap_map_of_isPrime_disjoint Ideal.LiesOver.over map_comap
subsingleton_primeSpectrum_of_mem_minimalPrimes 📖	mathematical	Ideal CommSemiring.toSemiring Set Set.instMembership minimalPrimes	PrimeSpectrum	—	PrimeSpectrum.ext Minimal.eq_of_le minimalPrimes_eq_minimals PrimeSpectrum.isPrime Equiv.subsingleton Unique.instSubsingleton

IsLocalization.AtPrime

Definitions

Name	Category	Theorems
equivQuotMaximalIdeal 📖	CompOp	4 math math: equivQuotMaximalIdeal_apply_mk, algebraMap_equivQuotMaximalIdeal_symm_apply, trace_quotient_eq_trace_localization_quotient, equivQuotMaximalIdeal_symm_apply_mk
equivQuotientMapMaximalIdeal 📖	CompOp	1 math math: equivQuotientMapMaximalIdeal_apply_mk
orderIsoOfPrime 📖	CompOp	2 math math: coe_orderIsoOfPrime_apply_coe, coe_orderIsoOfPrime_symm_apply_coe
primeSpectrumOrderIso 📖	CompOp	2 math math: coe_primeSpectrumOrderIso_symm_apply_asIdeal, coe_primeSpectrumOrderIso_apply_coe_asIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_orderIsoOfPrime_apply_coe 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike Ideal Ideal.IsPrime Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder DFunLike.coe RelIso RelIso.instFunLike orderIsoOfPrime Set.preimage RingHom RingHom.instFunLike algebraMap	—	—
coe_orderIsoOfPrime_symm_apply_coe 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike Ideal Ideal.IsPrime DFunLike.coe RelIso Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder RelIso.instFunLike RelIso.symm orderIsoOfPrime Set.iInter Set Set.instHasSubset Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike Ideal.primeCompl OrderIso Set.instMembership instFunLikeOrderIso OrderIso.symm OrderIso.setCongr Set.preimage RingHom RingHom.instFunLike algebraMap	—	Set.iInter_congr_Prop
coe_primeSpectrumOrderIso_apply_coe_asIdeal 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike PrimeSpectrum.asIdeal PrimeSpectrum Set Set.instMembership Set.Iic PartialOrder.toPreorder PrimeSpectrum.instPartialOrder DFunLike.coe RelIso Set.Elem Preorder.toLE RelIso.instFunLike primeSpectrumOrderIso Set.preimage RingHom RingHom.instFunLike algebraMap Ideal	—	—
coe_primeSpectrumOrderIso_symm_apply_asIdeal 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike PrimeSpectrum.asIdeal DFunLike.coe RelIso Set.Elem PrimeSpectrum Set.Iic PartialOrder.toPreorder PrimeSpectrum.instPartialOrder Preorder.toLE Set Set.instMembership RelIso.instFunLike RelIso.symm primeSpectrumOrderIso Set.iInter Set.instHasSubset Ideal Ideal.IsPrime Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike Ideal.primeCompl OrderIso Submodule.instPartialOrder instFunLikeOrderIso OrderIso.symm OrderIso.setCongr Set.preimage RingHom RingHom.instFunLike algebraMap	—	Set.iInter_congr_Prop
comap_map_eq_map 📖	mathematical	—	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass Ideal.map	—	Ideal.IsMaximal.isPrime' RingHom.instRingHomClass IsScalarTower.algebraMap_eq Ideal.map_map LE.le.antisymm Ideal.le_comap_map IsLocalization.mem_map_algebraMap_iff IsLocalization.eq_iff_exists map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Subtype.prop Algebra.smul_def Submonoid.coe_mul mul_assoc mul_comm Ideal.mul_mem_left Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective Ideal.Quotient.eq_zero_iff_mem map_sub RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass inv_mul_cancel₀ sub_self add_sub_cancel Submodule.add_mem_iff_left Ideal.mul_mem_right Ideal.mem_map_of_mem one_smul add_smul smul_smul
comap_map_of_isMaximal 📖	mathematical	—	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass Ideal.map	—	Ideal.comap_map_eq_self_of_isMaximal Ideal.IsPrime.ne_top isPrime_map_of_liesOver Ideal.IsMaximal.isPrime'
comap_maximalIdeal 📖	mathematical	—	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass IsLocalRing.maximalIdeal	—	Ideal.ext RingHom.instRingHomClass to_map_mem_maximal_iff isLocalRing
equivQuotMaximalIdeal_apply_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 IsLocalRing.maximalIdeal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equivQuotMaximalIdeal RingHom Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike algebraMap	—	Ideal.IsMaximal.isPrime' Ideal.instIsTwoSided_1
equivQuotMaximalIdeal_symm_apply_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 IsLocalRing.maximalIdeal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equivQuotMaximalIdeal RingHom Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike IsLocalization.mk' Ideal.primeCompl Ideal.IsMaximal.isPrime' InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Ideal.Quotient.field Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Ideal.IsMaximal.isPrime' Ideal.instIsTwoSided_1 Ideal.mem_primeCompl_iff Subtype.prop RingEquiv.map_ne_zero_iff RingEquiv.symm_apply_eq mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Ideal.Quotient.isDomain IsLocalRing.maximalIdeal.isMaximal map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass RingEquiv.instRingEquivClass mul_assoc inv_mul_cancel₀ map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass mul_one RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass IsLocalization.mk'_spec Ideal.Quotient.mk_algebraMap
faithfulSMul 📖	mathematical	—	FaithfulSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring	—	faithfulSMul_iff_algebraMap_injective IsLocalization.injective_iff_isRegular IsRegular.of_ne_zero NoZeroDivisors.to_isCancelMulZero AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
isLocalRing 📖	mathematical	—	IsLocalRing CommSemiring.toSemiring	—	IsLocalRing.of_nonunits_add nontrivial isUnit_iff_exists_inv instIsDedekindFiniteMonoid not_imp_comm IsLocalization.mk'_mul_mk'_eq_one' IsLocalization.exists_mk'_eq Submonoid.one_mem IsLocalization.eq IsLocalization.mk'_self IsLocalization.mk'_mul IsLocalization.mk'_add one_mul mul_one Ideal.mul_mem_left Ideal.mul_mem_right Ideal.instIsTwoSided Ideal.add_mem Ideal.IsPrime.mem_or_mem
isMaximal_map 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	map_eq_maximalIdeal IsLocalRing.maximalIdeal.isMaximal
isPrime_map_of_liesOver 📖	mathematical	—	Ideal.IsPrime CommSemiring.toSemiring Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsLocalization.isPrime_of_isPrime_disjoint Ideal.disjoint_primeCompl_of_liesOver
isUnit_mk'_iff 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring IsLocalization.mk' Ideal.primeCompl Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike	—	isLocalRing IsLocalization.mk'_mem_iff to_map_mem_maximal_iff isUnit_iff_exists_inv instIsDedekindFiniteMonoid IsLocalization.mk'_mul_mk'_eq_one
isUnit_to_map_iff 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Ideal.primeCompl	—	Ideal.IsPrime.ne_top IsLocalization.isPrime_of_isPrime_disjoint disjoint_compl_left Ideal.eq_top_of_isUnit_mem Ideal.mem_map_of_mem IsLocalization.map_units
liesOver_maximalIdeal 📖	mathematical	—	Ideal.LiesOver CommSemiring.toSemiring IsLocalRing.maximalIdeal	—	Ideal.liesOver_iff RingHom.instRingHomClass isLocalRing comap_maximalIdeal
map_eq_maximalIdeal 📖	mathematical	—	Ideal.map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap IsLocalRing.maximalIdeal	—	RingHom.instRingHomClass isLocalRing IsLocalization.map_comap comap_maximalIdeal
mk'_mem_maximal_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal IsLocalization.mk' Ideal.primeCompl	—	not_iff_not isUnit_mk'_iff
nontrivial 📖	mathematical	—	Nontrivial	—	nontrivial_of_ne IsLocalization.eq_iff_exists RingHom.map_zero RingHom.map_one mul_one MulZeroClass.mul_zero Ideal.zero_mem
to_map_mem_maximal_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	not_iff_not isUnit_to_map_iff

Localization

Definitions

Name	Category	Theorems
localAlgHom 📖	CompOp	1 math math: localAlgHom_apply
localRingHom 📖	CompOp	25 math math: localRingHom_mk', AlgebraicGeometry.localRingHom_comp_stalkIso_apply, localRingHom_to_map, localRingHom_injective_of_primesOver_eq_singleton, AlgebraicGeometry.stalkwise_SpecMap_iff, AlgebraicGeometry.StructureSheaf.comap_apply, localRingHom_id, localAlgHom_apply, RingHom.surjective_localRingHom_of_surjective, RingHom.HoldsForLocalization.localRingHom, AlgebraicGeometry.stalkwise_Spec_map_iff, localRingHom_unique, RingHom.Flat.localRingHom, RingHom.SurjectiveOnStalks.localRingHom_surjective, localRingHom_bijective_of_saturated_inf_eq_top, localRingHom_comp, isLocalHom_localRingHom, localRingHom_bijective_of_not_conductor_le, localRingHom_surjective_of_primesOver_eq_singleton, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, RingHom.surjectiveOnStalks_iff_forall_maximal, AlgebraicGeometry.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, RingHom.surjective_localRingHom_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulSMulAtPrimeOfNoZeroDivisors 📖	mathematical	—	FaithfulSMul AtPrime CommRing.toCommSemiring OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right	—	IsLocalization.AtPrime.faithfulSMul isLocalization
instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain 📖	mathematical	—	Module.IsTorsionFree AtPrime CommRing.toCommSemiring Localization CommRing.toCommMonoid Algebra.algebraMapSubmonoid CommSemiring.toSemiring Ideal.primeCompl OreLocalization.instSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule Algebra.toModule OreLocalization.instCommSemiring instAlgebraLocalizationAlgebraMapSubmonoid	—	Module.IsTorsionFree.of_isLocalization IsLocalization.isDomain_of_local_atPrime OreLocalization.instIsScalarTower IsScalarTower.right instIsScalarTowerLocalizationAlgebraMapSubmonoid Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors isLocalization
isLocalHom_localRingHom 📖	mathematical	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass	IsLocalHom AtPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instMonoid CommMonoid.toMonoid localRingHom	—	RingHom.instRingHomClass isLocalization IsLocalization.exists_mk'_eq IsLocalization.AtPrime.isUnit_mk'_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass le_comap_primeCompl_iff ge_of_eq localRingHom_mk' SetLike.ext_iff
le_comap_primeCompl_iff 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Ideal.primeCompl Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Ideal Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Ideal.comap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Mathlib.Tactic.Contrapose.contrapose₁
localAlgHom_apply 📖	mathematical	Ideal.comap AlgHom CommSemiring.toSemiring AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass	DFunLike.coe AtPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instAlgebra localAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike localRingHom AlgHom.toRingHom	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
localRingHom_bijective_of_saturated_inf_eq_top 📖	mathematical	Subalgebra.saturation Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid.instMin Ideal.primeCompl Subsemiring.toSubmonoid Subalgebra.toSubsemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Function.Bijective AtPrime SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommSemiring DFunLike.coe RingHom OreLocalization.instSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike localRingHom algebraMap Subalgebra.toAlgebra Algebra.id Ideal.over_def	—	Ideal.over_def Eq.ge Set.mem_univ Ideal.IsPrime.mul_notMem mul_assoc isLocalization Ideal.primeCompl.congr_simp MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass le_comap_primeCompl_iff ge_of_eq Function.Surjective.forall IsLocalization.mk'_surjective localRingHom_mk' IsLocalization.eq_iff_exists MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass Submonoid.mul_mem Submonoid.instSubmonoidClass Submonoid.one_mem Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Function.Surjective.exists
localRingHom_comp 📖	mathematical	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass	localRingHom RingHom.comp AtPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid	—	RingHom.instRingHomClass localRingHom_unique localRingHom_to_map
localRingHom_id 📖	mathematical	—	localRingHom RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring Ideal Ideal.comap RingHom RingHom.instFunLike RingHom.instRingHomClass Ideal.comap_id AtPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid	—	localRingHom_unique RingHom.instRingHomClass Ideal.comap_id
localRingHom_mk' 📖	mathematical	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass	DFunLike.coe AtPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid localRingHom IsLocalization.mk' OreLocalization.instCommSemiring OreLocalization.instAlgebra Algebra.id isLocalization Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Ideal Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule le_comap_primeCompl_iff ge_of_eq	—	RingHom.instRingHomClass IsLocalization.map_mk'
localRingHom_to_map 📖	mathematical	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass	DFunLike.coe AtPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid localRingHom algebraMap OreLocalization.instAlgebra Algebra.id	—	RingHom.instRingHomClass IsLocalization.map_eq
localRingHom_unique 📖	mathematical	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass DFunLike.coe AtPrime OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid algebraMap OreLocalization.instAlgebra Algebra.id	localRingHom	—	RingHom.instRingHomClass IsLocalization.map_unique

Localization.AtPrime

Definitions

Name	Category	Theorems
instAlgebraOfLiesOver 📖	CompOp	22 math math: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, instIsAlgebraicResidueFieldOfIsIntegral, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, Algebra.WeaklyQuasiFiniteAt.finite_residueField, instIsLocalHomAtPrimeRingHomAlgebraMap, instEssFiniteTypeResidueField_1, Ideal.Fiber.lift_residueField_surjective, instIsSeparableResidueFieldOfQuotientIdeal, Algebra.QuasiFinite.instFiniteResidueField, Algebra.isUnramifiedAt_iff_map_eq, Localization.finite_of_primesOver_eq_singleton, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt, instFlatAtPrime, instIsScalarTower_1, instIsScalarTower, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAt, Polynomial.residueFieldMapCAlgEquiv_symm_X, Algebra.isSeparable_residueField_iff, Polynomial.residueFieldMapCAlgEquiv_algebraMap, Polynomial.residueFieldMapCAlgEquiv_symm_C
mapPiEvalRingHom 📖	CompOp	3 math math: mapPiEvalRingHom_bijective, mapPiEvalRingHom_comp_algebraMap, mapPiEvalRingHom_algebraMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_maximalIdeal 📖	mathematical	—	Ideal.comap Localization CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring RingHom Localization.AtPrime Semiring.toNonAssocSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instCommSemiring RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id RingHom.instRingHomClass IsLocalRing.maximalIdeal isLocalRing	—	IsLocalization.AtPrime.comap_maximalIdeal Localization.isLocalization IsLocalization.AtPrime.isLocalRing
eq_maximalIdeal_iff_comap_eq 📖	mathematical	—	Ideal.comap Localization.AtPrime RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id RingHom.instRingHomClass IsLocalRing.maximalIdeal OreLocalization.instCommSemiring isLocalRing	—	RingHom.instRingHomClass isLocalRing le_antisymm IsLocalRing.le_maximalIdeal Ideal.IsPrime.ne_top Ideal.map_comap_le comap_maximalIdeal
instIsScalarTower 📖	mathematical	—	IsScalarTower Localization.AtPrime CommRing.toCommSemiring OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul IsScalarTower.right OreLocalization.instCommSemiring OreLocalization.instSemiring instAlgebraOfLiesOver	—	IsScalarTower.of_algebraMap_eq IsScalarTower.algebraMap_apply OreLocalization.instIsScalarTower IsScalarTower.right Localization.localRingHom_to_map
instIsScalarTower_1 📖	mathematical	—	IsScalarTower Localization.AtPrime CommRing.toCommSemiring Algebra.toSMul OreLocalization.instCommSemiring Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instSemiring instAlgebraOfLiesOver	—	IsScalarTower.of_algebraMap_eq' RingHom.instRingHomClass Localization.localRingHom.congr_simp
isLocalRing 📖	mathematical	—	IsLocalRing Localization CommSemiring.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm	—	IsLocalization.AtPrime.isLocalRing Localization.isLocalization
mapPiEvalRingHom_algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom Localization.AtPrime Pi.commSemiring Ideal.comap Pi.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Pi.evalRingHom RingHom.instRingHomClass Ideal.IsPrime.comap OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid mapPiEvalRingHom algebraMap OreLocalization.instAlgebra Algebra.id	—	Localization.localRingHom_to_map
mapPiEvalRingHom_bijective 📖	mathematical	—	Function.Bijective Localization.AtPrime Pi.commSemiring Ideal.comap RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Pi.evalRingHom RingHom.instRingHomClass Ideal.IsPrime.comap DFunLike.coe OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid mapPiEvalRingHom	—	Localization.mapPiEvalRingHom_bijective
mapPiEvalRingHom_comp_algebraMap 📖	mathematical	—	RingHom.comp Localization.AtPrime Pi.commSemiring Ideal.comap RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Pi.evalRingHom RingHom.instRingHomClass Ideal.IsPrime.comap OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid mapPiEvalRingHom algebraMap OreLocalization.instAlgebra Algebra.id	—	IsLocalization.map_comp RingHom.instRingHomClass Ideal.IsPrime.comap
map_eq_maximalIdeal 📖	mathematical	—	Ideal.map Localization.AtPrime RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id IsLocalRing.maximalIdeal Localization OreLocalization.instCommSemiring isLocalRing	—	isLocalRing RingHom.instRingHomClass IsLocalization.map_comap Localization.isLocalization comap_maximalIdeal

(root)

Definitions

Name	Category	Theorems
equivQuotMaximalIdealOfIsLocalization 📖	CompOp	—

---

← Back to Index