Commit 2024-11-09 16:48 7fc8954d

View on Github →

feat(CategoryTheory): codiscrete categories (#17174) This defines Codiscrete Categories which are dual to Discrete Categories. We also show the codiscrete functor is right adjoint to the objects functor.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/CodiscreteCategory.lean

added def CategoryTheory.Codiscrete.adj

added theorem CategoryTheory.Codiscrete.adj_counit_app

added theorem CategoryTheory.Codiscrete.adj_unit_app

added def CategoryTheory.Codiscrete.counitApp

added def CategoryTheory.Codiscrete.equivFunctorToCodiscrete

added def CategoryTheory.Codiscrete.functor

added def CategoryTheory.Codiscrete.functorOfFun

added def CategoryTheory.Codiscrete.functorToCat

added def CategoryTheory.Codiscrete.invFunctor

added theorem CategoryTheory.Codiscrete.left_triangle_components

added theorem CategoryTheory.Codiscrete.mk_as

added def CategoryTheory.Codiscrete.natIso

added def CategoryTheory.Codiscrete.natIsoFunctor

added def CategoryTheory.Codiscrete.natTrans

added def CategoryTheory.Codiscrete.oppositeEquivalence

added theorem CategoryTheory.Codiscrete.right_triangle_components

added def CategoryTheory.Codiscrete.unitApp

added structure CategoryTheory.Codiscrete

added def CategoryTheory.codiscreteEquiv