Commit 2026-09-07 13:06 a120a09d

chore: standardise names for coercions from morphism classes to morphisms (#43367) Following item (2) in #31365, the definition which implements the coercion from a morphism class FooHomClass to FooHoms should be called FooHom.ofClass.

• the name is easy to remember and guess
• it matches the existing names we have for the corresponding declarations for subobjects
• when Lean expects a FooHom, you can write .ofClass f. Make five more morphism classes follow this pattern.