universe juggling

Stream: general

[Patrick Massot]

In

import data.set.basic

universe variables u v

variables (X : Type u) (Y : Type v) (f : X → Y)

open set

#check subtype (range f)

How do I get the version of subtype (range f) that lives in Type u?

[Johan Commelin]

I guess you need the "first isomorphism theorem for ordinary functions". But that probably isn't in mathlib yet.

[Gabriel Ebner]

import data.set.basic
import data.equiv.basic
universes u v
variables {X : Type u} {Y : Type v}

def range' (f : X → Y) : Type u :=
quot (eq on f)

noncomputable def range'_equiv_subtype_range (f : X → Y) : range' f ≃ subtype (set.range f) :=
{ to_fun := λ x, quot.rec_on x (λ x, ⟨f x, _, rfl⟩) (by simp),
  inv_fun := λ y, quot.mk _ (classical.some y.2),
  right_inv := λ ⟨x, y, h⟩, by simp [@classical.some_spec _ (λ y, f y = x)],
  left_inv := λ x, quot.induction_on x $
    λ x, quot.sound (by simp [(on), @classical.some_spec _ (λ y, f y = f x)]) }

[Eric Wieser]

Note that subtype (set.range f) is defeq abuse and should be ↥(set.range f) or subtype (∈ set.range f)

[Eric Wieser]

Otherwise when you apply lemmas you get nonsense like set.range f i instead of i ∈ set.range f

[Gabriel Ebner]

Yeah, this definitional equality is a real footgun. Some time ago I started a refactor to turn set into a structure, but I kind of ran out of steam in the middle. https://github.com/leanprover-community/lean/compare/set_struct?expand=1 https://github.com/leanprover-community/mathlib/compare/set_struct?expand=1

[Eric Wieser]

I think it's kind of like the additive / multiplicative thing; it's a real footgun, but it's also necessary to work around the fact that structures don't have eta expansion (or whichever expansion I actually mean)

[Eric Wieser]

Maybe this is something a linter could look out for

[Patrick Massot]

Thanks Gabriel. I thought about using the quotient defined by f but I hoped it would already exist.

[Eric Wieser]

Is eq on f the same as docs#setoid.ker?

[Eric Wieser]

docs#setoid.quotient_ker_equiv_range looks like what you want

[Patrick Massot]

Great!

[Gabriel Ebner]

The set structure refactor was way less problematic than the additive/multiplicative one. The main issues are:

• API churn, like you can't use set.ext for elements of α → Prop anymore.
• The unifier can't solve x ∈ f =?= x ∈ set.mk ?m anymore. I think this can be fixed with a unification hint. Lean 4 also does this out of the box.
• You can't do inductive foo : α → set β anymore. But this is also no longer supported in Lean 4.
• I made set.ext protected, which requires quite a lot of inconsequential changes.

[Eric Wieser]

My understand was that such a refactor also stops {x | x ∈ s} = s being true by definition, which is what I assume is called structure eta-expansion?

[Gabriel Ebner]

Right, but I don't think I ran into that problem.