How to restrict the codomain of a function?

Stream: Is there code for X?

[Ching-Tsun Chou]

Any function f : A → B (where A and B are arbitrary types) naturally induces a surjective function of type:

f' : A → {y // y ∈ range f}

via the informal equation f' x = f x. Is the f ↦ f' map already defined in mathlib?

I know I can define it using Subtype.map, but am wondering whether it is already in mathlib with proved results. (For example, if f is injective, then so is f'. And so on.)

[Aaron Liu]

docs#Set.rangeFactorization

[Aaron Liu]

please report any missing lemmas you (don't) find I don't think the API around this area is complete

[Aaron Liu]

Ching-Tsun Chou said:

(For example, if f is injective, then so is f'. And so on.)

Surprisingly I don't think we have this result

[Aaron Liu]

are you willing to PR it to mathlib?

[Aaron Liu]

we do have the slightly stronger result of having a specified left inverse (actually stated as being a right inverse) in docs#Set.rightInverse_rangeSplitting

[Aaron Liu]

we also might want the version stating bijective

[Weiyi Wang]

Seeing ↑(range f) in the type makes me think of dependent type hell, which might be the reason it isn't used much (-> people don't add many lemma to it). Perhaps you can provide more context on what you want to do, and maybe there is a better way to avoid using this?

[Ching-Tsun Chou]

Actually, after thinking more, I wonder if mathlib has the following more useful result:
If a function f : A → B is injective, then there is an equivalence (≃) between the type A and the type {y // y ∈ range f}.

[Weiyi Wang]

docs#Equiv.ofInjective

[Weiyi Wang]

(Found by loogle Function.Injective, Equiv)

[Ching-Tsun Chou]

Ah, thanks! I still don't know how to loogle effectively.

[Aaron Liu]

Weiyi Wang said:

Seeing ↑(range f) in the type makes me think of dependent type hell, which might be the reason it isn't used much

cmon it's not that bad once you get used to it

[Ben Eltschig]

There's also docs#Set.codRestrict and docs#Subtype.coind for when you want to restrict to an arbitrary superset of the range instead of the range itself. I think the former has a bit more API than the latter

[Robert Maxton]

Aaron Liu said:

cmon it's not that bad once you get used to it

Yeah, sets-as-types is really not bad compared to most things called dependent type hell; the only place where it gets annoying is working with nested preimage vals/ ↓∩, IMO