Documentation Verification Report

HomEquiv

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

Statistics

Metric	Count
Definitions `HomEquiv`, `homEquiv`, `homMap`	3
Theorems `homEquiv_apply`, `homEquiv_comp`, `homEquiv_eq`, `homEquiv_id`, `homEquiv_isoOfHom_inv`, `homEquiv_map`, `homEquiv_refl`, `homEquiv_symm_apply`, `homEquiv_trans`, `homMap_apply`, `homMap_apply_assoc`, `homMap_comp`, `homMap_comp_assoc`, `homMap_homMap`, `homMap_id`, `homMap_map`, `id_homMap`	17
Total	20

CategoryTheory.FreeMonoidalCategory

Definitions

Name	Category	Theorems
`HomEquiv` 📖	CompData	—

CategoryTheory.Localization

Definitions

Name	Category	Theorems
`homEquiv` 📖	CompOp	11 math math: `homEquiv_eq`, `homEquiv_comp`, `homEquiv_symm_apply`, `homEquiv_apply`, `homEquiv_refl`, `homEquiv_trans`, `structuredArrowEquiv_symm_apply`, `homEquiv_map`, `homEquiv_isoOfHom_inv`, `homEquiv_id`, `structuredArrowEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.LocalizerMorphism.homMap` `CategoryTheory.LocalizerMorphism.id`	—	—
`homEquiv_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.LocalizerMorphism.homMap_comp`
`homEquiv_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`homEquiv_apply` `CategoryTheory.LocalizerMorphism.homMap_apply` `CategoryTheory.Iso.symm_hom` `CategoryTheory.Iso.symm_inv`
`homEquiv_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.LocalizerMorphism.homMap_id`
`homEquiv_isoOfHom_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.Iso.inv` `isoOfHom`	—	`CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.inv_hom_id` `isoOfHom_hom` `homEquiv_map` `homEquiv_comp` `isoOfHom_inv_hom_id` `homEquiv_id`
`homEquiv_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.Functor.map`	—	`CategoryTheory.LocalizerMorphism.homMap_map`
`homEquiv_refl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv`	—	`CategoryTheory.LocalizerMorphism.id_homMap`
`homEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv`	—	—
`homEquiv_trans` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv`	—	`CategoryTheory.LocalizerMorphism.homMap_homMap`

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
`homMap` 📖	CompOp	9 math math: `homMap_map`, `homMap_id`, `homMap_apply`, `homMap_apply_assoc`, `homMap_comp`, `CategoryTheory.Localization.homEquiv_apply`, `homMap_comp_assoc`, `id_homMap`, `homMap_homMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homMap_apply` 📖	mathematical	—	`homMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `functor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Iso.ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Localization.liftNatTrans_app` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.hom_inv_id_app_assoc` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.assoc`
`homMap_apply_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `functor` `homMap` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homMap_apply`
`homMap_comp` 📖	mathematical	—	`homMap` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `functor`	—	`CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`homMap_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `functor` `homMap`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homMap_comp`
`homMap_homMap` 📖	mathematical	—	`homMap` `CategoryTheory.Functor.obj` `functor` `comp`	—	`homMap_apply` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`homMap_id` 📖	mathematical	—	`homMap` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `functor`	—	`homMap.congr_simp` `CategoryTheory.Functor.map_id` `homMap_map`
`homMap_map` 📖	mathematical	—	`homMap` `CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `functor`	—	`CategoryTheory.CatCommSq.iso_inv_naturality` `CategoryTheory.Iso.hom_inv_id_app_assoc`
`id_homMap` 📖	mathematical	—	`homMap` `id`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `homMap_apply`

---

← Back to Index