Documentation Verification Report

SmallHom

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

Statistics

Metric	Count
Definitions `HasSmallLocalizedHom`, `SmallHom`, `chgUniv`, `comp`, `equiv`, `mk`, `mkInv`, `smallHomMap`, `smallHomMap'`	9
Theorems `small`, `comp_assoc`, `comp_mk_id`, `equiv_chgUniv`, `equiv_comp`, `equiv_equiv_symm`, `equiv_mk`, `equiv_mkInv`, `mkInv_comp_mk`, `mk_comp_mk`, `mk_comp_mkInv`, `mk_id_comp`, `hasSmallLocalizedHom_iff`, `hasSmallLocalizedHom_iff_of_isos`, `hasSmallLocalizedHom_iff_source`, `hasSmallLocalizedHom_iff_target`, `hasSmallLocalizedHom_of_isLocalization`, `hasSmallLocalizedHom_of_isos`, `small_of_hasSmallLocalizedHom`, `equiv_smallHomMap`, `equiv_smallHomMap'`, `smallHomMap'_comp`, `smallHomMap'_mk`, `smallHomMap_comp`, `smallHomMap_mk`	25
Total	34

CategoryTheory.Localization

Definitions

Name	Category	Theorems
`HasSmallLocalizedHom` 📖	CompData	11 math math: `hasSmallLocalizedHom_iff_of_isos`, `instHasSmallLocalizedHomObjShiftFunctor_1`, `hasSmallLocalizedHom_of_isos`, `hasSmallLocalizedHom_iff_source`, `hasSmallLocalizedHom_iff_target`, `instHasSmallLocalizedHomObjShiftFunctor`, `hasSmallLocalizedHom_of_isLocalization`, `instHasSmallLocalizedHomObjShiftFunctor_3`, `hasSmallLocalizedHom_iff`, `instHasSmallLocalizedHomObjShiftFunctor_2`, `hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀`
`SmallHom` 📖	CompOp	10 math math: `SmallHom.equiv_equiv_symm`, `SmallHom.equiv_mkInv`, `SmallHom.equiv_mk`, `SmallShiftedHom.equiv_shift'`, `CategoryTheory.LocalizerMorphism.equiv_smallHomMap'`, `SmallHom.equiv_chgUniv`, `SmallHom.equiv_comp`, `CategoryTheory.LocalizerMorphism.equiv_smallHomMap`, `SmallHom.equiv_shift`, `SmallShiftedHom.equiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSmallLocalizedHom_iff` 📖	mathematical	—	`HasSmallLocalizedHom` `Small` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`small_map` `HasSmallLocalizedHom.small` `CategoryTheory.Functor.q_isLocalization`
`hasSmallLocalizedHom_iff_of_isos` 📖	mathematical	—	`HasSmallLocalizedHom`	—	`hasSmallLocalizedHom_iff` `CategoryTheory.Functor.q_isLocalization` `small_congr`
`hasSmallLocalizedHom_iff_source` 📖	mathematical	—	`HasSmallLocalizedHom`	—	`hasSmallLocalizedHom_iff` `CategoryTheory.Functor.q_isLocalization` `small_congr`
`hasSmallLocalizedHom_iff_target` 📖	mathematical	—	`HasSmallLocalizedHom`	—	`hasSmallLocalizedHom_iff` `CategoryTheory.Functor.q_isLocalization` `small_congr`
`hasSmallLocalizedHom_of_isLocalization` 📖	mathematical	—	`HasSmallLocalizedHom`	—	`hasSmallLocalizedHom_iff` `small_self`
`hasSmallLocalizedHom_of_isos` 📖	mathematical	—	`HasSmallLocalizedHom`	—	`hasSmallLocalizedHom_iff_of_isos`
`small_of_hasSmallLocalizedHom` 📖	mathematical	—	`Small` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`hasSmallLocalizedHom_iff`

CategoryTheory.Localization.HasSmallLocalizedHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`small` 📖	mathematical	—	`Small` `Quiver.Hom` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.Q`	—	—

CategoryTheory.Localization.SmallHom

Definitions

Name	Category	Theorems
`chgUniv` 📖	CompOp	1 math math: `equiv_chgUniv`
`comp` 📖	CompOp	9 math math: `CategoryTheory.LocalizerMorphism.smallHomMap_comp`, `comp_mk_id`, `mk_comp_mk`, `comp_assoc`, `equiv_comp`, `CategoryTheory.LocalizerMorphism.smallHomMap'_comp`, `mk_comp_mkInv`, `mk_id_comp`, `mkInv_comp_mk`
`equiv` 📖	CompOp	10 math math: `equiv_equiv_symm`, `equiv_mkInv`, `equiv_mk`, `CategoryTheory.Localization.SmallShiftedHom.equiv_shift'`, `CategoryTheory.LocalizerMorphism.equiv_smallHomMap'`, `equiv_chgUniv`, `equiv_comp`, `CategoryTheory.LocalizerMorphism.equiv_smallHomMap`, `equiv_shift`, `CategoryTheory.Localization.SmallShiftedHom.equiv_apply`
`mk` 📖	CompOp	—
`mkInv` 📖	CompOp	3 math math: `equiv_mkInv`, `mk_comp_mkInv`, `mkInv_comp_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_assoc` 📖	mathematical	—	`comp`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_comp` `CategoryTheory.Category.assoc`
`comp_mk_id` 📖	mathematical	—	`comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`equiv_chgUniv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Localization.SmallHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `chgUniv`	—	`CategoryTheory.Functor.q_isLocalization` `Equiv.surjective` `Equiv.apply_symm_apply` `equiv_equiv_symm`
`equiv_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Localization.SmallHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `comp` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.Localization.HasSmallLocalizedHom.small` `Equiv.surjective` `CategoryTheory.Functor.q_isLocalization` `Equiv.symm_apply_apply` `CategoryTheory.Localization.homEquiv_refl` `CategoryTheory.Localization.homEquiv_comp`
`equiv_equiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Localization.SmallHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `Equiv.symm` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Localization.HasSmallLocalizedHom.small` `Equiv.symm_apply_apply` `CategoryTheory.Localization.homEquiv_trans` `CategoryTheory.Localization.homEquiv_eq`
`equiv_mk` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Localization.SmallHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Localization.HasSmallLocalizedHom.small` `CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Localization.homEquiv_refl` `Equiv.symm_apply_apply` `CategoryTheory.Localization.homEquiv_map`
`equiv_mkInv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Localization.SmallHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `mkInv` `CategoryTheory.Iso.inv` `CategoryTheory.Localization.isoOfHom`	—	`CategoryTheory.Localization.HasSmallLocalizedHom.small` `CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Localization.homEquiv_isoOfHom_inv` `Equiv.symm_apply_apply`
`mkInv_comp_mk` 📖	mathematical	—	`comp` `mkInv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_comp` `equiv_mkInv` `CategoryTheory.Localization.isoOfHom_inv_hom_id` `CategoryTheory.Functor.map_id`
`mk_comp_mk` 📖	mathematical	—	`comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_comp` `CategoryTheory.Functor.map_comp`
`mk_comp_mkInv` 📖	mathematical	—	`comp` `mkInv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_comp` `equiv_mkInv` `CategoryTheory.Localization.isoOfHom_hom_inv_id` `CategoryTheory.Functor.map_id`
`mk_id_comp` 📖	mathematical	—	`comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
`smallHomMap` 📖	CompOp	3 math math: `smallHomMap_comp`, `smallHomMap_mk`, `equiv_smallHomMap`
`smallHomMap'` 📖	CompOp	3 math math: `equiv_smallHomMap'`, `smallHomMap'_mk`, `smallHomMap'_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_smallHomMap` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Localization.SmallHom` `CategoryTheory.Functor.obj` `functor` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Localization.SmallHom.equiv` `smallHomMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.q_isLocalization` `Equiv.surjective` `Equiv.apply_symm_apply` `CategoryTheory.Localization.SmallHom.equiv_equiv_symm` `CategoryTheory.Localization.liftNatTrans_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.NatIso.naturality_1` `CategoryTheory.cancel_epi` `CategoryTheory.IsSplitEpi.epi` `CategoryTheory.IsSplitEpi.of_iso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.instIsSplitEpiMap` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Iso.hom_inv_id_app_assoc` `CategoryTheory.Iso.inv_hom_id_app`
`equiv_smallHomMap'` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Localization.SmallHom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Localization.SmallHom.equiv` `smallHomMap'` `CategoryTheory.CategoryStruct.comp` `functor` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`CategoryTheory.Localization.hasSmallLocalizedHom_of_isos` `CategoryTheory.Localization.SmallHom.equiv_comp` `equiv_smallHomMap` `CategoryTheory.Category.assoc`
`smallHomMap'_comp` 📖	mathematical	—	`smallHomMap'` `CategoryTheory.Localization.SmallHom.comp`	—	`CategoryTheory.Localization.hasSmallLocalizedHom_of_isos` `smallHomMap_comp` `CategoryTheory.Localization.SmallHom.comp_assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Localization.SmallHom.mk_id_comp`
`smallHomMap'_mk` 📖	mathematical	—	`smallHomMap'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `functor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	—
`smallHomMap_comp` 📖	mathematical	—	`smallHomMap` `CategoryTheory.Localization.SmallHom.comp` `CategoryTheory.Functor.obj` `functor`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_smallHomMap` `CategoryTheory.Localization.SmallHom.equiv_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`smallHomMap_mk` 📖	mathematical	—	`smallHomMap` `CategoryTheory.Functor.obj` `functor` `CategoryTheory.Functor.map`	—	`Equiv.injective` `CategoryTheory.Functor.q_isLocalization` `equiv_smallHomMap` `CategoryTheory.CatCommSq.iso_inv_naturality` `CategoryTheory.Iso.hom_inv_id_app_assoc`

---

← Back to Index