Commit 2026-09-07 19:40 6ff5028b

refactor: make several NonUnitalStarSubalgebra(Hom) definitions take a particular algebra homomorphism (#43377) as opposed to a NonUnitalAlgHomClass and StarHomClass. Specifically, this PR changes NonUnitalStarSubalgebra.{map, comap} as well as NonUnitalStarSubalgebra.{range,rangeRestrict,codRestrict,equalizer,ofLeftInverse'}. Since this removes all uses of a bundled morphism class, we also remove the assocated variable lines and align them with standard mathlib style. Adapt (almost) all theorems about them to take in a concrete morphism also. This follows the general patterns established in #31365:

we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions. Given a definition Bar that takes FooHom as an argument, a theorem whose statement involves Bar should only ever be written for FooHoms and never FooHomClasses. Indeed in the latter case, the statement would require the coercion from the morphism class to the morphism, thereby making it less general.