Documentation Verification Report

Localization

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

Statistics

Metric	Count
Definitions `localization`, `localizationRingHom`, `Localization`, `Localization`	4
Theorems `ext_of_localization`, `localization_add`, `localization_app`, `localization_mul`, `localization_one`, `localization_zero`	6
Total	10

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`

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`Localization` 📖	CompOp	54 math math: `CategoryTheory.Localization.isLocalization_op`, `CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.hasLimit'`, `CategoryTheory.Localization.instIsEquivalenceLocalizationLift`, `CategoryTheory.Localization.Construction.lift_obj`, `CategoryTheory.Localization.Construction.natTransExtension_hcomp`, `CategoryTheory.Localization.Construction.prodIsLocalization`, `CategoryTheory.Localization.Construction.wInv_eq_isoOfHom_inv`, `CategoryTheory.Localization.Construction.morphismProperty_eq_top'`, `CategoryTheory.Localization.instAdditiveLocalizationQ`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj`, `CategoryTheory.Localization.Construction.NatTransExtension.app_eq`, `CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac`, `CategoryTheory.Localization.Construction.instEssSurjLocalizationQ`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app`, `CategoryTheory.Localization.Construction.lift_map`, `CategoryTheory.Functor.HasLeftDerivedFunctor.hasRightKanExtension'`, `CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app`, `CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁`, `CategoryTheory.Shift.instLinearLocalizationShiftFunctorOfCommShiftOfQ`, `CategoryTheory.Localization.Construction.morphismProperty_is_top'`, `CategoryTheory.Localization.Construction.morphismProperty_eq_top`, `CategoryTheory.Triangulated.Localization.instAdditiveLocalizationShiftFunctorInt`, `CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_lift`, `CategoryTheory.Functor.HasRightDerivedFunctor.hasLeftKanExtension'`, `CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map`, `CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence`, `CategoryTheory.Localization.Construction.fac`, `CategoryTheory.Localization.Construction.whiskerLeft_natTransExtension`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj`, `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.guitartExact'`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_inv`, `CategoryTheory.Localization.instLinearLocalizationQ`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_inv`, `CategoryTheory.Localization.Construction.objEquiv_apply`, `CategoryTheory.Localization.instHasZeroObjectLocalization`, `CategoryTheory.Functor.q_isLocalization`, `CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.hasColimit'`, `CategoryTheory.Localization.Construction.objEquiv_symm_apply`, `CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`, `Q_inverts`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom`, `CategoryTheory.Functor.IsLocalization.isEquivalence`, `CategoryTheory.Localization.Construction.natTransExtension_app`, `CategoryTheory.Localization.instHasFiniteProductsLocalization`, `CategoryTheory.Localization.HasSmallLocalizedHom.small`, `CategoryTheory.Localization.Construction.wIso_eq_isoOfHom`, `CategoryTheory.Localization.instIsGroupoidLocalizationTopMorphismProperty`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom`, `CategoryTheory.Localization.Construction.morphismProperty_is_top`, `CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.guitartExact'`, `CategoryTheory.Localization.instPreservesFiniteProductsLocalizationQ`

CategoryTheory.MorphismProperty.LeftFraction

Definitions

Name	Category	Theorems
`Localization` 📖	CompOp	16 math math: `Localization.StrictUniversalPropertyFixedTarget.fac`, `Localization.homMk_comp_homMk`, `Localization.Qiso_hom_inv_id`, `Localization.StrictUniversalPropertyFixedTarget.inverts`, `Localization.Qiso_inv_hom_id_assoc`, `Localization.instIsLocalizationQ`, `Localization.Qiso_hom_inv_id_assoc`, `Localization.homMk_eq`, `Localization.instIsIsoQinv`, `Localization.Qiso_hom`, `Localization.Qiso_inv`, `Localization.Q_map`, `Localization.Qiso_inv_hom_id`, `Localization.Q_obj`, `Localization.map_eq_iff`, `Localization.Q_map_comp_Qinv`

---

← Back to Index