Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-06 06:18 7040c50c

View on Github →

feat(category_theory): the opposite of an abelian category is abelian (#7514)

Estimated changes

Created src/category_theory/abelian/opposite.lean

Modified src/category_theory/fin_category.lean

added def category_theory.fin_category_opposite

Modified src/category_theory/limits/opposites.lean

added theorem category_theory.limits.has_finite_colimits_opposite

added theorem category_theory.limits.has_finite_coproducts_opposite

added theorem category_theory.limits.has_finite_limits_opposite

added theorem category_theory.limits.has_finite_products_opposite

Modified src/category_theory/limits/shapes/normal_mono.lean

added def category_theory.normal_epi_of_normal_mono_unop

added def category_theory.normal_mono_of_normal_epi_unop

Modified src/category_theory/limits/shapes/zero.lean

Created src/category_theory/preadditive/opposite.lean

added theorem category_theory.unop_add

added theorem category_theory.unop_zero