Documentation Verification Report

Localization

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

Statistics

Metric	Count
Definitions `instModuleCarrierLocalizationLocalizedModule`, `localizedModule`, `localizedModuleMap`, `localizedModuleMkLinearMap`, `localizedModule_functor`	5
Theorems `instAdditiveLocalizationLocalizedModule_functor`, `instIsScalarTowerLocalizationCarrierLocalizedModule`, `instPreservesFiniteColimitsLocalizationLocalizedModule_functor`, `instPreservesFiniteLimitsLocalizationLocalizedModule_functor`, `localizedModuleMap_hom_apply`, `localizedModule_functor_map`, `localizedModule_functor_map_exact`, `localizedModule_functor_obj`, `localizedModule_isLocalizedModule`, `instSmallLocalizedModule`	10
Total	15

ModuleCat

Definitions

Name	Category	Theorems
`instModuleCarrierLocalizationLocalizedModule` 📖	CompOp	3 math math: `localizedModule_isLocalizedModule`, `instIsScalarTowerLocalizationCarrierLocalizedModule`, `localizedModuleMap_hom_apply`
`localizedModule` 📖	CompOp	4 math math: `localizedModule_isLocalizedModule`, `instIsScalarTowerLocalizationCarrierLocalizedModule`, `localizedModuleMap_hom_apply`, `localizedModule_functor_obj`
`localizedModuleMap` 📖	CompOp	2 math math: `localizedModule_functor_map`, `localizedModuleMap_hom_apply`
`localizedModuleMkLinearMap` 📖	CompOp	2 math math: `localizedModule_isLocalizedModule`, `localizedModuleMap_hom_apply`
`localizedModule_functor` 📖	CompOp	6 math math: `localizedModule_functor_map_exact`, `instAdditiveLocalizationLocalizedModule_functor`, `instPreservesFiniteColimitsLocalizationLocalizedModule_functor`, `localizedModule_functor_map`, `localizedModule_functor_obj`, `instPreservesFiniteLimitsLocalizationLocalizedModule_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAdditiveLocalizationLocalizedModule_functor` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `ModuleCat` `CommRing.toRing` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `moduleCategory` `instPreadditive` `localizedModule_functor`	—	`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`
`instPreservesFiniteColimitsLocalizationLocalizedModule_functor` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModule_functor`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModule_functor` `List.TFAE.out` `CategoryTheory.Functor.exact_tfae` `localizedModule_functor_map_exact`
`instPreservesFiniteLimitsLocalizationLocalizedModule_functor` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModule_functor`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModule_functor` `List.TFAE.out` `CategoryTheory.Functor.exact_tfae` `localizedModule_functor_map_exact`
`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_functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModule_functor` `localizedModuleMap`	—	—
`localizedModule_functor_map_exact` 📖	mathematical	`CategoryTheory.ShortComplex.Exact` `ModuleCat` `CommRing.toRing` `moduleCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	`Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `CategoryTheory.ShortComplex.map` `localizedModule_functor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModule_functor`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instAdditiveLocalizationLocalizedModule_functor` `CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact` `IsLocalizedModule.map_exact` `localizedModule_isLocalizedModule`
`localizedModule_functor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `ModuleCat` `CommRing.toRing` `moduleCategory` `Localization` `CommRing.toCommMonoid` `OreLocalization.instRing` `OreLocalization.oreSetComm` `localizedModule_functor` `localizedModule`	—	—
`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