instances on continuous subtype

Stream: general

[Anatole Dedecker]

In #8004, @Heather Macbeth suggested to remove the monoid, group, and ring instances on { f : α → β | continuous f }. The idea is that the corresponding instances on continuous_map α β should be used instead. But we would keep the fact that { f : α → β | continuous f } is a sub[monoid, group, ring] of α → β, because this can't be expressed with the bundled continuous_map. Is there a good reason to keep them ?

(cc @Scott Morrison @Nicolò Cavalleri )

[Eric Wieser]

I can't help feeling those instances have a typo and should be spelt with // not |

[Eric Wieser]

Because the current spelling just introduced an annoying coe_sort ∘ set_of

[Eric Wieser]

I'm increasingly becoming of the opinion that it would actually be easier to handle bundled homs if add_monoid_hom were defeq to subtype is_add_monoid_hom because then you can reuse all sorts of results about subtypes, and you can then prove things like (unit →* unit) = (unit →+ unit)!

[Anatole Dedecker]

I think the idea is that you need a set if you want to say is_subgroup, so it makes sense to state everything in term of the set

[Anatole Dedecker]

Eric Wieser said:

I'm increasingly becoming of the opinion that it would actually be easier to handle bundled homs if add_monoid_hom were defeq to subtype is_add_monoid_hom because then you can reuse all sorts of results about subtypes.

All of those is_... are deprecated anyway. The original goal of the PR was to remove them from this file

[Eric Wieser]

I'm referring to a hypothetical non-class is_add_monoid_hom not the one that already exists

[Anatole Dedecker]

Oh okay, I see what you mean now. I'm not experimented enough to have an opinion on that, but I get your point.

[Eric Wieser]

On the other hand "this vestigial code bears a resemblance to a large refactor that might be a good idea" isn't a particularly good argument to keep it around

[Eric Wieser]

Perhaps try making a follow-up PR to remove them all and see what if anything breaks?

[Eric Wieser]

The refactor in question is analogous to the one I'm attempting in #7834 (except not for continuous but measurable), while the instances you're proposing be removed are analogous to the ones I'm proposing be added in #7833

[Anatole Dedecker]

Wait I'm not sure to understand anymore :sweat_smile: I thought you were talking about removing the unbundled and already deprecated algebraic typeclasses :thinking:
Also, the idea is to remove them because they already exist for bundled continuous_maps, which are supposed to be used instead of subtype continuous, so your work on subtypes would only apply if we decided to switch back to subtype continuous > continuous_map.

I'm sorry if I'm misunderstanding something, which is possible since I'm not a native english speaker :sweat_smile:

[Scott Morrison]

Re: the original question --- I'm in favor of removing the instances. I think they predate meaningful development/usage of continuous_map.

[Nicolò Cavalleri]

I am also in favor of removing them: I was proposing to tag them as deprecated in PR #7844, but then people did not want to do that because it had nothing to do with the rest of the PR

[Nicolò Cavalleri]

I think Scott was thinking it was better to remove them one year ago but at the time continuous_map was just born and part of the library that is now written in terms of continuous_map was written with the subtype, so it was too early to do that if I recall correctly