setoid.ker, kinda

Stream: maths

[Arthur Paulino]

On this PR I added the following function in setoid/partition.lean:

/-- Given a function `f`, builds a function that consumes a `y` and returns the set of every `x`
    whose image is `y`. -/
def class_fn {β : Type*} (f : α → β) : β → set α := λ y, {x | f x = y}

The thing is... my intuition says that this is something that has a proper name and a proper place in mathematics. Do we already have this function defined somewhere else in mathlib?

And if not, how would you call it? And where would you place it? This function is used to prove two different results in the same file.

[Oliver Nash]

Is this just the preimage of a singleton, aka a fibre? E.g.,

example {α β : Type*} (f : α → β) (b : β) :
  class_fn f b = ({b} : set β).preimage f :=
rfl

[Arthur Paulino]

Indeed. Is there something equivalent to class_fn f (not class_fn f _ as in your example)?

[Yaël Dillies]

Not sure it deserves a name.

[Arthur Paulino]

How to proceed in this situation? This function was being defined inside two different proofs. How to avoid code duplication in this case?

[Yaël Dillies]

Just use {b}.preimage f

[Kyle Miller]

There's a certain philosophy that for small functions, the code itself is its name.

In this case, it's always being used as set.range (λ y, {x | f x = y}), which isn't so big of a name.

[Kyle Miller]

Theoretically speaking, class_fn is giving an extension of the canonical image -> cokernel function to codomain -> option cokernel, where none is being encoded using the empty set. This is a bit of an odd function to have theory about, so maybe it's best not to give it a name for now.