Function.Pullback

Stream: mathlib4

[Wrenna Robson]

Hi.
Why is Function.Pullback defined as a subtype rather than a set?

[Jireh Loreaux]

My guess: because you want to use it as a type more frequently. And note the following behavior about the coercion to Sort of a Set:

import Mathlib.Data.Set.Prod

variable {α β γ : Type*} (f : α → γ) (g : β → γ)

example : Function.Pullback f g = { p : α × β | f p.1 = g p.2 } := rfl -- works
example : Function.Pullback f g = { p : α × β | f p.1 = g p.2 } := by with_reducible rfl -- fails

[Wrenna Robson]

What is the significance of that?

[Jireh Loreaux]

sorry, perhaps the more significant bit that I should have written:

example : Function.Pullback f g = { p : α × β | f p.1 = g p.2 } := by with_reducible_and_instances rfl -- fails

So these are not interchangeable at the instance level. Basically, you have a choice to make, and your defeqs are affected accordingly. If you were planning to use something as a type virtually all the time, then you should probably go with a subtype (as Function.Pullback does) so that you don't end up in Set land for your defeqs, but if you are going to use it as a Set most of the time, then this is reversed.

[Wrenna Robson]

Thanks, that's interesting. Suppose you have two definitions, a set and a subtype, where the set happens to be equal to the set the subtype coerces to. How do you express that?

[Jireh Loreaux]

Set.range (Subtype.val : my_subtype → my_type) = my_set

[Wrenna Robson]

Nice, thanks

[Jireh Loreaux]

In fact, that's just a missing lemma for Function.Pullback. You should add it :wink:

[Wrenna Robson]

I don't think we have a name for that set (I was actually thinking of adding it, mainly actually because I wanted the Set version of Setoid.ker which it is a special case of.)

[Jireh Loreaux]

Right, I'm not suggesting giving it a name, only making a lemma of the form:

@[simp]
lemma Function.range_pullback : Set.range (Pullback f g) = { x | f x.1 = g x.2 } := sorry

[Wrenna Robson]

Ah got you

[Yakov Pechersky]

The pullback is worth having as a new type as opposed to being a subset because one might install different instances on it, not necessarily the ones that are implied, like subspace topology.

[Wrenna Robson]

Oh does that work even though it's an "abbrev".

[Jireh Loreaux]

no, abbrev means it will inherit those instances.

[Jireh Loreaux]

But I agree that this seems like the wrong choice.