Actions on SeparationQuotient

Stream: mathlib4

[Yury G. Kudryashov]

I'm going to introduce the instance

variable {M X : Type*} [SMul M X] [TopologicalSpace X]

instance instSMul [ContinuousConstSMul M X] : SMul M (SeparationQuotient X) where
  smul c := Quotient.map' (c • ·) fun _ _ h ↦ Inseparable.map h (continuous_const_smul c)

as well as algebraic operations on SeparationQuotient X. Should I also introduce this instance?

instance instSMul' [ContinuousSMul M X] : SMul (SeparationQuotient M) (SeparationQuotient X) := _

It may probably lead to diamonds, if we take SeparationQuotient (SeparationQuotient X). Should we care about this? Are there any other reasons to avoid it? @Eric Wieser

[Yury G. Kudryashov]

For my goals, I don't need it but it looks like a natural generalization of Mul (SeparationQuotient X).

[Anatole Dedecker]

SeparationQuotient is idempotent, so I think the risk of diamonds actually occuring in practice is quite low?

[Eric Wieser]

Generally [SMul A B] : SMul (F A) (F B) instances are a bad idea

[Eric Wieser]

We have them in a few places anyway, but they cause non-propeq diamonds. I think I shared a thesis chapter in another thread that discusses this further.

[Anatole Dedecker]

Yes I agree, e.g it's not clear what the action of Set Real on Set (Set Real) is. My point is that these issues only arise once you apply your F at least twice, and I don't see why one would do this with SeparationQuotient.

[Eric Wieser]

Maybe in this case the actions are propeq anyway, if it's really idempotent?

[Anatole Dedecker]

I think so yes.

[Yury G. Kudryashov]

Of course, it's idempotent up to an equivalence.

[Yury G. Kudryashov]

The second time you apply it, you take a quotient by the bot setoid.

[Yury G. Kudryashov]

I'll avoid the SMul (SeparationQuotient M) (SeparationQuotient X) instance for now.