Commit 2023-03-07 17:18 8de86ddd

View on Github →

feat: port CategoryTheory.Limits.ExactFunctor (#2697)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/FullSubcategory.lean

Created Mathlib/CategoryTheory/Limits/ExactFunctor.lean

added def CategoryTheory.ExactFunctor.forget

added theorem CategoryTheory.ExactFunctor.forget_map

added theorem CategoryTheory.ExactFunctor.forget_obj

added theorem CategoryTheory.ExactFunctor.forget_obj_of

added def CategoryTheory.ExactFunctor.of

added theorem CategoryTheory.ExactFunctor.of_fst

added def CategoryTheory.ExactFunctor

added def CategoryTheory.LeftExactFunctor.forget

added theorem CategoryTheory.LeftExactFunctor.forget_map

added theorem CategoryTheory.LeftExactFunctor.forget_obj

added theorem CategoryTheory.LeftExactFunctor.forget_obj_of

added def CategoryTheory.LeftExactFunctor.of

added def CategoryTheory.LeftExactFunctor.ofExact

added theorem CategoryTheory.LeftExactFunctor.ofExact_map

added theorem CategoryTheory.LeftExactFunctor.ofExact_obj

added theorem CategoryTheory.LeftExactFunctor.of_fst

added def CategoryTheory.LeftExactFunctor

added def CategoryTheory.RightExactFunctor.forget

added theorem CategoryTheory.RightExactFunctor.forget_map

added theorem CategoryTheory.RightExactFunctor.forget_obj

added theorem CategoryTheory.RightExactFunctor.forget_obj_of

added def CategoryTheory.RightExactFunctor.of

added def CategoryTheory.RightExactFunctor.ofExact

added theorem CategoryTheory.RightExactFunctor.ofExact_map

added theorem CategoryTheory.RightExactFunctor.ofExact_obj

added theorem CategoryTheory.RightExactFunctor.of_fst

added def CategoryTheory.RightExactFunctor