Basic

📁 Source: Mathlib/RingTheory/LocalProperties/Basic.lean

Statistics

Metric	Count
Definitions LocalizationPreserves, OfLocalizationMaximal, ContainsIdentities, HoldsForLocalization, HoldsForLocalizationAway, LocalizationAwayPreserves, LocalizationPreserves, OfLocalizationFiniteSpan, OfLocalizationFiniteSpanTarget, OfLocalizationPrime, OfLocalizationSpan, OfLocalizationSpanTarget, PropertyIsLocal, StableUnderCompositionWithLocalizationAway, StableUnderCompositionWithLocalizationAwaySource, StableUnderCompositionWithLocalizationAwayTarget	16
Theorems idealMap_eq_ofEq_comp_toLocalized₀, eq_of_localization_maximal, le_of_localization_maximal, localized'_eq_map, localized₀_eq_restrictScalars_map, mem_of_localization_maximal, holdsForLocalizationAway, isLocalizationMap, localRingHom, mk, containsIdentities, of_bijective, isLocalization_map, localizationPreserves, of_isLocalization, and, respectsIso, away, and, mk, ofIsLocalization, ofIsLocalization', and, ofIsLocalization, ofLocalizationSpan, HoldsForLocalizationAway, StableUnderCompositionWithLocalizationAwayTarget, and, localizationAwayPreserves, ofLocalizationSpan, ofLocalizationSpanTarget, respectsIso, stableUnderCompositionWithLocalizationAway, respectsIso, and, ofLocalizationSpanTarget_iff_finite, ofLocalizationSpan_iff_finite, eq_zero_of_localization, ideal_eq_bot_of_localization, ideal_eq_bot_of_localization'	40
Total	56

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealMap_eq_ofEq_comp_toLocalized₀ 📖	mathematical	—	idealMap CommSemiring.toSemiring LinearMap.comp Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike toModule Submodule.localized₀ linearMap instIsLocalizedModuleLinearMapOfIsLocalization Submodule.restrictScalars toSMul IsScalarTower.right Ideal.map RingHom RingHom.instFunLike algebraMap Submodule.addCommMonoid Submodule.module RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.ofEq Ideal.localized₀_eq_restrictScalars_map Submodule.toLocalized₀	—	IsScalarTower.right

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_localization_maximal 📖	—	map Localization.AtPrime IsMaximal.isPrime' RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	—	IsMaximal.isPrime' le_antisymm le_of_localization_maximal Eq.le Eq.ge
le_of_localization_maximal 📖	—	Ideal Localization.AtPrime IsMaximal.isPrime' OreLocalization.instSemiring CommSemiring.toSemiring primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	—	IsMaximal.isPrime' mem_of_localization_maximal mem_map_of_mem
localized'_eq_map 📖	mathematical	—	Submodule.localized' NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule IsScalarTower.right Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization map RingHom RingHom.instFunLike algebraMap	—	IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization map.eq_1 span.eq_1 Submodule.localized'_eq_span Algebra.coe_linearMap
localized₀_eq_restrictScalars_map 📖	mathematical	—	Submodule.localized₀ NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization Submodule.restrictScalars Algebra.toSMul IsScalarTower.right map RingHom RingHom.instFunLike algebraMap	—	instIsLocalizedModuleLinearMapOfIsLocalization IsScalarTower.right localized'_eq_map
mem_of_localization_maximal 📖	—	Localization.AtPrime IsMaximal.isPrime' Ideal OreLocalization.instSemiring CommSemiring.toSemiring primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id DFunLike.coe	—	—	IsMaximal.isPrime' Submodule.mem_of_localization_maximal IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization Localization.isLocalization localized'_eq_map

RingHom

Definitions

Name	Category	Theorems
ContainsIdentities 📖	MathDef	6 math math: HoldsForLocalizationAway.containsIdentities, Bijective.containsIdentities, IsStandardOpenImmersion.containsIdentities, finite_containsIdentities, Flat.containsIdentities, Etale.containsIdentities
HoldsForLocalization 📖	MathDef	3 math math: FormallyUnramified.holdsForLocalization, EssFiniteType.holdsForLocalization, HoldsForLocalization.mk
HoldsForLocalizationAway 📖	MathDef	12 math math: PropertyIsLocal.HoldsForLocalizationAway, finiteType_holdsForLocalizationAway, QuasiFinite.holdsForLocalizationAway, Smooth.holdsForLocalizationAway, IsStandardOpenImmersion.holdsForLocalizationAway, isStandardSmooth_holdsForLocalizationAway, isStandardSmoothOfRelativeDimension_holdsForLocalizationAway, HoldsForLocalization.holdsForLocalizationAway, FormallySmooth.holdsForLocalizationAway, Flat.holdsForLocalizationAway, FormallyUnramified.holdsForLocalizationAway, finitePresentation_holdsForLocalizationAway
LocalizationAwayPreserves 📖	MathDef	2 math math: PropertyIsLocal.localizationAwayPreserves, LocalizationPreserves.away
LocalizationPreserves 📖	MathDef	8 math math: isStandardSmoothOfRelativeDimension_localizationPreserves, FormallySmooth.localizationPreserves, finite_localizationPreserves, isStandardSmooth_localizationPreserves, IsStableUnderBaseChange.localizationPreserves, finitePresentation_localizationPreserves, surjective_localizationPreserves, finiteType_localizationPreserves
OfLocalizationFiniteSpan 📖	MathDef	1 math math: ofLocalizationSpan_iff_finite
OfLocalizationFiniteSpanTarget 📖	MathDef	1 math math: ofLocalizationSpanTarget_iff_finite
OfLocalizationPrime 📖	MathDef	2 math math: FormallyUnramified.ofLocalizationPrime, Flat.ofLocalizationPrime
OfLocalizationSpan 📖	MathDef	10 math math: OfLocalizationSpan.mk, Bijective.ofLocalizationSpan, isIntegral_ofLocalizationSpan, finiteType_ofLocalizationSpan, Etale.ofLocalizationSpan, OfLocalizationSpanTarget.ofLocalizationSpan, ofLocalizationSpan_iff_finite, finite_ofLocalizationSpan, PropertyIsLocal.ofLocalizationSpan, surjective_ofLocalizationSpan
OfLocalizationSpanTarget 📖	MathDef	10 math math: finiteType_ofLocalizationSpanTarget, QuasiFinite.ofLocalizationSpanTarget, ofLocalizationSpanTarget_iff_finite, PropertyIsLocal.ofLocalizationSpanTarget, Smooth.ofLocalizationSpanTarget, locally_ofLocalizationSpanTarget, FormallyUnramified.ofLocalizationSpanTarget, Flat.ofLocalizationSpanTarget, Etale.ofLocalizationSpanTarget, finitePresentation_ofLocalizationSpanTarget
PropertyIsLocal 📖	CompData	10 math math: QuasiFinite.propertyIsLocal, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, Etale.propertyIsLocal, finiteType_isLocal, finitePresentation_isLocal, Smooth.propertyIsLocal, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget, Flat.propertyIsLocal, FormallyUnramified.propertyIsLocal, locally_propertyIsLocal
StableUnderCompositionWithLocalizationAway 📖	MathDef	3 math math: isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway, isStandardSmooth_stableUnderCompositionWithLocalizationAway, StableUnderComposition.stableUnderCompositionWithLocalizationAway
StableUnderCompositionWithLocalizationAwaySource 📖	MathDef	—
StableUnderCompositionWithLocalizationAwayTarget 📖	MathDef	1 math math: PropertyIsLocal.StableUnderCompositionWithLocalizationAwayTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofLocalizationSpanTarget_iff_finite 📖	mathematical	—	OfLocalizationSpanTarget OfLocalizationFiniteSpanTarget	—	Ideal.span_eq_top_iff_finite Subtype.prop
ofLocalizationSpan_iff_finite 📖	mathematical	—	OfLocalizationSpan OfLocalizationFiniteSpan	—	Ideal.span_eq_top_iff_finite Subtype.prop

RingHom.HoldsForLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
holdsForLocalizationAway 📖	mathematical	RingHom.HoldsForLocalization	RingHom.HoldsForLocalizationAway	—	—
isLocalizationMap 📖	mathematical	RingHom.StableUnderComposition RingHom.LocalizationPreserves RingHom.HoldsForLocalization Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	IsLocalization.map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.right Localization.isLocalization IsLocalization.localization_isScalarTower_of_submonoid_le IsLocalization.isLocalization_of_submonoid_le Submonoid.le_comap_map IsLocalization.ringHom_ext RingHom.ext IsLocalization.map_comp IsLocalization.map_eq
localRingHom 📖	mathematical	RingHom.StableUnderComposition RingHom.LocalizationPreserves RingHom.HoldsForLocalization Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.instRingHomClass	Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Localization.localRingHom	—	RingHom.instRingHomClass isLocalizationMap
mk 📖	mathematical	RingHom.RespectsIso Localization CommRing.toCommMonoid OreLocalization.instCommRing OreLocalization.oreSetComm algebraMap CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.instAlgebra Algebra.id	RingHom.HoldsForLocalization	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Localization.isLocalization AlgHom.comp_algebraMap

RingHom.HoldsForLocalizationAway

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
containsIdentities 📖	mathematical	RingHom.HoldsForLocalizationAway	RingHom.ContainsIdentities	—	of_bijective Function.bijective_id
of_bijective 📖	—	RingHom.HoldsForLocalizationAway Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—	IsLocalization.at_units Submonoid.powers_one IsLocalization.isLocalization_of_algEquiv

RingHom.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization_map 📖	mathematical	RingHom.IsStableUnderBaseChange	IsLocalization.map CommRing.toCommSemiring Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map IsScalarTower.of_algebraMap_eq' of_isLocalization IsLocalization.map_comp
localizationPreserves 📖	mathematical	RingHom.IsStableUnderBaseChange	RingHom.LocalizationPreserves	—	isLocalization_map
of_isLocalization 📖	—	RingHom.IsStableUnderBaseChange algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	—	Algebra.isPushout_of_isLocalization

RingHom.LocalizationAwayPreserves

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	—	RingHom.LocalizationAwayPreserves	—	—	—
respectsIso 📖	mathematical	RingHom.LocalizationAwayPreserves	RingHom.RespectsIso	—	IsLocalization.away_of_isUnit_of_bijective isUnit_one Equiv.bijective map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingEquiv.bijective IsLocalization.Away.map.eq_1 IsLocalization.map_comp RingHom.comp_assoc RingEquiv.symm_comp RingHomCompTriple.comp_eq RingHomCompTriple.ids

RingHom.LocalizationPreserves

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
away 📖	mathematical	RingHom.LocalizationPreserves	RingHom.LocalizationAwayPreserves	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.map_powers

RingHom.OfLocalizationSpan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	—	RingHom.OfLocalizationSpan	—	—	—
mk 📖	mathematical	RingHom.RespectsIso algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	RingHom.OfLocalizationSpan	—	IsScalarTower.right Algebra.to_smulCommClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Localization.isLocalization IsLocalization.ringHom_ext RingHom.ext RingHomCompTriple.comp_apply RingHomCompTriple.right_ids Algebra.TensorProduct.tmul_one_eq_one_tmul MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map_eq AlgEquiv.commutes
ofIsLocalization 📖	—	RingHom.OfLocalizationSpan RingHom.RespectsIso Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—	Localization.isLocalization IsLocalization.ringHom_ext RingHom.ext RingHom.comp_apply IsLocalization.map_comp AlgEquiv.commutes
ofIsLocalization' 📖	—	RingHom.OfLocalizationSpan RingHom.RespectsIso Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away.map Set Set.instMembership	—	—	ofIsLocalization IsLocalization.map_comp

RingHom.OfLocalizationSpanTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	—	RingHom.OfLocalizationSpanTarget	—	—	—
ofIsLocalization 📖	—	RingHom.OfLocalizationSpanTarget RingHom.RespectsIso Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.comp algebraMap	—	—	RingHom.comp_assoc RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.toRingHom_eq_coe AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass AlgEquiv.toRingEquiv_eq_coe AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.toRingEquiv_toRingHom Localization.isLocalization le_rfl Localization.coe_algEquiv_symm IsLocalization.map_comp RingHom.comp_id
ofLocalizationSpan 📖	mathematical	RingHom.OfLocalizationSpanTarget RingHom.StableUnderCompositionWithLocalizationAwaySource	RingHom.OfLocalizationSpan	—	Ideal.map_top RingHom.instRingHomClass Ideal.map_span Localization.isLocalization IsLocalization.map_comp

RingHom.PropertyIsLocal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
HoldsForLocalizationAway 📖	mathematical	RingHom.PropertyIsLocal RingHom.ContainsIdentities	RingHom.HoldsForLocalizationAway	—	RingHomCompTriple.comp_eq RingHomCompTriple.ids StableUnderCompositionWithLocalizationAwayTarget
StableUnderCompositionWithLocalizationAwayTarget 📖	mathematical	RingHom.PropertyIsLocal	RingHom.StableUnderCompositionWithLocalizationAwayTarget	—	—
and 📖	—	RingHom.PropertyIsLocal	—	—	RingHom.LocalizationAwayPreserves.and localizationAwayPreserves RingHom.OfLocalizationSpanTarget.and ofLocalizationSpanTarget RingHom.OfLocalizationSpan.and ofLocalizationSpan RingHom.StableUnderCompositionWithLocalizationAwayTarget.and StableUnderCompositionWithLocalizationAwayTarget
localizationAwayPreserves 📖	mathematical	RingHom.PropertyIsLocal	RingHom.LocalizationAwayPreserves	—	—
ofLocalizationSpan 📖	mathematical	RingHom.PropertyIsLocal	RingHom.OfLocalizationSpan	—	—
ofLocalizationSpanTarget 📖	mathematical	RingHom.PropertyIsLocal	RingHom.OfLocalizationSpanTarget	—	—
respectsIso 📖	mathematical	RingHom.PropertyIsLocal	RingHom.RespectsIso	—	RingHom.LocalizationAwayPreserves.respectsIso localizationAwayPreserves

RingHom.StableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stableUnderCompositionWithLocalizationAway 📖	mathematical	RingHom.StableUnderComposition RingHom.HoldsForLocalizationAway	RingHom.StableUnderCompositionWithLocalizationAway	—	—

RingHom.StableUnderCompositionWithLocalizationAway

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
respectsIso 📖	mathematical	RingHom.StableUnderCompositionWithLocalizationAway	RingHom.RespectsIso	—	IsLocalization.away_of_isUnit_of_bijective isUnit_one RingEquiv.bijective

RingHom.StableUnderCompositionWithLocalizationAwayTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	—	RingHom.StableUnderCompositionWithLocalizationAwayTarget	—	—	—

(root)

Definitions

Name	Category	Theorems
LocalizationPreserves 📖	MathDef	1 math math: isReduced_localizationPreserves
OfLocalizationMaximal 📖	MathDef	2 math math: isIntegrallyClosed_ofLocalizationMaximal, isReduced_ofLocalizationMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_localization 📖	—	DFunLike.coe RingHom Localization.AtPrime Ideal.IsMaximal.isPrime' Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id OreLocalization.instZero CommMonoid.toMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toMulAction	—	—	Ideal.IsMaximal.isPrime' Module.eq_zero_of_localization_maximal instIsLocalizedModuleLinearMapOfIsLocalization Localization.isLocalization
ideal_eq_bot_of_localization 📖	mathematical	IsLocalization.coeSubmodule Localization.AtPrime Ideal.IsMaximal.isPrime' OreLocalization.instCommSemiring Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instAlgebra Algebra.id Bot.bot Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule.instBot	Ideal Semiring.toModule	—	Ideal.IsMaximal.isPrime' bot_unique eq_zero_of_localization Eq.le
ideal_eq_bot_of_localization' 📖	—	Ideal.map Localization.AtPrime Ideal.IsMaximal.isPrime' RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—	Ideal.IsMaximal.isPrime' Ideal.eq_of_localization_maximal Ideal.map_bot RingHom.instRingHomClass

---

← Back to Index