Documentation Verification Report

HomCongr

📁 Source: Mathlib/CategoryTheory/HomCongr.lean

Statistics

Metric	Count
Definitions `homCongr`, `isoCongr`, `isoCongrLeft`, `isoCongrRight`	4
Theorems `map_homCongr`, `map_isoCongr`, `homCongr_apply`, `homCongr_comp`, `homCongr_refl`, `homCongr_symm`, `homCongr_symm_apply`, `homCongr_trans`, `isoCongr_apply`, `isoCongr_symm_apply`	10
Total	14

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_homCongr` 📖	mathematical	—	`map` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Iso.homCongr` `obj` `mapIso`	—	`map_comp`
`map_isoCongr` 📖	mathematical	—	`mapIso` `DFunLike.coe` `Equiv` `CategoryTheory.Iso` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Iso.isoCongr` `obj`	—	`mapIso_trans`

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`homCongr` 📖	CompOp	9 math math: `CategoryTheory.Functor.map_homCongr`, `ModuleCat.Iso.homCongr_eq_arrowCongr`, `SemimoduleCat.Iso.homCongr_eq_arrowCongr`, `homCongr_trans`, `homCongr_comp`, `homCongr_refl`, `homCongr_apply`, `homCongr_symm_apply`, `homCongr_symm`
`isoCongr` 📖	CompOp	3 math math: `isoCongr_symm_apply`, `CategoryTheory.Functor.map_isoCongr`, `isoCongr_apply`
`isoCongrLeft` 📖	CompOp	—
`isoCongrRight` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `homCongr` `CategoryTheory.CategoryStruct.comp` `inv` `hom`	—	—
`homCongr_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `homCongr` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.Category.assoc` `hom_inv_id_assoc`
`homCongr_refl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `homCongr` `refl`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`homCongr_symm` 📖	mathematical	—	`Equiv.symm` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `homCongr` `symm`	—	—
`homCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homCongr` `CategoryTheory.CategoryStruct.comp` `hom` `inv`	—	—
`homCongr_trans` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `homCongr` `trans` `Equiv.trans`	—	`CategoryTheory.Category.assoc`
`isoCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Iso` `EquivLike.toFunLike` `Equiv.instEquivLike` `isoCongr` `trans` `symm`	—	—
`isoCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Iso` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `isoCongr` `trans` `symm`	—	—

---

← Back to Index