Documentation Verification Report

Localization

📁 Source: Mathlib/Algebra/Category/ModuleCat/Localization.lean

Statistics

Metric	Count
Definitions `instModuleCarrierLocalizationLocalizedModule`, `localizedModule`, `localizedModuleFunctor`, `localizedModuleMap`, `localizedModuleMkLinearMap`	5
Theorems `instAdditiveLocalizationLocalizedModuleFunctor`, `instIsScalarTowerLocalizationCarrierLocalizedModule`, `instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor`, `instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor`, `localizedModuleFunctor_map`, `localizedModuleFunctor_map_exact`, `localizedModuleFunctor_obj`, `localizedModuleMap_hom_apply`, `localizedModule_isLocalizedModule`, `instSmallLocalizedModule`	10
Total	15

ModuleCat

Definitions

Name	Category	Theorems
`instModuleCarrierLocalizationLocalizedModule` 📖	CompOp	3 math math: `localizedModule_isLocalizedModule`, `instIsScalarTowerLocalizationCarrierLocalizedModule`, `localizedModuleMap_hom_apply`
`localizedModule` 📖	CompOp	16 math math: `injectiveDimension_eq_iSup_localizedModule_prime`, `hasInjectiveDimensionLE_iff_forall_maximalSpectrum`, `localizedModuleFunctor_obj`, `localizedModule_isLocalizedModule`, `localizedModule_hasProjectiveDimensionLE`, `instIsScalarTowerLocalizationCarrierLocalizedModule`, `hasInjectiveDimensionLE_iff_forall_primeSpectrum`, `projectiveDimension_le_projectiveDimension_of_isLocalizedModule`, `hasProjectiveDimensionLE_iff_forall_primeSpectrum`, `hasProjectiveDimensionLE_iff_forall_maximalSpectrum`, `injectiveDimension_le_injectiveDimension_of_isLocalizedModule`, `projectiveDimension_eq_iSup_localizedModule_maximal`, `localizedModuleMap_hom_apply`, `projectiveDimension_eq_iSup_localizedModule_prime`, `injectiveDimension_eq_iSup_localizedModule_maximal`, `localizedModule_hasInjectiveDimensionLE`
`localizedModuleFunctor` 📖	CompOp	8 math math: `localizedModuleFunctor_map`, `instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor`, `localizedModuleFunctor_obj`, `instPreservesInjectiveObjectsLocalizationLocalizedModuleFunctorOfIsNoetherianRing`, `instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor`, `instPreservesProjectiveObjectsLocalizationLocalizedModuleFunctor`, `instAdditiveLocalizationLocalizedModuleFunctor`, `localizedModuleFunctor_map_exact`
`localizedModuleMap` 📖	CompOp	2 math math: `localizedModuleFunctor_map`, `localizedModuleMap_hom_apply`
`localizedModuleMkLinearMap` 📖	CompOp	2 math math: `localizedModule_isLocalizedModule`, `localizedModuleMap_hom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAdditiveLocalizationLocalizedModuleFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `ModuleCat` `CommRing.toRing` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `moduleCategory` `instPreadditive` `localizedModuleFunctor`	—	`hom_ext` `LinearMap.ext` `localizedModule_isLocalizedModule` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass`
`instIsScalarTowerLocalizationCarrierLocalizedModule` 📖	mathematical	—	`IsScalarTower` `Localization` `CommRing.toCommMonoid` `carrier` `OreLocalization.instRing` `CommRing.toRing` `OreLocalization.oreSetComm` `localizedModule` `OreLocalization.instSMulOfIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `isAddCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `OreLocalization.instMonoid` `Module.toDistribMulAction` `OreLocalization.instSemiring` `AddCommGroup.toAddCommMonoid` `isModule` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instModuleCarrierLocalizationLocalizedModule`	—	`Equiv.isScalarTower` `instSmallLocalizedModule` `IsScalarTower.right` `IsScalarTower.left` `OreLocalization.instIsScalarTower_1`
`instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModuleFunctor`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModuleFunctor` `List.TFAE.out` `CategoryTheory.Functor.exact_tfae` `localizedModuleFunctor_map_exact`
`instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModuleFunctor`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModuleFunctor` `List.TFAE.out` `CategoryTheory.Functor.exact_tfae` `localizedModuleFunctor_map_exact`
`localizedModuleFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModuleFunctor` `localizedModuleMap`	—	—
`localizedModuleFunctor_map_exact` 📖	mathematical	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `CommRing.toRing` `OreLocalization.oreSetComm` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `CategoryTheory.ShortComplex.map` `localizedModuleFunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModuleFunctor`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModuleFunctor` `CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact` `IsLocalizedModule.map_exact` `localizedModule_isLocalizedModule`
`localizedModuleFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModuleFunctor` `localizedModule`	—	—
`localizedModuleMap_hom_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Localization` `CommRing.toCommMonoid` `CommSemiring.toSemiring` `OreLocalization.instCommSemiring` `CommRing.toCommSemiring` `OreLocalization.oreSetComm` `RingHom.id` `Semiring.toNonAssocSemiring` `carrier` `OreLocalization.instRing` `CommRing.toRing` `localizedModule` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `LinearMap.instFunLike` `Hom.hom` `localizedModuleMap` `instModuleCarrierLocalizationLocalizedModule` `LinearMap.addCommMonoid` `LinearMap.module` `IsLocalizedModule.map` `localizedModuleMkLinearMap` `localizedModule_isLocalizedModule`	—	—
`localizedModule_isLocalizedModule` 📖	mathematical	—	`IsLocalizedModule` `CommRing.toCommSemiring` `carrier` `CommRing.toRing` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModule` `AddCommGroup.toAddCommMonoid` `isAddCommGroup` `isModule` `instModuleCarrierLocalizationLocalizedModule` `localizedModuleMkLinearMap`	—	`IsLocalizedModule.of_linearEquiv` `localizedModuleIsLocalizedModule`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSmallLocalizedModule` 📖	mathematical	—	`Small` `LocalizedModule` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`small_of_surjective` `small_prod` `UnivLE.small` `UnivLE.self` `small_subtype` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule` `IsLocalizedModule.mk'_surjective`

---

← Back to Index