Zulip Chat Archive

Stream: general

Topic: structure turned into class


Patrick Massot (Apr 08 2018 at 20:25):

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, (ts, is_open t)  is_open (⋃₀ s))

attribute [class] topological_space

Patrick Massot (Apr 08 2018 at 20:26):

Why not directly replacing structure with class?

Patrick Massot (Apr 08 2018 at 20:26):

What would be the difference?

Johannes Hölzl (Apr 08 2018 at 20:40):

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 (Apr 08 2018 at 20:42):

Thanks. What does this last line do then?

Johannes Hölzl (Apr 08 2018 at 20:43):

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 (Apr 08 2018 at 20:46):

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 (Apr 08 2018 at 20:57):

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 (Apr 08 2018 at 21:01):

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

Patrick Massot (Apr 08 2018 at 21:05):

But I can still do

Patrick Massot (Apr 08 2018 at 21:06):

class toto (α : Type)

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

Patrick Massot (Apr 08 2018 at 21:06):

So I don't understand what you mean

Patrick Massot (Apr 08 2018 at 21:07):

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 (Apr 08 2018 at 21:45):

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 (Apr 08 2018 at 22:51):

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 (Apr 08 2018 at 22:51):

Projections work differently.

Kevin Buzzard (Apr 08 2018 at 22:52):

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 (Apr 08 2018 at 22:58):

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...


Last updated: Dec 20 2023 at 11:08 UTC