Zulip Chat Archive

Stream: maths

Topic: Topology on R^n


view this post on Zulip Johan Commelin (May 14 2018 at 08:39):

I have the following code

import analysis.topology.topological_space analysis.real data.finsupp
open classical

definition type_pow : Type*    Type*
| α 0       := unit
| α (n+1) := type_pow α n × α

instance type_pow_instance : has_pow Type*  := type_pow

definition sum_in_Rn : Π (n : ), ^n  
| 0      x    :=  0
| (m+1) (x,y) := (sum_in_Rn m x) + y

definition standard_simplex (n : ) : set (^(n+1)) := λ x, sum_in_Rn (n+1) x = 1

namespace standard_simplex

variable {n : }

definition topology_Rn : Π (n : ), topological_space (^n)
| 0     := begin show topological_space unit, apply_instance end
| (n+1) := begin show topological_space (_ × _),
 have t₁ : topological_space (type_pow  (nat.add n 0)) := topology_Rn n,
 have t₂ : topological_space , begin apply_instance end,
 exact topological_space.induced prod.fst t₁  topological_space.induced prod.snd t₂,
 end

definition inclusion : standard_simplex n  ^(n+1) := λ x, x

instance : topological_space (standard_simplex n)
 := topological_space.induced inclusion (@topology_Rn (n+1))

end standard_simplex

view this post on Zulip Johan Commelin (May 14 2018 at 08:39):

I get red squiggles under topology_Rn, in its definition

view this post on Zulip Johan Commelin (May 14 2018 at 08:40):

The error is: rec_fn_macro only allowed in meta definitions

view this post on Zulip Johan Commelin (May 14 2018 at 08:41):

So, two questions: how do I get lean to automatically deduce the topology on R^n on the second line of the induction? There is already an instance of topological_space (α × β)...

view this post on Zulip Johan Commelin (May 14 2018 at 08:41):

The second is, how did I get this error, if I only copied a line from the proof of topological_space (α × β)...?

view this post on Zulip Johannes Hölzl (May 14 2018 at 08:56):

It looks like you need to mark your definitionnoncomputable (or your entire theory).

But in general I would not advice to use this type construction. I think for R ^ nthere are two options: Use vec n R (define the canonical topology on lists using lfp, and then use subtype for vec), or use fin n -> R and use the topological space construction on function spaces.

view this post on Zulip Johannes Hölzl (May 14 2018 at 08:58):

The advantage of seeing R^n as a function space is that you can do a lot of proofs assuming arbitrary functions, and no induction is necessary on your type itself.

view this post on Zulip Gabriel Ebner (May 14 2018 at 09:01):

@Johan Commelin You stumbled upon this bug: https://github.com/leanprover/lean/issues/1890 The unsoundness issue was fixed last year, but apparently there are still cases where you can accidentally use general recursion in non-meta definitions. The culprit is the begin apply_instance end, which defines t₂ in terms of itself.

view this post on Zulip Johan Commelin (May 14 2018 at 09:03):

So.. how do I fix it?

view this post on Zulip Johan Commelin (May 14 2018 at 09:03):

I some how wish I could skip those have-lines anyway

view this post on Zulip Johan Commelin (May 14 2018 at 09:04):

The system should figure that out itself..., although maybe the first have-line is to hard for it.

view this post on Zulip Johannes Hölzl (May 14 2018 at 09:04):

So.. how do I fix it?

Seriously: Use another type!

view this post on Zulip Johan Commelin (May 14 2018 at 09:05):

Like what? (Confused newbie behind this keyboard...)

view this post on Zulip Johannes Hölzl (May 14 2018 at 09:07):

Use fin n -> R, the topological space is already setup, i.e. it only needs the instance for α → β where β has a topological space.

view this post on Zulip Johan Commelin (May 14 2018 at 09:08):

Ok, I'll try that

view this post on Zulip Gabriel Ebner (May 14 2018 at 09:12):

So.. how do I fix it?

Aside from "don't do it" as Johannes already said, the main thing you can try if you see this bug is to move the have statements out of the begin-end block. In this case, it is enough if you move just the have t₁ before the begin.

view this post on Zulip Johan Commelin (May 14 2018 at 09:46):

@Johannes Hölzl Ok, so now I have fin n \to \R, but how do I get a topology on it? Because I can't find the instance that you just described...

view this post on Zulip Johannes Hölzl (May 14 2018 at 09:47):

Hm, works here:

import analysis.real

def test {α : Type*} {n:} [t : topological_space α] : topological_space (fin n  α) :=
by apply_instance

#print test
/-
def test : Π {α : Type u_1} {n : ℕ} [t : topological_space α], topological_space (fin n → α) :=
λ {α : Type u_1} {n : ℕ} [t : topological_space α], Pi.topological_space
-/

view this post on Zulip Johannes Hölzl (May 14 2018 at 09:49):

Or more specific

noncomputable def test {n:} : topological_space (fin n  ) :=
by apply_instance

set_option pp.all true
#print test
/-
noncomputable def test : Π {n : nat}, topological_space.{0} (fin n → real) :=
λ {n : nat},
  @Pi.topological_space.{0 0} (fin n) (λ (a : fin n), real)
    (λ (a : fin n),
       @uniform_space.to_topological_space.{0} real (@metric_space.to_uniform_space'.{0} real real.metric_space))
-/

Don't forget noncomputable Maybe you want to setup it for your theory: use noncomputable theory at the beginning (after the imports)

view this post on Zulip Johan Commelin (May 14 2018 at 10:01):

Ok, that helped.

definition topology_Rn : Π (n : ), topological_space (^n) :=
begin
intros n, show topological_space (fin n  ), apply_instance,
end

view this post on Zulip Johan Commelin (May 14 2018 at 10:02):

Not term-mode, but I don't care too much (-;


Last updated: May 10 2021 at 08:14 UTC