Commit 2024-04-29 12:02 a547a94f

View on Github →

feat(CategoryTheory/Category/RelCat): Show basic facts and self-duality of category of relations. (#11241) Add facts about rel somewhat like the facts about types, classify isos in rel, construct the inclusion from types to rel, show self-duality of rel.

Estimated changes

Modified Mathlib/CategoryTheory/Category/RelCat.lean

added theorem CategoryTheory.RelCat.Hom.rel_comp_apply₂

added theorem CategoryTheory.RelCat.Hom.rel_id_apply₂

added def CategoryTheory.RelCat.graphFunctor

added theorem CategoryTheory.RelCat.graphFunctor_map

added theorem CategoryTheory.RelCat.hom_ext

added def CategoryTheory.RelCat.opEquivalence

added def CategoryTheory.RelCat.opFunctor

added theorem CategoryTheory.RelCat.opFunctor_comp_unopFunctor_eq

added theorem CategoryTheory.RelCat.rel_iso_iff

added def CategoryTheory.RelCat.unopFunctor

added theorem CategoryTheory.RelCat.unopFunctor_comp_opFunctor_eq

Modified Mathlib/Data/Rel.lean

added theorem Function.graph_inj

added theorem Function.graph_injective