Zulip Chat Archive

Stream: new members

Topic: Products induces topology on fibers


view this post on Zulip Nicolò Cavalleri (Dec 20 2020 at 10:58):

I got a bit rusty: how do I prove something like this (supposing it says what I want to say)

example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y] :
   x : X, inducing (λ y : Y, prod.mk x y) := sorry

?

view this post on Zulip Mario Carneiro (Dec 20 2020 at 11:24):

One direction is going to be continuity of prod.mk

view this post on Zulip Mario Carneiro (Dec 20 2020 at 11:33):

example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y]
  (x : X) : inducing (λ y : Y, prod.mk x y) :=
begin
  refine le_antisymm (continuous_const.prod_mk continuous_id).le_induced (λ s h, _)⟩,
  convert is_open_induced (is_open_univ.prod h),
  ext x, simp
end

view this post on Zulip Nicolò Cavalleri (Dec 20 2020 at 11:51):

Ok thanks! I was trying this way:

lemma constant_induces_top {X : Type*} {Y : Type*} [t : topological_space X] {x : X} :
  t.induced (λ y : Y, x) =  := by { sorry, }

example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y] :
   x : X, inducing (λ y : Y, prod.mk x y) := λ z,
    by {rw prod.topological_space,
    simp only [induced_inf, induced_compose, function.comp, constant_induces_top, top_inf_eq],
    rw [induced_id], }⟩

but the last rw does not work... do you know why? (I missed a bit when I first pasted it, sorry)

view this post on Zulip Nicolò Cavalleri (Dec 20 2020 at 12:37):

Also what is a smart way to prove

lemma constant_induces_top {X : Type*} {Y : Type*} [t : topological_space X] {x : X} :
  t.induced (λ y : Y, x) =  := sorry

without going back to definitions?

view this post on Zulip Reid Barton (Dec 20 2020 at 12:40):

It's equivalent to the statement with >=, which is equivalent to λ y : Y, x being continuous w.r.t. (or any topology), which is continuous_const

view this post on Zulip Nicolò Cavalleri (Dec 20 2020 at 13:04):

Ok thanks. Is the name constant_induces_top appropriate?

view this post on Zulip Nicolò Cavalleri (Dec 20 2020 at 13:06):

Also my proof above works if I add this lemma

lemma induced_id' {α : Type*} [t : topological_space α] : t.induced (λ a : α, a) = t := induced_id

What should I do? Should this new lemma go into mathlib or should I report that id is not working properly?

view this post on Zulip Reid Barton (Dec 20 2020 at 13:11):

id isn't reducible so there is no surprise here

view this post on Zulip Reid Barton (Dec 20 2020 at 13:13):

Nicolò Cavalleri said:

Ok thanks. Is the name constant_induces_top appropriate?

I think we would call it something more like induced_const

view this post on Zulip Nicolò Cavalleri (Dec 20 2020 at 13:13):

Ok should we change the statement of induced_id? Or what solution do you propose?

view this post on Zulip Reid Barton (Dec 20 2020 at 13:15):

I don't really think any action is needed

view this post on Zulip Reid Barton (Dec 20 2020 at 13:15):

You could finish with exact induced_id.symm

view this post on Zulip Reid Barton (Dec 20 2020 at 13:16):

Certainly adding a lemma would be better than changing an existing lemma, but I'm not sure if it will ever see real use

view this post on Zulip Reid Barton (Dec 20 2020 at 13:19):

I'm not really sure if there is a reason that function.comp is reducible but not id... it is a bit confusing


Last updated: May 17 2021 at 22:15 UTC