Documentation Verification Report

Localization

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

Statistics

Metric	Count
Definitions `localized`, `commShiftOfLocalization`, `iso`, `localization`, `localization'`, `localized`, `commShift`, `instCommShiftLocalizedFunctor`, `IsCompatibleWithShift`, `Localization`, `Localization`, `commShift_Q`, `commShift_Q'`, `shiftLocalizerMorphism`	14
Theorems `iso_hom_app`, `iso_hom_app_assoc`, `iso_inv_app`, `iso_inv_app_assoc`, `commShiftOfLocalization_iso_hom_app`, `commShiftOfLocalization_iso_inv_app`, `commShift_iso_hom_app`, `commShift_iso_hom_app_assoc`, `commShift_iso_inv_app`, `commShift_iso_inv_app_assoc`, `instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`, `natTransCommShift_hom`, `condition`, `iff`, `shiftFunctor_comp_inverts`, `shift`, `commShift_iso_hom_of_localization`	17
Total	31

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`commShiftOfLocalization` 📖	CompOp	3 math math: `commShiftOfLocalization_iso_inv_app`, `commShiftOfLocalization_iso_hom_app`, `CategoryTheory.NatTrans.commShift_iso_hom_of_localization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftOfLocalization_iso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CommShift.commShiftIso` `commShiftOfLocalization` `obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `map` `CategoryTheory.Iso.inv` `CategoryTheory.Localization.Lifting.iso`	—	`commShiftOfLocalization.iso_hom_app`
`commShiftOfLocalization_iso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `CommShift.commShiftIso` `commShiftOfLocalization` `obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `map` `CategoryTheory.Iso.hom` `CategoryTheory.Localization.Lifting.iso`	—	`commShiftOfLocalization.iso_inv_app`

CategoryTheory.Functor.CommShift

Definitions

Name	Category	Theorems
`localized` 📖	CompOp	—

CategoryTheory.Functor.commShiftOfLocalization

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	4 math math: `iso_inv_app`, `iso_inv_app_assoc`, `iso_hom_app`, `iso_hom_app_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Localization.Lifting.iso`	—	`CategoryTheory.Localization.liftNatTrans_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`iso_hom_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Localization.Lifting.iso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_hom_app`
`iso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Localization.Lifting.iso` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Localization.liftNatTrans.congr_simp` `CategoryTheory.Category.assoc` `CategoryTheory.Localization.liftNatTrans_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`iso_inv_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Localization.Lifting.iso` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_app`

CategoryTheory.HasShift

Definitions

Name	Category	Theorems
`localization` 📖	CompOp	3 math math: `CategoryTheory.Triangulated.Localization.instAdditiveLocalizationShiftFunctorInt`, `CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization`, `CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`
`localization'` 📖	CompOp	2 math math: `CategoryTheory.Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt`, `CategoryTheory.Triangulated.Localization.instIsTriangulatedLocalization'`
`localized` 📖	CompOp	—

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
`commShift` 📖	CompOp	5 math math: `natTransCommShift_hom`, `commShift_iso_hom_app`, `commShift_iso_inv_app`, `commShift_iso_hom_app_assoc`, `commShift_iso_inv_app_assoc`
`instCommShiftLocalizedFunctor` 📖	CompOp	1 math math: `instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift_iso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `commShift` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `functor`	—	`CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Category.assoc`
`commShift_iso_hom_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `commShift` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `functor`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `commShift_iso_hom_app`
`commShift_iso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `commShift` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `functor` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app` `CategoryTheory.Functor.commShiftIso_comp_inv_app` `CategoryTheory.Category.assoc`
`commShift_iso_inv_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `commShift` `functor` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `commShift_iso_inv_app`
`instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.comp` `functor` `CategoryTheory.MorphismProperty.Q` `localizedFunctor` `CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.CatCommSq.iso` `catCommSq` `CategoryTheory.HasShift.localization` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.MorphismProperty.commShift_Q` `instCommShiftLocalizedFunctor`	—	`natTransCommShift_hom` `CategoryTheory.Functor.q_isLocalization`
`natTransCommShift_hom` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `functor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.comp` `commShift`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Category.assoc` `commShift_iso_hom_app` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.hom_inv_id_app_assoc`

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsCompatibleWithShift` 📖	CompData	3 math math: `CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso`, `IsCompatibleWithTriangulation.toIsCompatibleWithShift`, `CategoryTheory.ObjectProperty.instIsCompatibleWithShiftTrWIntOfIsStableUnderShift`
`Localization` 📖	CompOp	49 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.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.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.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.LocalizerMorphism.IsLeftDerivabilityStructure.guitartExact'`, `CategoryTheory.Localization.instPreservesFiniteProductsLocalizationQ`
`commShift_Q` 📖	CompOp	1 math math: `CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`
`commShift_Q'` 📖	CompOp	—
`shiftLocalizerMorphism` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shift` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map`	—	`IsCompatibleWithShift.iff`

CategoryTheory.MorphismProperty.IsCompatibleWithShift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.inverseImage` `CategoryTheory.shiftFunctor`	—	—
`iff` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map`	—	`condition`
`shiftFunctor_comp_inverts` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor`	—	`CategoryTheory.Localization.inverts`

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`

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift_iso_hom_of_localization` 📖	mathematical	—	`CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Localization.Lifting.iso` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.commShiftOfLocalization`	—	`ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id`

---

← Back to Index