category_theory.finrank_hom_simple_simple_le_one source