Zulip Chat Archive

Stream: maths

Topic: induced, coinduced, ...


view this post on Zulip Kenny Lau (Jun 15 2018 at 11:51):

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

view this post on Zulip Kenny Lau (Jun 15 2018 at 11:51):

@Mario Carneiro

view this post on Zulip Mario Carneiro (Jun 15 2018 at 11:52):

They are equal but not defeq

view this post on Zulip Kenny Lau (Jun 15 2018 at 11:55):

@Mario Carneiro how do you suggest I prove it?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 11:56):

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

view this post on Zulip Kenny Lau (Jun 15 2018 at 11:57):

we have induced_le but not le_induced, so...

view this post on Zulip Mario Carneiro (Jun 15 2018 at 11:58):

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

view this post on Zulip Kenny Lau (Jun 15 2018 at 11:58):

i'll try

view this post on Zulip Kenny Lau (Jun 15 2018 at 11:58):

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

view this post on Zulip Kenny Lau (Jun 15 2018 at 11:59):

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

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:01):

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

view this post on Zulip Kenny Lau (Jun 15 2018 at 12:01):

is that an idiom?

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:01):

I suppose

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:02):

I think induced_sup will help

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:02):

and induced_compose

view this post on Zulip Kenny Lau (Jun 15 2018 at 12:03):

why are they in continuity @_@

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:03):

because induced is really talking about continuous functions

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:03):

consider continuous_iff_induced_le

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:04):

also the proofs use continuity arguments

view this post on Zulip Kenny Lau (Jun 15 2018 at 12:08):

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

view this post on Zulip Kenny Lau (Jun 15 2018 at 12:09):

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

view this post on Zulip Kenny Lau (Jun 15 2018 at 12:09):

let's say f is surjective

view this post on Zulip Mario Carneiro (Jun 15 2018 at 12:19):

I expect so, try to prove it and find out

view this post on Zulip Reid Barton (Jun 15 2018 at 13:02):

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

view this post on Zulip Reid Barton (Jun 15 2018 at 13:04):

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.

view this post on Zulip Kenny Lau (Jun 15 2018 at 13:04):

I just proved it with one extra assumption

view this post on Zulip Reid Barton (Jun 15 2018 at 13:05):

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

view this post on Zulip Reid Barton (Jun 15 2018 at 13:06):

what was your extra assumption?

view this post on Zulip Kenny Lau (Jun 15 2018 at 13:06):

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⟩⟩)

view this post on Zulip Kenny Lau (Jun 15 2018 at 13:06):

that the map be open


Last updated: May 06 2021 at 18:20 UTC