Documentation Verification Report

Localization

📁 Source: Mathlib/CategoryTheory/Center/Localization.lean

Statistics

Metric	Count
Definitions `localization`, `localizationRingHom`	2
Theorems `ext_of_localization`, `localization_add`, `localization_app`, `localization_mul`, `localization_one`, `localization_zero`	6
Total	8

CategoryTheory.CatCenter

Definitions

Name	Category	Theorems
`localization` 📖	CompOp	5 math math: `localization_app`, `localization_zero`, `localization_mul`, `localization_one`, `localization_add`
`localizationRingHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_of_localization` 📖	—	`app` `CategoryTheory.Functor.obj`	—	—	`CategoryTheory.Localization.natTrans_ext`
`localization_add` 📖	mathematical	—	`localization` `CategoryTheory.CatCenter` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CategoryTheory.Preadditive.instRingEnd` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.id`	—	`ext_of_localization` `localization_app` `CategoryTheory.Functor.map_add`
`localization_app` 📖	mathematical	—	`app` `localization` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.Localization.liftNatTrans_app` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Iso.hom_inv_id_app_assoc`
`localization_mul` 📖	mathematical	—	`localization` `CategoryTheory.CatCenter` `CategoryTheory.End.mul` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	`ext_of_localization` `localization_app` `CategoryTheory.Functor.map_comp`
`localization_one` 📖	mathematical	—	`localization` `CategoryTheory.CatCenter` `CategoryTheory.End.one` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	`ext_of_localization` `localization_app` `CategoryTheory.Functor.map_id`
`localization_zero` 📖	mathematical	—	`localization` `CategoryTheory.CatCenter` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CategoryTheory.Preadditive.instRingEnd` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.id`	—	`ext_of_localization` `localization_app` `CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`

---

← Back to Index