Topology on R^n

Stream: maths

[Johan Commelin]

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

[Johan Commelin]

I get red squiggles under topology_Rn, in its definition

[Johan Commelin]

The error is: rec_fn_macro only allowed in meta definitions

[Johan Commelin]

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 (α × β)...

[Johan Commelin]

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

[Johannes Hölzl]

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.

[Johannes Hölzl]

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.

[Gabriel Ebner]

@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.

[Johan Commelin]

So.. how do I fix it?

[Johan Commelin]

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

[Johan Commelin]

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

[Johannes Hölzl]

So.. how do I fix it?

Seriously: Use another type!

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johan Commelin]

Ok, I'll try that

[Gabriel Ebner]

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.

[Johan Commelin]

@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...

[Johannes Hölzl]

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
-/

[Johannes Hölzl]

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)

[Johan Commelin]

Ok, that helped.

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

[Johan Commelin]

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