Documentation Verification Report

HasLocalization

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

Statistics

Metric	Count
Definitions `HasLocalization`, `D`, `L`, `hD`, `standard`, `Localization'`, `Q'`, `instCategoryLocalization'`	8
Theorems `hL`, `instIsLocalizationLocalization'Q'`	2
Total	10

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`HasLocalization` 📖	CompData	—
`Localization'` 📖	CompOp	9 math math: `CategoryTheory.Shift.instLinearLocalization'ShiftFunctorOfCommShiftOfQ'`, `CategoryTheory.Localization.instLinearLocalization'Q'`, `CategoryTheory.Localization.instAdditiveLocalization'Q'`, `CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q'`, `CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt`, `instIsLocalizationLocalization'Q'`, `CategoryTheory.Localization.instHasFiniteProductsLocalization'`, `CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization'`, `CategoryTheory.Localization.instHasZeroObjectLocalization'`
`Q'` 📖	CompOp	4 math math: `CategoryTheory.Localization.instLinearLocalization'Q'`, `CategoryTheory.Localization.instAdditiveLocalization'Q'`, `CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q'`, `instIsLocalizationLocalization'Q'`
`instCategoryLocalization'` 📖	CompOp	18 math math: `CategoryTheory.Shift.instLinearLocalization'ShiftFunctorOfCommShiftOfQ'`, `CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc`, `CategoryTheory.Localization.instLinearLocalization'Q'`, `HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso`, `CategoryTheory.Localization.instAdditiveLocalization'Q'`, `CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q'`, `HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences`, `CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt`, `CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso`, `HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy`, `instIsLocalizationLocalization'Q'`, `HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso`, `CategoryTheory.Localization.instHasFiniteProductsLocalization'`, `HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso`, `CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization'`, `CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app`, `CategoryTheory.Localization.instHasZeroObjectLocalization'`, `HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocalizationLocalization'Q'` 📖	mathematical	—	`CategoryTheory.Functor.IsLocalization` `Localization'` `instCategoryLocalization'` `Q'`	—	`HasLocalization.hL`

CategoryTheory.MorphismProperty.HasLocalization

Definitions

Name	Category	Theorems
`D` 📖	CompOp	1 math math: `hL`
`L` 📖	CompOp	1 math math: `hL`
`hD` 📖	CompOp	1 math math: `hL`
`standard` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hL` 📖	mathematical	—	`CategoryTheory.Functor.IsLocalization` `D` `hD` `L`	—	—

---

← Back to Index