Bicompactness

Stream: maths

[Yaël Dillies]

Do people know of a filter definition of bicompactness?

[Kevin Buzzard]

Why do we want this notion? I've never heard of it. I can think of 100 things I have heard of which we don't have and which would perhaps be more profitable to work on. Does anyone serious use this notion? Maybe they do -- I'm just asking

[Kevin Buzzard]

I don't even understand the definition. What's this thing about it must contain an element from each topology? What must? How about we add the empty set? That's in both

Is it different to the topology generated by the two topologies being compact?

[Kevin Buzzard]

A bi-group is a type with two group structures. We say it's bi-abelian if both of them are abelian. Let's not put this in mathlib.

[Yaël Dillies]

This is because of duality theory for distributive lattices. It is genuinely useful, Kevin :smile:

[Kevin Buzzard]

Do you even understand what is written on Wikipedia? It seems like a very vague comment about how something must contain an open from each topology.

[Kevin Buzzard]

That comment made me wonder about whether this stuff was just written by a randomer and was never clarified because this stuff is never used

[Yaël Dillies]

No, I don't understand that offhand comment because it seems like it adds a condition after the main sentence. However, I found the original paper.