Set union of spaces (abuse), identifying as subset?

Stream: new members

[Luigi Massacci]

(Noting by $E(X)$ some metric space of functions on $X$)
For $S \subseteq X$, I have an isometric embedding $E(S)\hookrightarrow E(X)$

I would like to make:

$$\bigcup \{E(Y) | Y \subseteq X, Y \text{ is finite} \} \subseteq E(X)$$

with the usual abuse of notation of identifying $E(Y)$ as a subset of $E(X)$ with the embedding, but I seem to be having some trouble with set comprehension. What is the canonical way to make this construction?

[Jireh Loreaux]

Can you provide an #mwe ?

[Luigi Massacci]

Not easily. I'll give it a try this weekend

[Luigi Massacci]

The space E(x) is defined as a structure if it helps

[Jireh Loreaux]

You can likely omit the details, but mainly I'm wondering whether X : Type* and S : Set X or not. And does E take a type as an argument, or a set?

[Luigi Massacci]

Good point. Indeed you guessed correctly X : Type* and S : Set X, and E takes a type, so it's technically E(↑S) (also note that up to the isometric embedding included, I have actual working lean proofs)

[Kevin Buzzard]

Great! Then it should be not too much trouble to make that #mwe which will make your question answerable.

[Kevin Buzzard]

Note that in a mwe you can sorry all proofs, the point is that you ask your chosen formalisation of your maths question so that other people don't waste their time answering a question which you didn't mean to ask (eg a question about a different implementation of the specification which you've already given above)

[Luigi Massacci]

Indeed. So this should hopefully be close enough to a #mwe

The following stuff is "all good" (by me at least):

import Mathlib.Tactic

variable {α : Type _} [MetricSpace α]

@[mk_iff]
structure IsKatetov (f : α → ℝ) : Prop where
  abs_sub_le_dist : ∀ x y, |f x - f y| ≤ dist x y
  dist_le_add : ∀ x y, dist x y ≤ f x + f y

structure KatetovMap (α : Type*) [MetricSpace α] where
  protected toFun : α → ℝ
  protected IsKatetovtoFun : IsKatetov toFun

notation "E(" α ")" => KatetovMap α

noncomputable instance: MetricSpace E(α) := by sorry
noncomputable instance : CompleteSpace E(α) := by sorry

theorem kuratwoski_embedding (α : Type*) [MetricSpace α] :
  ∃ f : α → E(α), Isometry f := by sorry

-- this has some actual work inside it
noncomputable def extend {α : Type*} (s : Set α) [MetricSpace α]
    (f : E(s)) : E(α) := by sorry

-- this does merely the obvious thing
def restrict {α : Type*} (s : Set α) [MetricSpace α] (f : E(α)) : E(s) := by sorry

--this uses "extend"
theorem subset_embedding (α : Type*) [MetricSpace α] (s : Set α) :
  ∃ f : E(s) → E(α), Isometry f := by sorry

To give context, I now want the set I described at the start as a metric space, with the same metric as E(α).
So the following "direct" adaptation I think is probably a terrible idea:

def FinSuppKatMaps : Set (E(α)) := ⋃₀ {subset_embed s '' (⊤ : Set E(s)) | (Set.Finite s) (s : Set α)}

(modulo the fact that it doesn't work because I clearly haven't understood how set comprehension works.)
Alternatively, I was thinking of doing something like this:

-- s here is called the "support" of f
def HasFinSuppKatMap (f : E(α)) : Prop :=
     ∃ s : Set α, Set.Finite s ∧ f = extend s (restrict s f)

structure FinSuppKatetovMap (α : Type*) [MetricSpace α] extends KatetovMap α  where
    protected HasFinSuppKatetovtoFun : HasFinSuppKatMap toKatetovMap

notation "E(" α ", ω)" => FinSuppKatetovMap α

Which should be equivalent to the thing above, but then I found it surprisingly painful to make E(α, ω), inherit the metric structure, so I was considering that other approach above

For further context, the next steps would be:

instance : MetricSpace E(α, ω) := by sorry
instance : CompleteSpace E(α, ω) := by sorry

theorem finsupp_kuratoswki_embedding (α : Type*) [MetricSpace α] :
  ∃ f : α → E(α, ω), Isometry f := by sorry  -- which is easy "mathematically", I just had the pain with E(α, ω)

Then I make a sequence α_{n+1} = E(αₙ, ω) and get the limit space with Metric.Inductive, which is what I am actually interested in. I don't suppose that should be a problem with a decent definition of E(α, ω)

[Kevin Buzzard]

Some tube thoughts (which fit after your first code block above):

variable (α)
-- I would go for this one
def foo : Set E(α) := {φ : E(α) | ∃ (s : Set α) (ψ : E(s)), s.Finite ∧ φ = extend s ψ}

-- `Finset` is constructive so is slightly harder to use, but has its benefits
def bar : Set E(α) := {φ : E(α) | ∃ (s : Finset α) (ψ : E(s)), φ = extend s ψ}

-- To prove they're "the same" you seem to need some more API.

section better_restrict_function

variable {α}
variable {β : Type*} [MetricSpace β]

def better_restrict (f : α → β) (hf : Isometry f) :
  E(β) → E(α) := sorry

def KatetovMap.equiv (α β : Type*) [MetricSpace α] [MetricSpace β] (f : α ≃ β) (hf : Isometry f) :
    E(α) ≃ E(β) where
  toFun := better_restrict f.symm sorry
  invFun := better_restrict f hf
  left_inv := sorry
  right_inv := sorry

example : foo α = bar α := by
  ext φ
  constructor
  · rintro ⟨s, ψ, hs, rfl⟩
    refine ⟨hs.toFinset, ?_⟩
    sorry
  · rintro ⟨t, ht⟩
    sorry

Lean treats types and subsets on different footings, as you'll be aware. My gut feeling is that your extend and restrict should be refactored to deal with the more general situation of an isometric injection of metric spaces rather than subets with the induced metric structure; in Lean the former situation is more general and more useful. foo is my proposed answer to your question.

[Luigi Massacci]

First off: thank you for the answer. Doing the refactoring you pointed out took a whole of two minutes, so that's good. But so you would still suggest going the set way? Presumably replacing s with something like this now:

def foo : Set E(α) := {φ : E(α) | ∃ (β : Type*) (hβ : MetricSpace β) (ρ : β → α) (hρ : Isometry ρ)
   (ψ : E(β)), Finite β ∧ φ = extend₂ ρ hρ ψ}

or to keep it constructive:

def bar : Set E(α) := {φ : E(α) | ∃ (β : Type*) (hβ : MetricSpace β) (hf : Fintype β) (ρ : β → α) (hρ : Isometry ρ)
   (ψ : E(β)), φ = extend₂ ρ hρ ψ}

It doesn't seem very mathlib-y? Also if I try instance : MetricSpace (@foo α _) := by infer_instance I get

compiler IR check failed at 'KatetovExtension.instMetricSpaceElemKatetovMapFoo._rarg', error: unknown declaration 'instMetricSpaceKatetovMap'

which is an error I've never seen before, so I guess at least I Iearned something.

[Jireh Loreaux]

the "compiler IR check" just means you need to mark it noncomputable

[Jireh Loreaux]

My version would have been:

def bar : Set E(α) := ⋃ s : Finset α, Set.range (extend s)

And presumably you want to show that Isometry (extend s) instead of just ∃ f : E(s) → E(α), Isometry f.

[Jireh Loreaux]

Also, I agree with Kevin. If you want make this material act on types and the appropriate kind of embeddings, I think it will be easier in the long run.

[Luigi Massacci]

Jireh Loreaux said:

the "compiler IR check" just means you need to mark it noncomputable

Ah, now it works!

For the second point, I have indeed eliminated all s : Set α and replaced it with (β : Type*) [MetricSpace β] (ρ : β → α) (hρ : Isometry ρ). But then bar would remain the outlier... That is why I was thinking of making it its own type via extends. But then I ran into all sorts of issues with the coercions between my new FinsuppKatMap type, KatetovMap, and α → ℝ

[Luigi Massacci]

On the other hand, prooving the embedding of α into bar was easy, so I might leave it at that...