old_structure_cmd in morphism type classes

Stream: general

[Frédéric Dupuis]

I just stumbled into an issue in the morphism type classes: we never standardized on whether to use the old structure command or not when defining these classes. This creates problems when a new morphism class extends two other ones that use opposite conventions in this respect. For example, continuous_semilinear_map_class extends semilinear_map_class which uses the old structure command and continuous_map which does not. Here's the sort of problem it can create:

import topology.algebra.module.basic

variables {M R : Type*} [add_comm_group M] [ring R] [topological_space M] [module R M]

example {F : Type*} [continuous_linear_map_class F R M M] (f : F) : true  :=
begin
  have h : f (0 + 0) = f 0 + f 0 := map_add f 0 0,
  sorry
end

The have fails because Lean is trying to find a coercion to a function via the two different possible pathways.

I think we should standardize on using the old structure command throughout, because it's much nicer to have the coe field directly in the structure rather than buried under possibly several levels of structure, but I thought this should be discussed here. (I already opened #16164 when I thought the problem was restricted to continuous_map_class, but clearly it's not.)

[Yaël Dillies]

Yeah, Anne and I came to the same conclusion several months ago but nothing has been done since.

[Eric Wieser]

I thought when we had this discussion last it was referring to the structures, not the typeclasses? (Perhaps you're not referring to the discussion on the centroid PR that I'm thinking of)