Deprecated ContinuousMap lemmas

Stream: mathlib4

[Winston Yin (尹維晨)]

I see a number of lemmas (e.g. docs#ContinuousMap.continuous) that are marked as deprecated in the docstring itself but not using @[deprecated]. Could somebody shed some light on this please? From git blame, let me ping @Yury G. Kudryashov

[Aaron Liu]

I'm still not sure whether I'm supposed to use them or not

[Yury G. Kudryashov]

We should migrate from these lemmas to ContinuousMapClass lemmas some day.

[Winston Yin (尹維晨)]

If this is a todo for the future, would you kindly document the plan in the docs, so someone else can also pick it up?

[Yury G. Kudryashov]

The plan is to migrate Mathlib to lemmas like map_continuous, then officially deprecate these lemmas using @[deprecated].

[Yury G. Kudryashov]

Let me try to do it now.

[Yury G. Kudryashov]

I've started #30790. I'm not sure about congr_fun/congr_arg: we have them for some bundled homs, but not for other.

[Yury G. Kudryashov]

So, I've started with ContinuousMap.continuous. It's used in many files. I've migrated some of them, I'll continue tonight after hours.

[Winston Yin (尹維晨)]

Thank you, Yury

[Robert Maxton]

Wait, why are we deprecating ContinuousMap.continuous? I will very much miss the ability to use projection notation in continuity proofs; I don't suppose we could make it an alias of some kind instead?

[Winston Yin (尹維晨)]

I have no opinions one way or another. I started the thread just to resolve the doc comments stating these lemmas are deprecated.

[Yury G. Kudryashov]

We deprecated, then removed, lemmas like AddMonoidHom.map_add. Why continuity is any different?

[Aaron Liu]

well map_add is an existing alternative lemma to use but continuous is not

[Aaron Liu]

it doesn't exist

[Yury G. Kudryashov]

docs#map_continuous

[Yury G. Kudryashov]

Sorry, docs#ContinuousMapClass.map_continuous (exported to the root NS)

[Yaël Dillies]

Yury G. Kudryashov said:

We deprecated, then removed, lemmas like AddMonoidHom.map_add. Why continuity is any different?

There is evidence that this was a mistake because map_add is much costlier in typeclass search than AddMonoidHom.map_add was

[Artie Khovanov]

hm
what is the solution to the resulting duplicated API?

[Yury G. Kudryashov]

Yaël Dillies said:

Yury G. Kudryashov said:

We deprecated, then removed, lemmas like AddMonoidHom.map_add. Why continuity is any different?

There is evidence that this was a mistake because map_add is much costlier in typeclass search than AddMonoidHom.map_add was

What do you suggest? Drop all of *HomClasses and go back to *Hom.map_add etc? Something else?

[Yury G. Kudryashov]

For now, I'm going to cherry-pick parts of my PR that make sense no matter what we decide to do with these lemmas, and postpone the rest.

[Andrew Yang]

I think it doesn't hurt to keep both?

[Andrew Yang]

(I am talking about *Hom.map_add. I don't have enough experience with ContinuousMapClass to have an opinion here)

[Yury G. Kudryashov]

So, the suggestion is to keep both of them, use _root_.map_* in simp lemmas but allow usage of *Hom.map_* in manual rw/simp only/apply?