Zulip Chat Archive

Stream: maths

Topic: setoid.ker, kinda


Arthur Paulino (Nov 22 2021 at 17:40):

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 (Nov 22 2021 at 17:46):

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 (Nov 22 2021 at 17:52):

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

Yaël Dillies (Nov 22 2021 at 17:53):

Not sure it deserves a name.

Arthur Paulino (Nov 22 2021 at 17:55):

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 (Nov 22 2021 at 18:02):

Just use {b}.preimage f

Kyle Miller (Nov 22 2021 at 18:06):

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 (Nov 22 2021 at 18:09):

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.


Last updated: Dec 20 2023 at 11:08 UTC