Commit 2024-09-07 08:37 ce32dd9c

View on Github →

feat(Category/Basic): make mono_comp and epi_comp instances and golf proofs (#16530) This PR attempts to make mono_comp and epi_comp instances.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Generators.lean

Modified Mathlib/Algebra/Homology/HomologySequenceLemmas.lean

Modified Mathlib/Algebra/Homology/ImageToKernel.lean

Modified Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

Modified Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

Modified Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

Modified Mathlib/CategoryTheory/Category/Basic.lean

added theorem CategoryTheory.cancel_epi_assoc_iff

added theorem CategoryTheory.cancel_mono_assoc_iff

deleted theorem CategoryTheory.epi_comp

modified theorem CategoryTheory.epi_of_epi

deleted theorem CategoryTheory.mono_comp

modified theorem CategoryTheory.mono_of_mono

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Images.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

Modified Mathlib/CategoryTheory/Simple.lean

Modified Mathlib/CategoryTheory/Subobject/Limits.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean