induced topology commutes with product

Stream: maths

[Filippo A. E. Nuccio]

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

[Sebastien Gouezel]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

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]

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]

OK, thanks, I will try to do so.

[Anatole Dedecker]

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

[Filippo A. E. Nuccio]

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

[Anatole Dedecker]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Filippo A. E. Nuccio]

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

[Patrick Massot]

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]

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]

Is it docs#function.dcomp ?