continuous action of submoduleclass terms

Stream: mathlib4

[Kevin Buzzard]

import Mathlib

variable (A : Type*) [Ring A] [TopologicalSpace A] [TopologicalRing A]
variable (R : Subring A)

-- all these exist
#synth Ring R
#synth TopologicalRing R
#synth SMul R A

-- but this fails
--#synth ContinuousSMul R A

instance Subring.instContinuousSMul : ContinuousSMul R A :=
  Topology.IsInducing.continuousSMul Topology.IsInducing.id continuous_subtype_val rfl

I would like this instance and obviously it's harmless because it's a prop (and because R : Subring A I don't think it will cause the kind of problems which subtypes acting on objects sometimes cause right now). But if we have this then probably we should have the submonoid version. But should we have the Submonoidclass version? I'm a bit scared about this because this fails:

variable (A : Type*) [Monoid A] (S : Type*)
  [SetLike S A] [SubmonoidClass S A] (R : S)

#synth Mul R -- yes
-- #synth SMul R A -- no

so if we go down this route I'd have to make that instance and I'm slightly worried that it will cause diamonds (aka I don't really know what I'm doing). However I tested it for submonoids, subrings and subalgebras and in all cases we have

example (r : R) (a : A) : r • a = (r : A) * a := rfl

Is it safe to make the SMul instance on SubmonoidClass?

variable (A : Type*) [Monoid A] (S : Type*)
  [SetLike S A] [SubmonoidClass S A] (R : S)

instance : SMul R A where
  smul r a := (r : A) * a

[Eric Wieser]

This looks safe to me from a diamond perspective

[Eric Wieser]

I guess from a performance perspective you'll have to just try and see

[Eric Wieser]

Actually, I'd expect something more general like

variable (R A : Type*) [SMul R A] (S : Type*)
  [SetLike S R] (s : S)

instance : SMul s A where
  smul r a := (r : R) • a

[Eric Wieser]

Promoting to SubmonoidClass for MulAction etc

[Kevin Buzzard]

That one does scare me though because now the moment you're looking for an action of a subtype on anything you open the door to a wild goose chase which my variant won't let you open.

[Kevin Buzzard]

cf lean taking a long time to fail trying to find SMul Complex Real because of instances like the above

[Eric Wieser]

I think the instance above already exists specialized to Subring and Subalgebra

[Kevin Buzzard]

OK so this is added in #20983 and now in theory it's possible to do some tidying up. For example the instance docs#Subgroup.continuousSMul is now not needed and probably I can remove several more instances. Should I remove them? (I removed this one but not the others, I guess it should probably be an all or nothing move here?) Sounds like it might be a use case for TryAtEachStep if we actually want to find them, although maybe shortcut instances are helpful and fine?

[Eric Wieser]

I'm not sure what our policy is here, in principle we could delete docs#Subring.toRing but we haven't done so

[Kevin Buzzard]

See the benchmarking for #11304 to see what happens when you start deleting instances. Maybe they're good shortcuts? I hadn't realised that this PR was going to take me several hours, but we may as well try and get it right.

[Matthew Ballard]

My guess: this is going to be painful performance-wise. But maybe not! #11304 has to be transient issue. The instructions don't match the wall clock.

[Kevin Buzzard]

My guess is that if I start deleting instances willy-nilly then it is going to be painful performance-wise. But if I just add the new instances I need (which generalize existing instances and which we don't have) and check I've not created any diamonds then I think I'm going to be OK.

[Kevin Buzzard]

Hopefully easy question: how do I get a submonoid from a submonoidclass?

import Mathlib

variable {M : Type*} [Monoid M]

variable {S : Type*} [SetLike S M] (s : S) [SubmonoidClass S M]

example : Submonoid M := s -- not like this, it seems

[Edward van de Meent]

looks like we're missing a toSubMonoid coersion...

[Edward van de Meent]

or actually, those seem to be missing for most of the "sub_" classes?

[Edward van de Meent]

you could use something like SubmonoidClass.subtype s |>.range, maybe?

[Edward van de Meent]

MonoidHom.mrange (SubmonoidClass.subtype s) seems to work

[Edward van de Meent]

but it's not pretty at all

[Artie Khovanov]

@Kevin Buzzard unlike for bundled function classes, there are no "concretisation" maps for bundled subject classes
Instead, the particular instance map is used (eg Subfield.toSubring)
There is no particular reason that this is the case, but it's the design across the library
Pinging @Anne Baanen because I asked them about this before

[Kevin Buzzard]

But I don't have a subfield in my case, I really have a submonoidclass! I don't need the submonoid, I was just trying to golf something.

[Eric Wieser]

What's the application where you actually end up working in the generality of SubmonoidClass?

[Kevin Buzzard]

This is not anything worth worrying about, I just was surprised. The use case was the following: the file Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean currently has

instance distribMulAction [AddMonoid α] [DistribMulAction M α] (S : Submonoid M) :
    DistribMulAction S α :=
  DistribMulAction.compHom _ S.subtype

i.e. a one-line proof, and in the PR proposing the change from Submonoid to SubmonoidClass I change it to

variable {S : Type*} [SetLike S M] (s : S) [SubmonoidClass S M]

instance [AddMonoid α] [DistribMulAction M α] : DistribMulAction s α where
  smul_zero r := smul_zero (r : M)
  smul_add r := smul_add (r : M)

which is a two-line proof. I was wondering if I could reuse the one line proof but for that I need access to Submonoid.subtype.

[Artie Khovanov]

Kevin Buzzard said:

But I don't have a subfield in my case, I really have a submonoidclass! I don't need the submonoid, I was just trying to golf something.

Yeah I understand, I guess I'm saying that in practice nothing nontrivial in Mathlib is ever stated via SubmonoidClass (due to the map you want not existing). I don't have anything against changing this, but it's what I've found after trying to do things your way in the past.