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	12 math math: CategoryTheory.Functor.map_homCongr, ModuleCat.Iso.homCongr_eq_arrowCongr, SemimoduleCat.Iso.homCongr_eq_arrowCongr, homCongr_trans, homCongr_comp, homCongr_refl, CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left, homCongr_apply, homCongr_symm_apply, homCongr_symm, CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left, CategoryTheory.Equivalence.symmEquivInverse_map_app
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