Trying to prove a lemma about group topologies

Stream: new members

[Sebastian Monnet]

Hi everyone! I'm trying to adapt this proof

@[to_additive]
lemma coinduced_continuous {α β : Type*} [t : topological_space α] [group β]
  (f : α → β) : cont t (coinduced f).to_topological_space f :=
begin
  rw continuous_iff_coinduced_le,
  refine le_Inf _,
  rintros _ ⟨t', ht', rfl⟩,
  exact ht',
end

from topology.algebra.group, to prove the corresponding lemma for induced topologies. That is, for a function $f : G \to X$ from a topological group to a topological space, we define induced f to be the coarsest group topology on G that is finer than the topology induced by f. In Lean, we define

def induced {G X : Type*} [t : topological_space X] [group G] (f : G → X) :
  group_topology G :=
Sup {a : group_topology G |  a.to_topological_space ≤ (topological_space.induced f t)}

The lemma I'm trying to prove is then

lemma induced_continuous {G X : Type*} [t : topological_space X] [group G]
  (f : G → X) : cont (induced f).to_topological_space t f := sorry

Now, the proof of coinduced_continuous begins with

rw continuous_iff_coinduced_le

so I begin my proof with

rw continuous_iff_le_induced

and this gives me a goal of the form

(induced f).to_topological_space ≤ topological_space.induced f t

The second line of the proof of coinduced_continuous is refine le_Inf _. I don't understand exactly what the refine tactic does, but I think I understand roughly what it is doing in this case. That is, we need to show that

topological_space.coinduced f t ≤ (coinduced f).to_topological_space

and the right hand side is the infinum of the set of group topologies coarser than the coinduced topology. Therefore, the theorem le_Inf tells us that it suffices to check that topological_space.coinduced f t is finer than every such group topology, and refine le_Inf _, makes that our goal.

By almost exactly the same reasoning, I am trying to use refine Sup_le _ to change the goal

(induced f).to_topological_space ≤ topological_space.induced f t

However, when I try to do this, I get the error

invalid type ascription, term has type
  Sup ?m_3 ≤ ?m_4
but is expected to have type
  (induced f).to_topological_space ≤ topological_space.induced f t

I don't understand why the tactic works in one case an not the other. They look exactly the same to me (modulo swapping Sup with Inf and greater with less). Any help would be much appreciated.

[Heather Macbeth]

@Sebastian Monnet First, can you try to present your future questions to include a minimal working example, #mwe ? It took me some time to construct one from your question:

import topology.algebra.group

def induced {G X : Type*} [t : topological_space X] [group G] (f : G → X) :
  group_topology G :=
Sup {a : group_topology G |  a.to_topological_space ≤ (topological_space.induced f t)}

lemma induced_continuous {G X : Type*} [t : topological_space X] [group G]
  (f : G → X) : @continuous _ _ (induced f).to_topological_space t f :=
begin
  rw continuous_iff_le_induced,

end

[Heather Macbeth]

I believe the error here is that topological_space.induced f t is not of type group_topology G, it's of type topological_space G.

[Heather Macbeth]

Maybe something like this will work (if in fact it's true):

begin
  rw continuous_iff_le_induced,
  convert @Sup_le (topological_space G) _ (group_topology.to_topological_space '' {a : group_topology G |  a.to_topological_space ≤ (topological_space.induced f t)}) (topological_space.induced f t) _,

end

[Sebastian Monnet]

@Heather Macbeth Sorry about the lack of minimal working example - I will include one next time. Thank you for your answer. I agree that it seems like the type inconsistency is the problem, since induced f is the supremum of a set of type group_topology G, and we are trying to compare topological spaces. In light of this, though, I can't understand why the second line of the proof of coinduced_continuous works. Shouldn't that fail for exactly the same reason?

[Heather Macbeth]

@Sebastian Monnet At a guess, it may be because docs#group_topology.complete_lattice, the complete lattice structure on group_topology G, has been constructed using docs#complete_lattice_of_complete_semilattice_Inf, which according to its docstring has bad definitional properties for the Sup:

/--
Any `complete_semilattice_Inf` is in fact a `complete_lattice`.

Note that this construction has bad definitional properties:
see the doc-string on `complete_lattice_of_Inf`.
-/
def complete_lattice_of_complete_semilattice_Inf (α : Type*) [complete_semilattice_Inf α] :
  complete_lattice α :=
complete_lattice_of_Inf α (λ s, is_glb_Inf s)

[Heather Macbeth]

In particular, this would account for the asymmetry in the behaviour of Sup and Inf for this complete lattice.

[Heather Macbeth]

It seems that the construction is due to @María Inés de Frutos Fernández, in #10531, so we could ask her about the design decision and whether it would be sensible to rewrite the complete lattice instance so it constructs the Sup directly.

[Adam Topaz]

There should be a Galois insertion between group topologies and topologies. I think the lattice structure would be better behaved if it was defined via such a Galois connection.

[Eric Wieser]

I think that only produces nice equalities if you implement galois_insertion.choice by hand

[Eric Wieser]

The default implementation doesn't make very nice equalities either

[María Inés de Frutos Fernández]

Heather Macbeth said:

Maybe something like this will work (if in fact it's true):

begin
  rw continuous_iff_le_induced,
  convert @Sup_le (topological_space G) _ (group_topology.to_topological_space '' {a : group_topology G |  a.to_topological_space ≤ (topological_space.induced f t)}) (topological_space.induced f t) _,

end

I don't think this is true; taking the Sup as topological spaces might not give you the correct topology.
The problem is that the intersection of two group topologies t and t' is not always a group topology; one defines the sup of t and t' as the finest group topology contained in their intersection. Would it help to make this field (and Sup) explicit in the definition of this complete lattice?

[Sebastian Monnet]

@Heather Macbeth okay, thank you!

[Kevin Buzzard]

@Bhavik Mehta you've helped me out of holes like this before -- do you know a trick here? The maths: if G is a group then there's a lattice of topologies on G (well-known) and a sublattice of topologies which happen to make G into a topological group. Maria proved the sublattice has all Sups and Infs, and Infs can be computed in the larger lattice (but Sups cannot; we have explicit counterexamples). How do we get a Galois insertion or coinsertion and does it help?

[Sebastian Monnet]

Edit: I guess the point is that the infinum is computed in the larger lattice. Is that why my attempt to dualise your proof didn't work?

@María Inés de Frutos Fernández would you mind explaining how the second line of your proof works? We have le_Inf : (∀b∈s, a ≤ b) → a ≤ Inf s, where α is a complete semilattice, s : set α, and a : α. Your proof seems to take a to be topological_space.coinduced f t and s to be the set of topological spaces underlying group topologies coarser than a. My problem is that a is a topology, not a group topology, but the infinum in the definition of coinduced f is taken in the complete lattice of group topologies, so I don't understand how we can apply the theorem.

It seems to me conceivable that the infinum of group topologies greater than or equal to topological_space.coinduced f t is not itself greater than or equal to topological_space.coinduced f t. I am convinced that this is not the case, but only because I've worked through the maths myself - I don't understand why Lean is happy with this step.

Not sure if I need to include a mwe with this sort of question, but here is one just in case:

import tactic
import topology.algebra.group
import data.set.basic

local notation `cont` := @continuous _ _


/-- If f : X → G is a function from a topolgoical space to a group, then `coinduced f` is the finest group topology on G such that f is continuous.-/
def coinduced {X G : Type*} [t : topological_space X] [group G] (f : X → G) :
  group_topology G :=
Inf {b : group_topology G | (topological_space.coinduced f t) ≤ b.to_topological_space}

lemma coinduced_continuous {X G : Type*} [t : topological_space X] [group G]
  (f : X → G) : cont t (coinduced f).to_topological_space f :=
begin
  rw continuous_iff_coinduced_le,
  refine le_Inf _,
  rintros _ ⟨t', ht', rfl⟩,
  exact ht',
end

[Reid Barton]

Kevin Buzzard said:

Maria proved the sublattice has all Sups and Infs, and Infs can be computed in the larger lattice (but Sups cannot; we have explicit counterexamples).

It might be worth adding a comment somewhere (maybe on instance [group γ] : complete_semilattice_Inf (group_topology γ) that explicitly says that sups cannot be computed in the original lattice, since it wasn't very clear to me one way or another; I guess the formation of the product topology doesn't play well with sups?

[Reid Barton]

@Sebastian Monnet Not only can the Inf be computed in the larger lattice, if you look at
https://github.com/leanprover-community/mathlib/blob/1367c19b1b5d53ec699e4003f7aaa40a8099a643/src/topology/algebra/group.lean#L860-L862
you will see that it is actually defined that way (and then one has to check that it really is an infimum).

[Reid Barton]

So I think the conclusion is that the lemma you were originally trying to prove is actually false, because X could be G with one of these topologies that is a sup of group topologies but isn't a group topology.

[María Inés de Frutos Fernández]

@Sebastian Monnet , the coinduced version works because in that case Inf(...).to_topological_spaces is equal to the Inf as topological spaces by definition. That is,

import topology.algebra.group

example {G : Type*} [group G] (S : set (group_topology G)) :
  (Inf S).to_topological_space = Inf (group_topology.to_topological_space '' S) := rfl

But this isn't true for the Sup.

[Kevin Buzzard]

María Inés showed me a counterexample to the sup thing. I don't remember the details but if memory served the counterexample was $A=\R^2$ as an additive abelian group in the usual way, and with the two topologies being maybe the order topology coming from the two total orders lex and lex \circ swap.

[María Inés de Frutos Fernández]

Reid Barton said:

Kevin Buzzard said:

Maria proved the sublattice has all Sups and Infs, and Infs can be computed in the larger lattice (but Sups cannot; we have explicit counterexamples).

It might be worth adding a comment somewhere (maybe on instance [group γ] : complete_semilattice_Inf (group_topology γ) that explicitly says that sups cannot be computed in the original lattice, since it wasn't very clear to me one way or another; I guess the formation of the product topology doesn't play well with sups?

I was trying to say this with the comment The supremum of two group topologies s and t is the infimum of the family of all group topologies contained in the intersection of s and t. But I would be very happy to change this to a clearer comment.

[Kevin Buzzard]

@María Inés de Frutos Fernández do you remember the details of the counterexample? I think it's an interesting one.

[Kevin Buzzard]

I wonder if there is some kind of universal object lurking

[Reid Barton]

María Inés de Frutos Fernández said:

I was trying to say this with the comment The supremum of two group topologies s and t is the infimum of the family of all group topologies contained in the intersection of s and t. But I would be very happy to change this to a clearer comment.

Right but this doesn't explicitly tell the reader that it sometimes isn't equal to the sup of underlying topologies--maybe you just didn't know or didn't care.

[María Inés de Frutos Fernández]

Yes, it's what you're describing - consider $R^2$ with the two lexicographical orders (which define two group topologies on $R^2$), and then look at a "Maltese cross" (say centered at 0) in the intersection topology. This is open, but it doesn't contain U + U for any open neighborhood of 0.

[Reid Barton]

In general, it may not be equal to the supremum of s and t as topologies.--or something like that

[María Inés de Frutos Fernández]

I'll see if I can find the reference for this counterexample and post it here.

[María Inés de Frutos Fernández]

Reid Barton said:

In general, it may not be equal to the supremum of s and t as topologies.--or something like that

I see your point, I should have made this more explicit.

[María Inés de Frutos Fernández]

Note that it may be coarser than the supremum of s and t as topologies?

[María Inés de Frutos Fernández]

María Inés de Frutos Fernández said:

I'll see if I can find the reference for this counterexample and post it here.

See page 166 of Pierre Samuel's "Ultrafilters and compactification of uniform spaces":
https://www.ams.org/journals/tran/1948-064-01/S0002-9947-1948-0025717-6/S0002-9947-1948-0025717-6.pdf

[Sebastian Monnet]

Reid Barton said:

So I think the conclusion is that the lemma you were originally trying to prove is actually false, because X could be G with one of these topologies that is a sup of group topologies but isn't a group topology.

Would you mind explaining why you think the original lemma is false? It seems to me that taking such an X just means that the supremum does not equal X. I don't think that prevents the supremum from being in the set.

[Eric Wieser]

María Inés de Frutos Fernández said:

Sebastian Monnet , the coinduced version works because in that case Inf(...).to_topological_spaces is equal to the Inf as topological spaces by definition. That is,

import topology.algebra.group

example {G : Type*} [group G] (S : set (group_topology G)) :
  (Inf S).to_topological_space = Inf (group_topology.to_topological_space '' S) := rfl

But this isn't true for the Sup.

I added this example as a lemma in #10792

[Reid Barton]

There's a complete lattice of topologies on G, and a subset of those that are the group topologies which apparently is closed under infs but not sups. That means there is a "(group topology)-ification" operation L which takes a topology T to the inf of all the group topologies bigger than T. In general we have T <= L(T) and the fixed points of L are the group topologies. We can compute sups in group topologies by computing sups of the underlying topologies and then applying L. In particular the sup in group topologies is always bigger than the sup of underlying topologies.

Now consider your lemma induced_continuous in the case X = G and f = id, and suppose t is a non-group topology which is a sup of two group topologies, say t1 and t2. Then the induced group topology is bigger than both t1 and t2, so it has to be at least the sup in group topologies of t1 and t2, which is strictly bigger than t (otherwise t would be a group topology). And then the inequality (induced id).to_topological_space <= t doesn't hold, so f is not continuous.

[Sebastian Monnet]

@Reid Barton
Thank you, I'm convinced!

[María Inés de Frutos Fernández]

Wait, when ( induced id).to_topological_space is finer than t, then id : (G, (induced id).to_topological_space) \to (G, t). is continuous (since there are more open sets on the left).

[Eric Wieser]

Eric Wieser said:

I added this example as a lemma in #10792

and was sniped into also added the corresponding lemmas for inf, top, and bot...