Standard for defining a structure as a class

Stream: general

[Keefer Rowan]

In what cases should a structure be defined as a class. E.g. it seems that algebraic structures such as group, ring, etc. are always defined as classes while on the other hand a topological space is not defined as a class. Doesn't defining say Group as a class make it so that every type has one (or zero) "canonical" group structure(s)? This seems like it is generally ok, but might cause problems/confusion. Do we just declare different types for each group structure on the same "underlying set" (in math terms)? E.g. is there a type for $\mathbb{Z}_4$ and a different one for $\mathbb{Z}_2 \times \mathbb{Z}_2$?

[Kevin Buzzard]

This is a really hard question. Fortunately the number of definitions which you'll make in any exposition of a theory is quite small, so you can just ask individually about each case. This is an implementation issue. The general rule is "if there will surely only be one such structure on your type, make it a class". So groups are classes because in general one does not put more than one group structure on a type (=set), and topological spaces are not, at least for some of the exposition, because for some of it people wanted to consider lots of topologies on one set.

[Kevin Buzzard]

But for some definitions (like group homomorphisms), they have been implemented in more than one way -- once using classes and once not, and the community has just experimented and found out which was best. If we'd known from the start, this experiment would not have occurred. There is a directory called deprecated where the bad decisions are put, and a lot of these are class related.

[Patrick Massot]

Keefer Rowan said:

E.g. is there a type for $\mathbb{Z}_4$ and a different one for $\mathbb{Z}_2 \times \mathbb{Z}_2$?

Of course! Why would you want them to be the same?!?

[Kenny Lau]

if you're in ZFC and are a beginner in group theory you might think that they are two group structures on the set {e,a,b,c}

[Kevin Buzzard]

If you're into ZFC then you might think of $\mathbb{Z}_4$ as being a group structure on $\{0,1,2,3\}$ and $\mathbb{Z}_2^2$ as being a group structure on $\{0,1\}^2$.

[Reid Barton]

topological_space is actually made into a class shortly after its definition. This style gives the field accessors more convenient types for when one does want to consider topologies explicitly as objects (mostly indeed because one wants to consider multiple topologies on the same type).

[Keefer Rowan]

Maybe the $\mathbb{Z}_2^2$ example wasn't the best since @Kevin Buzzard 's point holds, I just wanted a simple example of distinct algebraic structures that could be realized on the same underlying set.

[Kevin Buzzard]

Did you know that $\mathbb{N}=\mathbb{Z}$ is undecidable in Lean? Your concept of "the same underlying set" is surprisingly misleading when it comes to type theory.

[Keefer Rowan]

@Reid Barton how does making topological_space into a class help when considering multiple topologies on the type?

[Patrick Massot]

I'm not aware of any foundational system where $\mathbb{Z}/4$ and $\mathbb{Z}/2 \times \mathbb{Z}/2$ would have the same underlying whatever

[Kevin Buzzard]

The category of sets up to isomorphism

[Kenny Lau]

the discrete and indiscrete topology have the same underlying set

[Reid Barton]

If t1 t2 : topological_space \a then you can write, for example \forall s, t1.is_open s -> t2.is_open s. If topological_space was a class from the start then t1 would not be an explicit topology and writing this would require contortions.

[Patrick Massot]

What's this category? What are the homs in the category of sets up to isomorphism?

[Kenny Lau]

I guess group structures on the same torsor can be different

[Kevin Buzzard]

But this is the point -- mathematicians don't need to think clearly about what it means for two things to be "the same", so they assume that lots of things are the same when they're not actually syntactically equal (because this is a good way to think about mathematics).

[Patrick Massot]

Kenny, that's why we have predicate classes saying something is discrete

[Kevin Buzzard]

Given a compact Riemann surface of genus 1 (what a complex geometer might call an elliptic curve) you can choose a point on it and get a group structure (what an algebraic geometer might call an elliptic curve).

[Kenny Lau]

is it a torsor?

[Kevin Buzzard]

It's a torsor for its Jacobian

[Kevin Buzzard]

But this won't cause problems in Lean because one can just make a wrapper type, which is not syntactically equal to the curve, and put a group structure on that instead.

[Keefer Rowan]

One more related question: why would you make has_norm or normed_space a class from the start? In the infinite dimensional cases, it certainly can make sense to put two different norms on the same space.

[Reid Barton]

Often the reason is notation, e.g., writing g.mul a b where g : group \a gets old quickly

[Reid Barton]

But isn't the main purpose of using different norms that one really has different spaces, or at least different normed spaces?

[Reid Barton]

Basically we imagine that the type together with its instances form a single thing--but working with them unbundled has some advantages, like we can change our mind about which instances we include at different points.

[Kevin Buzzard]

There are always ways of doing what you want to do. Whether or not something should be a structure or a class, or more generally the question of how one takes a mathematical concept and turns it into a term in Lean 3's dependent type theory, is not something which can be solved by an algorithm -- this is an experimental science, and as mathlib grows we are learning more and more about it. Lean 4 will be similar, but not the same as, Lean 3, and some answers might change.

[Reid Barton]

I guess you just mean "why not do the same thing for normed_space as for topological_space". I guess the need just doesn't come up. In topology, we use different topologies on the same space a lot (for example to characterize continuous maps, or to define the product topology, or many other things).

[Keefer Rowan]

I think I'm getting a good general picture. Thanks all!

[Scott Morrison]

Maybe this wasn't said above, but it's important to remember that typeclass inference works on a syntactic, rather than definitional level.

This means that you can define "type synonyms" (e.g. just as def Y : Type := X), and give the two different "names-for-the-same-type" different instances.

[Yury G. Kudryashov]

Basically, we use classes if "in majority of cases" we have a canonical structure and want Lean to automatically find it for us. If we have a few structures on the same type, then we use type synonyms (e.g., nat and multiplicative nat).

[Yury G. Kudryashov]

It doesn't work if we want to deal with the type of structures on a type (e.g., all topological space structures).