structure turned into class

Stream: general

[Patrick Massot]

In topological_space.lean, I see:

structure topological_space (α : Type u) :=
(is_open : set α → Prop)
(is_open_univ : is_open univ)
(is_open_inter : ∀s t, is_open s → is_open t → is_open (s ∩ t))
(is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))

attribute [class] topological_space

[Patrick Massot]

Why not directly replacing structure with class?

[Patrick Massot]

What would be the difference?

[Johannes Hölzl]

Currently the operations topological_space.is_open has an explicit topological_space argument, when using class this would be a instance argument. So when working with multiple topologies on the same type the current way is a little bit simpler as one can just write t.is_open s, instead of @is_open _ t s.

[Patrick Massot]

Thanks. What does this last line do then?

[Johannes Hölzl]

we still want to use topological_space as a type class, for this we need to add this attribute. Later we add is_open etc as names in the root namespace with the corresponding instance arguments.

[Patrick Massot]

I sort of see. Do you have an example of a lemma involving two topological structures on the same type? I guess in this case you don't use square brackets arguments?

[Johannes Hölzl]

I should be more precise, it is not about structures on the same type, but a way to refer explicitly to the structure and not be force to only refer to it over the type. For example see: https://github.com/leanprover/mathlib/blob/master/analysis/topology/topological_space.lean#L712 and following.

[Patrick Massot]

You mean the same definition with class topological_space would not give you a type topological_space α?

[Patrick Massot]

But I can still do

[Patrick Massot]

class toto (α : Type)

instance {α : Type }: group (toto α) := sorry

[Patrick Massot]

So I don't understand what you mean

[Patrick Massot]

In my search for minimal example I noticed a class doesn't need to have any field :stuck_out_tongue_winking_eye:

[Johannes Hölzl]

No, class topological_space is nearly the same as structure topological_space. The main difference is the attribute added to topological_space and the binder information on the generated projections, i.e. that is_open has a explicit argument or that it has a type class instance argument.

[Kevin Buzzard]

structure foo (α : Type) :=
(bar : α → Prop)

attribute [class] foo

class foo' (α : Type) :=
(bar' : α → Prop)

example (α : Type) [foo α] (a : α) : foo.bar a := sorry -- this doesn't work

example (α : Type) [foo' α] (a : α) : foo'.bar' a := sorry -- this works

example (α : Type) [H : foo α] (a : α) : H.bar a := sorry -- this works

example (α : Type) [H' : foo' α] (a : α) : H'.bar' a := sorry -- this doesn't work

[Kevin Buzzard]

Projections work differently.

[Kevin Buzzard]

I am not saying I understand why we want topological space to be this way, but I think this is what Johannes is saying.

[Kevin Buzzard]

Johannes' link is to a construction partially ordering all topologies on a fixed type, so he likes foo better here because H.bar works nicely if we have H1, H2...