Zulip Chat Archive

Stream: maths

Topic: induced topology commutes with product


Filippo A. E. Nuccio (Feb 18 2022 at 09:56):

What is the best way to say that if I have (finitely many, if that helps) topological spaces XiX_i and subspaces YiXiY_i\subseteq X_i endowed with the induced topology, then the product topology on Yi\prod Y_i coincides with the induced topology from Xi\prod X_i?

Sebastien Gouezel (Feb 18 2022 at 10:01):

Can you say that the canonical inclusion is inducing? Or an embedding?

Filippo A. E. Nuccio (Feb 18 2022 at 10:01):

Well, my idea was to prove that it was inducing: that would be enough for what I need.

Filippo A. E. Nuccio (Feb 18 2022 at 10:10):

It seems that docs#prod_induced_induced does it for the product of two spaces, right?

Filippo A. E. Nuccio (Feb 18 2022 at 10:15):

Is there a "stupid" way to extend the case of two factors to more general pi or is it better to re-prove it along the same lines?

Sebastien Gouezel (Feb 18 2022 at 10:17):

It is certainly better to give a direct proof of the general case, as this property holds even for infinite products.

Filippo A. E. Nuccio (Feb 18 2022 at 10:33):

OK, thanks, I will try to do so.

Anatole Dedecker (Feb 18 2022 at 11:03):

This should be an easy consequence of docs#induced_infi, right ?

Filippo A. E. Nuccio (Feb 18 2022 at 11:06):

Oh right, thanks. I guess infi is for the infimum of the topologies, so the coarsest one. Is that correct?

Anatole Dedecker (Feb 18 2022 at 12:05):

It’s the coarsest of the topologies which are finer than all the topologies in your infimum

Patrick Massot (Feb 18 2022 at 12:24):

I can never remember what coarser and finer mean. I can only remember that the mathlib order on topologies ensures that ttt \le t' iff Id is continuous from t to t'.

Patrick Massot (Feb 18 2022 at 12:24):

And your lemma is indeed:

import topology.constructions

open topological_space

lemma pi_induced_induced {ι : Sort*} {X Y : ι  Type*} [t : Π i : ι, topological_space $ Y i] (f : Π i, X i  Y i) :
    @Pi.topological_space ι X (λ i, induced (f i) (t i)) = induced (λ (x : Π i, X i), (λ j,  f j (x j) : Π i, Y i)) Pi.topological_space :=
begin
  dsimp [Pi.topological_space],
  rw induced_infi,
  simp [induced_compose]
end

Patrick Massot (Feb 18 2022 at 12:25):

There should be a name somewhere for (λ (x : Π i, X i), (λ j, f j (x j) : Π i, Y i))

Filippo A. E. Nuccio (Feb 18 2022 at 13:09):

Thanks @Patrick Massot ! Are you going to PR this?

Patrick Massot (Feb 18 2022 at 14:10):

I'd like to get the name of the map above first. It should be Pi.map or something, but I can't find it

Filippo A. E. Nuccio (Feb 18 2022 at 14:12):

Ok, for the time being I have just imported as it is in LTE. If it lands into mathlib I will re-check its name.

Anatole Dedecker (Feb 18 2022 at 15:09):

Is it docs#function.dcomp ?


Last updated: Dec 20 2023 at 11:08 UTC