Transporting inducing maps along homeomorphisms #
A map is inducing exactly when its conjugate by homeomorphisms of the source and target is inducing. The product form transports a family of maps into the factors of a product along homeomorphisms of the source and of every factor.
Main results #
Homeomorph.isInducing_iff_of_homeomorph: maps intertwined by homeomorphisms of the source and target are inducing simultaneously.Homeomorph.isInducing_pi_iff_of_homeomorph: the same for maps into a product, with one homeomorphism for every factor.
theorem
Homeomorph.isInducing_iff_of_homeomorph
{X : Type u_1}
{X' : Type u_2}
{Y : Type u_3}
{Y' : Type u_4}
[TopologicalSpace X]
[TopologicalSpace X']
[TopologicalSpace Y]
[TopologicalSpace Y']
(e : X ≃ₜ X')
(e' : Y ≃ₜ Y')
{r : X → Y}
{r' : X' → Y'}
(h : ∀ (x : X), e' (r x) = r' (e x))
:
Maps intertwined by homeomorphisms of the source and of the target induce the topology simultaneously.
theorem
Homeomorph.isInducing_pi_iff_of_homeomorph
{X : Type u_1}
{X' : Type u_2}
{ι : Type u_3}
[TopologicalSpace X]
[TopologicalSpace X']
{Y : ι → Type u_4}
{Y' : ι → Type u_5}
[(i : ι) → TopologicalSpace (Y i)]
[(i : ι) → TopologicalSpace (Y' i)]
(e : X ≃ₜ X')
(e' : (i : ι) → Y i ≃ₜ Y' i)
{r : X → (i : ι) → Y i}
{r' : X' → (i : ι) → Y' i}
(h : ∀ (x : X) (i : ι), (e' i) (r x i) = r' (e x) i)
:
Restriction maps that commute with homeomorphisms of the source and of every target induce the topology simultaneously.