Localization

📁 Source: Mathlib/RingTheory/Flat/Localization.lean

Statistics

Metric	Count
Definitions	0
Theorems flat, of_isLocalization, of_isLocalizedModule, flat, flat_iff_of_isLocalization, flat_of_isLocalized_maximal, flat_of_isLocalized_span, flat_of_localized_maximal, flat_of_localized_span, instFlatAtPrime	10
Total	10

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flat 📖	mathematical	—	Module.Flat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule	—	Module.Flat.iff_lTensor_injectiveₛ RingHomSurjective.ids Algebra.to_smulCommClass TensorProduct.isScalarTower_left IsScalarTower.right TensorProduct.smulCommClass_left smulCommClass_self tensorProduct_isLocalizedModule Submodule.isScalarTower' IsLocalizedModule.isBaseChange Submodule.isLocalizedModule RingHomInvPair.ids RingHomSurjective.invPair RingHomCompTriple.ids Subtype.val_injective LinearMap.IsScalarTower.compatibleSMul TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass mul_one LinearEquiv.injective

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalization 📖	mathematical	IsSMulRegular Algebra.toSMul CommSemiring.toSemiring Algebra.id	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	of_isLocalizedModule IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization
of_isLocalizedModule 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsLocalization.flat of_flat_of_isBaseChange IsLocalizedModule.isBaseChange

Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flat 📖	mathematical	—	Module.Flat Localization CommSemiring.toCommMonoid OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Module.toDistribMulAction Semiring.toModule OreLocalization.instModuleOfIsScalarTower Algebra.toModule IsScalarTower.right	—	IsScalarTower.right IsLocalization.flat isLocalization Module.Flat.trans OreLocalization.instIsScalarTower

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flat_iff_of_isLocalization 📖	mathematical	—	Flat	—	isLocalizedModule_id IsLocalization.flat Flat.trans Flat.of_isLocalizedModule
flat_of_isLocalized_maximal 📖	—	IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction IsLocalizedModule.AtPrime Ideal.IsMaximal.isPrime' Flat	—	—	Ideal.IsMaximal.isPrime' IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.coe_lTensor injective_of_isLocalized_maximal IsLocalizedModule.rTensor IsLocalizedModule.map_lTensor
flat_of_isLocalized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsScalarTower Algebra.toSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction IsLocalizedModule.Away Set Set.instMembership Flat	—	—	IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.coe_lTensor injective_of_isLocalized_span IsLocalizedModule.rTensor IsLocalizedModule.map_lTensor
flat_of_localized_maximal 📖	—	Flat LocalizedModule Ideal.primeCompl CommSemiring.toSemiring Ideal.IsMaximal.isPrime' OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.oreSetComm CommSemiring.toCommMonoid toDistribMulAction OreLocalization.instModuleOfIsScalarTower Semiring.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id	—	—	Ideal.IsMaximal.isPrime' IsScalarTower.left IsScalarTower.right flat_of_isLocalized_maximal OreLocalization.instIsScalarTower localizedModuleIsLocalizedModule
flat_of_localized_span 📖	—	Ideal.span CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Flat LocalizedModule.Away Set Set.instMembership OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submonoid.powers OreLocalization.oreSetComm CommSemiring.toCommMonoid toDistribMulAction OreLocalization.instModuleOfIsScalarTower IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.right Algebra.id	—	—	IsScalarTower.left IsScalarTower.right flat_of_isLocalized_span OreLocalization.instIsScalarTower localizedModuleIsLocalizedModule

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFlatAtPrime 📖	mathematical	—	Module.Flat Localization.AtPrime CommRing.toCommSemiring OreLocalization.instCommSemiring Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Algebra.toModule OreLocalization.instSemiring Localization.AtPrime.instAlgebraOfLiesOver	—	IsScalarTower.right Module.flat_iff_of_isLocalization Localization.isLocalization Localization.AtPrime.instIsScalarTower IsScalarTower.left Module.Flat.trans OreLocalization.instIsScalarTower Localization.flat Module.Flat.of_free Module.Free.self

---

← Back to Index