Zulip Chat Archive

Stream: maths

Topic: continuous function to pi type


Johan Commelin (May 23 2018 at 09:58):

I have no clue how to prove this:

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[topological_space X] [Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) := sorry

Kevin Buzzard (May 23 2018 at 09:59):

Can you prove it in maths?

Kevin Buzzard (May 23 2018 at 09:59):

:-)

Kevin Buzzard (May 23 2018 at 09:59):

i.e. "is it true"

Johan Commelin (May 23 2018 at 09:59):

Unless I made a stupid mistake: yes

Mario Carneiro (May 23 2018 at 10:00):

how is the pi topology defined?

Johan Commelin (May 23 2018 at 10:00):

It just says that Pi is some sort of categorical product on steroids

Kevin Buzzard (May 23 2018 at 10:00):

what Mario said

Johan Commelin (May 23 2018 at 10:00):

If I have continuous maps to all the factors, I get a continuous map to the Pi

Kevin Buzzard (May 23 2018 at 10:00):

(in Lean)

Johan Commelin (May 23 2018 at 10:00):

instance Pi.topological_space {β : α  Type v} [t₂ : Πa, topological_space (β a)]
 : topological_space (Πa, β a) :=
a, topological_space.induced (λf, f a) (t₂ a)

Mario Carneiro (May 23 2018 at 10:01):

so look for theorems about continuity on induced

Johan Commelin (May 23 2018 at 10:01):

There are loads of those... but how do I deal with the ⨆a, that is in front?

Mario Carneiro (May 23 2018 at 10:01):

look for continuity on a Sup

Johan Commelin (May 23 2018 at 10:02):

there is only continuity for sup, not Sup

Mario Carneiro (May 23 2018 at 10:03):

I think it's called that... serach for the bigcup

Johan Commelin (May 23 2018 at 10:03):

I'm already down 5 rabbit holes, I really hope I don't need to go down this one as well...

Johan Commelin (May 23 2018 at 10:03):

Search for gives No results in continuity.lean

Mario Carneiro (May 23 2018 at 10:04):

hm, looks like it is missing from the list at continuity.lean

Johan Commelin (May 23 2018 at 10:05):

Right, there is constructors for products of two topological spaces, and continous maps towards them, etc... but for Pi types this seems missing. And I don't know exactly how to prove this stuff...

Johan Commelin (May 23 2018 at 10:06):

/me doesn't know anything about Sup and friends

Mario Carneiro (May 23 2018 at 10:06):

okay, so use the existing theorems as guides and write your own version for continuity on supr

Johan Commelin (May 23 2018 at 10:06):

\me goes down rabbit hole # 6

Mario Carneiro (May 23 2018 at 10:06):

(or I can, if this is going too far afield)

Mario Carneiro (May 23 2018 at 10:06):

I'm just showing you what I would do

Johan Commelin (May 23 2018 at 10:07):

Well, I'm trying to prove that the face map between two standard simplices is continuous...

Johan Commelin (May 23 2018 at 10:08):

@Mario Carneiro At the moment, I don't even know how to write the statement for Sup

Mario Carneiro (May 23 2018 at 10:20):

here you go:

lemma continuous_Sup_dom {t₁ : set (tspace α)} {t₂ : tspace β}
  {t : tspace α} (h₁ : t ∈ t₁) : cont t t₂ f → cont (Sup t₁) t₂ f :=
continuous_le_dom (le_Sup h₁)

lemma continuous_Sup_rng {t₁ : tspace α} {t₂ : set (tspace β)}
  (h : ∀t∈t₂, cont t₁ t f) : cont t₁ (Sup t₂) f :=
continuous_Inf_rng
  (λ t ht, show t ≤ coinduced f t₁, from h t ht)
  continuous_coinduced_rng

lemma continuous_supr_dom {t₁ : ι → tspace α} {t₂ : tspace β}
  {i : ι} : cont (t₁ i) t₂ f → cont (supr t₁) t₂ f :=
continuous_Sup_dom ⟨i, rfl⟩

lemma continuous_supr_rng {t₁ : tspace α} {t₂ : ι → tspace β}
  (h : ∀i, cont t₁ (t₂ i) f) : cont t₁ (supr t₂) f :=
continuous_Sup_rng $ assume t ⟨i, (t_eq : t = t₂ i)⟩, t_eq.symm ▸ h i

Mario Carneiro (May 23 2018 at 10:20):

I just copied the Inf stuff and dualized everything

Johan Commelin (May 23 2018 at 10:29):

Ok, thanks!

Johan Commelin (May 23 2018 at 10:29):

Let me see if I can continue with rabbit hole # 5 (-;

Johan Commelin (May 23 2018 at 10:53):

Hurray!

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) :=
begin
let YY := (Πi, Y i),
apply continuous_Sup_rng,
intros t ht,
cases ht with i hi,
simp at *,
rw hi,
apply continuous_induced_rng,
unfold function.comp,
exact H i,
end

Johan Commelin (May 23 2018 at 11:23):

Ok, so now I'm stuck with this MWE:

lemma continuous_sums {n : } : continuous (λ x : ((fin n)  ), univ.sum x) := sorry

Johan Commelin (May 23 2018 at 11:24):

Whatever I try, I'm pulled hard into all sorts of foldr stuff. And I'm completely out of my comfort zone.

Mario Carneiro (May 23 2018 at 11:24):

that's not a trivial theorem

Johan Commelin (May 23 2018 at 11:25):

I would like to mumble some think like... well, addition is continuous... if you repeatedly add, you get continuity by induction

Johan Commelin (May 23 2018 at 11:25):

Can I foldr the continuity proof off add?

Mario Carneiro (May 23 2018 at 11:25):

I guess you can prove it by induction on n, you will need to show that fin (succ n) -> R is homeomorphic to R x (fin n -> R)

Johan Commelin (May 23 2018 at 11:27):

To link back to the discussion with Kevin, from about an hour ago... do you think this could be made into a trivial theorem?

Mario Carneiro (May 23 2018 at 11:27):

no

Mario Carneiro (May 23 2018 at 11:28):

okay, maybe that's too strong, you might be able to prove it by induction on the set instead

Johan Commelin (May 23 2018 at 11:29):

that sounds closer to what I wanted to mumble

Mario Carneiro (May 23 2018 at 11:29):

in that case you want to use finset.induction_on

Mario Carneiro (May 23 2018 at 11:30):

and the IH says that a sum of continuous functions over set s is continuous

Johan Commelin (May 23 2018 at 11:33):

Ok, I'm going to try this. Thanks!

Patrick Massot (May 23 2018 at 12:43):

Johan, you may already know, but just in case: there very easy clean up steps you can run on such proofs. YY is never used. unfold is actually much less useful that one thinks in the beginning, so I always try to remove all unfold once a proof work. And then we always try to get rid of simp in the middle of proofs. The result is:

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) :=
begin
    apply continuous_Sup_rng,
    intros t ht,
    cases ht with i hi,
    rw hi,
    apply continuous_induced_rng,
    exact H i,
end

Patrick Massot (May 23 2018 at 12:44):

Out of curiosity, I also tried to build a term proof, but haven't succeeded because of the mysterious rewrite in the middle (which rewrites implicit arguments, which has the weird effect of not changing the visible goal)

Patrick Massot (May 23 2018 at 12:45):

I can't get more obfuscated than:

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) :=
continuous_Sup_rng $ λ t ht, match ht with i, hi := by rw hi ; apply continuous_induced_rng ; exact (H i) end

Johannes Hölzl (May 23 2018 at 12:49):

For the sum proof: its easiest to generalize for finset, and then go from list to multiset to finset. I will add this to mathlib:

lemma continuous_supr_rng
  {ι : Sort*} {α : Type*} {β : Type*} {t₁ : topological_space α} {t₂ : ι  topological_space β}
  {f : α  β}
  (h : i, @continuous _ _ t₁ (t₂ i) f) :
  @continuous _ _ t₁ (lattice.supr t₂) f :=
continuous_iff_le_coinduced.2 $ lattice.supr_le $ assume i, continuous_iff_le_coinduced.1 (h i)

lemma continuous.pi_mk
  {X I : Type*} {Y : I  Type*} [t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)]
  (f : Πi, X  (Y i)) (H : Πi, continuous (f i)) :
  continuous (λ x i, f i x) :=
continuous_supr_rng $ assume i, continuous_induced_rng $ H i

lemma continuous_list_sum {α : Type*} {β : Type*} {γ : Type*}
  [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β]
  {f : γ  α  β} :
  l:list γ, (cl, continuous (f c))  continuous (λa, (l.map (λc, f c a)).sum)
| []       _ := by simp [continuous_const]
| (f :: l) h :=
  begin
    simp,
    exact continuous_add
      (h f (list.mem_cons_self _ _))
      (continuous_list_sum l (assume c hc, h c (list.mem_cons_of_mem _ hc)))
  end

lemma continuous_multiset_sum {α : Type*} {β : Type*} {γ : Type*}
  [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β]
  {f : γ  α  β} (s : multiset γ) :
  (cs, continuous (f c))  continuous (λa, (s.map (λc, f c a)).sum) :=
quot.induction_on s $ by simp; exact continuous_list_sum

lemma continuous_finset_sum {α : Type*} {β : Type*} {γ : Type*}
  [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β]
  (f : γ  α  β) (s : finset γ) :
  (cs, continuous (f c))  continuous (λa, s.sum (λc, f c a)) :=
continuous_multiset_sum _

Johan Commelin (May 23 2018 at 12:50):

@Patrick Massot Yes, you are completely right. But it seems the work is now already done (-;

Mario Carneiro (May 23 2018 at 12:57):

you can see how Johannes built the term proof for pi_mk; the key is to use continuous_supr_rng not continuous_Sup_rng because the definition uses supr (the indexed supremum) not Sup (the set supremum). In fact supr is defined in terms of Sup, but if you apply the wrong theorem it unfolds this definition and things get harder.

Johan Commelin (May 23 2018 at 13:06):

Yes, I will take a closer look. I think I can learn a lot from how Johannes improved my kludge

Patrick Massot (May 23 2018 at 13:13):

Sure. But this is too efficient in a sense. My message was focused on easy local clean up, that you can actually do without any understanding of the proof. Of course this is only the first step. Really efficient proofs like Johannes' require actual thinking

Mario Carneiro (May 23 2018 at 13:15):

you can also look at my term proof of continuous_supr_rng, which uses the \t for rewriting

Patrick Massot (May 23 2018 at 13:17):

I'm a bit frustrated by this \t thing. I know it's somehow the term version of rw and I see it everywhere in mathlib, but I was almost never able to use it

Mario Carneiro (May 23 2018 at 13:17):

I admit it was a bit delicate for me at first

Mario Carneiro (May 23 2018 at 13:18):

it is so much weaker than the lean 2 version, it fails whenever the expected type or the thing to rewrite with has metavariables

Johan Commelin (May 23 2018 at 13:19):

Anyway, I just proved that the face map between standard simplices is continuous!

Johan Commelin (May 23 2018 at 13:19):

The proof is not cleaned up. But it works (-;

Mario Carneiro (May 23 2018 at 13:20):

but it's often just the thing when you want to rewrite with an equality in the context

Patrick Massot (May 23 2018 at 13:23):

What about my attempt? Can you use \t there? (without switching to continuous_supr_rng)

Mario Carneiro (May 23 2018 at 13:24):

yes, the proof should be almost identical to the one I pointed at

Johan Commelin (May 23 2018 at 13:25):

Ok, like I said, the proofs are still ugly. But here goes nothing: https://github.com/jcommelin/mathlib/commit/fec9db2028bea163352f574055dad44029d04788

Mario Carneiro (May 23 2018 at 13:25):

lemma continuous.pi_mk
  {X I : Type*} {Y : I → Type*} [t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)]
  (f : Πi, X → (Y i)) (H : Πi, continuous (f i)) :
  continuous (λ x i, f i x) :=
continuous_Sup_rng $ assume t ⟨i, e⟩, e.symm ▸ continuous_induced_rng (H i)

Patrick Massot (May 23 2018 at 15:06):

Hum, I think I stupidly missed the eq.symm when I tried

Johannes Hölzl (May 23 2018 at 15:31):

@Johan Commelin I forgot that there is already tendsto_sum, so you could also derive continuous_finset_sum from this.
Anyway, this all is now in mathlib.

Johan Commelin (May 23 2018 at 16:54):

Thanks a lot! I will merge into my fork. Once I clean my stuff up, I think I will make a PR


Last updated: Dec 20 2023 at 11:08 UTC