coinduced/product topologies

Stream: Is there code for X?

[Heather Macbeth]

Is this true?

import topology.constructions

example {X₀ X : Type*} (Y : Type*) [t₀ : topological_space X₀] [s : topological_space Y]
  (f : X₀ → X) :
  @prod.topological_space _ _ (t₀.coinduced f) s
    = (@prod.topological_space _ _ t₀ s).coinduced (λ p, (f p.1, p.2)) :=
sorry

It would imply what I really want, which is

example {X₀ X Y Z : Type*} [t₀ : topological_space X₀] [topological_space Y] [topological_space Z]
  (f : X₀ → X) {g : X × Y → Z} (hg : continuous (λ p : X₀ × Y, g (f p.1, p.2))) :
  let t : topological_space X := t₀.coinduced f in
  by exactI continuous g :=
sorry

but another route to the latter would be fine (we seem to be lacking lemmas for proving that a map with domain a product is continuous).

[Adam Topaz]

The product topology is an inf, so you can use lemmas about inf of topologies to obtain continuity.

[Adam Topaz]

We have docs#induced_inf and docs#coinduced_sup but no docs#coinduced_inf

[Heather Macbeth]

Adam Topaz said:

The product topology is an inf, so you can use lemmas about inf of topologies to obtain continuity.

Yes, but unfortunately as far as I can tell the only lemmas we have about proving continuity with respect to an inf-domain are trivial, docs#continuous_inf_dom_left and twin.

[Adam Topaz]

That's because a prroduct is a limit, so the universal property tells you how to map into the product, not out of it :sad:

[Patrick Massot]

I think this lemma is false.

[Patrick Massot]

Because docs#monotone.map_inf_le is the wrong way around

[Patrick Massot]

Note that if coinduced_inf were true then a product of quotient maps would be a quotient map, which is known to be false (product and quotients don't commute in Top).

[Patrick Massot]

It means you can probably cook up a counter-example using X_0 = ℚ, X = ℚ/ℤ andY = ℚ. In that case X₀ × Y → X × Y is not a quotient map.

[Heather Macbeth]

I got the second fact working under the condition of surjectivity of f and local compactness of Y, both of which are true in my use case -- not clear to me whether the second condition in particular is necessary, though (as opposed to just a hack to let me pass to the compact-open characterization of the product topology).

[Heather Macbeth]

import topology.compact_open

example {X₀ X Y Z : Type*} [t₀ : topological_space X₀] [topological_space Y] [topological_space Z]
  [locally_compact_space Y] {f : X₀ → X} (hf : function.surjective f) {g : X × Y → Z}
  (hg : continuous (λ p : X₀ × Y, g (f p.1, p.2))) :
  let t : topological_space X := t₀.coinduced f in
  by exactI continuous g :=
begin
  intros, resetI,
  let Gf : X₀ → C(Y, Z) := continuous_map.curry ⟨_, hg⟩,
  have hGf : continuous Gf := (continuous_map.curry ⟨_, hg⟩).continuous,
  have h₁ : ∀ x : X, continuous (λ y, g (x, y)),
  { intros x,
    obtain ⟨x₀, rfl⟩ := hf x,
    exact (Gf x₀).continuous },
  let G : X → C(Y, Z) := λ x, ⟨_, h₁ x⟩,
  suffices : continuous G,
  { convert continuous_map.continuous_uncurry_of_continuous ⟨G, this⟩,
    ext x,
    cases x,
    simp [G] },
  have : Gf = G ∘ f,
  { ext x,
    simp },
  rw this at hGf,
  exact continuous_coinduced_dom hGf,
end

[Heather Macbeth]

(This should be more nicely expressed using docs#quotient_map so I'll switch to that formulation.)

[Heather Macbeth]

Quotient map version (still curious about whether the local compactness of Y is needed):

import topology.compact_open

example {X₀ X Y Z : Type*} [t₀ : topological_space X₀] [topological_space X] [topological_space Y]
  [topological_space Z] [locally_compact_space Y]
  {f : X₀ → X} (hf : quotient_map f) {g : X × Y → Z} (hg : continuous (λ p : X₀ × Y, g (f p.1, p.2))) :
  continuous g :=
begin
  let Gf : C(X₀, C(Y, Z)) := continuous_map.curry ⟨_, hg⟩,
  have h : ∀ x : X, continuous (λ y, g (x, y)),
  { intros x,
    obtain ⟨x₀, rfl⟩ := hf.surjective x,
    exact (Gf x₀).continuous },
  let G : X → C(Y, Z) := λ x, ⟨_, h x⟩,
  have : continuous G,
  { rw hf.continuous_iff,
    exact Gf.continuous },
  convert continuous_map.continuous_uncurry_of_continuous ⟨G, this⟩,
  ext x,
  cases x,
  refl,
end

[Patrick Massot]

I'm not suprised you need assumptions on Y. The optimal assumption is probably something like weak Hausdorff compactly generated.

[Heather Macbeth]

Thanks! Always good to have a topologist on hand :)

[Yury G. Kudryashov]

/me should read before writing a reply.