Documentation Verification Report

Construction

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

Statistics

Metric	Count
Definitions `LocQuiver`, `obj`, `app`, `counitIso`, `functor`, `inverse`, `unitIso`, `instQuiverLocQuiver`, `liftToPathCategory`, `natTransExtension`, `objEquiv`, `relations`, `wInv`, `wIso`, `whiskeringLeftEquivalence`, `ιPaths`, `ψ₁`, `ψ₂`, `Q`, `instCategoryLocalization`	20
Theorems `app_eq`, `counitIso_hom`, `counitIso_inv`, `functor_map_hom_app`, `functor_obj_obj_map`, `functor_obj_obj_obj`, `inverse_map_app`, `inverse_obj_map`, `inverse_obj_obj`, `unitIso_hom`, `unitIso_inv`, `fac`, `liftToPathCategory_map`, `liftToPathCategory_obj`, `lift_map`, `lift_obj`, `morphismProperty_eq_top`, `morphismProperty_eq_top'`, `morphismProperty_is_top`, `morphismProperty_is_top'`, `natTransExtension_app`, `natTransExtension_hcomp`, `natTrans_hcomp_injective`, `objEquiv_apply`, `objEquiv_symm_apply`, `uniq`, `whiskerLeft_natTransExtension`, `Q_inverts`	28
Total	48

CategoryTheory.Localization.Construction

Definitions

Name	Category	Theorems
`LocQuiver` 📖	CompData	7 math math: `lift_obj`, `lift_map`, `WhiskeringLeftEquivalence.inverse_obj_map`, `WhiskeringLeftEquivalence.inverse_obj_obj`, `liftToPathCategory_map`, `objEquiv_symm_apply`, `liftToPathCategory_obj`
`instQuiverLocQuiver` 📖	CompOp	7 math math: `lift_obj`, `lift_map`, `WhiskeringLeftEquivalence.inverse_obj_map`, `WhiskeringLeftEquivalence.inverse_obj_obj`, `liftToPathCategory_map`, `objEquiv_symm_apply`, `liftToPathCategory_obj`
`liftToPathCategory` 📖	CompOp	4 math math: `lift_map`, `WhiskeringLeftEquivalence.inverse_obj_map`, `liftToPathCategory_map`, `liftToPathCategory_obj`
`natTransExtension` 📖	CompOp	3 math math: `natTransExtension_hcomp`, `whiskerLeft_natTransExtension`, `natTransExtension_app`
`objEquiv` 📖	CompOp	2 math math: `objEquiv_apply`, `objEquiv_symm_apply`
`relations` 📖	CompData	5 math math: `lift_obj`, `lift_map`, `WhiskeringLeftEquivalence.inverse_obj_map`, `WhiskeringLeftEquivalence.inverse_obj_obj`, `objEquiv_symm_apply`
`wInv` 📖	CompOp	1 math math: `wInv_eq_isoOfHom_inv`
`wIso` 📖	CompOp	1 math math: `wIso_eq_isoOfHom`
`whiskeringLeftEquivalence` 📖	CompOp	—
`ιPaths` 📖	CompOp	—
`ψ₁` 📖	CompOp	—
`ψ₂` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `lift`	—	`CategoryTheory.Functor.ext` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.composePath_toPath`
`liftToPathCategory_map` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.Functor.map` `CategoryTheory.Paths` `LocQuiver` `CategoryTheory.Paths.categoryPaths` `instQuiverLocQuiver` `liftToPathCategory` `CategoryTheory.composePath` `CategoryTheory.Functor.obj` `LocQuiver.obj` `Prefunctor.mapPath` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Quiver.Hom` `CategoryTheory.inv`	—	—
`liftToPathCategory_obj` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.Functor.obj` `CategoryTheory.Paths` `LocQuiver` `CategoryTheory.Paths.categoryPaths` `instQuiverLocQuiver` `liftToPathCategory` `LocQuiver.obj`	—	—
`lift_map` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `lift` `Quiver.Hom` `CategoryTheory.Paths` `LocQuiver` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Paths.categoryPaths` `instQuiverLocQuiver` `CategoryTheory.Quotient.as` `relations` `CategoryTheory.Functor.obj` `LocQuiver.obj` `CategoryTheory.HomRel.CompClosure` `CategoryTheory.composePath` `Prefunctor.mapPath` `CategoryTheory.inv` `liftToPathCategory`	—	—
`lift_obj` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `lift` `LocQuiver.obj` `CategoryTheory.Quotient.as` `CategoryTheory.Paths` `LocQuiver` `CategoryTheory.Paths.categoryPaths` `instQuiverLocQuiver` `relations`	—	—
`morphismProperty_eq_top` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.Functor.map` `wInv`	`Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`CategoryTheory.MorphismProperty.top_apply` `CategoryTheory.Functor.map_id` `CategoryTheory.Functor.map_comp` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.Quotient.full_functor` `CategoryTheory.Functor.map_preimage`
`morphismProperty_eq_top'` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	`Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`morphismProperty_eq_top`
`morphismProperty_is_top` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.Functor.map` `wInv`	`Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`morphismProperty_eq_top`
`morphismProperty_is_top'` 📖	mathematical	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	`Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`morphismProperty_eq_top'`
`natTransExtension_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `natTransExtension` `NatTransExtension.app`	—	—
`natTransExtension_hcomp` 📖	mathematical	—	`CategoryTheory.NatTrans.hcomp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `natTransExtension`	—	`CategoryTheory.Functor.id_hcomp` `whiskerLeft_natTransExtension`
`natTrans_hcomp_injective` 📖	—	`CategoryTheory.NatTrans.hcomp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	—	`CategoryTheory.NatTrans.ext'` `Equiv.right_inv` `CategoryTheory.NatTrans.id_hcomp_app`
`objEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.MorphismProperty.Localization` `EquivLike.toFunLike` `Equiv.instEquivLike` `objEquiv` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q`	—	—
`objEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.MorphismProperty.Localization` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `objEquiv` `LocQuiver.obj` `CategoryTheory.Quotient.as` `CategoryTheory.Paths` `LocQuiver` `CategoryTheory.Paths.categoryPaths` `instQuiverLocQuiver` `relations`	—	—
`uniq` 📖	—	`CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q`	—	—	`CategoryTheory.Paths.ext_functor` `CategoryTheory.Functor.congr_obj` `CategoryTheory.Functor.congr_hom` `CategoryTheory.Functor.congr_inv_of_congr_hom` `CategoryTheory.Functor.ext`
`whiskerLeft_natTransExtension` 📖	mathematical	—	`CategoryTheory.Functor.whiskerLeft` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `natTransExtension`	—	`CategoryTheory.NatTrans.ext'` `NatTransExtension.app_eq`

CategoryTheory.Localization.Construction.LocQuiver

Definitions

Name	Category	Theorems
`obj` 📖	CompOp	7 math math: `CategoryTheory.Localization.Construction.lift_obj`, `CategoryTheory.Localization.Construction.lift_map`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj`, `CategoryTheory.Localization.Construction.liftToPathCategory_map`, `CategoryTheory.Localization.Construction.objEquiv_symm_apply`, `CategoryTheory.Localization.Construction.liftToPathCategory_obj`

CategoryTheory.Localization.Construction.NatTransExtension

Definitions

Name	Category	Theorems
`app` 📖	CompOp	3 math math: `app_eq`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app`, `CategoryTheory.Localization.Construction.natTransExtension_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`app_eq` 📖	mathematical	—	`app` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`

CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence

Definitions

Name	Category	Theorems
`counitIso` 📖	CompOp	2 math math: `counitIso_inv`, `counitIso_hom`
`functor` 📖	CompOp	7 math math: `functor_obj_obj_map`, `functor_obj_obj_obj`, `functor_map_hom_app`, `unitIso_inv`, `counitIso_inv`, `unitIso_hom`, `counitIso_hom`
`inverse` 📖	CompOp	7 math math: `inverse_map_app`, `inverse_obj_map`, `inverse_obj_obj`, `unitIso_inv`, `counitIso_inv`, `unitIso_hom`, `counitIso_hom`
`unitIso` 📖	CompOp	2 math math: `unitIso_inv`, `unitIso_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counitIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `inverse` `functor` `CategoryTheory.Functor.id` `counitIso` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct`	—	—
`counitIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `inverse` `functor` `CategoryTheory.Functor.id` `counitIso` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct`	—	—
`functor_map_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `functor`	—	—
`functor_obj_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `functor` `CategoryTheory.MorphismProperty.Q`	—	—
`functor_obj_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `functor` `CategoryTheory.MorphismProperty.Q`	—	—
`inverse_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Localization.Construction.lift` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `inverse` `CategoryTheory.Localization.Construction.NatTransExtension.app` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.eqToHom` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`inverse_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inverse` `Quiver.Hom` `CategoryTheory.Paths` `CategoryTheory.Localization.Construction.LocQuiver` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Localization.Construction.instQuiverLocQuiver` `CategoryTheory.Quotient.as` `CategoryTheory.Localization.Construction.relations` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.Localization.Construction.LocQuiver.obj` `CategoryTheory.HomRel.CompClosure` `CategoryTheory.composePath` `Prefunctor.mapPath` `CategoryTheory.inv` `CategoryTheory.Localization.Construction.liftToPathCategory`	—	—
`inverse_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inverse` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.Localization.Construction.LocQuiver.obj` `CategoryTheory.Quotient.as` `CategoryTheory.Paths` `CategoryTheory.Localization.Construction.LocQuiver` `CategoryTheory.Paths.categoryPaths` `CategoryTheory.Localization.Construction.instQuiverLocQuiver` `CategoryTheory.Localization.Construction.relations`	—	—
`unitIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `functor` `inverse` `unitIso` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct`	—	—
`unitIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.FunctorsInverting` `CategoryTheory.MorphismProperty.instCategoryFunctorsInverting` `functor` `inverse` `unitIso` `CategoryTheory.eqToHom` `CategoryTheory.Category.toCategoryStruct`	—	—

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`Q` 📖	CompOp	31 math math: `CategoryTheory.Localization.isLocalization_op`, `CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.hasLimit'`, `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.Functor.HasLeftDerivedFunctor.hasRightKanExtension'`, `CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_hom_app`, `CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁`, `CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_lift`, `CategoryTheory.Functor.HasRightDerivedFunctor.hasLeftKanExtension'`, `CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence`, `CategoryTheory.Localization.Construction.fac`, `CategoryTheory.Localization.Construction.whiskerLeft_natTransExtension`, `CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.guitartExact'`, `CategoryTheory.Localization.instLinearLocalizationQ`, `CategoryTheory.Localization.Construction.objEquiv_apply`, `CategoryTheory.Functor.q_isLocalization`, `CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.hasColimit'`, `CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`, `Q_inverts`, `CategoryTheory.Localization.HasSmallLocalizedHom.small`, `CategoryTheory.Localization.Construction.wIso_eq_isoOfHom`, `CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.guitartExact'`, `CategoryTheory.Localization.instPreservesFiniteProductsLocalizationQ`
`instCategoryLocalization` 📖	CompOp	48 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.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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Q_inverts` 📖	mathematical	—	`IsInvertedBy` `Localization` `instCategoryLocalization` `Q`	—	`CategoryTheory.Iso.isIso_hom`

---

← Back to Index