Documentation Verification Report

RelCat

📁 Source: Mathlib/CategoryTheory/Category/RelCat.lean

Statistics

Metric	Count
Definitions `RelCat`, `rel`, `graphFunctor`, `instLargeCategory`, `opEquivalence`, `opFunctor`, `unopFunctor`, `instInhabitedRelCat`	8
Theorems `ext`, `ext_iff`, `rel_comp`, `rel_comp_apply₂`, `rel_id`, `rel_id_apply₂`, `graphFunctor_essSurj`, `graphFunctor_faithful`, `graphFunctor_obj`, `instIsEquivalenceOppositeOpFunctor`, `instIsEquivalenceOppositeUnopFunctor`, `opEquivalence_counitIso`, `opEquivalence_functor`, `opEquivalence_inverse`, `opEquivalence_unitIso`, `opFunctor_comp_unopFunctor_eq`, `rel_graphFunctor_map`, `rel_iso_iff`, `unopFunctor_comp_opFunctor_eq`	19
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
`RelCat` 📖	CompOp	17 math math: `RelCat.graphFunctor_essSurj`, `RelCat.rel_graphFunctor_map`, `RelCat.instIsEquivalenceOppositeUnopFunctor`, `RelCat.unopFunctor_comp_opFunctor_eq`, `RelCat.graphFunctor_obj`, `RelCat.Hom.rel_id_apply₂`, `RelCat.opEquivalence_functor`, `RelCat.graphFunctor_faithful`, `RelCat.opEquivalence_counitIso`, `RelCat.opEquivalence_inverse`, `RelCat.Hom.rel_comp_apply₂`, `RelCat.opFunctor_comp_unopFunctor_eq`, `RelCat.rel_iso_iff`, `RelCat.Hom.rel_comp`, `RelCat.instIsEquivalenceOppositeOpFunctor`, `RelCat.Hom.rel_id`, `RelCat.opEquivalence_unitIso`
`instInhabitedRelCat` 📖	CompOp	—

CategoryTheory.RelCat

Definitions

Name	Category	Theorems
`graphFunctor` 📖	CompOp	5 math math: `graphFunctor_essSurj`, `rel_graphFunctor_map`, `graphFunctor_obj`, `graphFunctor_faithful`, `rel_iso_iff`
`instLargeCategory` 📖	CompOp	17 math math: `graphFunctor_essSurj`, `rel_graphFunctor_map`, `instIsEquivalenceOppositeUnopFunctor`, `unopFunctor_comp_opFunctor_eq`, `graphFunctor_obj`, `Hom.rel_id_apply₂`, `opEquivalence_functor`, `graphFunctor_faithful`, `opEquivalence_counitIso`, `opEquivalence_inverse`, `Hom.rel_comp_apply₂`, `opFunctor_comp_unopFunctor_eq`, `rel_iso_iff`, `Hom.rel_comp`, `instIsEquivalenceOppositeOpFunctor`, `Hom.rel_id`, `opEquivalence_unitIso`
`opEquivalence` 📖	CompOp	4 math math: `opEquivalence_functor`, `opEquivalence_counitIso`, `opEquivalence_inverse`, `opEquivalence_unitIso`
`opFunctor` 📖	CompOp	5 math math: `unopFunctor_comp_opFunctor_eq`, `opEquivalence_functor`, `opEquivalence_counitIso`, `opFunctor_comp_unopFunctor_eq`, `instIsEquivalenceOppositeOpFunctor`
`unopFunctor` 📖	CompOp	5 math math: `instIsEquivalenceOppositeUnopFunctor`, `unopFunctor_comp_opFunctor_eq`, `opEquivalence_counitIso`, `opEquivalence_inverse`, `opFunctor_comp_unopFunctor_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`graphFunctor_essSurj` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `CategoryTheory.RelCat` `CategoryTheory.types` `instLargeCategory` `graphFunctor`	—	`CategoryTheory.Functor.essSurj_of_surj`
`graphFunctor_faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.types` `CategoryTheory.RelCat` `instLargeCategory` `graphFunctor`	—	`Function.graph_injective`
`graphFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.RelCat` `instLargeCategory` `graphFunctor`	—	—
`instIsEquivalenceOppositeOpFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.RelCat` `instLargeCategory` `Opposite` `CategoryTheory.Category.opposite` `opFunctor`	—	`CategoryTheory.Equivalence.isEquivalence_functor`
`instIsEquivalenceOppositeUnopFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `Opposite` `CategoryTheory.RelCat` `CategoryTheory.Category.opposite` `instLargeCategory` `unopFunctor`	—	`CategoryTheory.Equivalence.isEquivalence_inverse`
`opEquivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.RelCat` `Opposite` `instLargeCategory` `CategoryTheory.Category.opposite` `opEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `unopFunctor` `opFunctor`	—	—
`opEquivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.RelCat` `Opposite` `instLargeCategory` `CategoryTheory.Category.opposite` `opEquivalence` `opFunctor`	—	—
`opEquivalence_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.RelCat` `Opposite` `instLargeCategory` `CategoryTheory.Category.opposite` `opEquivalence` `unopFunctor`	—	—
`opEquivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.RelCat` `Opposite` `instLargeCategory` `CategoryTheory.Category.opposite` `opEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	—
`opFunctor_comp_unopFunctor_eq` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CategoryTheory.RelCat` `instLargeCategory` `Opposite` `CategoryTheory.Category.opposite` `opFunctor` `unopFunctor` `CategoryTheory.Functor.id`	—	—
`rel_graphFunctor_map` 📖	mathematical	—	`Hom.rel` `CategoryTheory.Functor.map` `CategoryTheory.types` `CategoryTheory.RelCat` `instLargeCategory` `graphFunctor` `Function.graph`	—	—
`rel_iso_iff` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.RelCat` `instLargeCategory` `CategoryTheory.Iso` `CategoryTheory.types` `CategoryTheory.Functor.map` `graphFunctor` `CategoryTheory.Iso.hom`	—	`CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.IsIso.inv_hom_id` `CategoryTheory.types_ext` `Hom.ext` `Set.ext` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Iso.isIso_hom`
`unopFunctor_comp_opFunctor_eq` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.RelCat` `CategoryTheory.Category.opposite` `instLargeCategory` `unopFunctor` `opFunctor` `CategoryTheory.Functor.id`	—	—

CategoryTheory.RelCat.Hom

Definitions

Name	Category	Theorems
`rel` 📖	CompOp	6 math math: `CategoryTheory.RelCat.rel_graphFunctor_map`, `rel_id_apply₂`, `rel_comp_apply₂`, `ext_iff`, `rel_comp`, `rel_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`rel`	—	—	—
`ext_iff` 📖	mathematical	—	`rel`	—	`ext`
`rel_comp` 📖	mathematical	—	`rel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.RelCat` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.RelCat.instLargeCategory` `SetRel.comp`	—	—
`rel_comp_apply₂` 📖	mathematical	—	`SetRel` `Set.instMembership` `rel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.RelCat` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.RelCat.instLargeCategory`	—	—
`rel_id` 📖	mathematical	—	`rel` `CategoryTheory.CategoryStruct.id` `CategoryTheory.RelCat` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.RelCat.instLargeCategory` `SetRel.id`	—	—
`rel_id_apply₂` 📖	mathematical	—	`SetRel` `Set.instMembership` `rel` `CategoryTheory.CategoryStruct.id` `CategoryTheory.RelCat` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.RelCat.instLargeCategory`	—	—

---

← Back to Index