smul_assoc_class

Stream: general

[Yaël Dillies]

What do people think of renaming is_scalar_tower to smul_assoc_class? That would make it fit with docs#smul_comm_class, docs#vadd_assoc_class, docs#vadd_comm_class.

[Yaël Dillies]

I've opened #16032 as a demonstration.

[Anne Baanen]

I don't mind either way as long as there are enough pointers from the concept of "tower" to this class. So in the module docs of src/group_theory/group_action/defs.lean and in the definition of smul_assoc_class itself.

[Eric Wieser]

I know we've already started down this road, but I'm not a huge fan of these _class suffices on algebraic typeclasses; they don't help the reader at all, and make everything longer. (I'm happy with them on monoid_hom_class where the suffix means "I am a polymorphic version of the corresponding structure")

[Eric Wieser]

Can we think of other names that avoid these suffices?

[Eric Wieser]

Even smul_associates to me seems marginally more readable than smul_assoc_class

[Eric Wieser]

(other offenders: docs#mul_zero_class, docs#mul_one_class, docs#covariant_class)

[Anne Baanen]

I don't like the _class name very much either, but it is nice how they connect with their contents: docs#vadd_assoc_class just wraps docs#vadd_assoc in a class.

[Eric Wieser]

By that argument we should rename docs#semigroup to mul_assoc_class!

[Anne Baanen]

If there's a well-known existing name then that seems to be obviously better. I'm just saying, as long as we're making up names, we might as well acknowledge the advantages of making up names systematically.

[Bhavik Mehta]

docs#initial_mono_class is another example (I made it and I don't really like its name), it's also I think the only such example in category theory. It's a slightly weird example because this property is true in abelian categories and in toposes (and useful in both), but true for different reasons in each

[Anne Baanen]

In branch#splitting_field-diamond I want to introduce a new class extending has_smul with the hypothesis (smul_zero : ∀ (a : α), a • (0 : β) = 0). In the theme of this thread, anyone have a better name than smul_zero_class?

[Anne Baanen]

Note that docs#smul_with_zero already exists, which in addition contains (zero_smul : ∀ (b : β), 0 • b = 0).

[Yaël Dillies]

Oooh, that would unlock #12880.

[Ruben Van de Velde]

smul_with_zero_right?

[Yaël Dillies]

I like smul_zero_class, personally.

[Anne Baanen]

#16123