Commit 2023-02-21 07:40 c2ce561f

View on Github →

feat: Port CategoryTheory.DiscreteCategory (#2326) Still WIP. Help would be much appreciated!

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/DiscreteCategory.lean

added def CategoryTheory.Discrete.compNatIsoDiscrete

added theorem CategoryTheory.Discrete.eq_of_hom

added def CategoryTheory.Discrete.equivOfEquivalence

added def CategoryTheory.Discrete.equivalence

added def CategoryTheory.Discrete.functor

added def CategoryTheory.Discrete.functorComp

added theorem CategoryTheory.Discrete.functor_map

added theorem CategoryTheory.Discrete.functor_map_id

added theorem CategoryTheory.Discrete.functor_obj

added theorem CategoryTheory.Discrete.id_def

added theorem CategoryTheory.Discrete.mk_as

added def CategoryTheory.Discrete.natIso

added def CategoryTheory.Discrete.natIsoFunctor

added theorem CategoryTheory.Discrete.natIso_app

added def CategoryTheory.Discrete.natTrans

added structure CategoryTheory.Discrete

added def CategoryTheory.discreteEquiv