Algebra

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

Statistics

Metric	Count
Definitions toKerIsLocalization, mapₐ, toKerIsLocalization	3
Theorems toKerIsLocalization_apply, toKerIsLocalization_isLocalizedModule, idealMap_isLocalizedModule, isLocalization_algebraMapSubmonoid_map_algHom, ker_map, mapExtendScalars_eq_toLinearMap_mapₐ, map_eq_toLinearMap_mapₐ, map_linearMap_eq_toLinearMap_mapₐ, mapₐ_coe, mapₐ_injective_of_injective, mapₐ_surjective_of_surjective, isLocalization, toKerIsLocalization_apply, toKerIsLocalization_isLocalizedModule	14
Total	17

AlgHom

Definitions

Name	Category	Theorems
toKerIsLocalization 📖	CompOp	2 math math: toKerIsLocalization_apply, toKerIsLocalization_isLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toKerIsLocalization_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.ker AlgHom funLike AlgHomClass.toRingHomClass algHomClass IsLocalization.mapₐ Submodule.addCommMonoid Submodule.module Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right LinearMap.instFunLike toKerIsLocalization RingHom RingHom.instFunLike RingHom.instRingHomClass toRingHom IsLocalization.map Algebra.algebraMapSubmonoid Algebra.algebraMapSubmonoid_le_comap RingHom.toKerIsLocalization	—	AlgHomClass.toRingHomClass algHomClass IsScalarTower.right
toKerIsLocalization_isLocalizedModule 📖	mathematical	—	IsLocalizedModule Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker AlgHom funLike AlgHomClass.toRingHomClass algHomClass IsLocalization.mapₐ Submodule.addCommMonoid Submodule.module Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right Algebra.algebraMapSubmonoid toKerIsLocalization	—	RingHom.toKerIsLocalization_isLocalizedModule Algebra.algebraMapSubmonoid_map_eq

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealMap_isLocalizedModule 📖	mathematical	—	IsLocalizedModule Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike algebraMap Submodule.addCommMonoid Submodule.module Submodule.module' toSMul toModule IsScalarTower.right idealMap	—	IsScalarTower.right smulCommClass_self IsScalarTower.left Module.End.isUnit_iff IsUnit.mul_right_injective IsLocalization.map_units smul_def Ideal.mul_mem_left SMulMemClass.smul_mem Submodule.smulMemClass smul_one_smul IsUnit.mul_val_inv one_mul Subtype.coe_eta IsLocalization.mem_map_algebraMap_iff mul_comm IsLocalization.exists_of_eq

IsLocalization

Definitions

Name	Category	Theorems
mapₐ 📖	CompOp	8 math math: mapₐ_injective_of_injective, AlgHom.toKerIsLocalization_apply, map_eq_toLinearMap_mapₐ, mapExtendScalars_eq_toLinearMap_mapₐ, mapₐ_surjective_of_surjective, mapₐ_coe, map_linearMap_eq_toLinearMap_mapₐ, AlgHom.toKerIsLocalization_isLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization_algebraMapSubmonoid_map_algHom 📖	mathematical	—	IsLocalization Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHom.toRingHom Algebra.algebraMapSubmonoid	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.toRingHom_eq_coe MonoidHom.instMonoidHomClass Submonoid.map_coe_toMonoidHom AlgHom.toRingHom_toMonoidHom Algebra.algebraMapSubmonoid_map_eq
ker_map 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	RingHom.ker map Submonoid Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap Submonoid.le_comap_map Ideal.map algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Ideal.ext Submonoid.le_comap_map exists_mk'_eq RingHom.ker.congr_simp map.congr_simp map_mk' map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
mapExtendScalars_eq_toLinearMap_mapₐ 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' LinearMap.instFunLike IsLocalizedModule.mapExtendScalars AlgHom.toLinearMap IsScalarTower.toAlgHom instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid mapₐ	—	LinearMap.restrictScalars_injective LinearMap.IsScalarTower.compatibleSMul smulCommClass_self IsScalarTower.to_smulCommClass' instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid IsLocalizedModule.linearMap_ext LinearMap.ext RingHomCompTriple.ids LinearMap.coe_comp LinearMap.coe_restrictScalars IsLocalizedModule.mapExtendScalars_apply_apply IsLocalizedModule.map_apply map_eq AlgHomClass.toRingHomClass AlgHom.algHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.algebraMapSubmonoid_le_comap
map_eq_toLinearMap_mapₐ 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike IsLocalizedModule.map AlgHom.toLinearMap IsScalarTower.toAlgHom instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul mapₐ	—	LinearMap.ext smulCommClass_self instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid LinearMap.IsScalarTower.compatibleSMul DFunLike.congr_fun IsScalarTower.to_smulCommClass' mapExtendScalars_eq_toLinearMap_mapₐ
map_linearMap_eq_toLinearMap_mapₐ 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike IsLocalizedModule.map Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization AlgHom.toLinearMap IsScalarTower.toAlgHom instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid LinearMap.restrictScalars Algebra.id LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero mapₐ IsScalarTower.left instIsLocalizationAlgebraMapSubmonoid IsScalarTower.right Algebra.ofId	—	map_eq_toLinearMap_mapₐ IsScalarTower.left instIsLocalizationAlgebraMapSubmonoid IsScalarTower.right
mapₐ_coe 📖	mathematical	—	DFunLike.coe AlgHom CommSemiring.toSemiring AlgHom.funLike mapₐ RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map Algebra.algebraMapSubmonoid AlgHom.toRingHom Algebra.algebraMapSubmonoid_le_comap	—	—
mapₐ_injective_of_injective 📖	mathematical	DFunLike.coe AlgHom CommSemiring.toSemiring AlgHom.funLike	mapₐ	—	map_injective_of_injective isLocalization_algebraMapSubmonoid_map_algHom
mapₐ_surjective_of_surjective 📖	mathematical	DFunLike.coe AlgHom CommSemiring.toSemiring AlgHom.funLike	mapₐ	—	map_surjective_of_surjective isLocalization_algebraMapSubmonoid_map_algHom

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization 📖	mathematical	—	IsLocalization Polynomial CommSemiring.toSemiring commSemiring Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring RingHom semiring RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass C algebra	—	instIsScalarTowerPolynomial IsScalarTower.left isLocalizedModule_iff_isLocalization isScalarTower IsScalarTower.right isLocalizedModule_iff_isBaseChange IsBaseChange.of_equiv Algebra.to_smulCommClass RingHomInvPair.ids one_smul

RingHom

Definitions

Name	Category	Theorems
toKerIsLocalization 📖	CompOp	3 math math: AlgHom.toKerIsLocalization_apply, toKerIsLocalization_apply, toKerIsLocalization_isLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toKerIsLocalization_apply 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker IsLocalization.map DFunLike.coe LinearMap id Submodule.addCommMonoid Submodule.module Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right LinearMap.instFunLike toKerIsLocalization algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass IsScalarTower.right
toKerIsLocalization_isLocalizedModule 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass	IsLocalizedModule Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ker IsLocalization.map Submonoid Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap Submonoid.le_comap_map Submodule.addCommMonoid Submodule.module Submodule.module' Algebra.toSMul Algebra.toModule IsScalarTower.right toKerIsLocalization	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass RingHomInvPair.ids Submonoid.le_comap_map IsLocalization.ker_map IsScalarTower.right RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul Submodule.isScalarTower' IsLocalizedModule.of_linearEquiv Algebra.idealMap_isLocalizedModule

---

← Back to Index