Variables, and picking typeclass instances

Stream: new members

[Philippe Duchon]

The recent discussion on variables made me think of this question.

Say I want to work with a specific instance of a typeclass. How do I make this clear to Lean?

Say, for instance, I want to work with formal power series: I have some ring R of coefficients, but I want the discrete topology on it so I can use the product topology. If I just write variable {R: Type*} [TopologicalSpace R], Lean will expect, based on what my concrete R is (probably the rationals, or the reals, or the complexes; with the integers, default typeclass synthesis would probably pick the one I want), to infer a topology on this, but this won't be the one I had in mind - and neither will the product topology on power series.

So, in a sense, I would like to say, "in this section, if you ever need a TopologicalSpace R, this is the one I have in mind". Now that I rephrase it this way, this is probably a very dumb question...

[Aaron Liu]

Do you want variable {R : Type*} [TopologicalSpace R] [DiscreteTopology R]?

[Aaron Liu]

Or do you want a type synonym to equip a type with the discrete topology

[Kevin Buzzard]

You might find that power series rings have got an optional topology which you can "switch on" which doesn't ask for a topology on R at all, but puts the maximal-ideal-adic topology on the power series ring.

[Philippe Duchon]

The topology example was just one that seemed to fit the question (a case where the exact wanted instance of a typeclass might reasonably depend on the situation); my question was more general in spirit.

[Kevin Buzzard]

The general solutions are type synonyms and prop-valued classes such as [Discrete topology R] or [IsModuleTopology R]

[Kevin Buzzard]

Similarly in measure theory there is [BorelSpace X] to say 'this arbitrary sigma algebra you just attached to this topological space is the Borel sigma algebra"