Commit 2025-08-14 17:52 fdf4f856
View on Github →chore(AlgebraicTopology/SimplexCategory): cleaning up lemmas about epi/mono (#27968)
Instance Mono and Epi assumptions are made more consistent in lemmas like
theorem len_le_of_mono {x y : SimplexCategory} (f : x ⟶ y) [Mono f] : x.len ≤ y.len
for which f used to be an implicit parameter and Mono f an explicit one.
A few additional lemmas regarding mono and epi in SimplexCategory are added. In particular, it is shown that SimplexCategory is a balanced category.
(This PR also adds a lemma saying that δ i = δ j implies i = j, and similarly for degeneracies.)