Should IsOpen be a class?

Stream: mathlib4

[Kevin Buzzard]

docs#IsClosed is a class, but docs#IsOpen is just a def. Should IsOpen be a class?

The reason I ask is that Antoine has had to articificially use a Fact in docs#RestrictedProduct.isTopologicalRing to insert the openness of a subring into the typeclass system, which means that now I have to insert Facts that things are open in #23542 and David Loeffler has flagged this.

Of course we could avoid Facts by demanding not that the sets were open, but that the complements were closed! But I am not sure I want to go down this route! Do topologists have an opinion on whether IsOpen should be a class?

[Yakov Pechersky]

How about having B map into docs#TopologicalSpace.Opens ?

[Kevin Buzzard]

I don't see how to get this to work. The way RestrictedProduct is set up is

variable {S : ι → Type*} -- subobject type
variable [Π i, SetLike (S i) (R i)]
variable {B : Π i, S i}

and in the applications S i is things like Submonoid (R i) or Subring (R i). Hmm, so in fact it could work if there were an OpenSubring structure like the OpenSubgroup structure. We would perhaps need an OpenSetLike class if we went down this route. It would certainly be a far less painful refactor. @Anatole Dedecker I'm guessing you wrote the TODO here; what do you think about this alternative approach?

[Kevin Buzzard]

I'll also need S i to be Subalgebra R0 (R i) soon in FLT, so we'll also need OpenSubalgebra with this approach. This feels like something which should really be decoupled rather than encouraged.

[Yakov Pechersky]

We already have the original sin of OpenSubgroup so it's hard to say in which direction the slope should be slippery

[Yakov Pechersky]

It seems one has to go either in the direction of IsOpen as a class, or Submonoidal as a class, if one wants to have TC know things like ContinuousMul.

[Sébastien Gouëzel]

IsClosed was changed to be a class to make sure that typeclass inference would notice that the quotient of a normed vector space by a closed subspace is a normed vector space (instead of just pseudo-normed), which is often important. It seems to me that this is the same kind of situation here, so making IsOpen a class looks natural to me.

[Kevin Buzzard]

Yes, here it is the claim that a restricted product of weakly locally compact spaces with respect to open subsets is a weakly locally compact space.

[Anatole Dedecker]

Yes, this is precisely what I had in mind when writing the TODO: we will probably want an instance of DiscreteTopology on the quotient by an open subgroup, so we probably want IsOpen as a class anyways.

[Anatole Dedecker]

Arguably OpenSubgroup/OpenSubmodule/... should work as well, but I think that's a lot of trouble for not that many use cases.

[Anatole Dedecker]

Kevin Buzzard said:

The reason I ask is that Antoine has had to articificially use a Fact in docs#RestrictedProduct.isTopologicalRing to insert the openness of a subring into the typeclass system, which means that now I have to insert Facts that things are open in #23542 and David Loeffler has flagged this.

(Casually learning that I am now called Antoine ! :scream:)

[Eric Wieser]

isOpen vs IsClosed has been discussed before, possible multiple times. I'm not sure there was a clear decision over keeping it as a class vs wrapping it in Fact

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/IsOpen.20vs.2E.20IsClosed/near/416330706

[Kevin Buzzard]

Apologies Anatole! (I am terrible at names)

[Anatole Dedecker]

No worries!