## Stream: general

### Topic: embeddings and subtypes

#### Peter Nelson (Feb 01 2021 at 21:02):

Given an embedding emb : α ↪ β, I am trying to use the natural correspondence between α and the subtype of β induced by set.range emb. I am also in a context where I want to do this with the subtype coming from another set E that is propeq but not defeq to set.range emb.

My first concern is whether this is just plain unidiomatic; doing this seems to be 'fighting' mathlib in the sense that I can't see how to use it directly. My second is more specific: the following code is an attempt to convert a function defined on subsets of α to one on subsets of the range of emb; and I get a strange error.

import tactic

noncomputable theory
open_locale classical

/-- Given an embedding from α to β and a set E equal to its range, gives an equivalence between α and the subtype of β corresponding to E -/
def subtype_inv_inj {α β: Type}(emb : α ↪ β){E : set β}(hE : E = set.range emb) : E ≃ α :=
let h : Π (y : E), (∃ x : α, emb x = y) :=
by {rintros ⟨y,hy⟩, rw [hE, set.mem_range] at hy, cases hy with x hx, from ⟨x, by simp [hx]⟩},
desc : Π (y : E), {x : α  // emb x = y} :=
λ y, classical.indefinite_description _ (h y) in
{
to_fun    := λ y, (desc y).val,
inv_fun   := λ x, ⟨emb x, by {rw [hE, set.mem_range], from ⟨x, rfl⟩} ⟩,
left_inv  := λ y, by {simp_rw (desc y).property, simp},
right_inv := λ x, by {cases emb with f h_inj, from h_inj (desc ⟨f x,_⟩).property},
}

/-- given a function f on the subsets of α, and an embedding f from α to β, returns the corresponding function on subsets of the range of the embedding  -/
def pullback_r {α β: Type}(emb : α ↪ β)(f : set α → ℤ) : set (set.range emb) → ℤ :=
let pb_emb := subtype_inv_inj emb rfl in
λ X, f (pb_emb '' X)


The second function gives the error message: failed to generate bytecode for 'pullback_r' code generation failed, VM does not have code for 'classical.indefinite_description'

Any advice on either a more principled way to do this, or a way to fix this specific error, would be appreciated.

#### Mario Carneiro (Feb 01 2021 at 21:05):

The error is easy enough to fix: write noncomputable def

#### Yakov Pechersky (Feb 01 2021 at 21:05):

Do you know if α β are finite? Then you could in theory have a computable one

#### Peter Nelson (Feb 01 2021 at 21:05):

I've tried that with no success

#### Yakov Pechersky (Feb 01 2021 at 21:06):

noncomputable def pullback_r doesn't work?

that's right

#### Peter Nelson (Feb 01 2021 at 21:07):

I do happen to know they're finite, but suppose I didnt? I don't have a constructivist bone in my body and would rather not do extra work to make things constructive.

#### Yakov Pechersky (Feb 01 2021 at 21:09):

My relevant PRs on this are #5872 and #5875

#### Mario Carneiro (Feb 01 2021 at 21:09):

I got it working with noncomputable def subtype_inv_inj and theorem pullback_r

#### Peter Nelson (Feb 01 2021 at 21:10):

Thanks - do you mind explaining your thought process? It feels odd to put theorem in front of a function definition.

#### Mario Carneiro (Feb 01 2021 at 21:11):

It has to do with the way lean interprets the keywords def vs theorem; specifically the latter does not get codegen

#### Mario Carneiro (Feb 01 2021 at 21:11):

this can cause a problem for downstream definitions, which is why we have the rule that data should be def

#### Mario Carneiro (Feb 01 2021 at 21:11):

but classical.indefinite_description is a theorem

#### Mario Carneiro (Feb 01 2021 at 21:12):

and that causes the error you are seeing

#### Mario Carneiro (Feb 01 2021 at 21:14):

I'm not saying this is a proper solution to the problem, indeed I think it will cause problems for the next definition using pullback_r

#### Mario Carneiro (Feb 01 2021 at 21:15):

Oh, inlining the let works

noncomputable def pullback_r {α β: Type}(emb : α ↪ β)(f : set α → ℤ) : set (set.range emb) → ℤ :=
λ X, f (subtype_inv_inj emb rfl '' X)


#### Peter Nelson (Feb 01 2021 at 21:16):

Mario Carneiro said:

Oh, inlining the let works

noncomputable def pullback_r {α β: Type}(emb : α ↪ β)(f : set α → ℤ) : set (set.range emb) → ℤ :=
λ X, f (subtype_inv_inj emb rfl '' X)


Well, I never would have guessed that!

#### Mario Carneiro (Feb 01 2021 at 21:17):

It's because subtype_inv_inj emb rfl '' X is computationally irrelevant. In fact it's probably not even noncomputable

#### Mario Carneiro (Feb 01 2021 at 21:17):

yep, noncomputable def subtype_inv_inj and def pullback_r works, even without the noncomputable theory at the top

#### Mario Carneiro (Feb 01 2021 at 21:19):

But when you hoist the subtype function to the top level, it means that it has to be evaluated. I suspect that the reason for the weird error is because it is not inlined for the noncomputable check but inlined later and lean gets confused about whether it's computable or not

Thanks!

#### Yury G. Kudryashov (Feb 02 2021 at 03:45):

BTW, you can use docs#equiv.set.range together with docs#equiv.set.of_eq to get the desired equiv.

#### Yury G. Kudryashov (Feb 02 2021 at 03:46):

Something like (equiv.set.range emb emb.injective).trans (equiv.set.of_eq hE)

Last updated: May 13 2021 at 17:42 UTC