induced, coinduced, ...

Stream: maths

[Kenny Lau]

If I have a function f:A->B with a topology on B, are the following two topologies on A x A the same?
1. equip A with the induced topology, and then do the product topology
2. build fxf:AxA->BxB and then use the induced topology, where BxB has the product topology

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

They are equal but not defeq

[Kenny Lau]

@Mario Carneiro how do you suggest I prove it?

[Mario Carneiro]

you should be able to use some nonsense in the lattice of top spaces to prove it relatively easily

[Kenny Lau]

we have induced_le but not le_induced, so...

[Mario Carneiro]

isn't induced defined as some kind of supremum? That gives you a proof approach

[Kenny Lau]

i'll try

[Kenny Lau]

(no, prod is supremum, induced isn't)

[Kenny Lau]

oh and is there an idiom to obtain the categorical product of two functions?

[Mario Carneiro]

not particularly, embedding_prod_mk just uses (λx:α×γ, (f x.1, g x.2))

[Kenny Lau]

is that an idiom?

[Mario Carneiro]

I suppose

[Mario Carneiro]

I think induced_sup will help

[Mario Carneiro]

and induced_compose

[Kenny Lau]

why are they in continuity @_@

[Mario Carneiro]

because induced is really talking about continuous functions

[Mario Carneiro]

consider continuous_iff_induced_le

[Mario Carneiro]

also the proofs use continuity arguments

[Kenny Lau]

@Mario Carneiro oh my god I just realized I have been asking the wrong question

[Kenny Lau]

f:A->B be a set-theoretic function, and a topology on A. Are the following two topologies on BxB the same?
1. equip B with coinduced, and then product
2. coinduced from fxf:AxA->BxB, where AxA has the product topology

[Kenny Lau]

let's say f is surjective

[Mario Carneiro]

I expect so, try to prove it and find out

[Reid Barton]

I'm almost certain they are not the same in general.

[Reid Barton]

If A->B is a quotient map, then XxA->XxB need not be a quotient map. But I don't know the counterexample off-hand.

[Kenny Lau]

I just proved it with one extra assumption

[Reid Barton]

It's true if X is locally compact, or in your original question if A and B are

[Reid Barton]

what was your extra assumption?

[Kenny Lau]

example (α : Type*) (β : Type*)
  [t : topological_space α] (f : α → β)
  (hf1 : function.surjective f)
  (hf2 : ∀ S, is_open S → is_open (f ⁻¹' (f '' S))) :
  @prod.topological_space β β
        (@topological_space.coinduced α β f t)
        (@topological_space.coinduced α β f t)
    = @topological_space.coinduced (α × α) (β × β)
        (λ p, (f p.1, f p.2)) prod.topological_space :=
have H1 : prod.fst ∘ (λ p : α × α, (f p.1, f p.2)) = f ∘ prod.fst,
  from rfl,
have H2 : prod.snd ∘ (λ p : α × α, (f p.1, f p.2)) = f ∘ prod.snd,
  from rfl,
have H3 : topological_space.induced f (topological_space.coinduced f t) ≤ t,
  from induced_le_iff_le_coinduced.2 $ le_refl _,
by letI := topological_space.coinduced f t;
from le_antisymm
  (lattice.sup_le
    (induced_le_iff_le_coinduced.1 (by rw [induced_compose, H1, ← induced_compose];
      from le_trans (induced_mono H3) lattice.le_sup_left))
    (induced_le_iff_le_coinduced.1 (by rw [induced_compose, H2, ← induced_compose];
      from le_trans (induced_mono H3) lattice.le_sup_right)))
  (λ S hs, is_open_prod_iff.2 $ λ x y hxy,
  let ⟨m, hm⟩ := hf1 x, ⟨n, hn⟩ := hf1 y in
  let ⟨u, v, hu, hv, hmu, hnv, H⟩ := is_open_prod_iff.1 hs m n (by simpa [hm, hn] using hxy) in
  ⟨f '' u, f '' v, hf2 u hu, hf2 v hv, ⟨m, hmu, hm⟩, ⟨n, hnv, hn⟩,
    λ ⟨p, q⟩ ⟨⟨P, hp1, hp2⟩, ⟨Q, hq1, hq2⟩⟩,
    by simp at hp2 hq2; rw [← hp2, ← hq2]; from @H (P, Q) ⟨hp1, hq1⟩⟩)

[Kenny Lau]

that the map be open