product of pushforward topologies

Stream: maths

[Kevin Buzzard]

I have an informal proof of False and I'm trying to figure out where my error is. One "obviously true" fact I've assumed is that the pushforward of a product topology along a product of maps is the product of the pushforward topologies. More precisely, we have a product of topological spaces $A\times B$ and maps $f$ and $g$ from $A$ to $X$ and $B$ to $Y$ with $X$ and $Y$ just types. How can we put a topology on $X\times Y$? We can pushforward and product, or product and pushforward. Can these be different?? In my application $X=A$ and $f$ is the identity function.

import Mathlib.Topology.Constructions
import Mathlib.Topology.Basic

-- Is this false?
lemma coinduced_prod (X Y X' Y' : Type) [τX : TopologicalSpace X] [τY : TopologicalSpace Y]
  (f : X → X') (g : Y → Y') :
    TopologicalSpace.coinduced (Prod.map f g) instTopologicalSpaceProd =
    @instTopologicalSpaceProd X' Y' (τX.coinduced f) (τY.coinduced g) := by
  unfold instTopologicalSpaceProd
  sorry

[Patrick Massot]

I don’t see any reason to expect those topologies to be the same.

[Patrick Massot]

The push forward and product play opposite roles. The first one tell you how to build continuous functions out of a type while the second one tells you how to build continuous functions into the product. So there is little hope to find a universal property that would be shared by both your topologies.

[Kevin Buzzard]

Oh interesting! This is surely the error in my proof then. Even if X=A and f is the identity function you think these might be different? A pushforward topology can be affected by a random orthogonal topological space?

[Patrick Massot]

I just scribbled an inequality proof: I can prove the identity is continuous from the pushed product topology to the product of pushed topologies.

[Kevin Buzzard]

Here's another way to ask my question. Say $g:Y\to B$ is a function and we have a topology on $Y$. How to get a topology on $B$? Here's a way: push forward the topology on Y. Here's another way: consider the product topology on $Y\times\R$, now push forward to $B\times\R$ along $g\times id$ and then push forward down to $B$. You're saying that this could give a different answer because $\R$ was involved despite there never being any map to or from $\R$ other than the identity map involved in the construction? I mean, I guess you are saying this and I guess I'm saying it goes against my intuition, but at least I can't prove false any more! Thanks!

[Patrick Massot]

I’m not saying I have a counter-example, I am only saying I don’t see an abstract non-sense reason to expect an inequality.

[Patrick Massot]

We really need something like slim-check to help us here. It should be able to exhaustively search for a counter-example among all A, B, X, Y with cardinal at most 3 and every maps between those. Maybe @Jure Taslak already has something doing this?

[Patrick Massot]

Unfortunately, I need to go away from internet for at least four hours so I won’t get the answer immediately.

[Kevin Buzzard]

I agree that slim_check for this would be really useful. This is not the first time I've been a situation where I've thought "it wouldn't surprise me if there's just a stupid counterexample to this" but not in the concrete context of Nat.

FWIW here's the proof of false I made; maybe it translates into an example.

The set-up: $R$ is a topological space, and acts on $X$ and $Y$ (i.e. SMul R X and SMul R Y).

If $Y$ also has a topology and the $R$-action on $Y$ is continuous, I proved that the $R$-action on $X$ with the pullback topology is continuous (this is basically docs#Inducing.continuousSMul), and I also thought I proved that if $X$ has a topology and the action is continuous, then the action on $Y$ with the pushforward topology is continuous, using this fake argument that the pushforward of the product topology is the product of the pushforward topologies. But here is a counterexample: let $\R$ act on 1-dimensional real vector spaces $X$ and $Y$, and consider the zero map from $X$ to $Y$. If we give $Y$ the usual topology then the pullback topology on $X$ is the top topology, and $R\times X\to X$ is always continuous with respect to this topology. However if we give $X$ the usual topology then the pushforward topology on $Y$ is the bottom topology, and the map is not continuous with respect to this topology. So perhaps this will lead to an explicit counterexample above.

[Yury G. Kudryashov]

See https://math.stackexchange.com/questions/31697/when-is-the-product-of-two-quotient-maps-a-quotient-map

[Mario Carneiro]

Also https://math.stackexchange.com/a/228994 which has an actual counterexample. Apparently this is related to why Top is not a CCC

[Yury G. Kudryashov]

31697 has a counterexample too, but it's hidden in a comment to an answer.

[Mario Carneiro]

incidentally, it's the same counterexample by the same person

[Yakov Pechersky]

We now show that 4.3.2 is false without some assumptions on B. Let f :
Q → Q/Z be the identification map and let h = f×1 : Q×Q → (Q/Z)×Q.
Then h is not an identification map.
Proof For each n in Z let rn =
√
2/(|n| + 1)—thus rn is irrational and
rn → 0 as n → ∞. Let An be any open subset of [n, n+1]×R such that the
closure of An meets {n, n + 1} × R in the two points (n, rn) and (n, rn+1)
(such a set An is shaded in Fig. 4.10.) Let A be the union of these sets An,
n ∈ Z, and let B = A ∩ (Q × Q). Then B is closed in Q × Q and saturated
with respect to h. We leave it as an exercise to the reader to prove that in
(Q/Z) × Q the point (f0, 0) belongs to the closure of h[B].

[Yakov Pechersky]

The PDF is available on his website

[Yakov Pechersky]

https://groupoids.org.uk/pdffiles/topgrpds-e.pdf

[Kevin Buzzard]

My example (extracted from above): consider $\R$ with its usual topology, and define a map from $\R\times\R$ (with its product topology) to $\R\times\R$ (with no topology) sending $(x,y)$ to $(x,37)$. The product of the pushforward topologies is (usual) x (bot), but the pushforward of the product topology is much weirder, the open sets in $\R^2$ are the sets whose intersection with $\R\times{37}$, when identified with $\R$ in the usual way, are open. This is clearly not the product of the pushforward topology because, for example, the definition depends on 37.

[Antoine Chambert-Loir]

Mario Carneiro said:

Also https://math.stackexchange.com/a/228994 which has an actual counterexample. Apparently this is related to why Top is not a CCC

That mistake has been made by Bourbaki in their first edition of their Topologies générale. There's a counterexample of an equivalence relation R on a space X and 1 space Y such that the canonical continuous map fro (X x Y)/R to (X/R) x Y is not a homeomorphism.

[Yury G. Kudryashov]

I'm looking at "Day and Kelly, On topological quotient maps preserved by pullbacks or products". They define the following topology on Opens X (should work for any complete lattice): S : Set (Opens X) is open iff IsUpperSet S ∧ ∀ U : Set (Opens X), sSup U ∈ S → ∃ u ⊆ U, u.Finite ∧ sSup u ∈ S

[Yury G. Kudryashov]

The latter property is very close to docs#CompleteLattice.IsCompactElement and is equivalent to it, if S = Set.Ici V.

[Yury G. Kudryashov]

@Oliver Nash You defined IsCompactElement. Is it useful to add IsCompactUpperSet? Does it have a standard name in the literature?

[Yury G. Kudryashov]

Also, Day and Kelly introduce a property which follows from LocallyCompactSpace and implies it for R1Spaces.

[Yury G. Kudryashov]

This property is the answer to the following question: for what spaces Z, for any quotient map f : X → Y, the map Prod.map f id : X × Z → Y × Z is a quotient map?"

[Yury G. Kudryashov]

The condition is the following one: for any x and its open nhd U : Opens X, there exists S : Set (Opens X) such that

• S is open in the sense of the topology described above;
• U ∈ S;
• the intersection of all sets in S is a nhd of x.

They write that they don't know if the condition is in fact always equivalent to being (weakly?) locally compact.

[Yury G. Kudryashov]

Was this question about equivalence answered since then? Or nobody cares? Or people tried and failed?

[Yury G. Kudryashov]

@Steven Clontz :up:

[Steven Clontz]

nothing comes immediately to mind. I'll note that weakly locally compact implies the strongest compactly generated property (topology is witnessed by its compact, not necessarily T2, subsets), but $\mathbb Q$ is an example of an $R_1$ (in fact, metrizable) compactly generated space that fails to be weakly locally compact, so that candidate for being a weaker characterization seems to be ruled out.

[Yury G. Kudryashov]

Is the property above related to being compactly generated?

[Oliver Nash]

Yury G. Kudryashov said:

Oliver Nash You defined IsCompactElement. Is it useful to add IsCompactUpperSet? Does it have a standard name in the literature?

I'm afraid I don't know. Sorry not to be of more use!

[Yury G. Kudryashov]

UPD: I formalized all theorems from the paper [Day and Kelly, On topological quotient maps preserved by pullbacks or products"], see #15943

[Yury G. Kudryashov]

In this PR I define

• IsOpenQuotientMap; e.g., QuotientGroup.mk satisfies this;
• IsPullbackQuotientMap: a map f : X → Y such that for any continuous g : Z → Y, the map Pullback.snd : f.Pullback g → Z is a quotient map;
• IsProdQuotientMap: a map f : X → Y such that for any Z, the map Prod.map f id : X × Z → Y × Z is a quotient map;
• ProdQuotientMapSpace : a space Z such that for any quotient map f : X → Y, the map Prod.map f id : X × Z → Y × Z is a quotient map.

Following the paper, all these properties are defined in terms of f or Z, so we have no issues with universes etc.

I'm not sure which parts of this should go to files that are imported by a large part of Mathlib, and which parts should stay in a leaf file.

[Yury G. Kudryashov]

@Kevin Buzzard This gives a complete answer to your question.

[Yury G. Kudryashov]

(almost complete: I don't know if ProdQuotientMapSpace is equivalent to LocallyCompactSpace for non-R1 spaces)

[Kevin Buzzard]

Here is what I need for FLT: the third of these results.

import Mathlib.Topology.Algebra.Monoid

variable {A : Type*} [AddCommGroup A]
variable {B : Type*} [AddCommGroup B]

lemma AddMonoidHom.sub_mem_ker_iff (φ : A →+ B) {x y : A} :
    x - y ∈ AddMonoidHom.ker φ ↔ φ x = φ y := by
  rw [AddMonoidHom.mem_ker, map_sub, sub_eq_zero]

variable [τA : TopologicalSpace A] [ContinuousAdd A]
variable [τB : TopologicalSpace B]

open TopologicalSpace

lemma isOpenMap_of_coinduced (φ : A →+ B) (hφc : Continuous φ)
    (h : coinduced φ τA = τB) :
    IsOpenMap φ := by
  intro U hU
  rw [← h, isOpen_coinduced]
  suffices ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ φ.ker, (fun x ↦ x + k) ⁻¹' U by
    exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by continuity) _ hU)
  ext x
  constructor
  · rintro ⟨y, hyU, hyx⟩
    apply Set.mem_iUnion_of_mem (y - x)
    suffices y - x ∈ AddMonoidHom.ker φ by simp_all
    rwa [AddMonoidHom.sub_mem_ker_iff]
  · rintro ⟨_, ⟨k, rfl⟩, _, ⟨hk, rfl⟩, hx⟩
    use x + k, hx
    rw [AddMonoidHom.map_add, hk, add_zero]

lemma coinduced_prod_eq_prod_coinduced (X Y S T : Type*) [AddCommGroup X] [AddCommGroup Y]
    [AddCommGroup S] [AddCommGroup T] (f : X →+ S) (g : Y →+ T)
    (hf : Function.Surjective f) (hg : Function.Surjective g)
    [τX : TopologicalSpace X] [ContinuousAdd X] [τY : TopologicalSpace Y] [ContinuousAdd Y] :
    coinduced (Prod.map f g) instTopologicalSpaceProd =
      @instTopologicalSpaceProd S T (coinduced f τX) (coinduced g τY) := by
  ext U
  rw [@isOpen_prod_iff, isOpen_coinduced, isOpen_prod_iff]
  constructor
  · intro h s t hst
    obtain ⟨x, rfl⟩ := hf s
    obtain ⟨y, rfl⟩ := hg t
    obtain ⟨V1, V2, hV1, hV2, hx1, hy2, h12⟩ := h x y hst
    use f '' V1, g '' V2,
      isOpenMap_of_coinduced (τB := coinduced f τX) f
        (by rw [continuous_iff_coinduced_le]) rfl V1 hV1,
      isOpenMap_of_coinduced (τB := coinduced g τY) g
        (by rw [continuous_iff_coinduced_le]) rfl V2 hV2,
      ⟨x, hx1, rfl⟩, ⟨y, hy2, rfl⟩
    rintro ⟨s, t⟩ ⟨⟨x', hx', rfl⟩, ⟨y', hy', rfl⟩⟩
    exact @h12 (x', y') ⟨hx', hy'⟩
  · intro h x y hxy
    rw [Set.mem_preimage, Prod.map_apply] at hxy
    obtain ⟨U1, U2, hU1, hU2, hx1, hy2, h12⟩ := h (f x) (g y) hxy
    use f ⁻¹' U1, g ⁻¹' U2, hU1, hU2, hx1, hy2
    intro ⟨x', y'⟩ ⟨hx', hy'⟩
    exact h12 ⟨hx', hy'⟩

This sort of proof is less painful to write once you realise the trick that if you name instances [τB : TopologicalSpace B] then you can make explicit choices for them in theorems e.g. isOpenMap_of_coinduced (τB := coinduced f τX), rather than putting @ everywhere. But am I getting some of this for free with your approach?

[Yury G. Kudryashov]

This is IsOpenQuotientMap.prodMap from my branch (+ a proof that this is an open map in 2nd lemma)

[Yury G. Kudryashov]

No, you don't require surjectivity in 2nd lemma. 3rd lemma still requires it, so it can use (IsOpenMap.prod _ _).to_quotientMap _ _ (or add IsOpenQuotientMap as I did in my branch).

[Yury G. Kudryashov]

About the IsOpenMap lemma: is there a statement that generalizes both your lemma and isOpenMap_quotient_mk'_mul?

[Kevin Buzzard]

Sorry to take so long on this, since you asked this question I've been around the world, to the USA twice, and I'm about to go there again. It's taken me a few months to realise that this kind of jet-setting lifestyle isn't actually conducive to getting things done.

Mathematically, your question is the following rather beautiful observation. If a group $\Gamma$ acts via continuous automorphisms on a topological space $T$ and we give the quotient $\Gamma\backslash T$ the coinduced topology coming from the canonical map $T\to\Gamma\backslash T$, then this map is open. Proof: need to show preimage of image is open, but preimage of image of $U$ is just $\bigcup_{g}gU$ is open. My observation is that if $A\to B$ is a group homomorphism between topological groups which is "coinducing", i.e. the topology on $B$ is the one coinduced from the topology on $A$ along the morphism, then this is also an open map, and the proof is the same: we need to show the preimage of the image of $U$ is open, but this is just the union of $kU$, this time as $k$ runs over the kernel. However my map might not be surjective (although it is in the application). Is there a common generalization?

[Johan Commelin]

cc @Yury G. Kudryashov, I guess.

[Yury G. Kudryashov]

Thanks for the explanation! Note: I don't have plans to actually add some generalization to Mathlib (at least, right now).